Theorem List for Intuitionistic Logic Explorer - 11501-11600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | oexpneg 11501 |
The exponential of the negative of a number, when the exponent is odd.
(Contributed by Mario Carneiro, 25-Apr-2015.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁) → (-𝐴↑𝑁) = -(𝐴↑𝑁)) |
|
Theorem | mod2eq0even 11502 |
An integer is 0 modulo 2 iff it is even (i.e. divisible by 2), see example
2 in [ApostolNT] p. 107. (Contributed
by AV, 21-Jul-2021.)
|
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 0 ↔ 2 ∥ 𝑁)) |
|
Theorem | mod2eq1n2dvds 11503 |
An integer is 1 modulo 2 iff it is odd (i.e. not divisible by 2), see
example 3 in [ApostolNT] p. 107.
(Contributed by AV, 24-May-2020.)
|
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 1 ↔ ¬ 2 ∥ 𝑁)) |
|
Theorem | oddnn02np1 11504* |
A nonnegative integer is odd iff it is one plus twice another
nonnegative integer. (Contributed by AV, 19-Jun-2021.)
|
⊢ (𝑁 ∈ ℕ0 → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈
ℕ0 ((2 · 𝑛) + 1) = 𝑁)) |
|
Theorem | oddge22np1 11505* |
An integer greater than one is odd iff it is one plus twice a positive
integer. (Contributed by AV, 16-Aug-2021.)
|
⊢ (𝑁 ∈ (ℤ≥‘2)
→ (¬ 2 ∥ 𝑁
↔ ∃𝑛 ∈
ℕ ((2 · 𝑛) +
1) = 𝑁)) |
|
Theorem | evennn02n 11506* |
A nonnegative integer is even iff it is twice another nonnegative
integer. (Contributed by AV, 12-Aug-2021.)
|
⊢ (𝑁 ∈ ℕ0 → (2
∥ 𝑁 ↔
∃𝑛 ∈
ℕ0 (2 · 𝑛) = 𝑁)) |
|
Theorem | evennn2n 11507* |
A positive integer is even iff it is twice another positive integer.
(Contributed by AV, 12-Aug-2021.)
|
⊢ (𝑁 ∈ ℕ → (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ (2 ·
𝑛) = 𝑁)) |
|
Theorem | 2tp1odd 11508 |
A number which is twice an integer increased by 1 is odd. (Contributed
by AV, 16-Jul-2021.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 = ((2 · 𝐴) + 1)) → ¬ 2 ∥ 𝐵) |
|
Theorem | mulsucdiv2z 11509 |
An integer multiplied with its successor divided by 2 yields an integer,
i.e. an integer multiplied with its successor is even. (Contributed by
AV, 19-Jul-2021.)
|
⊢ (𝑁 ∈ ℤ → ((𝑁 · (𝑁 + 1)) / 2) ∈
ℤ) |
|
Theorem | sqoddm1div8z 11510 |
A squared odd number minus 1 divided by 8 is an integer. (Contributed
by AV, 19-Jul-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (((𝑁↑2) − 1) / 8) ∈
ℤ) |
|
Theorem | 2teven 11511 |
A number which is twice an integer is even. (Contributed by AV,
16-Jul-2021.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 = (2 · 𝐴)) → 2 ∥ 𝐵) |
|
Theorem | zeo5 11512 |
An integer is either even or odd, version of zeo3 11492
avoiding the negation
of the representation of an odd number. (Proposed by BJ, 21-Jun-2021.)
(Contributed by AV, 26-Jun-2020.)
|
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ∨ 2 ∥ (𝑁 + 1))) |
|
Theorem | evend2 11513 |
An integer is even iff its quotient with 2 is an integer. This is a
representation of even numbers without using the divides relation, see
zeo 9124 and zeo2 9125. (Contributed by AV, 22-Jun-2021.)
|
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ (𝑁 / 2) ∈ ℤ)) |
|
Theorem | oddp1d2 11514 |
An integer is odd iff its successor divided by 2 is an integer. This is a
representation of odd numbers without using the divides relation, see
zeo 9124 and zeo2 9125. (Contributed by AV, 22-Jun-2021.)
|
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥
𝑁 ↔ ((𝑁 + 1) / 2) ∈
ℤ)) |
|
Theorem | zob 11515 |
Alternate characterizations of an odd number. (Contributed by AV,
7-Jun-2020.)
|
⊢ (𝑁 ∈ ℤ → (((𝑁 + 1) / 2) ∈ ℤ ↔ ((𝑁 − 1) / 2) ∈
ℤ)) |
|
Theorem | oddm1d2 11516 |
An integer is odd iff its predecessor divided by 2 is an integer. This is
another representation of odd numbers without using the divides relation.
(Contributed by AV, 18-Jun-2021.) (Proof shortened by AV,
22-Jun-2021.)
|
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥
𝑁 ↔ ((𝑁 − 1) / 2) ∈
ℤ)) |
|
Theorem | ltoddhalfle 11517 |
An integer is less than half of an odd number iff it is less than or
equal to the half of the predecessor of the odd number (which is an even
number). (Contributed by AV, 29-Jun-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2))) |
|
Theorem | halfleoddlt 11518 |
An integer is greater than half of an odd number iff it is greater than
or equal to the half of the odd number. (Contributed by AV,
1-Jul-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑀 ∈ ℤ) → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)) |
|
Theorem | opoe 11519 |
The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.)
(Revised by Mario Carneiro, 19-Apr-2014.)
|
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵)) → 2 ∥ (𝐴 + 𝐵)) |
|
Theorem | omoe 11520 |
The difference of two odds is even. (Contributed by Scott Fenton,
7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵)) → 2 ∥ (𝐴 − 𝐵)) |
|
Theorem | opeo 11521 |
The sum of an odd and an even is odd. (Contributed by Scott Fenton,
7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ 2 ∥ 𝐵)) → ¬ 2 ∥
(𝐴 + 𝐵)) |
|
Theorem | omeo 11522 |
The difference of an odd and an even is odd. (Contributed by Scott
Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ 2 ∥ 𝐵)) → ¬ 2 ∥
(𝐴 − 𝐵)) |
|
Theorem | m1expe 11523 |
Exponentiation of -1 by an even power. Variant of m1expeven 10308.
(Contributed by AV, 25-Jun-2021.)
|
⊢ (2 ∥ 𝑁 → (-1↑𝑁) = 1) |
|
Theorem | m1expo 11524 |
Exponentiation of -1 by an odd power. (Contributed by AV,
26-Jun-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (-1↑𝑁) = -1) |
|
Theorem | m1exp1 11525 |
Exponentiation of negative one is one iff the exponent is even.
(Contributed by AV, 20-Jun-2021.)
|
⊢ (𝑁 ∈ ℤ → ((-1↑𝑁) = 1 ↔ 2 ∥ 𝑁)) |
|
Theorem | nn0enne 11526 |
A positive integer is an even nonnegative integer iff it is an even
positive integer. (Contributed by AV, 30-May-2020.)
|
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ0 ↔
(𝑁 / 2) ∈
ℕ)) |
|
Theorem | nn0ehalf 11527 |
The half of an even nonnegative integer is a nonnegative integer.
(Contributed by AV, 22-Jun-2020.) (Revised by AV, 28-Jun-2021.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 2 ∥
𝑁) → (𝑁 / 2) ∈
ℕ0) |
|
Theorem | nnehalf 11528 |
The half of an even positive integer is a positive integer. (Contributed
by AV, 28-Jun-2021.)
|
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℕ) |
|
Theorem | nn0o1gt2 11529 |
An odd nonnegative integer is either 1 or greater than 2. (Contributed by
AV, 2-Jun-2020.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 = 1 ∨ 2 < 𝑁)) |
|
Theorem | nno 11530 |
An alternate characterization of an odd integer greater than 1.
(Contributed by AV, 2-Jun-2020.)
|
⊢ ((𝑁 ∈ (ℤ≥‘2)
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((𝑁 − 1) / 2) ∈
ℕ) |
|
Theorem | nn0o 11531 |
An alternate characterization of an odd nonnegative integer. (Contributed
by AV, 28-May-2020.) (Proof shortened by AV, 2-Jun-2020.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((𝑁 − 1) / 2) ∈
ℕ0) |
|
Theorem | nn0ob 11532 |
Alternate characterizations of an odd nonnegative integer. (Contributed
by AV, 4-Jun-2020.)
|
⊢ (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈
ℕ0 ↔ ((𝑁 − 1) / 2) ∈
ℕ0)) |
|
Theorem | nn0oddm1d2 11533 |
A positive integer is odd iff its predecessor divided by 2 is a positive
integer. (Contributed by AV, 28-Jun-2021.)
|
⊢ (𝑁 ∈ ℕ0 → (¬ 2
∥ 𝑁 ↔ ((𝑁 − 1) / 2) ∈
ℕ0)) |
|
Theorem | nnoddm1d2 11534 |
A positive integer is odd iff its successor divided by 2 is a positive
integer. (Contributed by AV, 28-Jun-2021.)
|
⊢ (𝑁 ∈ ℕ → (¬ 2 ∥
𝑁 ↔ ((𝑁 + 1) / 2) ∈
ℕ)) |
|
Theorem | z0even 11535 |
0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV,
23-Jun-2021.)
|
⊢ 2 ∥ 0 |
|
Theorem | n2dvds1 11536 |
2 does not divide 1 (common case). That means 1 is odd. (Contributed by
David A. Wheeler, 8-Dec-2018.)
|
⊢ ¬ 2 ∥ 1 |
|
Theorem | n2dvdsm1 11537 |
2 does not divide -1. That means -1 is odd. (Contributed by AV,
15-Aug-2021.)
|
⊢ ¬ 2 ∥ -1 |
|
Theorem | z2even 11538 |
2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV,
23-Jun-2021.)
|
⊢ 2 ∥ 2 |
|
Theorem | n2dvds3 11539 |
2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV,
28-Feb-2021.)
|
⊢ ¬ 2 ∥ 3 |
|
Theorem | z4even 11540 |
4 is an even number. (Contributed by AV, 23-Jul-2020.) (Revised by AV,
4-Jul-2021.)
|
⊢ 2 ∥ 4 |
|
Theorem | 4dvdseven 11541 |
An integer which is divisible by 4 is an even integer. (Contributed by
AV, 4-Jul-2021.)
|
⊢ (4 ∥ 𝑁 → 2 ∥ 𝑁) |
|
5.1.3 The division algorithm
|
|
Theorem | divalglemnn 11542* |
Lemma for divalg 11548. Existence for a positive denominator.
(Contributed by Jim Kingdon, 30-Nov-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
|
Theorem | divalglemqt 11543 |
Lemma for divalg 11548. The 𝑄 = 𝑇 case involved in showing uniqueness.
(Contributed by Jim Kingdon, 5-Dec-2021.)
|
⊢ (𝜑 → 𝐷 ∈ ℤ) & ⊢ (𝜑 → 𝑅 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℤ) & ⊢ (𝜑 → 𝑄 ∈ ℤ) & ⊢ (𝜑 → 𝑇 ∈ ℤ) & ⊢ (𝜑 → 𝑄 = 𝑇)
& ⊢ (𝜑 → ((𝑄 · 𝐷) + 𝑅) = ((𝑇 · 𝐷) + 𝑆)) ⇒ ⊢ (𝜑 → 𝑅 = 𝑆) |
|
Theorem | divalglemnqt 11544 |
Lemma for divalg 11548. The 𝑄 < 𝑇 case involved in showing uniqueness.
(Contributed by Jim Kingdon, 4-Dec-2021.)
|
⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℤ) & ⊢ (𝜑 → 𝑄 ∈ ℤ) & ⊢ (𝜑 → 𝑇 ∈ ℤ) & ⊢ (𝜑 → 0 ≤ 𝑆)
& ⊢ (𝜑 → 𝑅 < 𝐷)
& ⊢ (𝜑 → ((𝑄 · 𝐷) + 𝑅) = ((𝑇 · 𝐷) + 𝑆)) ⇒ ⊢ (𝜑 → ¬ 𝑄 < 𝑇) |
|
Theorem | divalglemeunn 11545* |
Lemma for divalg 11548. Uniqueness for a positive denominator.
(Contributed by Jim Kingdon, 4-Dec-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
|
Theorem | divalglemex 11546* |
Lemma for divalg 11548. The quotient and remainder exist.
(Contributed by
Jim Kingdon, 30-Nov-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
|
Theorem | divalglemeuneg 11547* |
Lemma for divalg 11548. Uniqueness for a negative denominator.
(Contributed by Jim Kingdon, 4-Dec-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
|
Theorem | divalg 11548* |
The division algorithm (theorem). Dividing an integer 𝑁 by a
nonzero integer 𝐷 produces a (unique) quotient 𝑞 and a
unique
remainder 0 ≤ 𝑟 < (abs‘𝐷). Theorem 1.14 in [ApostolNT]
p. 19. (Contributed by Paul Chapman, 21-Mar-2011.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
|
Theorem | divalgb 11549* |
Express the division algorithm as stated in divalg 11548 in terms of
∥. (Contributed by Paul Chapman,
31-Mar-2011.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℕ0 (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))) |
|
Theorem | divalg2 11550* |
The division algorithm (theorem) for a positive divisor. (Contributed
by Paul Chapman, 21-Mar-2011.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℕ0
(𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟))) |
|
Theorem | divalgmod 11551 |
The result of the mod operator satisfies the
requirements for the
remainder 𝑅 in the division algorithm for a
positive divisor
(compare divalg2 11550 and divalgb 11549). This demonstration theorem
justifies the use of mod to yield an explicit
remainder from this
point forward. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by
AV, 21-Aug-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 ∈ ℕ0 ∧ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅))))) |
|
Theorem | divalgmodcl 11552 |
The result of the mod operator satisfies the
requirements for the
remainder 𝑅 in the division algorithm for a
positive divisor. Variant
of divalgmod 11551. (Contributed by Stefan O'Rear,
17-Oct-2014.) (Proof
shortened by AV, 21-Aug-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝑅 ∈ ℕ0) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅)))) |
|
Theorem | modremain 11553* |
The result of the modulo operation is the remainder of the division
algorithm. (Contributed by AV, 19-Aug-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷)) → ((𝑁 mod 𝐷) = 𝑅 ↔ ∃𝑧 ∈ ℤ ((𝑧 · 𝐷) + 𝑅) = 𝑁)) |
|
Theorem | ndvdssub 11554 |
Corollary of the division algorithm. If an integer 𝐷 greater than
1 divides 𝑁, then it does not divide any of
𝑁 −
1,
𝑁
− 2... 𝑁 − (𝐷 − 1). (Contributed by Paul
Chapman,
31-Mar-2011.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐾 < 𝐷)) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 − 𝐾))) |
|
Theorem | ndvdsadd 11555 |
Corollary of the division algorithm. If an integer 𝐷 greater than
1 divides 𝑁, then it does not divide any of
𝑁 +
1,
𝑁 +
2... 𝑁 + (𝐷 − 1). (Contributed by Paul
Chapman,
31-Mar-2011.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐾 < 𝐷)) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 + 𝐾))) |
|
Theorem | ndvdsp1 11556 |
Special case of ndvdsadd 11555. If an integer 𝐷 greater than 1
divides 𝑁, it does not divide 𝑁 + 1.
(Contributed by Paul
Chapman, 31-Mar-2011.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 1 < 𝐷) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 + 1))) |
|
Theorem | ndvdsi 11557 |
A quick test for non-divisibility. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝐴 ∈ ℕ & ⊢ 𝑄 ∈
ℕ0
& ⊢ 𝑅 ∈ ℕ & ⊢ ((𝐴 · 𝑄) + 𝑅) = 𝐵
& ⊢ 𝑅 < 𝐴 ⇒ ⊢ ¬ 𝐴 ∥ 𝐵 |
|
Theorem | flodddiv4 11558 |
The floor of an odd integer divided by 4. (Contributed by AV,
17-Jun-2021.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) → (⌊‘(𝑁 / 4)) = if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2))) |
|
Theorem | fldivndvdslt 11559 |
The floor of an integer divided by a nonzero integer not dividing the
first integer is less than the integer divided by the positive integer.
(Contributed by AV, 4-Jul-2021.)
|
⊢ ((𝐾 ∈ ℤ ∧ (𝐿 ∈ ℤ ∧ 𝐿 ≠ 0) ∧ ¬ 𝐿 ∥ 𝐾) → (⌊‘(𝐾 / 𝐿)) < (𝐾 / 𝐿)) |
|
Theorem | flodddiv4lt 11560 |
The floor of an odd number divided by 4 is less than the odd number
divided by 4. (Contributed by AV, 4-Jul-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (⌊‘(𝑁 / 4)) < (𝑁 / 4)) |
|
Theorem | flodddiv4t2lthalf 11561 |
The floor of an odd number divided by 4, multiplied by 2 is less than the
half of the odd number. (Contributed by AV, 4-Jul-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → ((⌊‘(𝑁 / 4)) · 2) < (𝑁 / 2)) |
|
5.1.4 The greatest common divisor
operator
|
|
Syntax | cgcd 11562 |
Extend the definition of a class to include the greatest common divisor
operator.
|
class gcd |
|
Definition | df-gcd 11563* |
Define the gcd operator. For example, (-6 gcd 9) = 3
(ex-gcd 12870). (Contributed by Paul Chapman,
21-Mar-2011.)
|
⊢ gcd = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦)}, ℝ, < ))) |
|
Theorem | gcdmndc 11564 |
Decidablity lemma used in various proofs related to gcd.
(Contributed by Jim Kingdon, 12-Dec-2021.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
DECID (𝑀 =
0 ∧ 𝑁 =
0)) |
|
Theorem | zsupcllemstep 11565* |
Lemma for zsupcl 11567. Induction step. (Contributed by Jim
Kingdon,
7-Dec-2021.)
|
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → DECID
𝜓)
⇒ ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) → ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))))) |
|
Theorem | zsupcllemex 11566* |
Lemma for zsupcl 11567. Existence of the supremum. (Contributed
by Jim
Kingdon, 7-Dec-2021.)
|
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜒)
& ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → DECID
𝜓) & ⊢ (𝜑 → ∃𝑗 ∈ (ℤ≥‘𝑀)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) |
|
Theorem | zsupcl 11567* |
Closure of supremum for decidable integer properties. The property
which defines the set we are taking the supremum of must (a) be true at
𝑀 (which corresponds to the nonempty
condition of classical supremum
theorems), (b) decidable at each value after 𝑀, and (c) be false
after 𝑗 (which corresponds to the upper bound
condition found in
classical supremum theorems). (Contributed by Jim Kingdon,
7-Dec-2021.)
|
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜒)
& ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → DECID
𝜓) & ⊢ (𝜑 → ∃𝑗 ∈ (ℤ≥‘𝑀)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ 𝜓) ⇒ ⊢ (𝜑 → sup({𝑛 ∈ ℤ ∣ 𝜓}, ℝ, < ) ∈
(ℤ≥‘𝑀)) |
|
Theorem | zssinfcl 11568* |
The infimum of a set of integers is an element of the set. (Contributed
by Jim Kingdon, 16-Jan-2022.)
|
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐵 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐵 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ⊆ ℤ) & ⊢ (𝜑 → inf(𝐵, ℝ, < ) ∈
ℤ) ⇒ ⊢ (𝜑 → inf(𝐵, ℝ, < ) ∈ 𝐵) |
|
Theorem | infssuzex 11569* |
Existence of the infimum of a subset of an upper set of integers.
(Contributed by Jim Kingdon, 13-Jan-2022.)
|
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑆 = {𝑛 ∈ (ℤ≥‘𝑀) ∣ 𝜓}
& ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝐴)) → DECID 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑆 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝑆 𝑧 < 𝑦))) |
|
Theorem | infssuzledc 11570* |
The infimum of a subset of an upper set of integers is less than or
equal to all members of the subset. (Contributed by Jim Kingdon,
13-Jan-2022.)
|
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑆 = {𝑛 ∈ (ℤ≥‘𝑀) ∣ 𝜓}
& ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝐴)) → DECID 𝜓) ⇒ ⊢ (𝜑 → inf(𝑆, ℝ, < ) ≤ 𝐴) |
|
Theorem | infssuzcldc 11571* |
The infimum of a subset of an upper set of integers belongs to the
subset. (Contributed by Jim Kingdon, 20-Jan-2022.)
|
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑆 = {𝑛 ∈ (ℤ≥‘𝑀) ∣ 𝜓}
& ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝐴)) → DECID 𝜓) ⇒ ⊢ (𝜑 → inf(𝑆, ℝ, < ) ∈ 𝑆) |
|
Theorem | dvdsbnd 11572* |
There is an upper bound to the divisors of a nonzero integer.
(Contributed by Jim Kingdon, 11-Dec-2021.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → ∃𝑛 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑛) ¬ 𝑚 ∥ 𝐴) |
|
Theorem | gcdsupex 11573* |
Existence of the supremum used in defining gcd.
(Contributed by
Jim Kingdon, 12-Dec-2021.)
|
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬ (𝑋 = 0 ∧ 𝑌 = 0)) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)}𝑦 < 𝑧))) |
|
Theorem | gcdsupcl 11574* |
Closure of the supremum used in defining gcd. A lemma
for gcdval 11575
and gcdn0cl 11578. (Contributed by Jim Kingdon, 11-Dec-2021.)
|
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬ (𝑋 = 0 ∧ 𝑌 = 0)) → sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)}, ℝ, < ) ∈
ℕ) |
|
Theorem | gcdval 11575* |
The value of the gcd operator. (𝑀 gcd 𝑁) is the greatest
common divisor of 𝑀 and 𝑁. If 𝑀 and
𝑁
are both 0,
the result is defined conventionally as 0.
(Contributed by Paul
Chapman, 21-Mar-2011.) (Revised by Mario Carneiro, 10-Nov-2013.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ))) |
|
Theorem | gcd0val 11576 |
The value, by convention, of the gcd operator when both
operands are
0. (Contributed by Paul Chapman, 21-Mar-2011.)
|
⊢ (0 gcd 0) = 0 |
|
Theorem | gcdn0val 11577* |
The value of the gcd operator when at least one operand
is nonzero.
(Contributed by Paul Chapman, 21-Mar-2011.)
|
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) |
|
Theorem | gcdn0cl 11578 |
Closure of the gcd operator. (Contributed by Paul
Chapman,
21-Mar-2011.)
|
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) ∈ ℕ) |
|
Theorem | gcddvds 11579 |
The gcd of two integers divides each of them. (Contributed by Paul
Chapman, 21-Mar-2011.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) |
|
Theorem | dvdslegcd 11580 |
An integer which divides both operands of the gcd
operator is
bounded by it. (Contributed by Paul Chapman, 21-Mar-2011.)
|
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ≤ (𝑀 gcd 𝑁))) |
|
Theorem | nndvdslegcd 11581 |
A positive integer which divides both positive operands of the gcd
operator is bounded by it. (Contributed by AV, 9-Aug-2020.)
|
⊢ ((𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ≤ (𝑀 gcd 𝑁))) |
|
Theorem | gcdcl 11582 |
Closure of the gcd operator. (Contributed by Paul
Chapman,
21-Mar-2011.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈
ℕ0) |
|
Theorem | gcdnncl 11583 |
Closure of the gcd operator. (Contributed by Thierry
Arnoux,
2-Feb-2020.)
|
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℕ) |
|
Theorem | gcdcld 11584 |
Closure of the gcd operator. (Contributed by Mario
Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ)
⇒ ⊢ (𝜑 → (𝑀 gcd 𝑁) ∈
ℕ0) |
|
Theorem | gcd2n0cl 11585 |
Closure of the gcd operator if the second operand is
not 0.
(Contributed by AV, 10-Jul-2021.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑀 gcd 𝑁) ∈ ℕ) |
|
Theorem | zeqzmulgcd 11586* |
An integer is the product of an integer and the gcd of it and another
integer. (Contributed by AV, 11-Jul-2021.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∃𝑛 ∈ ℤ 𝐴 = (𝑛 · (𝐴 gcd 𝐵))) |
|
Theorem | divgcdz 11587 |
An integer divided by the gcd of it and a nonzero integer is an integer.
(Contributed by AV, 11-Jul-2021.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ) |
|
Theorem | gcdf 11588 |
Domain and codomain of the gcd operator. (Contributed
by Paul
Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 16-Nov-2013.)
|
⊢ gcd :(ℤ ×
ℤ)⟶ℕ0 |
|
Theorem | gcdcom 11589 |
The gcd operator is commutative. Theorem 1.4(a) in [ApostolNT]
p. 16. (Contributed by Paul Chapman, 21-Mar-2011.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)) |
|
Theorem | divgcdnn 11590 |
A positive integer divided by the gcd of it and another integer is a
positive integer. (Contributed by AV, 10-Jul-2021.)
|
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ) → (𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ) |
|
Theorem | divgcdnnr 11591 |
A positive integer divided by the gcd of it and another integer is a
positive integer. (Contributed by AV, 10-Jul-2021.)
|
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ) → (𝐴 / (𝐵 gcd 𝐴)) ∈ ℕ) |
|
Theorem | gcdeq0 11592 |
The gcd of two integers is zero iff they are both zero. (Contributed by
Paul Chapman, 21-Mar-2011.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) = 0 ↔ (𝑀 = 0 ∧ 𝑁 = 0))) |
|
Theorem | gcdn0gt0 11593 |
The gcd of two integers is positive (nonzero) iff they are not both zero.
(Contributed by Paul Chapman, 22-Jun-2011.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑀 = 0 ∧ 𝑁 = 0) ↔ 0 < (𝑀 gcd 𝑁))) |
|
Theorem | gcd0id 11594 |
The gcd of 0 and an integer is the integer's absolute value. (Contributed
by Paul Chapman, 21-Mar-2011.)
|
⊢ (𝑁 ∈ ℤ → (0 gcd 𝑁) = (abs‘𝑁)) |
|
Theorem | gcdid0 11595 |
The gcd of an integer and 0 is the integer's absolute value. Theorem
1.4(d)2 in [ApostolNT] p. 16.
(Contributed by Paul Chapman,
31-Mar-2011.)
|
⊢ (𝑁 ∈ ℤ → (𝑁 gcd 0) = (abs‘𝑁)) |
|
Theorem | nn0gcdid0 11596 |
The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul
Chapman, 31-Mar-2011.)
|
⊢ (𝑁 ∈ ℕ0 → (𝑁 gcd 0) = 𝑁) |
|
Theorem | gcdneg 11597 |
Negating one operand of the gcd operator does not alter
the result.
(Contributed by Paul Chapman, 21-Mar-2011.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁)) |
|
Theorem | neggcd 11598 |
Negating one operand of the gcd operator does not alter
the result.
(Contributed by Paul Chapman, 22-Jun-2011.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁)) |
|
Theorem | gcdaddm 11599 |
Adding a multiple of one operand of the gcd operator to
the other does
not alter the result. (Contributed by Paul Chapman, 31-Mar-2011.)
|
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑀 gcd (𝑁 + (𝐾 · 𝑀)))) |
|
Theorem | gcdadd 11600 |
The GCD of two numbers is the same as the GCD of the left and their sum.
(Contributed by Scott Fenton, 20-Apr-2014.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑀 gcd (𝑁 + 𝑀))) |