Theorem List for Intuitionistic Logic Explorer - 11601-11700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | zeo3 11601 |
An integer is even or odd. (Contributed by AV, 17-Jun-2021.)
|
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ∨ ¬ 2 ∥ 𝑁)) |
|
Theorem | zeoxor 11602 |
An integer is even or odd but not both. (Contributed by Jim Kingdon,
10-Nov-2021.)
|
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ⊻ ¬ 2 ∥ 𝑁)) |
|
Theorem | zeo4 11603 |
An integer is even or odd but not both. (Contributed by AV,
17-Jun-2021.)
|
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥
𝑁)) |
|
Theorem | zeneo 11604 |
No even integer equals an odd integer (i.e. no integer can be both even
and odd). Exercise 10(a) of [Apostol] p.
28. This variant of zneo 9176
follows immediately from the fact that a contradiction implies anything,
see pm2.21i 636. (Contributed by AV, 22-Jun-2021.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵) → 𝐴 ≠ 𝐵)) |
|
Theorem | odd2np1lem 11605* |
Lemma for odd2np1 11606. (Contributed by Scott Fenton, 3-Apr-2014.)
(Revised by Mario Carneiro, 19-Apr-2014.)
|
⊢ (𝑁 ∈ ℕ0 →
(∃𝑛 ∈ ℤ
((2 · 𝑛) + 1) =
𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
|
Theorem | odd2np1 11606* |
An integer is odd iff it is one plus twice another integer.
(Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥
𝑁 ↔ ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) |
|
Theorem | even2n 11607* |
An integer is even iff it is twice another integer. (Contributed by AV,
25-Jun-2020.)
|
⊢ (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (2 · 𝑛) = 𝑁) |
|
Theorem | oddm1even 11608 |
An integer is odd iff its predecessor is even. (Contributed by Mario
Carneiro, 5-Sep-2016.)
|
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥
𝑁 ↔ 2 ∥ (𝑁 − 1))) |
|
Theorem | oddp1even 11609 |
An integer is odd iff its successor is even. (Contributed by Mario
Carneiro, 5-Sep-2016.)
|
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥
𝑁 ↔ 2 ∥ (𝑁 + 1))) |
|
Theorem | oexpneg 11610 |
The exponential of the negative of a number, when the exponent is odd.
(Contributed by Mario Carneiro, 25-Apr-2015.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁) → (-𝐴↑𝑁) = -(𝐴↑𝑁)) |
|
Theorem | mod2eq0even 11611 |
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 11612 |
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 11613* |
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 11614* |
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 11615* |
A nonnegative integer is even iff it is twice another nonnegative
integer. (Contributed by AV, 12-Aug-2021.)
|
⊢ (𝑁 ∈ ℕ0 → (2
∥ 𝑁 ↔
∃𝑛 ∈
ℕ0 (2 · 𝑛) = 𝑁)) |
|
Theorem | evennn2n 11616* |
A positive integer is even iff it is twice another positive integer.
(Contributed by AV, 12-Aug-2021.)
|
⊢ (𝑁 ∈ ℕ → (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ (2 ·
𝑛) = 𝑁)) |
|
Theorem | 2tp1odd 11617 |
A number which is twice an integer increased by 1 is odd. (Contributed
by AV, 16-Jul-2021.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 = ((2 · 𝐴) + 1)) → ¬ 2 ∥ 𝐵) |
|
Theorem | mulsucdiv2z 11618 |
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 11619 |
A squared odd number minus 1 divided by 8 is an integer. (Contributed
by AV, 19-Jul-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (((𝑁↑2) − 1) / 8) ∈
ℤ) |
|
Theorem | 2teven 11620 |
A number which is twice an integer is even. (Contributed by AV,
16-Jul-2021.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 = (2 · 𝐴)) → 2 ∥ 𝐵) |
|
Theorem | zeo5 11621 |
An integer is either even or odd, version of zeo3 11601
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 11622 |
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 9180 and zeo2 9181. (Contributed by AV, 22-Jun-2021.)
|
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ (𝑁 / 2) ∈ ℤ)) |
|
Theorem | oddp1d2 11623 |
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 9180 and zeo2 9181. (Contributed by AV, 22-Jun-2021.)
|
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥
𝑁 ↔ ((𝑁 + 1) / 2) ∈
ℤ)) |
|
Theorem | zob 11624 |
Alternate characterizations of an odd number. (Contributed by AV,
7-Jun-2020.)
|
⊢ (𝑁 ∈ ℤ → (((𝑁 + 1) / 2) ∈ ℤ ↔ ((𝑁 − 1) / 2) ∈
ℤ)) |
|
Theorem | oddm1d2 11625 |
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 11626 |
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 11627 |
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 11628 |
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 11629 |
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 11630 |
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 11631 |
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 11632 |
Exponentiation of -1 by an even power. Variant of m1expeven 10371.
(Contributed by AV, 25-Jun-2021.)
|
⊢ (2 ∥ 𝑁 → (-1↑𝑁) = 1) |
|
Theorem | m1expo 11633 |
Exponentiation of -1 by an odd power. (Contributed by AV,
26-Jun-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (-1↑𝑁) = -1) |
|
Theorem | m1exp1 11634 |
Exponentiation of negative one is one iff the exponent is even.
(Contributed by AV, 20-Jun-2021.)
|
⊢ (𝑁 ∈ ℤ → ((-1↑𝑁) = 1 ↔ 2 ∥ 𝑁)) |
|
Theorem | nn0enne 11635 |
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 11636 |
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 11637 |
The half of an even positive integer is a positive integer. (Contributed
by AV, 28-Jun-2021.)
|
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℕ) |
|
Theorem | nn0o1gt2 11638 |
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 11639 |
An alternate characterization of an odd integer greater than 1.
(Contributed by AV, 2-Jun-2020.)
|
⊢ ((𝑁 ∈ (ℤ≥‘2)
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((𝑁 − 1) / 2) ∈
ℕ) |
|
Theorem | nn0o 11640 |
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 11641 |
Alternate characterizations of an odd nonnegative integer. (Contributed
by AV, 4-Jun-2020.)
|
⊢ (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈
ℕ0 ↔ ((𝑁 − 1) / 2) ∈
ℕ0)) |
|
Theorem | nn0oddm1d2 11642 |
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 11643 |
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 11644 |
0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV,
23-Jun-2021.)
|
⊢ 2 ∥ 0 |
|
Theorem | n2dvds1 11645 |
2 does not divide 1 (common case). That means 1 is odd. (Contributed by
David A. Wheeler, 8-Dec-2018.)
|
⊢ ¬ 2 ∥ 1 |
|
Theorem | n2dvdsm1 11646 |
2 does not divide -1. That means -1 is odd. (Contributed by AV,
15-Aug-2021.)
|
⊢ ¬ 2 ∥ -1 |
|
Theorem | z2even 11647 |
2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV,
23-Jun-2021.)
|
⊢ 2 ∥ 2 |
|
Theorem | n2dvds3 11648 |
2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV,
28-Feb-2021.)
|
⊢ ¬ 2 ∥ 3 |
|
Theorem | z4even 11649 |
4 is an even number. (Contributed by AV, 23-Jul-2020.) (Revised by AV,
4-Jul-2021.)
|
⊢ 2 ∥ 4 |
|
Theorem | 4dvdseven 11650 |
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 11651* |
Lemma for divalg 11657. Existence for a positive denominator.
(Contributed by Jim Kingdon, 30-Nov-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
|
Theorem | divalglemqt 11652 |
Lemma for divalg 11657. The 𝑄 = 𝑇 case involved in showing uniqueness.
(Contributed by Jim Kingdon, 5-Dec-2021.)
|
⊢ (𝜑 → 𝐷 ∈ ℤ) & ⊢ (𝜑 → 𝑅 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℤ) & ⊢ (𝜑 → 𝑄 ∈ ℤ) & ⊢ (𝜑 → 𝑇 ∈ ℤ) & ⊢ (𝜑 → 𝑄 = 𝑇)
& ⊢ (𝜑 → ((𝑄 · 𝐷) + 𝑅) = ((𝑇 · 𝐷) + 𝑆)) ⇒ ⊢ (𝜑 → 𝑅 = 𝑆) |
|
Theorem | divalglemnqt 11653 |
Lemma for divalg 11657. The 𝑄 < 𝑇 case involved in showing uniqueness.
(Contributed by Jim Kingdon, 4-Dec-2021.)
|
⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℤ) & ⊢ (𝜑 → 𝑄 ∈ ℤ) & ⊢ (𝜑 → 𝑇 ∈ ℤ) & ⊢ (𝜑 → 0 ≤ 𝑆)
& ⊢ (𝜑 → 𝑅 < 𝐷)
& ⊢ (𝜑 → ((𝑄 · 𝐷) + 𝑅) = ((𝑇 · 𝐷) + 𝑆)) ⇒ ⊢ (𝜑 → ¬ 𝑄 < 𝑇) |
|
Theorem | divalglemeunn 11654* |
Lemma for divalg 11657. Uniqueness for a positive denominator.
(Contributed by Jim Kingdon, 4-Dec-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
|
Theorem | divalglemex 11655* |
Lemma for divalg 11657. The quotient and remainder exist.
(Contributed by
Jim Kingdon, 30-Nov-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
|
Theorem | divalglemeuneg 11656* |
Lemma for divalg 11657. Uniqueness for a negative denominator.
(Contributed by Jim Kingdon, 4-Dec-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) |
|
Theorem | divalg 11657* |
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 11658* |
Express the division algorithm as stated in divalg 11657 in terms of
∥. (Contributed by Paul Chapman,
31-Mar-2011.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℕ0 (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))) |
|
Theorem | divalg2 11659* |
The division algorithm (theorem) for a positive divisor. (Contributed
by Paul Chapman, 21-Mar-2011.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℕ0
(𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟))) |
|
Theorem | divalgmod 11660 |
The result of the mod operator satisfies the
requirements for the
remainder 𝑅 in the division algorithm for a
positive divisor
(compare divalg2 11659 and divalgb 11658). 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 11661 |
The result of the mod operator satisfies the
requirements for the
remainder 𝑅 in the division algorithm for a
positive divisor. Variant
of divalgmod 11660. (Contributed by Stefan O'Rear,
17-Oct-2014.) (Proof
shortened by AV, 21-Aug-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝑅 ∈ ℕ0) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅)))) |
|
Theorem | modremain 11662* |
The result of the modulo operation is the remainder of the division
algorithm. (Contributed by AV, 19-Aug-2021.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷)) → ((𝑁 mod 𝐷) = 𝑅 ↔ ∃𝑧 ∈ ℤ ((𝑧 · 𝐷) + 𝑅) = 𝑁)) |
|
Theorem | ndvdssub 11663 |
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 11664 |
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 11665 |
Special case of ndvdsadd 11664. If an integer 𝐷 greater than 1
divides 𝑁, it does not divide 𝑁 + 1.
(Contributed by Paul
Chapman, 31-Mar-2011.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 1 < 𝐷) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 + 1))) |
|
Theorem | ndvdsi 11666 |
A quick test for non-divisibility. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝐴 ∈ ℕ & ⊢ 𝑄 ∈
ℕ0
& ⊢ 𝑅 ∈ ℕ & ⊢ ((𝐴 · 𝑄) + 𝑅) = 𝐵
& ⊢ 𝑅 < 𝐴 ⇒ ⊢ ¬ 𝐴 ∥ 𝐵 |
|
Theorem | flodddiv4 11667 |
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 11668 |
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 11669 |
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 11670 |
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 11671 |
Extend the definition of a class to include the greatest common divisor
operator.
|
class gcd |
|
Definition | df-gcd 11672* |
Define the gcd operator. For example, (-6 gcd 9) = 3
(ex-gcd 13114). (Contributed by Paul Chapman,
21-Mar-2011.)
|
⊢ gcd = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦)}, ℝ, < ))) |
|
Theorem | gcdmndc 11673 |
Decidablity lemma used in various proofs related to gcd.
(Contributed by Jim Kingdon, 12-Dec-2021.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
DECID (𝑀 =
0 ∧ 𝑁 =
0)) |
|
Theorem | zsupcllemstep 11674* |
Lemma for zsupcl 11676. Induction step. (Contributed by Jim
Kingdon,
7-Dec-2021.)
|
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → DECID
𝜓)
⇒ ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) → ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))))) |
|
Theorem | zsupcllemex 11675* |
Lemma for zsupcl 11676. Existence of the supremum. (Contributed
by Jim
Kingdon, 7-Dec-2021.)
|
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜒)
& ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → DECID
𝜓) & ⊢ (𝜑 → ∃𝑗 ∈ (ℤ≥‘𝑀)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) |
|
Theorem | zsupcl 11676* |
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 11677* |
The infimum of a set of integers is an element of the set. (Contributed
by Jim Kingdon, 16-Jan-2022.)
|
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐵 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐵 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ⊆ ℤ) & ⊢ (𝜑 → inf(𝐵, ℝ, < ) ∈
ℤ) ⇒ ⊢ (𝜑 → inf(𝐵, ℝ, < ) ∈ 𝐵) |
|
Theorem | infssuzex 11678* |
Existence of the infimum of a subset of an upper set of integers.
(Contributed by Jim Kingdon, 13-Jan-2022.)
|
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑆 = {𝑛 ∈ (ℤ≥‘𝑀) ∣ 𝜓}
& ⊢ (𝜑 → 𝐴 ∈ 𝑆)
& ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝐴)) → DECID 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑆 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝑆 𝑧 < 𝑦))) |
|
Theorem | infssuzledc 11679* |
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 11680* |
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 11681* |
There is an upper bound to the divisors of a nonzero integer.
(Contributed by Jim Kingdon, 11-Dec-2021.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → ∃𝑛 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑛) ¬ 𝑚 ∥ 𝐴) |
|
Theorem | gcdsupex 11682* |
Existence of the supremum used in defining gcd.
(Contributed by
Jim Kingdon, 12-Dec-2021.)
|
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬ (𝑋 = 0 ∧ 𝑌 = 0)) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)}𝑦 < 𝑧))) |
|
Theorem | gcdsupcl 11683* |
Closure of the supremum used in defining gcd. A lemma
for gcdval 11684
and gcdn0cl 11687. (Contributed by Jim Kingdon, 11-Dec-2021.)
|
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬ (𝑋 = 0 ∧ 𝑌 = 0)) → sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)}, ℝ, < ) ∈
ℕ) |
|
Theorem | gcdval 11684* |
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 11685 |
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 11686* |
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 11687 |
Closure of the gcd operator. (Contributed by Paul
Chapman,
21-Mar-2011.)
|
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) ∈ ℕ) |
|
Theorem | gcddvds 11688 |
The gcd of two integers divides each of them. (Contributed by Paul
Chapman, 21-Mar-2011.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) |
|
Theorem | dvdslegcd 11689 |
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 11690 |
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 11691 |
Closure of the gcd operator. (Contributed by Paul
Chapman,
21-Mar-2011.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈
ℕ0) |
|
Theorem | gcdnncl 11692 |
Closure of the gcd operator. (Contributed by Thierry
Arnoux,
2-Feb-2020.)
|
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℕ) |
|
Theorem | gcdcld 11693 |
Closure of the gcd operator. (Contributed by Mario
Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ)
⇒ ⊢ (𝜑 → (𝑀 gcd 𝑁) ∈
ℕ0) |
|
Theorem | gcd2n0cl 11694 |
Closure of the gcd operator if the second operand is
not 0.
(Contributed by AV, 10-Jul-2021.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑀 gcd 𝑁) ∈ ℕ) |
|
Theorem | zeqzmulgcd 11695* |
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 11696 |
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 11697 |
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 11698 |
The gcd operator is commutative. Theorem 1.4(a) in [ApostolNT]
p. 16. (Contributed by Paul Chapman, 21-Mar-2011.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)) |
|
Theorem | divgcdnn 11699 |
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 11700 |
A positive integer divided by the gcd of it and another integer is a
positive integer. (Contributed by AV, 10-Jul-2021.)
|
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ) → (𝐴 / (𝐵 gcd 𝐴)) ∈ ℕ) |