Type | Label | Description |
Statement |
|
Theorem | qnumcl 12201 |
The canonical numerator of a rational is an integer. (Contributed by
Stefan O'Rear, 13-Sep-2014.)
|
β’ (π΄ β β β (numerβπ΄) β
β€) |
|
Theorem | qdencl 12202 |
The canonical denominator is a positive integer. (Contributed by Stefan
O'Rear, 13-Sep-2014.)
|
β’ (π΄ β β β (denomβπ΄) β
β) |
|
Theorem | fnum 12203 |
Canonical numerator defines a function. (Contributed by Stefan O'Rear,
13-Sep-2014.)
|
β’
numer:ββΆβ€ |
|
Theorem | fden 12204 |
Canonical denominator defines a function. (Contributed by Stefan
O'Rear, 13-Sep-2014.)
|
β’
denom:ββΆβ |
|
Theorem | qnumdenbi 12205 |
Two numbers are the canonical representation of a rational iff they are
coprime and have the right quotient. (Contributed by Stefan O'Rear,
13-Sep-2014.)
|
β’ ((π΄ β β β§ π΅ β β€ β§ πΆ β β) β (((π΅ gcd πΆ) = 1 β§ π΄ = (π΅ / πΆ)) β ((numerβπ΄) = π΅ β§ (denomβπ΄) = πΆ))) |
|
Theorem | qnumdencoprm 12206 |
The canonical representation of a rational is fully reduced.
(Contributed by Stefan O'Rear, 13-Sep-2014.)
|
β’ (π΄ β β β ((numerβπ΄) gcd (denomβπ΄)) = 1) |
|
Theorem | qeqnumdivden 12207 |
Recover a rational number from its canonical representation.
(Contributed by Stefan O'Rear, 13-Sep-2014.)
|
β’ (π΄ β β β π΄ = ((numerβπ΄) / (denomβπ΄))) |
|
Theorem | qmuldeneqnum 12208 |
Multiplying a rational by its denominator results in an integer.
(Contributed by Stefan O'Rear, 13-Sep-2014.)
|
β’ (π΄ β β β (π΄ Β· (denomβπ΄)) = (numerβπ΄)) |
|
Theorem | divnumden 12209 |
Calculate the reduced form of a quotient using gcd.
(Contributed
by Stefan O'Rear, 13-Sep-2014.)
|
β’ ((π΄ β β€ β§ π΅ β β) β
((numerβ(π΄ / π΅)) = (π΄ / (π΄ gcd π΅)) β§ (denomβ(π΄ / π΅)) = (π΅ / (π΄ gcd π΅)))) |
|
Theorem | divdenle 12210 |
Reducing a quotient never increases the denominator. (Contributed by
Stefan O'Rear, 13-Sep-2014.)
|
β’ ((π΄ β β€ β§ π΅ β β) β (denomβ(π΄ / π΅)) β€ π΅) |
|
Theorem | qnumgt0 12211 |
A rational is positive iff its canonical numerator is. (Contributed by
Stefan O'Rear, 15-Sep-2014.)
|
β’ (π΄ β β β (0 < π΄ β 0 <
(numerβπ΄))) |
|
Theorem | qgt0numnn 12212 |
A rational is positive iff its canonical numerator is a positive
integer. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|
β’ ((π΄ β β β§ 0 < π΄) β (numerβπ΄) β
β) |
|
Theorem | nn0gcdsq 12213 |
Squaring commutes with GCD, in particular two coprime numbers have
coprime squares. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|
β’ ((π΄ β β0 β§ π΅ β β0)
β ((π΄ gcd π΅)β2) = ((π΄β2) gcd (π΅β2))) |
|
Theorem | zgcdsq 12214 |
nn0gcdsq 12213 extended to integers by symmetry.
(Contributed by Stefan
O'Rear, 15-Sep-2014.)
|
β’ ((π΄ β β€ β§ π΅ β β€) β ((π΄ gcd π΅)β2) = ((π΄β2) gcd (π΅β2))) |
|
Theorem | numdensq 12215 |
Squaring a rational squares its canonical components. (Contributed by
Stefan O'Rear, 15-Sep-2014.)
|
β’ (π΄ β β β ((numerβ(π΄β2)) = ((numerβπ΄)β2) β§
(denomβ(π΄β2)) =
((denomβπ΄)β2))) |
|
Theorem | numsq 12216 |
Square commutes with canonical numerator. (Contributed by Stefan
O'Rear, 15-Sep-2014.)
|
β’ (π΄ β β β (numerβ(π΄β2)) = ((numerβπ΄)β2)) |
|
Theorem | densq 12217 |
Square commutes with canonical denominator. (Contributed by Stefan
O'Rear, 15-Sep-2014.)
|
β’ (π΄ β β β (denomβ(π΄β2)) = ((denomβπ΄)β2)) |
|
Theorem | qden1elz 12218 |
A rational is an integer iff it has denominator 1. (Contributed by
Stefan O'Rear, 15-Sep-2014.)
|
β’ (π΄ β β β ((denomβπ΄) = 1 β π΄ β β€)) |
|
Theorem | nn0sqrtelqelz 12219 |
If a nonnegative integer has a rational square root, that root must be
an integer. (Contributed by Jim Kingdon, 24-May-2022.)
|
β’ ((π΄ β β0 β§
(ββπ΄) β
β) β (ββπ΄) β β€) |
|
Theorem | nonsq 12220 |
Any integer strictly between two adjacent squares has a non-rational
square root. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|
β’ (((π΄ β β0 β§ π΅ β β0)
β§ ((π΅β2) <
π΄ β§ π΄ < ((π΅ + 1)β2))) β Β¬
(ββπ΄) β
β) |
|
5.2.5 Euler's theorem
|
|
Syntax | codz 12221 |
Extend class notation with the order function on the class of integers
modulo N.
|
class odβ€ |
|
Syntax | cphi 12222 |
Extend class notation with the Euler phi function.
|
class Ο |
|
Definition | df-odz 12223* |
Define the order function on the class of integers modulo N.
(Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by AV,
26-Sep-2020.)
|
β’ odβ€ = (π β β β¦ (π₯ β {π₯ β β€ β£ (π₯ gcd π) = 1} β¦ inf({π β β β£ π β₯ ((π₯βπ) β 1)}, β, <
))) |
|
Definition | df-phi 12224* |
Define the Euler phi function (also called "Euler totient function"),
which counts the number of integers less than π and coprime to it,
see definition in [ApostolNT] p. 25.
(Contributed by Mario Carneiro,
23-Feb-2014.)
|
β’ Ο = (π β β β¦
(β―β{π₯ β
(1...π) β£ (π₯ gcd π) = 1})) |
|
Theorem | phivalfi 12225* |
Finiteness of an expression used to define the Euler Ο function.
(Contributed by Jim Kingon, 28-May-2022.)
|
β’ (π β β β {π₯ β (1...π) β£ (π₯ gcd π) = 1} β Fin) |
|
Theorem | phival 12226* |
Value of the Euler Ο function. (Contributed by
Mario Carneiro,
23-Feb-2014.)
|
β’ (π β β β (Οβπ) = (β―β{π₯ β (1...π) β£ (π₯ gcd π) = 1})) |
|
Theorem | phicl2 12227 |
Bounds and closure for the value of the Euler Ο
function.
(Contributed by Mario Carneiro, 23-Feb-2014.)
|
β’ (π β β β (Οβπ) β (1...π)) |
|
Theorem | phicl 12228 |
Closure for the value of the Euler Ο function.
(Contributed by
Mario Carneiro, 28-Feb-2014.)
|
β’ (π β β β (Οβπ) β
β) |
|
Theorem | phibndlem 12229* |
Lemma for phibnd 12230. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
β’ (π β (β€β₯β2)
β {π₯ β
(1...π) β£ (π₯ gcd π) = 1} β (1...(π β 1))) |
|
Theorem | phibnd 12230 |
A slightly tighter bound on the value of the Euler Ο function.
(Contributed by Mario Carneiro, 23-Feb-2014.)
|
β’ (π β (β€β₯β2)
β (Οβπ)
β€ (π β
1)) |
|
Theorem | phicld 12231 |
Closure for the value of the Euler Ο function.
(Contributed by
Mario Carneiro, 29-May-2016.)
|
β’ (π β π β β)
β β’ (π β (Οβπ) β β) |
|
Theorem | phi1 12232 |
Value of the Euler Ο function at 1. (Contributed
by Mario Carneiro,
23-Feb-2014.)
|
β’ (Οβ1) = 1 |
|
Theorem | dfphi2 12233* |
Alternate definition of the Euler Ο function.
(Contributed by
Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro,
2-May-2016.)
|
β’ (π β β β (Οβπ) = (β―β{π₯ β (0..^π) β£ (π₯ gcd π) = 1})) |
|
Theorem | hashdvds 12234* |
The number of numbers in a given residue class in a finite set of
integers. (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof
shortened by Mario Carneiro, 7-Jun-2016.)
|
β’ (π β π β β) & β’ (π β π΄ β β€) & β’ (π β π΅ β
(β€β₯β(π΄ β 1))) & β’ (π β πΆ β β€)
β β’ (π β (β―β{π₯ β (π΄...π΅) β£ π β₯ (π₯ β πΆ)}) = ((ββ((π΅ β πΆ) / π)) β (ββ(((π΄ β 1) β πΆ) / π)))) |
|
Theorem | phiprmpw 12235 |
Value of the Euler Ο function at a prime power.
Theorem 2.5(a) in
[ApostolNT] p. 28. (Contributed by
Mario Carneiro, 24-Feb-2014.)
|
β’ ((π β β β§ πΎ β β) β
(Οβ(πβπΎ)) = ((πβ(πΎ β 1)) Β· (π β 1))) |
|
Theorem | phiprm 12236 |
Value of the Euler Ο function at a prime.
(Contributed by Mario
Carneiro, 28-Feb-2014.)
|
β’ (π β β β (Οβπ) = (π β 1)) |
|
Theorem | crth 12237* |
The Chinese Remainder Theorem: the function that maps π₯ to its
remainder classes mod π and mod π is 1-1 and onto when
π
and
π are coprime. (Contributed by Mario
Carneiro, 24-Feb-2014.)
(Proof shortened by Mario Carneiro, 2-May-2016.)
|
β’ π = (0..^(π Β· π)) & β’ π = ((0..^π) Γ (0..^π)) & β’ πΉ = (π₯ β π β¦ β¨(π₯ mod π), (π₯ mod π)β©) & β’ (π β (π β β β§ π β β β§ (π gcd π) = 1)) β β’ (π β πΉ:πβ1-1-ontoβπ) |
|
Theorem | phimullem 12238* |
Lemma for phimul 12239. (Contributed by Mario Carneiro,
24-Feb-2014.)
|
β’ π = (0..^(π Β· π)) & β’ π = ((0..^π) Γ (0..^π)) & β’ πΉ = (π₯ β π β¦ β¨(π₯ mod π), (π₯ mod π)β©) & β’ (π β (π β β β§ π β β β§ (π gcd π) = 1)) & β’ π = {π¦ β (0..^π) β£ (π¦ gcd π) = 1} & β’ π = {π¦ β (0..^π) β£ (π¦ gcd π) = 1} & β’ π = {π¦ β π β£ (π¦ gcd (π Β· π)) = 1} β β’ (π β (Οβ(π Β· π)) = ((Οβπ) Β· (Οβπ))) |
|
Theorem | phimul 12239 |
The Euler Ο function is a multiplicative function,
meaning that it
distributes over multiplication at relatively prime arguments. Theorem
2.5(c) in [ApostolNT] p. 28.
(Contributed by Mario Carneiro,
24-Feb-2014.)
|
β’ ((π β β β§ π β β β§ (π gcd π) = 1) β (Οβ(π Β· π)) = ((Οβπ) Β· (Οβπ))) |
|
Theorem | eulerthlem1 12240* |
Lemma for eulerth 12246. (Contributed by Mario Carneiro,
8-May-2015.)
|
β’ (π β (π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1)) & β’ π = {π¦ β (0..^π) β£ (π¦ gcd π) = 1} & β’ π = (1...(Οβπ)) & β’ (π β πΉ:πβ1-1-ontoβπ)
& β’ πΊ = (π₯ β π β¦ ((π΄ Β· (πΉβπ₯)) mod π)) β β’ (π β πΊ:πβΆπ) |
|
Theorem | eulerthlemfi 12241* |
Lemma for eulerth 12246. The set π is finite. (Contributed by Mario
Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
|
β’ (π β (π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1)) & β’ π = {π¦ β (0..^π) β£ (π¦ gcd π) = 1} β β’ (π β π β Fin) |
|
Theorem | eulerthlemrprm 12242* |
Lemma for eulerth 12246. π and
βπ₯ β (1...(Οβπ))(πΉβπ₯) are relatively prime.
(Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim
Kingdon, 2-Sep-2024.)
|
β’ (π β (π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1)) & β’ π = {π¦ β (0..^π) β£ (π¦ gcd π) = 1} & β’ (π β πΉ:(1...(Οβπ))β1-1-ontoβπ) β β’ (π β (π gcd βπ₯ β (1...(Οβπ))(πΉβπ₯)) = 1) |
|
Theorem | eulerthlema 12243* |
Lemma for eulerth 12246. (Contributed by Mario Carneiro,
28-Feb-2014.)
(Revised by Jim Kingdon, 2-Sep-2024.)
|
β’ (π β (π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1)) & β’ π = {π¦ β (0..^π) β£ (π¦ gcd π) = 1} & β’ (π β πΉ:(1...(Οβπ))β1-1-ontoβπ) β β’ (π β (((π΄β(Οβπ)) Β· βπ₯ β (1...(Οβπ))(πΉβπ₯)) mod π) = (βπ₯ β (1...(Οβπ))((π΄ Β· (πΉβπ₯)) mod π) mod π)) |
|
Theorem | eulerthlemh 12244* |
Lemma for eulerth 12246. A permutation of (1...(Οβπ)).
(Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim
Kingdon, 5-Sep-2024.)
|
β’ (π β (π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1)) & β’ π = {π¦ β (0..^π) β£ (π¦ gcd π) = 1} & β’ (π β πΉ:(1...(Οβπ))β1-1-ontoβπ)
& β’ π» = (β‘πΉ β (π¦ β (1...(Οβπ)) β¦ ((π΄ Β· (πΉβπ¦)) mod π))) β β’ (π β π»:(1...(Οβπ))β1-1-ontoβ(1...(Οβπ))) |
|
Theorem | eulerthlemth 12245* |
Lemma for eulerth 12246. The result. (Contributed by Mario
Carneiro,
28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
|
β’ (π β (π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1)) & β’ π = {π¦ β (0..^π) β£ (π¦ gcd π) = 1} & β’ (π β πΉ:(1...(Οβπ))β1-1-ontoβπ) β β’ (π β ((π΄β(Οβπ)) mod π) = (1 mod π)) |
|
Theorem | eulerth 12246 |
Euler's theorem, a generalization of Fermat's little theorem. If π΄
and π are coprime, then π΄βΟ(π)β‘1 (mod π). This
is Metamath 100 proof #10. Also called Euler-Fermat theorem, see
theorem 5.17 in [ApostolNT] p. 113.
(Contributed by Mario Carneiro,
28-Feb-2014.)
|
β’ ((π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1) β ((π΄β(Οβπ)) mod π) = (1 mod π)) |
|
Theorem | fermltl 12247 |
Fermat's little theorem. When π is prime, π΄βπβ‘π΄ (mod π)
for any π΄, see theorem 5.19 in [ApostolNT] p. 114. (Contributed by
Mario Carneiro, 28-Feb-2014.) (Proof shortened by AV, 19-Mar-2022.)
|
β’ ((π β β β§ π΄ β β€) β ((π΄βπ) mod π) = (π΄ mod π)) |
|
Theorem | prmdiv 12248 |
Show an explicit expression for the modular inverse of π΄ mod π.
(Contributed by Mario Carneiro, 24-Jan-2015.)
|
β’ π
= ((π΄β(π β 2)) mod π) β β’ ((π β β β§ π΄ β β€ β§ Β¬ π β₯ π΄) β (π
β (1...(π β 1)) β§ π β₯ ((π΄ Β· π
) β 1))) |
|
Theorem | prmdiveq 12249 |
The modular inverse of π΄ mod π is unique. (Contributed by Mario
Carneiro, 24-Jan-2015.)
|
β’ π
= ((π΄β(π β 2)) mod π) β β’ ((π β β β§ π΄ β β€ β§ Β¬ π β₯ π΄) β ((π β (0...(π β 1)) β§ π β₯ ((π΄ Β· π) β 1)) β π = π
)) |
|
Theorem | prmdivdiv 12250 |
The (modular) inverse of the inverse of a number is itself.
(Contributed by Mario Carneiro, 24-Jan-2015.)
|
β’ π
= ((π΄β(π β 2)) mod π) β β’ ((π β β β§ π΄ β (1...(π β 1))) β π΄ = ((π
β(π β 2)) mod π)) |
|
Theorem | hashgcdlem 12251* |
A correspondence between elements of specific GCD and relative primes in
a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|
β’ π΄ = {π¦ β (0..^(π / π)) β£ (π¦ gcd (π / π)) = 1} & β’ π΅ = {π§ β (0..^π) β£ (π§ gcd π) = π}
& β’ πΉ = (π₯ β π΄ β¦ (π₯ Β· π)) β β’ ((π β β β§ π β β β§ π β₯ π) β πΉ:π΄β1-1-ontoβπ΅) |
|
Theorem | hashgcdeq 12252* |
Number of initial positive integers with specified divisors.
(Contributed by Stefan O'Rear, 12-Sep-2015.)
|
β’ ((π β β β§ π β β) β
(β―β{π₯ β
(0..^π) β£ (π₯ gcd π) = π}) = if(π β₯ π, (Οβ(π / π)), 0)) |
|
Theorem | phisum 12253* |
The divisor sum identity of the totient function. Theorem 2.2 in
[ApostolNT] p. 26. (Contributed by
Stefan O'Rear, 12-Sep-2015.)
|
β’ (π β β β Ξ£π β {π₯ β β β£ π₯ β₯ π} (Οβπ) = π) |
|
Theorem | odzval 12254* |
Value of the order function. This is a function of functions; the inner
argument selects the base (i.e., mod π for some π, often prime)
and the outer argument selects the integer or equivalence class (if you
want to think about it that way) from the integers mod π. In
order
to ensure the supremum is well-defined, we only define the expression
when π΄ and π are coprime.
(Contributed by Mario Carneiro,
23-Feb-2014.) (Revised by AV, 26-Sep-2020.)
|
β’ ((π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1) β
((odβ€βπ)βπ΄) = inf({π β β β£ π β₯ ((π΄βπ) β 1)}, β, <
)) |
|
Theorem | odzcllem 12255 |
- Lemma for odzcl 12256, showing existence of a recurrent point for
the
exponential. (Contributed by Mario Carneiro, 28-Feb-2014.) (Proof
shortened by AV, 26-Sep-2020.)
|
β’ ((π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1) β
(((odβ€βπ)βπ΄) β β β§ π β₯ ((π΄β((odβ€βπ)βπ΄)) β 1))) |
|
Theorem | odzcl 12256 |
The order of a group element is an integer. (Contributed by Mario
Carneiro, 28-Feb-2014.)
|
β’ ((π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1) β
((odβ€βπ)βπ΄) β β) |
|
Theorem | odzid 12257 |
Any element raised to the power of its order is 1.
(Contributed by
Mario Carneiro, 28-Feb-2014.)
|
β’ ((π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1) β π β₯ ((π΄β((odβ€βπ)βπ΄)) β 1)) |
|
Theorem | odzdvds 12258 |
The only powers of π΄ that are congruent to 1 are the multiples
of the order of π΄. (Contributed by Mario Carneiro,
28-Feb-2014.)
(Proof shortened by AV, 26-Sep-2020.)
|
β’ (((π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1) β§ πΎ β β0) β (π β₯ ((π΄βπΎ) β 1) β
((odβ€βπ)βπ΄) β₯ πΎ)) |
|
Theorem | odzphi 12259 |
The order of any group element is a divisor of the Euler Ο
function. (Contributed by Mario Carneiro, 28-Feb-2014.)
|
β’ ((π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1) β
((odβ€βπ)βπ΄) β₯ (Οβπ)) |
|
5.2.6 Arithmetic modulo a prime
number
|
|
Theorem | modprm1div 12260 |
A prime number divides an integer minus 1 iff the integer modulo the prime
number is 1. (Contributed by Alexander van der Vekens, 17-May-2018.)
(Proof shortened by AV, 30-May-2023.)
|
β’ ((π β β β§ π΄ β β€) β ((π΄ mod π) = 1 β π β₯ (π΄ β 1))) |
|
Theorem | m1dvdsndvds 12261 |
If an integer minus 1 is divisible by a prime number, the integer itself
is not divisible by this prime number. (Contributed by Alexander van der
Vekens, 30-Aug-2018.)
|
β’ ((π β β β§ π΄ β β€) β (π β₯ (π΄ β 1) β Β¬ π β₯ π΄)) |
|
Theorem | modprminv 12262 |
Show an explicit expression for the modular inverse of π΄ mod π.
This is an application of prmdiv 12248. (Contributed by Alexander van der
Vekens, 15-May-2018.)
|
β’ π
= ((π΄β(π β 2)) mod π) β β’ ((π β β β§ π΄ β β€ β§ Β¬ π β₯ π΄) β (π
β (1...(π β 1)) β§ ((π΄ Β· π
) mod π) = 1)) |
|
Theorem | modprminveq 12263 |
The modular inverse of π΄ mod π is unique. (Contributed by
Alexander
van der Vekens, 17-May-2018.)
|
β’ π
= ((π΄β(π β 2)) mod π) β β’ ((π β β β§ π΄ β β€ β§ Β¬ π β₯ π΄) β ((π β (0...(π β 1)) β§ ((π΄ Β· π) mod π) = 1) β π = π
)) |
|
Theorem | vfermltl 12264 |
Variant of Fermat's little theorem if π΄ is not a multiple of π,
see theorem 5.18 in [ApostolNT] p. 113.
(Contributed by AV, 21-Aug-2020.)
(Proof shortened by AV, 5-Sep-2020.)
|
β’ ((π β β β§ π΄ β β€ β§ Β¬ π β₯ π΄) β ((π΄β(π β 1)) mod π) = 1) |
|
Theorem | powm2modprm 12265 |
If an integer minus 1 is divisible by a prime number, then the integer to
the power of the prime number minus 2 is 1 modulo the prime number.
(Contributed by Alexander van der Vekens, 30-Aug-2018.)
|
β’ ((π β β β§ π΄ β β€) β (π β₯ (π΄ β 1) β ((π΄β(π β 2)) mod π) = 1)) |
|
Theorem | reumodprminv 12266* |
For any prime number and for any positive integer less than this prime
number, there is a unique modular inverse of this positive integer.
(Contributed by Alexander van der Vekens, 12-May-2018.)
|
β’ ((π β β β§ π β (1..^π)) β β!π β (1...(π β 1))((π Β· π) mod π) = 1) |
|
Theorem | modprm0 12267* |
For two positive integers less than a given prime number there is always
a nonnegative integer (less than the given prime number) so that the sum
of one of the two positive integers and the other of the positive
integers multiplied by the nonnegative integer is 0 ( modulo the given
prime number). (Contributed by Alexander van der Vekens,
17-May-2018.)
|
β’ ((π β β β§ π β (1..^π) β§ πΌ β (1..^π)) β βπ β (0..^π)((πΌ + (π Β· π)) mod π) = 0) |
|
Theorem | nnnn0modprm0 12268* |
For a positive integer and a nonnegative integer both less than a given
prime number there is always a second nonnegative integer (less than the
given prime number) so that the sum of this second nonnegative integer
multiplied with the positive integer and the first nonnegative integer
is 0 ( modulo the given prime number). (Contributed by Alexander van
der Vekens, 8-Nov-2018.)
|
β’ ((π β β β§ π β (1..^π) β§ πΌ β (0..^π)) β βπ β (0..^π)((πΌ + (π Β· π)) mod π) = 0) |
|
Theorem | modprmn0modprm0 12269* |
For an integer not being 0 modulo a given prime number and a nonnegative
integer less than the prime number, there is always a second nonnegative
integer (less than the given prime number) so that the sum of this
second nonnegative integer multiplied with the integer and the first
nonnegative integer is 0 ( modulo the given prime number). (Contributed
by Alexander van der Vekens, 10-Nov-2018.)
|
β’ ((π β β β§ π β β€ β§ (π mod π) β 0) β (πΌ β (0..^π) β βπ β (0..^π)((πΌ + (π Β· π)) mod π) = 0)) |
|
5.2.7 Pythagorean Triples
|
|
Theorem | coprimeprodsq 12270 |
If three numbers are coprime, and the square of one is the product of the
other two, then there is a formula for the other two in terms of gcd
and square. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario
Carneiro, 19-Apr-2014.)
|
β’ (((π΄ β β0 β§ π΅ β β€ β§ πΆ β β0)
β§ ((π΄ gcd π΅) gcd πΆ) = 1) β ((πΆβ2) = (π΄ Β· π΅) β π΄ = ((π΄ gcd πΆ)β2))) |
|
Theorem | coprimeprodsq2 12271 |
If three numbers are coprime, and the square of one is the product of the
other two, then there is a formula for the other two in terms of gcd
and square. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by
Mario Carneiro, 19-Apr-2014.)
|
β’ (((π΄ β β€ β§ π΅ β β0 β§ πΆ β β0)
β§ ((π΄ gcd π΅) gcd πΆ) = 1) β ((πΆβ2) = (π΄ Β· π΅) β π΅ = ((π΅ gcd πΆ)β2))) |
|
Theorem | oddprm 12272 |
A prime not equal to 2 is odd. (Contributed by Mario
Carneiro,
4-Feb-2015.) (Proof shortened by AV, 10-Jul-2022.)
|
β’ (π β (β β {2}) β
((π β 1) / 2) β
β) |
|
Theorem | nnoddn2prm 12273 |
A prime not equal to 2 is an odd positive integer.
(Contributed by
AV, 28-Jun-2021.)
|
β’ (π β (β β {2}) β (π β β β§ Β¬ 2
β₯ π)) |
|
Theorem | oddn2prm 12274 |
A prime not equal to 2 is odd. (Contributed by AV,
28-Jun-2021.)
|
β’ (π β (β β {2}) β Β¬
2 β₯ π) |
|
Theorem | nnoddn2prmb 12275 |
A number is a prime number not equal to 2 iff it is an
odd prime
number. Conversion theorem for two representations of odd primes.
(Contributed by AV, 14-Jul-2021.)
|
β’ (π β (β β {2}) β (π β β β§ Β¬ 2
β₯ π)) |
|
Theorem | prm23lt5 12276 |
A prime less than 5 is either 2 or 3. (Contributed by AV, 5-Jul-2021.)
|
β’ ((π β β β§ π < 5) β (π = 2 β¨ π = 3)) |
|
Theorem | prm23ge5 12277 |
A prime is either 2 or 3 or greater than or equal to 5. (Contributed by
AV, 5-Jul-2021.)
|
β’ (π β β β (π = 2 β¨ π = 3 β¨ π β
(β€β₯β5))) |
|
Theorem | pythagtriplem1 12278* |
Lemma for pythagtrip 12296. Prove a weaker version of one direction of
the
theorem. (Contributed by Scott Fenton, 28-Mar-2014.) (Revised by Mario
Carneiro, 19-Apr-2014.)
|
β’ (βπ β β βπ β β βπ β β (π΄ = (π Β· ((πβ2) β (πβ2))) β§ π΅ = (π Β· (2 Β· (π Β· π))) β§ πΆ = (π Β· ((πβ2) + (πβ2)))) β ((π΄β2) + (π΅β2)) = (πΆβ2)) |
|
Theorem | pythagtriplem2 12279* |
Lemma for pythagtrip 12296. Prove the full version of one direction of
the
theorem. (Contributed by Scott Fenton, 28-Mar-2014.) (Revised by Mario
Carneiro, 19-Apr-2014.)
|
β’ ((π΄ β β β§ π΅ β β) β (βπ β β βπ β β βπ β β ({π΄, π΅} = {(π Β· ((πβ2) β (πβ2))), (π Β· (2 Β· (π Β· π)))} β§ πΆ = (π Β· ((πβ2) + (πβ2)))) β ((π΄β2) + (π΅β2)) = (πΆβ2))) |
|
Theorem | pythagtriplem3 12280 |
Lemma for pythagtrip 12296. Show that πΆ and π΅ are
relatively prime
under some conditions. (Contributed by Scott Fenton, 8-Apr-2014.)
(Revised by Mario Carneiro, 19-Apr-2014.)
|
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β (π΅ gcd πΆ) = 1) |
|
Theorem | pythagtriplem4 12281 |
Lemma for pythagtrip 12296. Show that πΆ β π΅ and πΆ + π΅ are relatively
prime. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario
Carneiro, 19-Apr-2014.)
|
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β ((πΆ β π΅) gcd (πΆ + π΅)) = 1) |
|
Theorem | pythagtriplem10 12282 |
Lemma for pythagtrip 12296. Show that πΆ β π΅ is positive. (Contributed
by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2)) β 0 < (πΆ β π΅)) |
|
Theorem | pythagtriplem6 12283 |
Lemma for pythagtrip 12296. Calculate (ββ(πΆ β π΅)).
(Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β (ββ(πΆ β π΅)) = ((πΆ β π΅) gcd π΄)) |
|
Theorem | pythagtriplem7 12284 |
Lemma for pythagtrip 12296. Calculate (ββ(πΆ + π΅)).
(Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β (ββ(πΆ + π΅)) = ((πΆ + π΅) gcd π΄)) |
|
Theorem | pythagtriplem8 12285 |
Lemma for pythagtrip 12296. Show that (ββ(πΆ β π΅)) is a
positive integer. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised
by Mario Carneiro, 19-Apr-2014.)
|
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β (ββ(πΆ β π΅)) β β) |
|
Theorem | pythagtriplem9 12286 |
Lemma for pythagtrip 12296. Show that (ββ(πΆ + π΅)) is a
positive integer. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised
by Mario Carneiro, 19-Apr-2014.)
|
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β (ββ(πΆ + π΅)) β β) |
|
Theorem | pythagtriplem11 12287 |
Lemma for pythagtrip 12296. Show that π (which will eventually
be
closely related to the π in the final statement) is a natural.
(Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
β’ π = (((ββ(πΆ + π΅)) + (ββ(πΆ β π΅))) / 2) β β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β π β β) |
|
Theorem | pythagtriplem12 12288 |
Lemma for pythagtrip 12296. Calculate the square of π.
(Contributed
by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
β’ π = (((ββ(πΆ + π΅)) + (ββ(πΆ β π΅))) / 2) β β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β (πβ2) = ((πΆ + π΄) / 2)) |
|
Theorem | pythagtriplem13 12289 |
Lemma for pythagtrip 12296. Show that π (which will eventually
be
closely related to the π in the final statement) is a natural.
(Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
β’ π = (((ββ(πΆ + π΅)) β (ββ(πΆ β π΅))) / 2) β β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β π β β) |
|
Theorem | pythagtriplem14 12290 |
Lemma for pythagtrip 12296. Calculate the square of π.
(Contributed
by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
β’ π = (((ββ(πΆ + π΅)) β (ββ(πΆ β π΅))) / 2) β β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β (πβ2) = ((πΆ β π΄) / 2)) |
|
Theorem | pythagtriplem15 12291 |
Lemma for pythagtrip 12296. Show the relationship between π, π,
and π΄. (Contributed by Scott Fenton,
17-Apr-2014.) (Revised by
Mario Carneiro, 19-Apr-2014.)
|
β’ π = (((ββ(πΆ + π΅)) + (ββ(πΆ β π΅))) / 2) & β’ π = (((ββ(πΆ + π΅)) β (ββ(πΆ β π΅))) / 2) β β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β π΄ = ((πβ2) β (πβ2))) |
|
Theorem | pythagtriplem16 12292 |
Lemma for pythagtrip 12296. Show the relationship between π, π,
and π΅. (Contributed by Scott Fenton,
17-Apr-2014.) (Revised by
Mario Carneiro, 19-Apr-2014.)
|
β’ π = (((ββ(πΆ + π΅)) + (ββ(πΆ β π΅))) / 2) & β’ π = (((ββ(πΆ + π΅)) β (ββ(πΆ β π΅))) / 2) β β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β π΅ = (2 Β· (π Β· π))) |
|
Theorem | pythagtriplem17 12293 |
Lemma for pythagtrip 12296. Show the relationship between π, π,
and πΆ. (Contributed by Scott Fenton,
17-Apr-2014.) (Revised by
Mario Carneiro, 19-Apr-2014.)
|
β’ π = (((ββ(πΆ + π΅)) + (ββ(πΆ β π΅))) / 2) & β’ π = (((ββ(πΆ + π΅)) β (ββ(πΆ β π΅))) / 2) β β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β πΆ = ((πβ2) + (πβ2))) |
|
Theorem | pythagtriplem18 12294* |
Lemma for pythagtrip 12296. Wrap the previous π and π up in
quantifiers. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by
Mario Carneiro, 19-Apr-2014.)
|
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β βπ β β βπ β β (π΄ = ((πβ2) β (πβ2)) β§ π΅ = (2 Β· (π Β· π)) β§ πΆ = ((πβ2) + (πβ2)))) |
|
Theorem | pythagtriplem19 12295* |
Lemma for pythagtrip 12296. Introduce π and remove the relative
primality requirement. (Contributed by Scott Fenton, 18-Apr-2014.)
(Revised by Mario Carneiro, 19-Apr-2014.)
|
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ Β¬ 2 β₯ (π΄ / (π΄ gcd π΅))) β βπ β β βπ β β βπ β β (π΄ = (π Β· ((πβ2) β (πβ2))) β§ π΅ = (π Β· (2 Β· (π Β· π))) β§ πΆ = (π Β· ((πβ2) + (πβ2))))) |
|
Theorem | pythagtrip 12296* |
Parameterize the Pythagorean triples. If π΄, π΅, and πΆ are
naturals, then they obey the Pythagorean triple formula iff they are
parameterized by three naturals. This proof follows the Isabelle proof
at http://afp.sourceforge.net/entries/Fermat3_4.shtml.
This is
Metamath 100 proof #23. (Contributed by Scott Fenton, 19-Apr-2014.)
|
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (((π΄β2) + (π΅β2)) = (πΆβ2) β βπ β β βπ β β βπ β β ({π΄, π΅} = {(π Β· ((πβ2) β (πβ2))), (π Β· (2 Β· (π Β· π)))} β§ πΆ = (π Β· ((πβ2) + (πβ2)))))) |
|
5.2.8 The prime count function
|
|
Syntax | cpc 12297 |
Extend class notation with the prime count function.
|
class pCnt |
|
Definition | df-pc 12298* |
Define the prime count function, which returns the largest exponent of a
given prime (or other positive integer) that divides the number. For
rational numbers, it returns negative values according to the power of a
prime in the denominator. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
β’ pCnt = (π β β, π β β β¦ if(π = 0, +β, (β©π§βπ₯ β β€ βπ¦ β β (π = (π₯ / π¦) β§ π§ = (sup({π β β0 β£ (πβπ) β₯ π₯}, β, < ) β sup({π β β0
β£ (πβπ) β₯ π¦}, β, < )))))) |
|
Theorem | pclem0 12299* |
Lemma for the prime power pre-function's properties. (Contributed by
Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon,
7-Oct-2024.)
|
β’ π΄ = {π β β0 β£ (πβπ) β₯ π} β β’ ((π β (β€β₯β2)
β§ (π β β€
β§ π β 0)) β 0
β π΄) |
|
Theorem | pclemub 12300* |
Lemma for the prime power pre-function's properties. (Contributed by
Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon,
7-Oct-2024.)
|
β’ π΄ = {π β β0 β£ (πβπ) β₯ π} β β’ ((π β (β€β₯β2)
β§ (π β β€
β§ π β 0)) β
βπ₯ β β€
βπ¦ β π΄ π¦ β€ π₯) |