![]() |
Metamath
Proof Explorer Theorem List (p. 168 of 482) | < 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: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | qdenval 16701* | Value of the canonical denominator function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β (denomβπ΄) = (2nd β(β©π₯ β (β€ Γ β)(((1st βπ₯) gcd (2nd βπ₯)) = 1 β§ π΄ = ((1st βπ₯) / (2nd βπ₯)))))) | ||
Theorem | qnumdencl 16702 | Lemma for qnumcl 16703 and qdencl 16704. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β ((numerβπ΄) β β€ β§ (denomβπ΄) β β)) | ||
Theorem | qnumcl 16703 | The canonical numerator of a rational is an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β (numerβπ΄) β β€) | ||
Theorem | qdencl 16704 | The canonical denominator is a positive integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β (denomβπ΄) β β) | ||
Theorem | fnum 16705 | Canonical numerator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ numer:ββΆβ€ | ||
Theorem | fden 16706 | Canonical denominator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ denom:ββΆβ | ||
Theorem | qnumdenbi 16707 | 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 16708 | The canonical representation of a rational is fully reduced. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β ((numerβπ΄) gcd (denomβπ΄)) = 1) | ||
Theorem | qeqnumdivden 16709 | Recover a rational number from its canonical representation. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β π΄ = ((numerβπ΄) / (denomβπ΄))) | ||
Theorem | qmuldeneqnum 16710 | Multiplying a rational by its denominator results in an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ (π΄ β β β (π΄ Β· (denomβπ΄)) = (numerβπ΄)) | ||
Theorem | divnumden 16711 | Calculate the reduced form of a quotient using gcd. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ ((π΄ β β€ β§ π΅ β β) β ((numerβ(π΄ / π΅)) = (π΄ / (π΄ gcd π΅)) β§ (denomβ(π΄ / π΅)) = (π΅ / (π΄ gcd π΅)))) | ||
Theorem | divdenle 16712 | Reducing a quotient never increases the denominator. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ ((π΄ β β€ β§ π΅ β β) β (denomβ(π΄ / π΅)) β€ π΅) | ||
Theorem | qnumgt0 16713 | A rational is positive iff its canonical numerator is. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ (π΄ β β β (0 < π΄ β 0 < (numerβπ΄))) | ||
Theorem | qgt0numnn 16714 | A rational is positive iff its canonical numerator is a positive integer. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ ((π΄ β β β§ 0 < π΄) β (numerβπ΄) β β) | ||
Theorem | nn0gcdsq 16715 | 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 16716 | nn0gcdsq 16715 extended to integers by symmetry. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€) β ((π΄ gcd π΅)β2) = ((π΄β2) gcd (π΅β2))) | ||
Theorem | numdensq 16717 | 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 16718 | Square commutes with canonical numerator. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ (π΄ β β β (numerβ(π΄β2)) = ((numerβπ΄)β2)) | ||
Theorem | densq 16719 | Square commutes with canonical denominator. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ (π΄ β β β (denomβ(π΄β2)) = ((denomβπ΄)β2)) | ||
Theorem | qden1elz 16720 | A rational is an integer iff it has denominator 1. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ (π΄ β β β ((denomβπ΄) = 1 β π΄ β β€)) | ||
Theorem | zsqrtelqelz 16721 | 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 16722 | 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 16723 | Extend class notation with the order function on the class of integers modulo N. |
class odβ€ | ||
Syntax | cphi 16724 | Extend class notation with the Euler phi function. |
class Ο | ||
Definition | df-odz 16725* | 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 16726* | 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 16727* | Value of the Euler Ο function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ (π β β β (Οβπ) = (β―β{π₯ β (1...π) β£ (π₯ gcd π) = 1})) | ||
Theorem | phicl2 16728 | Bounds and closure for the value of the Euler Ο function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ (π β β β (Οβπ) β (1...π)) | ||
Theorem | phicl 16729 | Closure for the value of the Euler Ο function. (Contributed by Mario Carneiro, 28-Feb-2014.) |
β’ (π β β β (Οβπ) β β) | ||
Theorem | phibndlem 16730* | Lemma for phibnd 16731. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ (π β (β€β₯β2) β {π₯ β (1...π) β£ (π₯ gcd π) = 1} β (1...(π β 1))) | ||
Theorem | phibnd 16731 | A slightly tighter bound on the value of the Euler Ο function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ (π β (β€β₯β2) β (Οβπ) β€ (π β 1)) | ||
Theorem | phicld 16732 | Closure for the value of the Euler Ο function. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π β β) β β’ (π β (Οβπ) β β) | ||
Theorem | phi1 16733 | Value of the Euler Ο function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ (Οβ1) = 1 | ||
Theorem | dfphi2 16734* | 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 16735* | 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 16736 | 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 16737 | Value of the Euler Ο function at a prime. (Contributed by Mario Carneiro, 28-Feb-2014.) |
β’ (π β β β (Οβπ) = (π β 1)) | ||
Theorem | crth 16738* | 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 16739* | Lemma for phimul 16740. (Contributed by Mario Carneiro, 24-Feb-2014.) |
β’ π = (0..^(π Β· π)) & β’ π = ((0..^π) Γ (0..^π)) & β’ πΉ = (π₯ β π β¦ β¨(π₯ mod π), (π₯ mod π)β©) & β’ (π β (π β β β§ π β β β§ (π gcd π) = 1)) & β’ π = {π¦ β (0..^π) β£ (π¦ gcd π) = 1} & β’ π = {π¦ β (0..^π) β£ (π¦ gcd π) = 1} & β’ π = {π¦ β π β£ (π¦ gcd (π Β· π)) = 1} β β’ (π β (Οβ(π Β· π)) = ((Οβπ) Β· (Οβπ))) | ||
Theorem | phimul 16740 | 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 16741* | Lemma for eulerth 16743. (Contributed by Mario Carneiro, 8-May-2015.) |
β’ (π β (π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1)) & β’ π = {π¦ β (0..^π) β£ (π¦ gcd π) = 1} & β’ π = (1...(Οβπ)) & β’ (π β πΉ:πβ1-1-ontoβπ) & β’ πΊ = (π₯ β π β¦ ((π΄ Β· (πΉβπ₯)) mod π)) β β’ (π β πΊ:πβΆπ) | ||
Theorem | eulerthlem2 16742* | Lemma for eulerth 16743. (Contributed by Mario Carneiro, 28-Feb-2014.) |
β’ (π β (π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1)) & β’ π = {π¦ β (0..^π) β£ (π¦ gcd π) = 1} & β’ π = (1...(Οβπ)) & β’ (π β πΉ:πβ1-1-ontoβπ) & β’ πΊ = (π₯ β π β¦ ((π΄ Β· (πΉβπ₯)) mod π)) β β’ (π β ((π΄β(Οβπ)) mod π) = (1 mod π)) | ||
Theorem | eulerth 16743 | 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 16744 | 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 16745 | Show an explicit expression for the modular inverse of π΄ mod π. (Contributed by Mario Carneiro, 24-Jan-2015.) |
β’ π = ((π΄β(π β 2)) mod π) β β’ ((π β β β§ π΄ β β€ β§ Β¬ π β₯ π΄) β (π β (1...(π β 1)) β§ π β₯ ((π΄ Β· π ) β 1))) | ||
Theorem | prmdiveq 16746 | The modular inverse of π΄ mod π is unique. (Contributed by Mario Carneiro, 24-Jan-2015.) |
β’ π = ((π΄β(π β 2)) mod π) β β’ ((π β β β§ π΄ β β€ β§ Β¬ π β₯ π΄) β ((π β (0...(π β 1)) β§ π β₯ ((π΄ Β· π) β 1)) β π = π )) | ||
Theorem | prmdivdiv 16747 | 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 16748* | 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 16749* | Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ ((π β β β§ π β β) β (β―β{π₯ β (0..^π) β£ (π₯ gcd π) = π}) = if(π β₯ π, (Οβ(π / π)), 0)) | ||
Theorem | phisum 16750* | 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 16751* | 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 16752 | - Lemma for odzcl 16753, 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 16753 | The order of a group element is an integer. (Contributed by Mario Carneiro, 28-Feb-2014.) |
β’ ((π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1) β ((odβ€βπ)βπ΄) β β) | ||
Theorem | odzid 16754 | Any element raised to the power of its order is 1. (Contributed by Mario Carneiro, 28-Feb-2014.) |
β’ ((π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1) β π β₯ ((π΄β((odβ€βπ)βπ΄)) β 1)) | ||
Theorem | odzdvds 16755 | 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 16756 | The order of any group element is a divisor of the Euler Ο function. (Contributed by Mario Carneiro, 28-Feb-2014.) |
β’ ((π β β β§ π΄ β β€ β§ (π΄ gcd π) = 1) β ((odβ€βπ)βπ΄) β₯ (Οβπ)) | ||
Theorem | modprm1div 16757 | 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 16758 | 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 16759 | Show an explicit expression for the modular inverse of π΄ mod π. This is an application of prmdiv 16745. (Contributed by Alexander van der Vekens, 15-May-2018.) |
β’ π = ((π΄β(π β 2)) mod π) β β’ ((π β β β§ π΄ β β€ β§ Β¬ π β₯ π΄) β (π β (1...(π β 1)) β§ ((π΄ Β· π ) mod π) = 1)) | ||
Theorem | modprminveq 16760 | The modular inverse of π΄ mod π is unique. (Contributed by Alexander van der Vekens, 17-May-2018.) |
β’ π = ((π΄β(π β 2)) mod π) β β’ ((π β β β§ π΄ β β€ β§ Β¬ π β₯ π΄) β ((π β (0...(π β 1)) β§ ((π΄ Β· π) mod π) = 1) β π = π )) | ||
Theorem | vfermltl 16761 | 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 | vfermltlALT 16762 | Alternate proof of vfermltl 16761, not using Euler's theorem. (Contributed by AV, 21-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ ((π β β β§ π΄ β β€ β§ Β¬ π β₯ π΄) β ((π΄β(π β 1)) mod π) = 1) | ||
Theorem | powm2modprm 16763 | 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 16764* | 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 16765* | 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 16766* | 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 16767* | 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)) | ||
Theorem | coprimeprodsq 16768 | 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 16769 | 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 16770 | 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 16771 | A prime not equal to 2 is an odd positive integer. (Contributed by AV, 28-Jun-2021.) |
β’ (π β (β β {2}) β (π β β β§ Β¬ 2 β₯ π)) | ||
Theorem | oddn2prm 16772 | A prime not equal to 2 is odd. (Contributed by AV, 28-Jun-2021.) |
β’ (π β (β β {2}) β Β¬ 2 β₯ π) | ||
Theorem | nnoddn2prmb 16773 | 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 16774 | A prime less than 5 is either 2 or 3. (Contributed by AV, 5-Jul-2021.) |
β’ ((π β β β§ π < 5) β (π = 2 β¨ π = 3)) | ||
Theorem | prm23ge5 16775 | 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 16776* | Lemma for pythagtrip 16794. 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 16777* | Lemma for pythagtrip 16794. 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 16778 | Lemma for pythagtrip 16794. 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 16779 | Lemma for pythagtrip 16794. 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 16780 | Lemma for pythagtrip 16794. Show that πΆ β π΅ is positive. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2)) β 0 < (πΆ β π΅)) | ||
Theorem | pythagtriplem6 16781 | Lemma for pythagtrip 16794. Calculate (ββ(πΆ β π΅)). (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β (ββ(πΆ β π΅)) = ((πΆ β π΅) gcd π΄)) | ||
Theorem | pythagtriplem7 16782 | Lemma for pythagtrip 16794. Calculate (ββ(πΆ + π΅)). (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β (ββ(πΆ + π΅)) = ((πΆ + π΅) gcd π΄)) | ||
Theorem | pythagtriplem8 16783 | Lemma for pythagtrip 16794. 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 16784 | Lemma for pythagtrip 16794. 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 16785 | Lemma for pythagtrip 16794. 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 16786 | Lemma for pythagtrip 16794. 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 16787 | Lemma for pythagtrip 16794. 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 16788 | Lemma for pythagtrip 16794. 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 16789 | Lemma for pythagtrip 16794. 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 16790 | Lemma for pythagtrip 16794. 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 16791 | Lemma for pythagtrip 16794. 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 16792* | Lemma for pythagtrip 16794. 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 16793* | Lemma for pythagtrip 16794. 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 16794* | 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)))))) | ||
Theorem | iserodd 16795* | Collect the odd terms in a sequence. (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by AV, 10-Jul-2022.) |
β’ ((π β§ π β β0) β πΆ β β) & β’ (π = ((2 Β· π) + 1) β π΅ = πΆ) β β’ (π β (seq0( + , (π β β0 β¦ πΆ)) β π΄ β seq1( + , (π β β β¦ if(2 β₯ π, 0, π΅))) β π΄)) | ||
Syntax | cpc 16796 | Extend class notation with the prime count function. |
class pCnt | ||
Definition | df-pc 16797* | 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 | pclem 16798* | - Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ π΄ = {π β β0 β£ (πβπ) β₯ π} β β’ ((π β (β€β₯β2) β§ (π β β€ β§ π β 0)) β (π΄ β β€ β§ π΄ β β β§ βπ₯ β β€ βπ¦ β π΄ π¦ β€ π₯)) | ||
Theorem | pcprecl 16799* | Closure of the prime power pre-function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ π΄ = {π β β0 β£ (πβπ) β₯ π} & β’ π = sup(π΄, β, < ) β β’ ((π β (β€β₯β2) β§ (π β β€ β§ π β 0)) β (π β β0 β§ (πβπ) β₯ π)) | ||
Theorem | pcprendvds 16800* | Non-divisibility property of the prime power pre-function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ π΄ = {π β β0 β£ (πβπ) β₯ π} & β’ π = sup(π΄, β, < ) β β’ ((π β (β€β₯β2) β§ (π β β€ β§ π β 0)) β Β¬ (πβ(π + 1)) β₯ π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |