Home | Metamath
Proof Explorer Theorem List (p. 457 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | dfodd5 45601 | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ Odd = {π§ β β€ β£ (π§ mod 2) β 0} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | zefldiv2ALTV 45602 | The floor of an even number divided by 2 is equal to the even number divided by 2. (Contributed by AV, 7-Jun-2020.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β Even β (ββ(π / 2)) = (π / 2)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | zofldiv2ALTV 45603 | The floor of an odd numer divided by 2 is equal to the odd number first decreased by 1 and then divided by 2. (Contributed by AV, 7-Jun-2020.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β Odd β (ββ(π / 2)) = ((π β 1) / 2)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | oddflALTV 45604 | Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (πΎ β Odd β πΎ = ((2 Β· (ββ(πΎ / 2))) + 1)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iseven5 45605 | The predicate "is an even number". An even number and 2 have 2 as greatest common divisor. (Contributed by AV, 1-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β Even β (π β β€ β§ (2 gcd π) = 2)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isodd7 45606 | The predicate "is an odd number". An odd number and 2 have 1 as greatest common divisor. (Contributed by AV, 1-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β Odd β (π β β€ β§ (2 gcd π) = 1)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | dfeven5 45607 | Alternate definition for even numbers. (Contributed by AV, 1-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ Even = {π§ β β€ β£ (2 gcd π§) = 2} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | dfodd7 45608 | Alternate definition for odd numbers. (Contributed by AV, 1-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ Odd = {π§ β β€ β£ (2 gcd π§) = 1} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gcd2odd1 45609 | The greatest common divisor of an odd number and 2 is 1, i.e., 2 and any odd number are coprime. Remark: The proof using dfodd7 45608 is longer (see proof in comment)! (Contributed by AV, 5-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β Odd β (π gcd 2) = 1) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | zneoALTV 45610 | No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of [Apostol] p. 28. (Contributed by NM, 31-Jul-2004.) (Revised by AV, 16-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β Even β§ π΅ β Odd ) β π΄ β π΅) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | zeoALTV 45611 | An integer is even or odd. (Contributed by NM, 1-Jan-2006.) (Revised by AV, 16-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β β€ β (π β Even β¨ π β Odd )) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | zeo2ALTV 45612 | An integer is even or odd but not both. (Contributed by Mario Carneiro, 12-Sep-2015.) (Revised by AV, 16-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β β€ β (π β Even β Β¬ π β Odd )) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nneoALTV 45613 | A positive integer is even or odd but not both. (Contributed by NM, 1-Jan-2006.) (Revised by AV, 19-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β β β (π β Even β Β¬ π β Odd )) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nneoiALTV 45614 | A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001.) (Revised by AV, 19-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ π β β β β’ (π β Even β Β¬ π β Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | odd2np1ALTV 45615* | An integer is odd iff it is one plus twice another integer. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by AV, 19-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β β€ β (π β Odd β βπ β β€ ((2 Β· π) + 1) = π)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | oddm1evenALTV 45616 | An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β β€ β (π β Odd β (π β 1) β Even )) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | oddp1evenALTV 45617 | An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β β€ β (π β Odd β (π + 1) β Even )) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | oexpnegALTV 45618 | The exponential of the negative of a number, when the exponent is odd. (Contributed by Mario Carneiro, 25-Apr-2015.) (Revised by AV, 19-Jun-2020.) (Proof shortened by AV, 10-Jul-2022.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β β β§ π β β β§ π β Odd ) β (-π΄βπ) = -(π΄βπ)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | oexpnegnz 45619 | The exponential of the negative of a number not being 0, when the exponent is odd. (Contributed by AV, 19-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β β β§ π΄ β 0 β§ π β Odd ) β (-π΄βπ) = -(π΄βπ)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | bits0ALTV 45620 | Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β β€ β (0 β (bitsβπ) β π β Odd )) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | bits0eALTV 45621 | The zeroth bit of an even number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β Even β Β¬ 0 β (bitsβπ)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | bits0oALTV 45622 | The zeroth bit of an odd number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β Odd β 0 β (bitsβπ)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | divgcdoddALTV 45623 | Either π΄ / (π΄ gcd π΅) is odd or π΅ / (π΄ gcd π΅) is odd. (Contributed by Scott Fenton, 19-Apr-2014.) (Revised by AV, 21-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β β β§ π΅ β β) β ((π΄ / (π΄ gcd π΅)) β Odd β¨ (π΅ / (π΄ gcd π΅)) β Odd )) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opoeALTV 45624 | The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by AV, 20-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β Odd β§ π΅ β Odd ) β (π΄ + π΅) β Even ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opeoALTV 45625 | The sum of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by AV, 20-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β Odd β§ π΅ β Even ) β (π΄ + π΅) β Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | omoeALTV 45626 | The difference of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by AV, 20-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β Odd β§ π΅ β Odd ) β (π΄ β π΅) β Even ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | omeoALTV 45627 | The difference of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by AV, 20-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β Odd β§ π΅ β Even ) β (π΄ β π΅) β Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | oddprmALTV 45628 | A prime not equal to 2 is odd. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by AV, 21-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β (β β {2}) β π β Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 0evenALTV 45629 | 0 is an even number. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 17-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ 0 β Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 0noddALTV 45630 | 0 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 17-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ 0 β Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 1oddALTV 45631 | 1 is an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ 1 β Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 1nevenALTV 45632 | 1 is not an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ 1 β Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 2evenALTV 45633 | 2 is an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ 2 β Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 2noddALTV 45634 | 2 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ 2 β Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nn0o1gt2ALTV 45635 | An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 21-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β β0 β§ π β Odd ) β (π = 1 β¨ 2 < π)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnoALTV 45636 | An alternate characterization of an odd number greater than 1. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 21-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β (β€β₯β2) β§ π β Odd ) β ((π β 1) / 2) β β) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nn0oALTV 45637 | An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020.) (Revised by AV, 21-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β β0 β§ π β Odd ) β ((π β 1) / 2) β β0) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nn0e 45638 | An alternate characterization of an even nonnegative integer. (Contributed by AV, 22-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β β0 β§ π β Even ) β (π / 2) β β0) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nneven 45639 | An alternate characterization of an even positive integer. (Contributed by AV, 5-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β β β§ π β Even ) β (π / 2) β β) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nn0onn0exALTV 45640* | For each odd nonnegative integer there is a nonnegative integer which, multiplied by 2 and increased by 1, results in the odd nonnegative integer. (Contributed by AV, 30-May-2020.) (Revised by AV, 22-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β β0 β§ π β Odd ) β βπ β β0 π = ((2 Β· π) + 1)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nn0enn0exALTV 45641* | For each even nonnegative integer there is a nonnegative integer which, multiplied by 2, results in the even nonnegative integer. (Contributed by AV, 30-May-2020.) (Revised by AV, 22-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β β0 β§ π β Even ) β βπ β β0 π = (2 Β· π)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnennexALTV 45642* | For each even positive integer there is a positive integer which, multiplied by 2, results in the even positive integer. (Contributed by AV, 5-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β β β§ π β Even ) β βπ β β π = (2 Β· π)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnpw2evenALTV 45643 | 2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 20-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β β β (2βπ) β Even ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | epoo 45644 | The sum of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β Even β§ π΅ β Odd ) β (π΄ + π΅) β Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | emoo 45645 | The difference of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β Even β§ π΅ β Odd ) β (π΄ β π΅) β Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | epee 45646 | The sum of two even numbers is even. (Contributed by AV, 21-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β Even β§ π΅ β Even ) β (π΄ + π΅) β Even ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | emee 45647 | The difference of two even numbers is even. (Contributed by AV, 21-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β Even β§ π΅ β Even ) β (π΄ β π΅) β Even ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | evensumeven 45648 | If a summand is even, the other summand is even iff the sum is even. (Contributed by AV, 21-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π΄ β β€ β§ π΅ β Even ) β (π΄ β Even β (π΄ + π΅) β Even )) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 3odd 45649 | 3 is an odd number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ 3 β Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 4even 45650 | 4 is an even number. (Contributed by AV, 23-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ 4 β Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 5odd 45651 | 5 is an odd number. (Contributed by AV, 23-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ 5 β Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 6even 45652 | 6 is an even number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ 6 β Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 7odd 45653 | 7 is an odd number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ 7 β Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 8even 45654 | 8 is an even number. (Contributed by AV, 23-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ 8 β Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | evenprm2 45655 | A prime number is even iff it is 2. (Contributed by AV, 21-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β β β (π β Even β π = 2)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | oddprmne2 45656 | Every prime number not being 2 is an odd prime number. (Contributed by AV, 21-Aug-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β β β§ π β Odd ) β π β (β β {2})) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | oddprmuzge3 45657 | A prime number which is odd is an integer greater than or equal to 3. (Contributed by AV, 20-Jul-2020.) (Proof shortened by AV, 21-Aug-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β β β§ π β Odd ) β π β (β€β₯β3)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | evenltle 45658 | If an even number is greater than another even number, then it is greater than or equal to the other even number plus 2. (Contributed by AV, 25-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β Even β§ π β Even β§ π < π) β (π + 2) β€ π) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | odd2prm2 45659 | If an odd number is the sum of two prime numbers, one of the prime numbers must be 2. (Contributed by AV, 26-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β Odd β§ (π β β β§ π β β) β§ π = (π + π)) β (π = 2 β¨ π = 2)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | even3prm2 45660 | If an even number is the sum of three prime numbers, one of the prime numbers must be 2. (Contributed by AV, 25-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β Even β§ (π β β β§ π β β β§ π β β) β§ π = ((π + π) + π )) β (π = 2 β¨ π = 2 β¨ π = 2)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mogoldbblem 45661* | Lemma for mogoldbb 45726. (Contributed by AV, 26-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (((π β β β§ π β β β§ π β β) β§ π β Even β§ (π + 2) = ((π + π) + π )) β βπ β β βπ β β π = (π + π)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | perfectALTVlem1 45662 | Lemma for perfectALTV 45664. (Contributed by Mario Carneiro, 7-Jun-2016.) (Revised by AV, 1-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΅ β Odd ) & β’ (π β (1 Ο ((2βπ΄) Β· π΅)) = (2 Β· ((2βπ΄) Β· π΅))) β β’ (π β ((2β(π΄ + 1)) β β β§ ((2β(π΄ + 1)) β 1) β β β§ (π΅ / ((2β(π΄ + 1)) β 1)) β β)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | perfectALTVlem2 45663 | Lemma for perfectALTV 45664. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by AV, 1-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΅ β Odd ) & β’ (π β (1 Ο ((2βπ΄) Β· π΅)) = (2 Β· ((2βπ΄) Β· π΅))) β β’ (π β (π΅ β β β§ π΅ = ((2β(π΄ + 1)) β 1))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | perfectALTV 45664* | The Euclid-Euler theorem, or Perfect Number theorem. A positive even integer π is a perfect number (that is, its divisor sum is 2π) if and only if it is of the form 2β(π β 1) Β· (2βπ β 1), where 2βπ β 1 is prime (a Mersenne prime). (It follows from this that π is also prime.) This is Metamath 100 proof #70. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by AV, 1-Jul-2020.) (Proof modification is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β β β§ π β Even ) β ((1 Ο π) = (2 Β· π) β βπ β β€ (((2βπ) β 1) β β β§ π = ((2β(π β 1)) Β· ((2βπ) β 1))))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
"In number theory, the Fermat pseudoprimes make up the most important class of pseudoprimes that come from Fermat's little theorem ... [which] states that if p is prime and a is coprime to p, then a^(p-1)-1 is divisible by p [see fermltl 16590]. For an integer a > 1, if a composite integer x divides a^(x-1)-1, then x is called a Fermat pseudoprime to base a. In other words, a composite integer is a Fermat pseudoprime to base a if it successfully passes the Fermat primality test for the base a. The false statement [see nfermltl2rev 45684] that all numbers that pass the Fermat primality test for base 2, are prime, is called the Chinese hypothesis.", see Wikipedia "Fermat pseudoprime", https://en.wikipedia.org/wiki/Fermat_pseudoprime 45684, 29-May-2023. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cfppr 45665 | Extend class notation with the Fermat pseudoprimes. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class FPPr | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-fppr 45666* | Define the function that maps a positive integer to the set of Fermat pseudoprimes to the base of this positive integer. Since Fermat pseudoprimes shall be composite (positive) integers, they must be nonprime integers greater than or equal to 4 (we cannot use π₯ β β β§ π₯ β β because π₯ = 1 would fulfil this requirement, but should not be regarded as "composite" integer). (Contributed by AV, 29-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ FPPr = (π β β β¦ {π₯ β (β€β₯β4) β£ (π₯ β β β§ π₯ β₯ ((πβ(π₯ β 1)) β 1))}) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fppr 45667* | The set of Fermat pseudoprimes to the base π. (Contributed by AV, 29-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β β β ( FPPr βπ) = {π₯ β (β€β₯β4) β£ (π₯ β β β§ π₯ β₯ ((πβ(π₯ β 1)) β 1))}) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fpprmod 45668* | The set of Fermat pseudoprimes to the base π, expressed by a modulo operation instead of the divisibility relation. (Contributed by AV, 30-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β β β ( FPPr βπ) = {π₯ β (β€β₯β4) β£ (π₯ β β β§ ((πβ(π₯ β 1)) mod π₯) = 1)}) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fpprel 45669 | A Fermat pseudoprime to the base π. (Contributed by AV, 30-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β β β (π β ( FPPr βπ) β (π β (β€β₯β4) β§ π β β β§ ((πβ(π β 1)) mod π) = 1))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fpprbasnn 45670 | The base of a Fermat pseudoprime is a positive integer. (Contributed by AV, 30-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β ( FPPr βπ) β π β β) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fpprnn 45671 | A Fermat pseudoprime to the base π is a positive integer. (Contributed by AV, 30-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β ( FPPr βπ) β π β β) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fppr2odd 45672 | A Fermat pseudoprime to the base 2 is odd. (Contributed by AV, 5-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β ( FPPr β2) β π β Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 11t31e341 45673 | 341 is the product of 11 and 31. (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (;11 Β· ;31) = ;;341 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 2exp340mod341 45674 | Eight to the eighth power modulo nine is one. (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((2β;;340) mod ;;341) = 1 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 341fppr2 45675 | 341 is the (smallest) Poulet number (Fermat pseudoprime to the base 2). (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ;;341 β ( FPPr β2) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 4fppr1 45676 | 4 is the (smallest) Fermat pseudoprime to the base 1. (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ 4 β ( FPPr β1) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 8exp8mod9 45677 | Eight to the eighth power modulo nine is one. (Contributed by AV, 2-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((8β8) mod 9) = 1 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 9fppr8 45678 | 9 is the (smallest) Fermat pseudoprime to the base 8. (Contributed by AV, 2-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ 9 β ( FPPr β8) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | dfwppr 45679 | Alternate definition of a weak pseudoprime π, which fulfils (πβπ)β‘π (modulo π), see Wikipedia "Fermat pseudoprime", https://en.wikipedia.org/wiki/Fermat_pseudoprime, 29-May-2023. (Contributed by AV, 31-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π β β β§ π β β) β (((πβπ) mod π) = (π mod π) β π β₯ ((πβπ) β π))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fpprwppr 45680 | A Fermat pseudoprime to the base π is a weak pseudoprime (see Wikipedia "Fermat pseudoprime", 29-May-2023, https://en.wikipedia.org/wiki/Fermat_pseudoprime. (Contributed by AV, 31-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β ( FPPr βπ) β ((πβπ) mod π) = (π mod π)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fpprwpprb 45681 | An integer π which is coprime with an integer π is a Fermat pseudoprime to the base π iff it is a weak pseudoprime to the base π. (Contributed by AV, 2-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ ((π gcd π) = 1 β (π β ( FPPr βπ) β ((π β (β€β₯β4) β§ π β β) β§ (π β β β§ ((πβπ) mod π) = (π mod π))))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fpprel2 45682 | An alternate definition for a Fermat pseudoprime to the base 2. (Contributed by AV, 5-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β ( FPPr β2) β ((π β (β€β₯β2) β§ π β Odd β§ π β β) β§ ((2βπ) mod π) = 2)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nfermltl8rev 45683 | Fermat's little theorem with base 8 reversed is not generally true: There is an integer π (for example 9, see 9fppr8 45678) so that "π is prime" does not follow from 8βπβ‘8 (mod π). (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ βπ β (β€β₯β3) Β¬ (((8βπ) mod π) = (8 mod π) β π β β) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nfermltl2rev 45684 | Fermat's little theorem with base 2 reversed is not generally true: There is an integer π (for example 341, see 341fppr2 45675) so that "π is prime" does not follow from 2βπβ‘2 (mod π). (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ βπ β (β€β₯β3) Β¬ (((2βπ) mod π) = (2 mod π) β π β β) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nfermltlrev 45685* | Fermat's little theorem reversed is not generally true: There are integers π and π so that "π is prime" does not follow from πβπβ‘π (mod π). (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ βπ β β€ βπ β (β€β₯β3) Β¬ (((πβπ) mod π) = (π mod π) β π β β) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
According to Wikipedia ("Goldbach's conjecture", 20-Jul-2020,
https://en.wikipedia.org/wiki/Goldbach's_conjecture) "Goldbach's
conjecture ... states: Every even integer greater than 2 can be expressed as
the sum of two primes." "It is also known as strong, even or binary Goldbach
conjecture, to distinguish it from a weaker conjecture, known ... as the
_Goldbach's weak conjecture_, the _odd Goldbach conjecture_, or the _ternary
Goldbach conjecture_. This weak conjecture asserts that all odd numbers
greater than 7 are the sum of three odd primes.". In the following, the
terms "binary Goldbach conjecture" resp. "ternary Goldbach conjecture" will
be used (following the terminology used in [Helfgott] p. 2), because there
are a strong and a weak version of the ternary Goldbach conjecture. The term
_Goldbach partition_ is used for a sum of two resp. three (odd) primes
resulting in an even resp. odd number without further specialization.
Summary/glossary:
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cgbe 45686 | Extend the definition of a class to include the set of even numbers which have a Goldbach partition. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cgbow 45687 | Extend the definition of a class to include the set of odd numbers which can be written as a sum of three primes. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class GoldbachOddW | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cgbo 45688 | Extend the definition of a class to include the set of odd numbers which can be written as a sum of three odd primes. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-gbe 45689* | Define the set of (even) Goldbach numbers, which are positive even integers that can be expressed as the sum of two odd primes. By this definition, the binary Goldbach conjecture can be expressed as βπ β Even (4 < π β π β GoldbachEven ). (Contributed by AV, 14-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ GoldbachEven = {π§ β Even β£ βπ β β βπ β β (π β Odd β§ π β Odd β§ π§ = (π + π))} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-gbow 45690* | Define the set of weak odd Goldbach numbers, which are positive odd integers that can be expressed as the sum of three primes. By this definition, the weak ternary Goldbach conjecture can be expressed as βπ β Odd (5 < π β π β GoldbachOddW ). (Contributed by AV, 14-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ GoldbachOddW = {π§ β Odd β£ βπ β β βπ β β βπ β β π§ = ((π + π) + π)} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-gbo 45691* | Define the set of (strong) odd Goldbach numbers, which are positive odd integers that can be expressed as the sum of three odd primes. By this definition, the strong ternary Goldbach conjecture can be expressed as βπ β Odd (7 < π β π β GoldbachOdd ). (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ GoldbachOdd = {π§ β Odd β£ βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π§ = ((π + π) + π))} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isgbe 45692* | The predicate "is an even Goldbach number". An even Goldbach number is an even integer having a Goldbach partition, i.e. which can be written as a sum of two odd primes. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β GoldbachEven β (π β Even β§ βπ β β βπ β β (π β Odd β§ π β Odd β§ π = (π + π)))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isgbow 45693* | The predicate "is a weak odd Goldbach number". A weak odd Goldbach number is an odd integer having a Goldbach partition, i.e. which can be written as a sum of three primes. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β GoldbachOddW β (π β Odd β§ βπ β β βπ β β βπ β β π = ((π + π) + π))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isgbo 45694* | The predicate "is an odd Goldbach number". An odd Goldbach number is an odd integer having a Goldbach partition, i.e. which can be written as sum of three odd primes. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β GoldbachOdd β (π β Odd β§ βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbeeven 45695 | An even Goldbach number is even. (Contributed by AV, 25-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β GoldbachEven β π β Even ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbowodd 45696 | A weak odd Goldbach number is odd. (Contributed by AV, 25-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β GoldbachOddW β π β Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbogbow 45697 | A (strong) odd Goldbach number is a weak Goldbach number. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β GoldbachOdd β π β GoldbachOddW ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gboodd 45698 | An odd Goldbach number is odd. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β GoldbachOdd β π β Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbepos 45699 | Any even Goldbach number is positive. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β GoldbachEven β π β β) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbowpos 45700 | Any weak odd Goldbach number is positive. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
β’ (π β GoldbachOddW β π β β) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |