Home | Metamath
Proof Explorer Theorem List (p. 166 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dvdsnprmd 16501 | If a number is divisible by an integer greater than 1 and less than the number, the number is not prime. (Contributed by AV, 24-Jul-2021.) |
β’ (π β 1 < π΄) & β’ (π β π΄ < π) & β’ (π β π΄ β₯ π) β β’ (π β Β¬ π β β) | ||
Theorem | prm2orodd 16502 | A prime number is either 2 or odd. (Contributed by AV, 19-Jun-2021.) |
β’ (π β β β (π = 2 β¨ Β¬ 2 β₯ π)) | ||
Theorem | 2prm 16503 | 2 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Fan Zheng, 16-Jun-2016.) |
β’ 2 β β | ||
Theorem | 2mulprm 16504 | A multiple of two is prime iff the multiplier is one. (Contributed by AV, 8-Jun-2023.) |
β’ (π΄ β β€ β ((2 Β· π΄) β β β π΄ = 1)) | ||
Theorem | 3prm 16505 | 3 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ 3 β β | ||
Theorem | 4nprm 16506 | 4 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 18-Feb-2014.) |
β’ Β¬ 4 β β | ||
Theorem | prmuz2 16507 | A prime number is an integer greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.) |
β’ (π β β β π β (β€β₯β2)) | ||
Theorem | prmgt1 16508 | A prime number is an integer greater than 1. (Contributed by Alexander van der Vekens, 17-May-2018.) |
β’ (π β β β 1 < π) | ||
Theorem | prmm2nn0 16509 | Subtracting 2 from a prime number results in a nonnegative integer. (Contributed by Alexander van der Vekens, 30-Aug-2018.) |
β’ (π β β β (π β 2) β β0) | ||
Theorem | oddprmgt2 16510 | An odd prime is greater than 2. (Contributed by AV, 20-Aug-2021.) |
β’ (π β (β β {2}) β 2 < π) | ||
Theorem | oddprmge3 16511 | An odd prime is greater than or equal to 3. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 20-Aug-2021.) |
β’ (π β (β β {2}) β π β (β€β₯β3)) | ||
Theorem | ge2nprmge4 16512 | A composite integer greater than or equal to 2 is greater than or equal to 4. (Contributed by AV, 5-Jun-2023.) |
β’ ((π β (β€β₯β2) β§ π β β) β π β (β€β₯β4)) | ||
Theorem | sqnprm 16513 | A square is never prime. (Contributed by Mario Carneiro, 20-Jun-2015.) |
β’ (π΄ β β€ β Β¬ (π΄β2) β β) | ||
Theorem | dvdsprm 16514 | An integer greater than or equal to 2 divides a prime number iff it is equal to it. (Contributed by Paul Chapman, 26-Oct-2012.) |
β’ ((π β (β€β₯β2) β§ π β β) β (π β₯ π β π = π)) | ||
Theorem | exprmfct 16515* | Every integer greater than or equal to 2 has a prime factor. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 20-Jun-2015.) |
β’ (π β (β€β₯β2) β βπ β β π β₯ π) | ||
Theorem | prmdvdsfz 16516* | Each integer greater than 1 and less then or equal to a fixed number is divisible by a prime less then or equal to this fixed number. (Contributed by AV, 15-Aug-2020.) |
β’ ((π β β β§ πΌ β (2...π)) β βπ β β (π β€ π β§ π β₯ πΌ)) | ||
Theorem | nprmdvds1 16517 | No prime number divides 1. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 2-Jul-2015.) |
β’ (π β β β Β¬ π β₯ 1) | ||
Theorem | isprm5 16518* | One need only check prime divisors of π up to βπ in order to ensure primality. (Contributed by Mario Carneiro, 18-Feb-2014.) |
β’ (π β β β (π β (β€β₯β2) β§ βπ§ β β ((π§β2) β€ π β Β¬ π§ β₯ π))) | ||
Theorem | isprm7 16519* | One need only check prime divisors of π up to βπ in order to ensure primality. This version of isprm5 16518 combines the primality and bound on π§ into a finite interval of prime numbers. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
β’ (π β β β (π β (β€β₯β2) β§ βπ§ β ((2...(ββ(ββπ))) β© β) Β¬ π§ β₯ π)) | ||
Theorem | maxprmfct 16520* | The set of prime factors of an integer greater than or equal to 2 satisfies the conditions to have a supremum, and that supremum is a member of the set. (Contributed by Paul Chapman, 17-Nov-2012.) |
β’ π = {π§ β β β£ π§ β₯ π} β β’ (π β (β€β₯β2) β ((π β β€ β§ π β β β§ βπ₯ β β€ βπ¦ β π π¦ β€ π₯) β§ sup(π, β, < ) β π)) | ||
Theorem | divgcdodd 16521 | Either π΄ / (π΄ gcd π΅) is odd or π΅ / (π΄ gcd π΅) is odd. (Contributed by Scott Fenton, 19-Apr-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (Β¬ 2 β₯ (π΄ / (π΄ gcd π΅)) β¨ Β¬ 2 β₯ (π΅ / (π΄ gcd π΅)))) | ||
This section is about coprimality with respect to primes, and a special version of Euclid's lemma for primes is provided, see euclemma 16524. | ||
Theorem | coprm 16522 | A prime number either divides an integer or is coprime to it, but not both. Theorem 1.8 in [ApostolNT] p. 17. (Contributed by Paul Chapman, 22-Jun-2011.) |
β’ ((π β β β§ π β β€) β (Β¬ π β₯ π β (π gcd π) = 1)) | ||
Theorem | prmrp 16523 | Unequal prime numbers are relatively prime. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ ((π β β β§ π β β) β ((π gcd π) = 1 β π β π)) | ||
Theorem | euclemma 16524 | Euclid's lemma. A prime number divides the product of two integers iff it divides at least one of them. Theorem 1.9 in [ApostolNT] p. 17. (Contributed by Paul Chapman, 17-Nov-2012.) |
β’ ((π β β β§ π β β€ β§ π β β€) β (π β₯ (π Β· π) β (π β₯ π β¨ π β₯ π))) | ||
Theorem | isprm6 16525* | A number is prime iff it satisfies Euclid's lemma euclemma 16524. (Contributed by Mario Carneiro, 6-Sep-2015.) |
β’ (π β β β (π β (β€β₯β2) β§ βπ₯ β β€ βπ¦ β β€ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦)))) | ||
Theorem | prmdvdsexp 16526 | A prime divides a positive power of an integer iff it divides the integer. (Contributed by Mario Carneiro, 24-Feb-2014.) (Revised by Mario Carneiro, 17-Jul-2014.) |
β’ ((π β β β§ π΄ β β€ β§ π β β) β (π β₯ (π΄βπ) β π β₯ π΄)) | ||
Theorem | prmdvdsexpb 16527 | A prime divides a positive power of another iff they are equal. (Contributed by Paul Chapman, 30-Nov-2012.) (Revised by Mario Carneiro, 24-Feb-2014.) |
β’ ((π β β β§ π β β β§ π β β) β (π β₯ (πβπ) β π = π)) | ||
Theorem | prmdvdsexpr 16528 | If a prime divides a nonnegative power of another, then they are equal. (Contributed by Mario Carneiro, 16-Jan-2015.) |
β’ ((π β β β§ π β β β§ π β β0) β (π β₯ (πβπ) β π = π)) | ||
Theorem | prmdvdssq 16529 | Condition for a prime dividing a square. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by SN, 21-Aug-2024.) |
β’ ((π β β β§ π β β€) β (π β₯ π β π β₯ (πβ2))) | ||
Theorem | prmdvdssqOLD 16530 | Obsolete version of prmdvdssq 16529 as of 21-Aug-2024. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π β β β§ π β β€) β (π β₯ π β π β₯ (πβ2))) | ||
Theorem | prmexpb 16531 | Two positive prime powers are equal iff the primes and the powers are equal. (Contributed by Paul Chapman, 30-Nov-2012.) |
β’ (((π β β β§ π β β) β§ (π β β β§ π β β)) β ((πβπ) = (πβπ) β (π = π β§ π = π))) | ||
Theorem | prmfac1 16532 | The factorial of a number only contains primes less than the base. (Contributed by Mario Carneiro, 6-Mar-2014.) |
β’ ((π β β0 β§ π β β β§ π β₯ (!βπ)) β π β€ π) | ||
Theorem | rpexp 16533 | If two numbers π΄ and π΅ are relatively prime, then they are still relatively prime if raised to a power. (Contributed by Mario Carneiro, 24-Feb-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π β β) β (((π΄βπ) gcd π΅) = 1 β (π΄ gcd π΅) = 1)) | ||
Theorem | rpexp1i 16534 | Relative primality passes to asymmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π β β0) β ((π΄ gcd π΅) = 1 β ((π΄βπ) gcd π΅) = 1)) | ||
Theorem | rpexp12i 16535 | Relative primality passes to symmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ (π β β0 β§ π β β0)) β ((π΄ gcd π΅) = 1 β ((π΄βπ) gcd (π΅βπ)) = 1)) | ||
Theorem | prmndvdsfaclt 16536 | A prime number does not divide the factorial of a nonnegative integer less than the prime number. (Contributed by AV, 13-Jul-2021.) |
β’ ((π β β β§ π β β0) β (π < π β Β¬ π β₯ (!βπ))) | ||
Theorem | prmdvdsncoprmbd 16537* | Two positive integers are not coprime iff a prime divides both integers. Deduction version of ncoprmgcdne1b 16461 with the existential quantifier over the primes instead of integers greater than or equal to 2. (Contributed by SN, 24-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (βπ β β (π β₯ π΄ β§ π β₯ π΅) β (π΄ gcd π΅) β 1)) | ||
Theorem | ncoprmlnprm 16538 | If two positive integers are not coprime, the larger of them is not a prime number. (Contributed by AV, 9-Aug-2020.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ < π΅) β (1 < (π΄ gcd π΅) β π΅ β β)) | ||
Theorem | cncongrprm 16539 | Corollary 2 of Cancellability of Congruences: Two products with a common factor are congruent modulo a prime number not dividing the common factor iff the other factors are congruent modulo the prime number. (Contributed by AV, 13-Jul-2021.) |
β’ (((π΄ β β€ β§ π΅ β β€ β§ πΆ β β€) β§ (π β β β§ Β¬ π β₯ πΆ)) β (((π΄ Β· πΆ) mod π) = ((π΅ Β· πΆ) mod π) β (π΄ mod π) = (π΅ mod π))) | ||
Theorem | isevengcd2 16540 | The predicate "is an even number". An even number and 2 have 2 as greatest common divisor. (Contributed by AV, 1-Jul-2020.) (Revised by AV, 8-Aug-2021.) |
β’ (π β β€ β (2 β₯ π β (2 gcd π) = 2)) | ||
Theorem | isoddgcd1 16541 | The predicate "is an odd number". An odd number and 2 have 1 as greatest common divisor. (Contributed by AV, 1-Jul-2020.) (Revised by AV, 8-Aug-2021.) |
β’ (π β β€ β (Β¬ 2 β₯ π β (2 gcd π) = 1)) | ||
Theorem | 3lcm2e6 16542 | The least common multiple of three and two is six. The operands are unequal primes and thus coprime, so the result is (the absolute value of) their product. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 27-Aug-2020.) |
β’ (3 lcm 2) = 6 | ||
Syntax | cnumer 16543 | Extend class notation to include canonical numerator function. |
class numer | ||
Syntax | cdenom 16544 | Extend class notation to include canonical denominator function. |
class denom | ||
Definition | df-numer 16545* | The canonical numerator of a rational is the numerator of the rational's reduced fraction representation (no common factors, denominator positive). (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ numer = (π¦ β β β¦ (1st β(β©π₯ β (β€ Γ β)(((1st βπ₯) gcd (2nd βπ₯)) = 1 β§ π¦ = ((1st βπ₯) / (2nd βπ₯)))))) | ||
Definition | df-denom 16546* | The canonical denominator of a rational is the denominator of the rational's reduced fraction representation (no common factors, denominator positive). (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ denom = (π¦ β β β¦ (2nd β(β©π₯ β (β€ Γ β)(((1st βπ₯) gcd (2nd βπ₯)) = 1 β§ π¦ = ((1st βπ₯) / (2nd βπ₯)))))) | ||
Theorem | qnumval 16547* | Value of the canonical numerator function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β (numerβπ΄) = (1st β(β©π₯ β (β€ Γ β)(((1st βπ₯) gcd (2nd βπ₯)) = 1 β§ π΄ = ((1st βπ₯) / (2nd βπ₯)))))) | ||
Theorem | qdenval 16548* | Value of the canonical denominator function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β (denomβπ΄) = (2nd β(β©π₯ β (β€ Γ β)(((1st βπ₯) gcd (2nd βπ₯)) = 1 β§ π΄ = ((1st βπ₯) / (2nd βπ₯)))))) | ||
Theorem | qnumdencl 16549 | Lemma for qnumcl 16550 and qdencl 16551. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β ((numerβπ΄) β β€ β§ (denomβπ΄) β β)) | ||
Theorem | qnumcl 16550 | The canonical numerator of a rational is an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β (numerβπ΄) β β€) | ||
Theorem | qdencl 16551 | The canonical denominator is a positive integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β (denomβπ΄) β β) | ||
Theorem | fnum 16552 | Canonical numerator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ numer:ββΆβ€ | ||
Theorem | fden 16553 | Canonical denominator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ denom:ββΆβ | ||
Theorem | qnumdenbi 16554 | 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 16555 | The canonical representation of a rational is fully reduced. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β ((numerβπ΄) gcd (denomβπ΄)) = 1) | ||
Theorem | qeqnumdivden 16556 | Recover a rational number from its canonical representation. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β π΄ = ((numerβπ΄) / (denomβπ΄))) | ||
Theorem | qmuldeneqnum 16557 | Multiplying a rational by its denominator results in an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β (π΄ Β· (denomβπ΄)) = (numerβπ΄)) | ||
Theorem | divnumden 16558 | Calculate the reduced form of a quotient using gcd. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ ((π΄ β β€ β§ π΅ β β) β ((numerβ(π΄ / π΅)) = (π΄ / (π΄ gcd π΅)) β§ (denomβ(π΄ / π΅)) = (π΅ / (π΄ gcd π΅)))) | ||
Theorem | divdenle 16559 | Reducing a quotient never increases the denominator. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ ((π΄ β β€ β§ π΅ β β) β (denomβ(π΄ / π΅)) β€ π΅) | ||
Theorem | qnumgt0 16560 | A rational is positive iff its canonical numerator is. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ (π΄ β β β (0 < π΄ β 0 < (numerβπ΄))) | ||
Theorem | qgt0numnn 16561 | A rational is positive iff its canonical numerator is a positive integer. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ ((π΄ β β β§ 0 < π΄) β (numerβπ΄) β β) | ||
Theorem | nn0gcdsq 16562 | 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 16563 | nn0gcdsq 16562 extended to integers by symmetry. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€) β ((π΄ gcd π΅)β2) = ((π΄β2) gcd (π΅β2))) | ||
Theorem | numdensq 16564 | 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 16565 | Square commutes with canonical numerator. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ (π΄ β β β (numerβ(π΄β2)) = ((numerβπ΄)β2)) | ||
Theorem | densq 16566 | Square commutes with canonical denominator. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ (π΄ β β β (denomβ(π΄β2)) = ((denomβπ΄)β2)) | ||
Theorem | qden1elz 16567 | A rational is an integer iff it has denominator 1. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ (π΄ β β β ((denomβπ΄) = 1 β π΄ β β€)) | ||
Theorem | zsqrtelqelz 16568 | If an integer has a rational square root, that root is must be an integer. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ ((π΄ β β€ β§ (ββπ΄) β β) β (ββπ΄) β β€) | ||
Theorem | nonsq 16569 | Any integer strictly between two adjacent squares has an irrational square root. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ (((π΄ β β0 β§ π΅ β β0) β§ ((π΅β2) < π΄ β§ π΄ < ((π΅ + 1)β2))) β Β¬ (ββπ΄) β β) | ||
Syntax | codz 16570 | Extend class notation with the order function on the class of integers modulo N. |
class odβ€ | ||
Syntax | cphi 16571 | Extend class notation with the Euler phi function. |
class Ο | ||
Definition | df-odz 16572* | 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 16573* | 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 | phival 16574* | Value of the Euler Ο function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ (π β β β (Οβπ) = (β―β{π₯ β (1...π) β£ (π₯ gcd π) = 1})) | ||
Theorem | phicl2 16575 | Bounds and closure for the value of the Euler Ο function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ (π β β β (Οβπ) β (1...π)) | ||
Theorem | phicl 16576 | Closure for the value of the Euler Ο function. (Contributed by Mario Carneiro, 28-Feb-2014.) |
β’ (π β β β (Οβπ) β β) | ||
Theorem | phibndlem 16577* | Lemma for phibnd 16578. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ (π β (β€β₯β2) β {π₯ β (1...π) β£ (π₯ gcd π) = 1} β (1...(π β 1))) | ||
Theorem | phibnd 16578 | A slightly tighter bound on the value of the Euler Ο function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ (π β (β€β₯β2) β (Οβπ) β€ (π β 1)) | ||
Theorem | phicld 16579 | Closure for the value of the Euler Ο function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π β β) β β’ (π β (Οβπ) β β) | ||
Theorem | phi1 16580 | Value of the Euler Ο function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ (Οβ1) = 1 | ||
Theorem | dfphi2 16581* | 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 16582* | 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 16583 | 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 16584 | Value of the Euler Ο function at a prime. (Contributed by Mario Carneiro, 28-Feb-2014.) |
β’ (π β β β (Οβπ) = (π β 1)) | ||
Theorem | crth 16585* | 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 16586* | Lemma for phimul 16587. (Contributed by Mario Carneiro, 24-Feb-2014.) |
β’ π = (0..^(π Β· π)) & β’ π = ((0..^π) Γ (0..^π)) & β’ πΉ = (π₯ β π β¦ β¨(π₯ mod π), (π₯ mod π)β©) & β’ (π β (π β β β§ π β β β§ (π gcd π) = 1)) & β’ π = {π¦ β (0..^π) β£ (π¦ gcd π) = 1} & β’ π = {π¦ β (0..^π) β£ (π¦ gcd π) = 1} & β’ π = {π¦ β π β£ (π¦ gcd (π Β· π)) = 1} β β’ (π β (Οβ(π Β· π)) = ((Οβπ) Β· (Οβπ))) | ||
Theorem | phimul 16587 | 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 16588* | Lemma for eulerth 16590. (Contributed by Mario Carneiro, 8-May-2015.) |
β’ (π β (π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1)) & β’ π = {π¦ β (0..^π) β£ (π¦ gcd π) = 1} & β’ π = (1...(Οβπ)) & β’ (π β πΉ:πβ1-1-ontoβπ) & β’ πΊ = (π₯ β π β¦ ((π΄ Β· (πΉβπ₯)) mod π)) β β’ (π β πΊ:πβΆπ) | ||
Theorem | eulerthlem2 16589* | Lemma for eulerth 16590. (Contributed by Mario Carneiro, 28-Feb-2014.) |
β’ (π β (π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1)) & β’ π = {π¦ β (0..^π) β£ (π¦ gcd π) = 1} & β’ π = (1...(Οβπ)) & β’ (π β πΉ:πβ1-1-ontoβπ) & β’ πΊ = (π₯ β π β¦ ((π΄ Β· (πΉβπ₯)) mod π)) β β’ (π β ((π΄β(Οβπ)) mod π) = (1 mod π)) | ||
Theorem | eulerth 16590 | 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 16591 | 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 16592 | Show an explicit expression for the modular inverse of π΄ mod π. (Contributed by Mario Carneiro, 24-Jan-2015.) |
β’ π = ((π΄β(π β 2)) mod π) β β’ ((π β β β§ π΄ β β€ β§ Β¬ π β₯ π΄) β (π β (1...(π β 1)) β§ π β₯ ((π΄ Β· π ) β 1))) | ||
Theorem | prmdiveq 16593 | The modular inverse of π΄ mod π is unique. (Contributed by Mario Carneiro, 24-Jan-2015.) |
β’ π = ((π΄β(π β 2)) mod π) β β’ ((π β β β§ π΄ β β€ β§ Β¬ π β₯ π΄) β ((π β (0...(π β 1)) β§ π β₯ ((π΄ Β· π) β 1)) β π = π )) | ||
Theorem | prmdivdiv 16594 | 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 16595* | 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 16596* | Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ ((π β β β§ π β β) β (β―β{π₯ β (0..^π) β£ (π₯ gcd π) = π}) = if(π β₯ π, (Οβ(π / π)), 0)) | ||
Theorem | phisum 16597* | 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 16598* | 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 16599 | - Lemma for odzcl 16600, 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 16600 | The order of a group element is an integer. (Contributed by Mario Carneiro, 28-Feb-2014.) |
β’ ((π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1) β ((odβ€βπ)βπ΄) β β) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |