Home | Metamath
Proof Explorer Theorem List (p. 417 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 1oddALTV 41601 | 1 is an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 1nevenALTV 41602 | 1 is not an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 2evenALTV 41603 | 2 is an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 2noddALTV 41604 | 2 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nn0o1gt2ALTV 41605 | An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 21-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnoALTV 41606 | An alternate characterization of an odd number greater than 1. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 21-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nn0oALTV 41607 | An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020.) (Revised by AV, 21-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nn0e 41608 | An alternate characterization of an even nonnegative integer. (Contributed by AV, 22-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nn0onn0exALTV 41609* | 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nn0enn0exALTV 41610* | 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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnpw2evenALTV 41611 | 2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 20-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | epoo 41612 | The sum of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even Odd Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | emoo 41613 | The difference of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even Odd Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | epee 41614 | The sum of two even numbers is even. (Contributed by AV, 21-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even Even Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | emee 41615 | The difference of two even numbers is even. (Contributed by AV, 21-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even Even Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | evensumeven 41616 | 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 41617 | 3 is an odd number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 4even 41618 | 4 is an even number. (Contributed by AV, 23-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 5odd 41619 | 5 is an odd number. (Contributed by AV, 23-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 6even 41620 | 6 is an even number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 7odd 41621 | 7 is an odd number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 8even 41622 | 8 is an even number. (Contributed by AV, 23-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | evenprm2 41623 | A prime number is even iff it is 2. (Contributed by AV, 21-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | oddprmne2 41624 | Every prime number not being 2 is an odd prime number. (Contributed by AV, 21-Aug-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | oddprmuzge3 41625 | 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 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | evenltle 41626 | 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 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | odd2prm2 41627 | 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 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | even3prm2 41628 | 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 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mogoldbblem 41629* | Lemma for mogoldbb 41673. (Contributed by AV, 26-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | perfectALTVlem1 41630 | Lemma for perfectALTV 41632. (Contributed by Mario Carneiro, 7-Jun-2016.) (Revised by AV, 1-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | perfectALTVlem2 41631 | Lemma for perfectALTV 41632. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by AV, 1-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | perfectALTV 41632* | The Euclid-Euler theorem, or Perfect Number theorem. A positive even integer is a perfect number (that is, its divisor sum is ) if and only if it is of the form , where 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 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
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 41633 | Extend the definition of a class to include the set of even numbers which have a Goldbach partition. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cgbow 41634 | Extend the definition of a class to include the set of odd numbers which can be written as a sum of three primes. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachOddW | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cgbo 41635 | Extend the definition of a class to include the set of odd numbers which can be written as a sum of three odd primes. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-gbe 41636* | 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 GoldbachEven . (Contributed by AV, 14-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachEven Even Odd Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-gbow 41637* | 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 GoldbachOddW . (Contributed by AV, 14-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachOddW Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-gbo 41638* | 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 GoldbachOdd . (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachOdd Odd Odd Odd Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isgbe 41639* | 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 41640* | 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 41641* | 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 41642 | An even Goldbach number is even. (Contributed by AV, 25-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachEven Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbowodd 41643 | A weak odd Goldbach number is odd. (Contributed by AV, 25-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachOddW Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbogbow 41644 | A (strong) odd Goldbach number is a weak Goldbach number. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachOdd GoldbachOddW | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gboodd 41645 | An odd Goldbach number is odd. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachOdd Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbepos 41646 | Any even Goldbach number is positive. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbowpos 41647 | Any weak odd Goldbach number is positive. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachOddW | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbopos 41648 | Any odd Goldbach number is positive. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbegt5 41649 | Any even Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbowgt5 41650 | Any weak odd Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachOddW | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbowge7 41651 | Any weak odd Goldbach number is greater than or equal to 7. Because of 7gbow 41660, this bound is strict. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachOddW | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gboge9 41652 | Any odd Goldbach number is greater than or equal to 9. Because of 9gbo 41662, this bound is strict. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbege6 41653 | Any even Goldbach number is greater than or equal to 6. Because of 6gbe 41659, this bound is strict. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbpart6 41654 | The Goldbach partition of 6. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbpart7 41655 | The (weak) Goldbach partition of 7. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbpart8 41656 | The Goldbach partition of 8. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbpart9 41657 | The (strong) Goldbach partition of 9. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbpart11 41658 | The (strong) Goldbach partition of 11. (Contributed by AV, 29-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
; | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 6gbe 41659 | 6 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 7gbow 41660 | 7 is a weak odd Goldbach number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachOddW | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 8gbe 41661 | 8 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 9gbo 41662 | 9 is an odd Goldbach number. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 11gbo 41663 | 11 is an odd Goldbach number. (Contributed by AV, 29-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
; GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | stgoldbwt 41664 | If the strong ternary Goldbach conjecture is valid, then the weak ternary Goldbach conjecture holds, too. (Contributed by AV, 27-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd GoldbachOdd Odd GoldbachOddW | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbwt 41665* | If the strong binary Goldbach conjecture is valid, then the (weak) ternary Goldbach conjecture holds, too. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even GoldbachEven Odd GoldbachOddW | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbst 41666* | If the strong binary Goldbach conjecture is valid, then the (strong) ternary Goldbach conjecture holds, too. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even GoldbachEven Odd GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbaltlem1 41667 | Lemma 1 for sbgoldbalt 41669: If an even number greater than 4 is the sum of two primes, one of the prime summands must be odd, i.e. not 2. (Contributed by AV, 22-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbaltlem2 41668 | Lemma 2 for sbgoldbalt 41669: If an even number greater than 4 is the sum of two primes, the primes must be odd, i.e. not 2. (Contributed by AV, 22-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even Odd Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbalt 41669* | An alternate (related to the original) formulation of the binary Goldbach conjecture: Every even integer greater than 2 can be expressed as the sum of two primes. (Contributed by AV, 22-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even GoldbachEven Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbb 41670* | If the strong binary Goldbach conjecture is valid, the binary Goldbach conjecture is valid. (Contributed by AV, 23-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even GoldbachEven Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sgoldbeven3prm 41671* | If the binary Goldbach conjecture is valid, then an even integer greater than 5 can be expressed as the sum of three primes: Since is even iff is even, there would be primes and with , and therefore . (Contributed by AV, 24-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even GoldbachEven Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbm 41672* | If the strong binary Goldbach conjecture is valid, the modern version of the original formulation of the Goldbach conjecture also holds: Every integer greater than 5 can be expressed as the sum of three primes. (Contributed by AV, 24-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mogoldbb 41673* | If the modern version of the original formulation of the Goldbach conjecture is valid, the (weak) binary Goldbach conjecture also holds. (Contributed by AV, 26-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbmb 41674* | The strong binary Goldbach conjecture and the modern version of the original formulation of the Goldbach conjecture are equivalent. (Contributed by AV, 26-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbo 41675* | If the strong binary Goldbach conjecture is valid, the original formulation of the Goldbach conjecture also holds: Every integer greater than 2 can be expressed as the sum of three "primes" with regarding 1 to be a prime (as Goldbach did). Original text: "Es scheint wenigstens, dass eine jede Zahl, die groesser ist als 2, ein aggregatum trium numerorum primorum sey." (Goldbach, 1742). (Contributed by AV, 25-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnsum3primes4 41676* | 4 is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnsum4primes4 41677* | 4 is the sum of at most 4 (actually 2) primes. (Contributed by AV, 23-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnsum3primesprm 41678* | Every prime is "the sum of at most 3" (actually one - the prime itself) primes. (Contributed by AV, 2-Aug-2020.) (Proof shortened by AV, 17-Apr-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnsum4primesprm 41679* | Every prime is "the sum of at most 4" (actually one - the prime itself) primes. (Contributed by AV, 23-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnsum3primesgbe 41680* | Any even Goldbach number is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnsum4primesgbe 41681* | Any even Goldbach number is the sum of at most 4 (actually 2) primes. (Contributed by AV, 23-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnsum3primesle9 41682* | Every integer greater than 1 and less than or equal to 8 is the sum of at most 3 primes. (Contributed by AV, 2-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnsum4primesle9 41683* | Every integer greater than 1 and less than or equal to 8 is the sum of at most 4 primes. (Contributed by AV, 24-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnsum4primesodd 41684* | If the (weak) ternary Goldbach conjecture is valid, then every odd integer greater than 5 is the sum of 3 primes. (Contributed by AV, 2-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd GoldbachOddW Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnsum4primesoddALTV 41685* | If the (strong) ternary Goldbach conjecture is valid, then every odd integer greater than 7 is the sum of 3 primes. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd GoldbachOdd Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | evengpop3 41686* | If the (weak) ternary Goldbach conjecture is valid, then every even integer greater than 8 is the sum of an odd Goldbach number and 3. (Contributed by AV, 24-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd GoldbachOddW Even GoldbachOddW | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | evengpoap3 41687* | If the (strong) ternary Goldbach conjecture is valid, then every even integer greater than 10 is the sum of an odd Goldbach number and 3. (Contributed by AV, 27-Jul-2020.) (Proof shortened by AV, 15-Sep-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd GoldbachOdd ; Even GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnsum4primeseven 41688* | If the (weak) ternary Goldbach conjecture is valid, then every even integer greater than 8 is the sum of 4 primes. (Contributed by AV, 25-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd GoldbachOddW Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnsum4primesevenALTV 41689* | If the (strong) ternary Goldbach conjecture is valid, then every even integer greater than 10 is the sum of 4 primes. (Contributed by AV, 27-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd GoldbachOdd ; Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wtgoldbnnsum4prm 41690* | If the (weak) ternary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 4 primes, showing that Schnirelmann's constant would be less than or equal to 4. See corollary 1.1 in [Helfgott] p. 4. (Contributed by AV, 25-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd GoldbachOddW | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | stgoldbnnsum4prm 41691* | If the (strong) ternary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 4 primes. (Contributed by AV, 27-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | bgoldbnnsum3prm 41692* | If the binary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 3 primes, showing that Schnirelmann's constant would be equal to 3. (Contributed by AV, 2-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | bgoldbtbndlem1 41693 | Lemma 1 for bgoldbtbnd 41697: the odd numbers between 7 and 13 (exclusive) are odd Goldbach numbers. (Contributed by AV, 29-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Odd ; GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | bgoldbtbndlem2 41694* | Lemma 2 for bgoldbtbnd 41697. (Contributed by AV, 1-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
; ; Even GoldbachEven RePart ..^ ; Odd ..^ Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | bgoldbtbndlem3 41695* | Lemma 3 for bgoldbtbnd 41697. (Contributed by AV, 1-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
; ; Even GoldbachEven RePart ..^ ; Odd ..^ Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | bgoldbtbndlem4 41696* | Lemma 4 for bgoldbtbnd 41697. (Contributed by AV, 1-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
; ; Even GoldbachEven RePart ..^ ; ..^ Odd Odd Odd Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | bgoldbtbnd 41697* | If the binary Goldbach conjecture is valid up to an integer , and there is a series ("ladder") of primes with a difference of at most up to an integer , then the strong ternary Goldbach conjecture is valid up to , see section 1.2.2 in [Helfgott] p. 4 with N = 4 x 10^18, taken from [OeSilva], and M = 8.875 x 10^30. (Contributed by AV, 1-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
; ; Even GoldbachEven RePart ..^ ; Odd GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Axiom | ax-bgbltosilva 41698 | The binary Goldbach conjecture is valid for all even numbers less than or equal to 4x10^18, see section 2 in [OeSilva] p. 2042. Temporarily provided as "axiom". (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Even ;; GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Axiom | ax-tgoldbachgt 41699* | Temporary duplicate of tgoldbachgt 30741, provided as "axiom" as long as this theorem is in the mathbox of Thierry Arnoux: Odd integers greater than ;; have at least a representation as a sum of three odd primes. Final statement in section 7.4 of [Helfgott] p. 70 , expressed using the set of odd numbers which can be written as a sum of three odd primes. (Contributed by Thierry Arnoux, 22-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
;; | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | tgoldbachgtALTV 41700* | Variant of Thierry Arnoux's tgoldbachgt 30741 using the symbols Odd and GoldbachOdd: The ternary Goldbach conjecture is valid for large odd numbers (i.e. for all odd numbers greater than a fixed ). This is proven by Helfgott (see section 7.4 in [Helfgott] p. 70) for = 10^27. (Contributed by AV, 2-Aug-2020.) (Revised by AV, 15-Jan-2022.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
;; Odd GoldbachOdd |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |