Type | Label | Description |
Statement |
|
Theorem | opeo 11901 |
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 11902 |
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 11903 |
Exponentiation of -1 by an even power. Variant of m1expeven 10566.
(Contributed by AV, 25-Jun-2021.)
|
β’ (2 β₯ π β (-1βπ) = 1) |
|
Theorem | m1expo 11904 |
Exponentiation of -1 by an odd power. (Contributed by AV,
26-Jun-2021.)
|
β’ ((π β β€ β§ Β¬ 2 β₯ π) β (-1βπ) = -1) |
|
Theorem | m1exp1 11905 |
Exponentiation of negative one is one iff the exponent is even.
(Contributed by AV, 20-Jun-2021.)
|
β’ (π β β€ β ((-1βπ) = 1 β 2 β₯ π)) |
|
Theorem | nn0enne 11906 |
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 11907 |
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 11908 |
The half of an even positive integer is a positive integer. (Contributed
by AV, 28-Jun-2021.)
|
β’ ((π β β β§ 2 β₯ π) β (π / 2) β β) |
|
Theorem | nn0o1gt2 11909 |
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 11910 |
An alternate characterization of an odd integer greater than 1.
(Contributed by AV, 2-Jun-2020.)
|
β’ ((π β (β€β₯β2)
β§ ((π + 1) / 2) β
β0) β ((π β 1) / 2) β
β) |
|
Theorem | nn0o 11911 |
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 11912 |
Alternate characterizations of an odd nonnegative integer. (Contributed
by AV, 4-Jun-2020.)
|
β’ (π β β0 β (((π + 1) / 2) β
β0 β ((π β 1) / 2) β
β0)) |
|
Theorem | nn0oddm1d2 11913 |
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 11914 |
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 11915 |
0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV,
23-Jun-2021.)
|
β’ 2 β₯ 0 |
|
Theorem | n2dvds1 11916 |
2 does not divide 1 (common case). That means 1 is odd. (Contributed by
David A. Wheeler, 8-Dec-2018.)
|
β’ Β¬ 2 β₯ 1 |
|
Theorem | n2dvdsm1 11917 |
2 does not divide -1. That means -1 is odd. (Contributed by AV,
15-Aug-2021.)
|
β’ Β¬ 2 β₯ -1 |
|
Theorem | z2even 11918 |
2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV,
23-Jun-2021.)
|
β’ 2 β₯ 2 |
|
Theorem | n2dvds3 11919 |
2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV,
28-Feb-2021.)
|
β’ Β¬ 2 β₯ 3 |
|
Theorem | z4even 11920 |
4 is an even number. (Contributed by AV, 23-Jul-2020.) (Revised by AV,
4-Jul-2021.)
|
β’ 2 β₯ 4 |
|
Theorem | 4dvdseven 11921 |
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 11922* |
Lemma for divalg 11928. Existence for a positive denominator.
(Contributed by Jim Kingdon, 30-Nov-2021.)
|
β’ ((π β β€ β§ π· β β) β βπ β β€ βπ β β€ (0 β€ π β§ π < (absβπ·) β§ π = ((π Β· π·) + π))) |
|
Theorem | divalglemqt 11923 |
Lemma for divalg 11928. The π = π case involved in showing uniqueness.
(Contributed by Jim Kingdon, 5-Dec-2021.)
|
β’ (π β π· β β€) & β’ (π β π
β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π = π)
& β’ (π β ((π Β· π·) + π
) = ((π Β· π·) + π)) β β’ (π β π
= π) |
|
Theorem | divalglemnqt 11924 |
Lemma for divalg 11928. The π < π case involved in showing uniqueness.
(Contributed by Jim Kingdon, 4-Dec-2021.)
|
β’ (π β π· β β) & β’ (π β π
β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β 0 β€ π)
& β’ (π β π
< π·)
& β’ (π β ((π Β· π·) + π
) = ((π Β· π·) + π)) β β’ (π β Β¬ π < π) |
|
Theorem | divalglemeunn 11925* |
Lemma for divalg 11928. Uniqueness for a positive denominator.
(Contributed by Jim Kingdon, 4-Dec-2021.)
|
β’ ((π β β€ β§ π· β β) β β!π β β€ βπ β β€ (0 β€ π β§ π < (absβπ·) β§ π = ((π Β· π·) + π))) |
|
Theorem | divalglemex 11926* |
Lemma for divalg 11928. The quotient and remainder exist.
(Contributed by
Jim Kingdon, 30-Nov-2021.)
|
β’ ((π β β€ β§ π· β β€ β§ π· β 0) β βπ β β€ βπ β β€ (0 β€ π β§ π < (absβπ·) β§ π = ((π Β· π·) + π))) |
|
Theorem | divalglemeuneg 11927* |
Lemma for divalg 11928. Uniqueness for a negative denominator.
(Contributed by Jim Kingdon, 4-Dec-2021.)
|
β’ ((π β β€ β§ π· β β€ β§ π· < 0) β β!π β β€ βπ β β€ (0 β€ π β§ π < (absβπ·) β§ π = ((π Β· π·) + π))) |
|
Theorem | divalg 11928* |
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 11929* |
Express the division algorithm as stated in divalg 11928 in terms of
β₯. (Contributed by Paul Chapman,
31-Mar-2011.)
|
β’ ((π β β€ β§ π· β β€ β§ π· β 0) β (β!π β β€ βπ β β€ (0 β€ π β§ π < (absβπ·) β§ π = ((π Β· π·) + π)) β β!π β β0 (π < (absβπ·) β§ π· β₯ (π β π)))) |
|
Theorem | divalg2 11930* |
The division algorithm (theorem) for a positive divisor. (Contributed
by Paul Chapman, 21-Mar-2011.)
|
β’ ((π β β€ β§ π· β β) β β!π β β0
(π < π· β§ π· β₯ (π β π))) |
|
Theorem | divalgmod 11931 |
The result of the mod operator satisfies the
requirements for the
remainder π
in the division algorithm for a
positive divisor
(compare divalg2 11930 and divalgb 11929). 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 11932 |
The result of the mod operator satisfies the
requirements for the
remainder π
in the division algorithm for a
positive divisor. Variant
of divalgmod 11931. (Contributed by Stefan O'Rear,
17-Oct-2014.) (Proof
shortened by AV, 21-Aug-2021.)
|
β’ ((π β β€ β§ π· β β β§ π
β β0) β (π
= (π mod π·) β (π
< π· β§ π· β₯ (π β π
)))) |
|
Theorem | modremain 11933* |
The result of the modulo operation is the remainder of the division
algorithm. (Contributed by AV, 19-Aug-2021.)
|
β’ ((π β β€ β§ π· β β β§ (π
β β0 β§ π
< π·)) β ((π mod π·) = π
β βπ§ β β€ ((π§ Β· π·) + π
) = π)) |
|
Theorem | ndvdssub 11934 |
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 11935 |
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 11936 |
Special case of ndvdsadd 11935. If an integer π· greater than 1
divides π, it does not divide π + 1.
(Contributed by Paul
Chapman, 31-Mar-2011.)
|
β’ ((π β β€ β§ π· β β β§ 1 < π·) β (π· β₯ π β Β¬ π· β₯ (π + 1))) |
|
Theorem | ndvdsi 11937 |
A quick test for non-divisibility. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
β’ π΄ β β & β’ π β
β0
& β’ π
β β & β’ ((π΄ Β· π) + π
) = π΅
& β’ π
< π΄ β β’ Β¬ π΄ β₯ π΅ |
|
Theorem | flodddiv4 11938 |
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 11939 |
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 11940 |
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 11941 |
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 11942 |
Extend the definition of a class to include the greatest common divisor
operator.
|
class gcd |
|
Definition | df-gcd 11943* |
Define the gcd operator. For example, (-6 gcd 9) = 3
(ex-gcd 14453). (Contributed by Paul Chapman,
21-Mar-2011.)
|
β’ gcd = (π₯ β β€, π¦ β β€ β¦ if((π₯ = 0 β§ π¦ = 0), 0, sup({π β β€ β£ (π β₯ π₯ β§ π β₯ π¦)}, β, < ))) |
|
Theorem | gcdmndc 11944 |
Decidablity lemma used in various proofs related to gcd.
(Contributed by Jim Kingdon, 12-Dec-2021.)
|
β’ ((π β β€ β§ π β β€) β
DECID (π =
0 β§ π =
0)) |
|
Theorem | zsupcllemstep 11945* |
Lemma for zsupcl 11947. Induction step. (Contributed by Jim
Kingdon,
7-Dec-2021.)
|
β’ ((π β§ π β (β€β₯βπ)) β DECID
π)
β β’ (πΎ β (β€β₯βπ) β (((π β§ βπ β (β€β₯βπΎ) Β¬ π) β βπ₯ β β€ (βπ¦ β {π β β€ β£ π} Β¬ π₯ < π¦ β§ βπ¦ β β (π¦ < π₯ β βπ§ β {π β β€ β£ π}π¦ < π§))) β ((π β§ βπ β (β€β₯β(πΎ + 1)) Β¬ π) β βπ₯ β β€ (βπ¦ β {π β β€ β£ π} Β¬ π₯ < π¦ β§ βπ¦ β β (π¦ < π₯ β βπ§ β {π β β€ β£ π}π¦ < π§))))) |
|
Theorem | zsupcllemex 11946* |
Lemma for zsupcl 11947. Existence of the supremum. (Contributed
by Jim
Kingdon, 7-Dec-2021.)
|
β’ (π β π β β€) & β’ (π = π β (π β π)) & β’ (π β π)
& β’ ((π β§ π β (β€β₯βπ)) β DECID
π) & β’ (π β βπ β (β€β₯βπ)βπ β (β€β₯βπ) Β¬ π) β β’ (π β βπ₯ β β€ (βπ¦ β {π β β€ β£ π} Β¬ π₯ < π¦ β§ βπ¦ β β (π¦ < π₯ β βπ§ β {π β β€ β£ π}π¦ < π§))) |
|
Theorem | zsupcl 11947* |
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 11948* |
The infimum of a set of integers is an element of the set. (Contributed
by Jim Kingdon, 16-Jan-2022.)
|
β’ (π β βπ₯ β β (βπ¦ β π΅ Β¬ π¦ < π₯ β§ βπ¦ β β (π₯ < π¦ β βπ§ β π΅ π§ < π¦))) & β’ (π β π΅ β β€) & β’ (π β inf(π΅, β, < ) β
β€) β β’ (π β inf(π΅, β, < ) β π΅) |
|
Theorem | infssuzex 11949* |
Existence of the infimum of a subset of an upper set of integers.
(Contributed by Jim Kingdon, 13-Jan-2022.)
|
β’ (π β π β β€) & β’ π = {π β (β€β₯βπ) β£ π}
& β’ (π β π΄ β π)
& β’ ((π β§ π β (π...π΄)) β DECID π) β β’ (π β βπ₯ β β (βπ¦ β π Β¬ π¦ < π₯ β§ βπ¦ β β (π₯ < π¦ β βπ§ β π π§ < π¦))) |
|
Theorem | infssuzledc 11950* |
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 11951* |
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 | suprzubdc 11952* |
The supremum of a bounded-above decidable set of integers is greater
than any member of the set. (Contributed by Mario Carneiro,
21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
|
β’ (π β π΄ β β€) & β’ (π β βπ₯ β β€
DECID π₯
β π΄) & β’ (π β βπ₯ β β€ βπ¦ β π΄ π¦ β€ π₯)
& β’ (π β π΅ β π΄) β β’ (π β π΅ β€ sup(π΄, β, < )) |
|
Theorem | nninfdcex 11953* |
A decidable set of natural numbers has an infimum. (Contributed by Jim
Kingdon, 28-Sep-2024.)
|
β’ (π β π΄ β β) & β’ (π β βπ₯ β β
DECID π₯
β π΄) & β’ (π β βπ¦ π¦ β π΄) β β’ (π β βπ₯ β β (βπ¦ β π΄ Β¬ π¦ < π₯ β§ βπ¦ β β (π₯ < π¦ β βπ§ β π΄ π§ < π¦))) |
|
Theorem | zsupssdc 11954* |
An inhabited decidable bounded subset of integers has a supremum in the
set. (The proof does not use ax-pre-suploc 7931.) (Contributed by Mario
Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
|
β’ (π β π΄ β β€) & β’ (π β βπ₯ π₯ β π΄)
& β’ (π β βπ₯ β β€ DECID π₯ β π΄)
& β’ (π β βπ₯ β β€ βπ¦ β π΄ π¦ β€ π₯) β β’ (π β βπ₯ β π΄ (βπ¦ β π΄ Β¬ π₯ < π¦ β§ βπ¦ β π΅ (π¦ < π₯ β βπ§ β π΄ π¦ < π§))) |
|
Theorem | suprzcl2dc 11955* |
The supremum of a bounded-above decidable set of integers is a member of
the set. (This theorem avoids ax-pre-suploc 7931.) (Contributed by Mario
Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 6-Oct-2024.)
|
β’ (π β π΄ β β€) & β’ (π β βπ₯ β β€
DECID π₯
β π΄) & β’ (π β βπ₯ β β€ βπ¦ β π΄ π¦ β€ π₯)
& β’ (π β βπ₯ π₯ β π΄) β β’ (π β sup(π΄, β, < ) β π΄) |
|
Theorem | dvdsbnd 11956* |
There is an upper bound to the divisors of a nonzero integer.
(Contributed by Jim Kingdon, 11-Dec-2021.)
|
β’ ((π΄ β β€ β§ π΄ β 0) β βπ β β βπ β (β€β₯βπ) Β¬ π β₯ π΄) |
|
Theorem | gcdsupex 11957* |
Existence of the supremum used in defining gcd.
(Contributed by
Jim Kingdon, 12-Dec-2021.)
|
β’ (((π β β€ β§ π β β€) β§ Β¬ (π = 0 β§ π = 0)) β βπ₯ β β€ (βπ¦ β {π β β€ β£ (π β₯ π β§ π β₯ π)} Β¬ π₯ < π¦ β§ βπ¦ β β (π¦ < π₯ β βπ§ β {π β β€ β£ (π β₯ π β§ π β₯ π)}π¦ < π§))) |
|
Theorem | gcdsupcl 11958* |
Closure of the supremum used in defining gcd. A lemma
for gcdval 11959
and gcdn0cl 11962. (Contributed by Jim Kingdon, 11-Dec-2021.)
|
β’ (((π β β€ β§ π β β€) β§ Β¬ (π = 0 β§ π = 0)) β sup({π β β€ β£ (π β₯ π β§ π β₯ π)}, β, < ) β
β) |
|
Theorem | gcdval 11959* |
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 11960 |
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 11961* |
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 11962 |
Closure of the gcd operator. (Contributed by Paul
Chapman,
21-Mar-2011.)
|
β’ (((π β β€ β§ π β β€) β§ Β¬ (π = 0 β§ π = 0)) β (π gcd π) β β) |
|
Theorem | gcddvds 11963 |
The gcd of two integers divides each of them. (Contributed by Paul
Chapman, 21-Mar-2011.)
|
β’ ((π β β€ β§ π β β€) β ((π gcd π) β₯ π β§ (π gcd π) β₯ π)) |
|
Theorem | dvdslegcd 11964 |
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 11965 |
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 11966 |
Closure of the gcd operator. (Contributed by Paul
Chapman,
21-Mar-2011.)
|
β’ ((π β β€ β§ π β β€) β (π gcd π) β
β0) |
|
Theorem | gcdnncl 11967 |
Closure of the gcd operator. (Contributed by Thierry
Arnoux,
2-Feb-2020.)
|
β’ ((π β β β§ π β β) β (π gcd π) β β) |
|
Theorem | gcdcld 11968 |
Closure of the gcd operator. (Contributed by Mario
Carneiro,
29-May-2016.)
|
β’ (π β π β β€) & β’ (π β π β β€)
β β’ (π β (π gcd π) β
β0) |
|
Theorem | gcd2n0cl 11969 |
Closure of the gcd operator if the second operand is
not 0.
(Contributed by AV, 10-Jul-2021.)
|
β’ ((π β β€ β§ π β β€ β§ π β 0) β (π gcd π) β β) |
|
Theorem | zeqzmulgcd 11970* |
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 11971 |
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 11972 |
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 11973 |
The gcd operator is commutative. Theorem 1.4(a) in [ApostolNT]
p. 16. (Contributed by Paul Chapman, 21-Mar-2011.)
|
β’ ((π β β€ β§ π β β€) β (π gcd π) = (π gcd π)) |
|
Theorem | gcdcomd 11974 |
The gcd operator is commutative, deduction version.
(Contributed by
SN, 24-Aug-2024.)
|
β’ (π β π β β€) & β’ (π β π β β€)
β β’ (π β (π gcd π) = (π gcd π)) |
|
Theorem | divgcdnn 11975 |
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 11976 |
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 11977 |
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 11978 |
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 11979 |
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 11980 |
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 11981 |
The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul
Chapman, 31-Mar-2011.)
|
β’ (π β β0 β (π gcd 0) = π) |
|
Theorem | gcdneg 11982 |
Negating one operand of the gcd operator does not alter
the result.
(Contributed by Paul Chapman, 21-Mar-2011.)
|
β’ ((π β β€ β§ π β β€) β (π gcd -π) = (π gcd π)) |
|
Theorem | neggcd 11983 |
Negating one operand of the gcd operator does not alter
the result.
(Contributed by Paul Chapman, 22-Jun-2011.)
|
β’ ((π β β€ β§ π β β€) β (-π gcd π) = (π gcd π)) |
|
Theorem | gcdaddm 11984 |
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 11985 |
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 (π + π))) |
|
Theorem | gcdid 11986 |
The gcd of a number and itself is its absolute value. (Contributed by
Paul Chapman, 31-Mar-2011.)
|
β’ (π β β€ β (π gcd π) = (absβπ)) |
|
Theorem | gcd1 11987 |
The gcd of a number with 1 is 1. Theorem 1.4(d)1 in [ApostolNT] p. 16.
(Contributed by Mario Carneiro, 19-Feb-2014.)
|
β’ (π β β€ β (π gcd 1) = 1) |
|
Theorem | gcdabs 11988 |
The gcd of two integers is the same as that of their absolute values.
(Contributed by Paul Chapman, 31-Mar-2011.)
|
β’ ((π β β€ β§ π β β€) β ((absβπ) gcd (absβπ)) = (π gcd π)) |
|
Theorem | gcdabs1 11989 |
gcd of the absolute value of the first operator.
(Contributed by
Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
β’ ((π β β€ β§ π β β€) β ((absβπ) gcd π) = (π gcd π)) |
|
Theorem | gcdabs2 11990 |
gcd of the absolute value of the second operator.
(Contributed by
Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
β’ ((π β β€ β§ π β β€) β (π gcd (absβπ)) = (π gcd π)) |
|
Theorem | modgcd 11991 |
The gcd remains unchanged if one operand is replaced with its remainder
modulo the other. (Contributed by Paul Chapman, 31-Mar-2011.)
|
β’ ((π β β€ β§ π β β) β ((π mod π) gcd π) = (π gcd π)) |
|
Theorem | 1gcd 11992 |
The GCD of one and an integer is one. (Contributed by Scott Fenton,
17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
β’ (π β β€ β (1 gcd π) = 1) |
|
Theorem | gcdmultipled 11993 |
The greatest common divisor of a nonnegative integer π and a
multiple of it is π itself. (Contributed by Rohan
Ridenour,
3-Aug-2023.)
|
β’ (π β π β β0) & β’ (π β π β β€)
β β’ (π β (π gcd (π Β· π)) = π) |
|
Theorem | dvdsgcdidd 11994 |
The greatest common divisor of a positive integer and another integer it
divides is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|
β’ (π β π β β) & β’ (π β π β β€) & β’ (π β π β₯ π) β β’ (π β (π gcd π) = π) |
|
Theorem | 6gcd4e2 11995 |
The greatest common divisor of six and four is two. To calculate this
gcd, a simple form of Euclid's algorithm is used:
(6 gcd 4) = ((4 + 2) gcd 4) = (2 gcd 4) and
(2 gcd 4) = (2 gcd (2 + 2)) = (2 gcd 2) = 2.
(Contributed by
AV, 27-Aug-2020.)
|
β’ (6 gcd 4) = 2 |
|
5.1.5 BΓ©zout's identity
|
|
Theorem | bezoutlemnewy 11996* |
Lemma for BΓ©zout's identity. The is-bezout predicate holds for
(π¦ mod π). (Contributed by Jim Kingdon,
6-Jan-2022.)
|
β’ (π β βπ β β€ βπ‘ β β€ π = ((π΄ Β· π ) + (π΅ Β· π‘))) & β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ (π β π β β) & β’ (π β [π¦ / π]π)
& β’ (π β π¦ β β0) & β’ (π β [π / π]π) β β’ (π β [(π¦ mod π) / π]π) |
|
Theorem | bezoutlemstep 11997* |
Lemma for BΓ©zout's identity. This is the induction step for
the proof by induction. (Contributed by Jim Kingdon, 3-Jan-2022.)
|
β’ (π β βπ β β€ βπ‘ β β€ π = ((π΄ Β· π ) + (π΅ Β· π‘))) & β’ (π β π΄ β β0) & β’ (π β π΅ β β0) & β’ (π β π β β) & β’ (π β [π¦ / π]π)
& β’ (π β π¦ β β0) & β’ (π β [π / π]π)
& β’ (π β βπ§ β β0 (π§ β₯ π β (π§ β₯ π₯ β§ π§ β₯ π¦))) & β’ ((π β§ [(π¦ mod π) / π]π) β βπ β β0 ([(π¦ mod π) / π₯][π / π¦]π β§ π)) & β’ β²π₯π
& β’ β²ππ β β’ (π β βπ β β0 ([π / π₯]π β§ π)) |
|
Theorem | bezoutlemmain 11998* |
Lemma for BΓ©zout's identity. This is the main result which we
prove by induction and which represents the application of the Extended
Euclidean algorithm. (Contributed by Jim Kingdon, 30-Dec-2021.)
|
β’ (π β βπ β β€ βπ‘ β β€ π = ((π΄ Β· π ) + (π΅ Β· π‘))) & β’ (π β βπ§ β β0
(π§ β₯ π β (π§ β₯ π₯ β§ π§ β₯ π¦))) & β’ (π β π΄ β β0) & β’ (π β π΅ β
β0) β β’ (π β βπ₯ β β0 ([π₯ / π]π β βπ¦ β β0 ([π¦ / π]π β βπ β β0 (π β§ π)))) |
|
Theorem | bezoutlema 11999* |
Lemma for BΓ©zout's identity. The is-bezout condition is
satisfied by π΄. (Contributed by Jim Kingdon,
30-Dec-2021.)
|
β’ (π β βπ β β€ βπ‘ β β€ π = ((π΄ Β· π ) + (π΅ Β· π‘))) & β’ (π β π΄ β β0) & β’ (π β π΅ β
β0) β β’ (π β [π΄ / π]π) |
|
Theorem | bezoutlemb 12000* |
Lemma for BΓ©zout's identity. The is-bezout condition is
satisfied by π΅. (Contributed by Jim Kingdon,
30-Dec-2021.)
|
β’ (π β βπ β β€ βπ‘ β β€ π = ((π΄ Β· π ) + (π΅ Β· π‘))) & β’ (π β π΄ β β0) & β’ (π β π΅ β
β0) β β’ (π β [π΅ / π]π) |