P. 387 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38601-38700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iseven5 38601	The predicate "is an even number". An even number and 2 have 2 as greatest common divisor. (Contributed by AV, 1-Jul-2020.)
|- ( Z e. Even <-> ( Z e. ZZ /\ ( 2 gcd Z ) = 2 ) )
Theorem	isodd7 38602	The predicate "is an odd number". An odd number and 2 have 1 as greatest common divisor. (Contributed by AV, 1-Jul-2020.)
|- ( Z e. Odd <-> ( Z e. ZZ /\ ( 2 gcd Z ) = 1 ) )
Theorem	dfeven5 38603	Alternate definition for even numbers. (Contributed by AV, 1-Jul-2020.)
|- Even = { z e. ZZ | ( 2 gcd z ) = 2 }
Theorem	dfodd7 38604	Alternate definition for odd numbers. (Contributed by AV, 1-Jul-2020.)
|- Odd = { z e. ZZ | ( 2 gcd z ) = 1 }
21.33.4.5  Theorems of part 5 revised
Theorem	zneoALTV 38605	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.)
|- ( ( A e. Even /\ B e. Odd ) -> A =/= B )
Theorem	zeoALTV 38606	An integer is even or odd. (Contributed by NM, 1-Jan-2006.) (Revised by AV, 16-Jun-2020.)
|- ( Z e. ZZ -> ( Z e. Even \/ Z e. Odd ) )
Theorem	zeo2ALTV 38607	An integer is even or odd but not both. (Contributed by Mario Carneiro, 12-Sep-2015.) (Revised by AV, 16-Jun-2020.)
|- ( Z e. ZZ -> ( Z e. Even <-> -. Z e. Odd ) )
Theorem	nneoALTV 38608	A positive integer is even or odd but not both. (Contributed by NM, 1-Jan-2006.) (Revised by AV, 19-Jun-2020.)
|- ( N e. NN -> ( N e. Even <-> -. N e. Odd ) )
Theorem	nneoiALTV 38609	A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001.) (Revised by AV, 19-Jun-2020.)
|- N e. NN   =>    |- ( N e. Even <-> -. N e. Odd )
21.33.4.6  Theorems of part 6 revised
Theorem	odd2np1ALTV 38610*	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.)
|- ( N e. ZZ -> ( N e. Odd <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N ) )
Theorem	oddm1evenALTV 38611	An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.)
|- ( N e. ZZ -> ( N e. Odd <-> ( N - 1 ) e. Even ) )
Theorem	oddp1evenALTV 38612	An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.)
|- ( N e. ZZ -> ( N e. Odd <-> ( N + 1 ) e. Even ) )
Theorem	oexpnegALTV 38613	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.)
|- ( ( A e. CC /\ N e. NN /\ N e. Odd ) -> ( -u A ^ N ) = -u ( A ^ N ) )
Theorem	oexpnegnz 38614	The exponential of the negative of a number not being 0, when the exponent is odd. (Contributed by AV, 19-Jun-2020.)
|- ( ( A e. CC /\ A =/= 0 /\ N e. Odd ) -> ( -u A ^ N ) = -u ( A ^ N ) )
Theorem	bits0ALTV 38615	Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.)
|- ( N e. ZZ -> ( 0 e. (bits ` N ) <-> N e. Odd ) )
Theorem	bits0eALTV 38616	The zeroth bit of an even number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.)
|- ( N e. Even -> -. 0 e. (bits ` N ) )
Theorem	bits0oALTV 38617	The zeroth bit of an odd number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.)
|- ( N e. Odd -> 0 e. (bits ` N ) )
Theorem	divgcdoddALTV 38618	Either A / ( A gcd B ) is odd or B / ( A gcd B ) is odd. (Contributed by Scott Fenton, 19-Apr-2014.) (Revised by AV, 21-Jun-2020.)
|- ( ( A e. NN /\ B e. NN ) -> ( ( A / ( A gcd B ) ) e. Odd \/ ( B / ( A gcd B ) ) e. Odd ) )
Theorem	opoeALTV 38619	The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by AV, 20-Jun-2020.)
|- ( ( A e. Odd /\ B e. Odd ) -> ( A + B ) e. Even )
Theorem	opeoALTV 38620	The sum of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by AV, 20-Jun-2020.)
|- ( ( A e. Odd /\ B e. Even ) -> ( A + B ) e. Odd )
Theorem	omoeALTV 38621	The difference of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by AV, 20-Jun-2020.)
|- ( ( A e. Odd /\ B e. Odd ) -> ( A - B ) e. Even )
Theorem	omeoALTV 38622	The difference of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by AV, 20-Jun-2020.)
|- ( ( A e. Odd /\ B e. Even ) -> ( A - B ) e. Odd )
Theorem	oddprmALTV 38623	A prime not equal to 2 is odd. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by AV, 21-Jun-2020.)
|- ( N e. ( Prime \ { 2 } ) -> N e. Odd )
21.33.4.7  Theorems of AV's mathbox revised
Theorem	0evenALTV 38624	0 is an even number. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 17-Jun-2020.)
|- 0 e. Even
Theorem	0noddALTV 38625	0 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 17-Jun-2020.)
|- 0 e/ Odd
Theorem	1oddALTV 38626	1 is an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.)
|- 1 e. Odd
Theorem	1nevenALTV 38627	1 is not an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.)
|- 1 e/ Even
Theorem	2evenALTV 38628	2 is an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.)
|- 2 e. Even
Theorem	2noddALTV 38629	2 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.)
|- 2 e/ Odd
Theorem	nn0o1gt2ALTV 38630	An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 21-Jun-2020.)
|- ( ( N e. NN0 /\ N e. Odd ) -> ( N = 1 \/ 2 < N ) )
Theorem	nnoALTV 38631	An alternate characterization of an odd number greater than 1. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 21-Jun-2020.)
|- ( ( N e. ( ZZ>= ` 2 ) /\ N e. Odd ) -> ( ( N - 1 ) / 2 ) e. NN )
Theorem	nn0oALTV 38632	An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020.) (Revised by AV, 21-Jun-2020.)
|- ( ( N e. NN0 /\ N e. Odd ) -> ( ( N - 1 ) / 2 ) e. NN0 )
Theorem	nn0e 38633	An alternate characterization of an even nonnegative integer. (Contributed by AV, 22-Jun-2020.)
|- ( ( N e. NN0 /\ N e. Even ) -> ( N / 2 ) e. NN0 )
Theorem	nn0onn0exALTV 38634*	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.)
|- ( ( N e. NN0 /\ N e. Odd ) -> E. m e. NN0 N = ( ( 2 x. m ) + 1 ) )
Theorem	nn0enn0exALTV 38635*	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.)
|- ( ( N e. NN0 /\ N e. Even ) -> E. m e. NN0 N = ( 2 x. m ) )
Theorem	nnpw2evenALTV 38636	2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 20-Jun-2020.)
|- ( N e. NN -> ( 2 ^ N ) e. Even )
21.33.4.8  Additional theorems
Theorem	epoo 38637	The sum of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.)
|- ( ( A e. Even /\ B e. Odd ) -> ( A + B ) e. Odd )
Theorem	emoo 38638	The difference of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.)
|- ( ( A e. Even /\ B e. Odd ) -> ( A - B ) e. Odd )
Theorem	epee 38639	The sum of two even numbers is even. (Contributed by AV, 21-Jul-2020.)
|- ( ( A e. Even /\ B e. Even ) -> ( A + B ) e. Even )
Theorem	emee 38640	The difference of two even numbers is even. (Contributed by AV, 21-Jul-2020.)
|- ( ( A e. Even /\ B e. Even ) -> ( A - B ) e. Even )
Theorem	evensumeven 38641	If a summand is even, the other summand is even iff the sum is even. (Contributed by AV, 21-Jul-2020.)
|- ( ( A e. ZZ /\ B e. Even ) -> ( A e. Even <-> ( A + B ) e. Even ) )
Theorem	3odd 38642	3 is an odd number. (Contributed by AV, 20-Jul-2020.)
|- 3 e. Odd
Theorem	4even 38643	4 is an even number. (Contributed by AV, 23-Jul-2020.)
|- 4 e. Even
Theorem	5odd 38644	5 is an odd number. (Contributed by AV, 23-Jul-2020.)
|- 5 e. Odd
Theorem	6even 38645	6 is an even number. (Contributed by AV, 20-Jul-2020.)
|- 6 e. Even
Theorem	7odd 38646	7 is an odd number. (Contributed by AV, 20-Jul-2020.)
|- 7 e. Odd
Theorem	8even 38647	8 is an even number. (Contributed by AV, 23-Jul-2020.)
|- 8 e. Even
Theorem	oddprmuzge3 38648	A prime number which is odd is an integer greater than or equal to 3. (Contributed by AV, 20-Jul-2020.)
|- ( ( P e. Prime /\ P e. Odd ) -> P e. ( ZZ>= ` 3 ) )
Theorem	evenprm2 38649	A prime number is even iff it is 2. (Contributed by AV, 21-Jul-2020.)
|- ( P e. Prime -> ( P e. Even <-> P = 2 ) )
21.33.4.9  Perfect Number Theorem (revised)
Theorem	perfectALTVlem1 38650	Lemma for perfectALTV 38652. (Contributed by Mario Carneiro, 7-Jun-2016.) (Revised by AV, 1-Jul-2020.)
|- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> B e. Odd )   &    |- ( ph -> ( 1 sigma ( ( 2 ^ A ) x. B ) ) = ( 2 x. ( ( 2 ^ A ) x. B ) ) )   =>    |- ( ph -> ( ( 2 ^ ( A + 1 ) ) e. NN /\ ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN /\ ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN ) )
Theorem	perfectALTVlem2 38651	Lemma for perfectALTV 38652. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by AV, 1-Jul-2020.)
|- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> B e. Odd )   &    |- ( ph -> ( 1 sigma ( ( 2 ^ A ) x. B ) ) = ( 2 x. ( ( 2 ^ A ) x. B ) ) )   =>    |- ( ph -> ( B e. Prime /\ B = ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
Theorem	perfectALTV 38652*	The Euclid-Euler theorem, or Perfect Number theorem. A positive even integer N is a perfect number (that is, its divisor sum is 2 N) if and only if it is of the form 2 ^ ( p - 1 ) x. ( 2 ^ p - 1 ), where 2 ^ p - 1 is prime (a Mersenne prime). (It follows from this that p 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.)
|- ( ( N e. NN /\ N e. Even ) -> ( ( 1 sigma N ) = ( 2 x. N ) <-> E. p e. ZZ ( ( ( 2 ^ p ) - 1 ) e. Prime /\ N = ( ( 2 ^ ( p - 1 ) ) x. ( ( 2 ^ p ) - 1 ) ) ) ) )
21.33.4.10  Goldbach's conjectures 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, because there are are a strong and a weak version of the ternary Goldbach conjecture. The term Goldbach partion is used for a sum of two resp. three (odd) primes resulting in an even resp. odd number without further specialization. Using the definition of a Goldbach number, which is "a positive even integer that can be expressed as the sum of two odd primes." (see df-gbe 38656), "another form of the statement of Goldbach's conjecture is that all even integers greater than 4 are Goldbach numbers.". 4 is not a Goldbach number, but it is the sum of two primes (2 and 2) nevertheless. sgoldbalt 38689 shows that both forms are equivalent. Hint (see Wikipedia, ("Goldbach's weak conjecture", 26-Jul-2020, https://en.wikipedia.org/wiki/Goldbach's_weak_conjecture): "Some state the [weak] conjecture as 'Every odd number greater than 7 can be expressed as the sum of three odd primes.' This version excludes 7 = 2+2+3 because this requires the even prime 2. On odd numbers larger than 7 it is slightly stronger as it also excludes sums like 17 = 2+2+13, which are allowed in the other formulation. Helfgott's proof [see below] covers both versions of the conjecture. Like the other formulation, this one also immediately follows from Goldbach's strong conjecture." Our definition of "odd Goldbach Numbers", see df-gbo 38657, is the basis for "the other formulation", to formulate the weak ternary Goldbach conjecture. Alternatively, df-gboa 38658 provides a definition allowing for stating the strong ternaty Goldbach conjecture. In contrast to the two versions of the binary Goldbach conjecture, the two versions of the ternary Goldbach conjecture are different not only for small numbers, but the strong version excludes cases like a=2+2+b in general, e.g. 23=2+2+19. Therefore, it seems to be more difficult to prove the strong ternary Goldbach conjecture than the weak version, because there are fewer possible partitions available. Although the binary Goldbach conjecture is not proven yet, the ternary Goldbach conjecture seems to be proven by Harald Helfgott in 2014 (the weak as well as the strong version, see Main theorem in [Helfgott] p. 2. It would be great if this proof can be formalized with Metamath (although it is not in the Metamath 100 list), providing the still missing official acceptance (usually obtained by a publication in a peer-reviewed journal). This section should be a starting point for this. The main problem will be to provide means to express the results from checking "small" numbers (performed with a computer): numbers up to about 4 x 10^18 for the strong Goldbach conjecture (see result of [OeSilva] p. ?) resp. about 9 x 10^30 for the weak Goldbach conjecture (see section 1.2.2 in [Helfgott] p. 4). Maybe each of the results must be provided as theorem, like 6gbe 38679, which would be quite a lot... As proposed in the Google group discussion https://groups.google.com/g/metamath/c/DOXS4pg0h8w/m/O3oBPuzhBAAJ , this problem could be solved by using a reflective verifier or adding a concept of verification certificates that can be added into the metamath databases as a reference. To sidestep the computation problem for now, the corresponding theorems are temporarily provided as axioms, see ax-bgbltosilva 38712, ax-hgprmladder 38714 and ax-tgoldbachgt 38717.
Syntax	cgbe 38653	Extend the definition of a class to include the set of even numbers which have a Goldbach partition.
class GoldbachEven
Syntax	cgbo 38654	Extend the definition of a class to include the set of odd numbers which can be written as sum of three primes.
class GoldbachOdd
Syntax	cgboa 38655	Extend the definition of a class to include the set of odd numbers which can be written as sum of three odd primes.
class GoldbachOddALTV
Definition	df-gbe 38656*	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 A. n e. Even ( 4 < n -> n e. GoldbachEven ). (Contributed by AV, 14-Jun-2020.)
|- GoldbachEven = { z e. Even | E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ z = ( p + q ) ) }
Definition	df-gbo 38657*	Define the set of 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 A. m e. Odd ( 5 < m -> m e. GoldbachOdd ). (Contributed by AV, 14-Jun-2020.)
|- GoldbachOdd = { z e. Odd | E. p e. Prime E. q e. Prime E. r e. Prime z = ( ( p + q ) + r ) }
Definition	df-gboa 38658*	Define the set of 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 A. m e. Odd ( 7 < m -> m e. GoldbachOddALTV ). (Contributed by AV, 26-Jul-2020.)
|- GoldbachOddALTV = { z e. Odd | E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ z = ( ( p + q ) + r ) ) }
Theorem	isgbe 38659*	The predicate "is an even Goldbach number". An even Goldbach number is an even number having a Goldbach partition, i.e. which can be written as sum of two odd primes. (Contributed by AV, 20-Jul-2020.)
|- ( Z e. GoldbachEven <-> ( Z e. Even /\ E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ Z = ( p + q ) ) ) )
Theorem	isgbo 38660*	The predicate "is an odd Goldbach number". An odd Goldbach number is an odd number integer having a Goldbach partition, i.e. which which can be written as sum of three primes. (Contributed by AV, 20-Jul-2020.)
|- ( Z e. GoldbachOdd <-> ( Z e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime Z = ( ( p + q ) + r ) ) )
Theorem	isgboa 38661*	The predicate "is an odd Goldbach number". An odd Goldbach number is an odd number integer having a Goldbach partition, i.e. which can be written as sum of three odd primes. (Contributed by AV, 26-Jul-2020.)
|- ( Z e. GoldbachOddALTV <-> ( Z e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ Z = ( ( p + q ) + r ) ) ) )
Theorem	gbeeven 38662	An even Goldbach number is even. (Contributed by AV, 25-Jul-2020.)
|- ( Z e. GoldbachEven -> Z e. Even )
Theorem	gboodd 38663	An odd Goldbach number is odd. (Contributed by AV, 25-Jul-2020.)
|- ( Z e. GoldbachOdd -> Z e. Odd )
Theorem	gboagbo 38664	An odd Goldbach number (strong version) is an odd Goldbach number (weak version). (Contributed by AV, 26-Jul-2020.)
|- ( Z e. GoldbachOddALTV -> Z e. GoldbachOdd )
Theorem	gboaodd 38665	An odd Goldbach number is odd. (Contributed by AV, 26-Jul-2020.)
|- ( Z e. GoldbachOddALTV -> Z e. Odd )
Theorem	gbepos 38666	Any even Goldbach number is positive. (Contributed by AV, 20-Jul-2020.)
|- ( Z e. GoldbachEven -> Z e. NN )
Theorem	gbopos 38667	Any odd Goldbach number is positive. (Contributed by AV, 20-Jul-2020.)
|- ( Z e. GoldbachOdd -> Z e. NN )
Theorem	gboapos 38668	Any odd Goldbach number is positive. (Contributed by AV, 26-Jul-2020.)
|- ( Z e. GoldbachOddALTV -> Z e. NN )
Theorem	gbegt5 38669	Any even Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.)
|- ( Z e. GoldbachEven -> 5 < Z )
Theorem	gbogt5 38670	Any odd Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.)
|- ( Z e. GoldbachOdd -> 5 < Z )
Theorem	gboge7 38671	Any odd Goldbach number is greater than or equal to 7. Because of 7gbo 38680, this bound is strict. (Contributed by AV, 20-Jul-2020.)
|- ( Z e. GoldbachOdd -> 7 <_ Z )
Theorem	gboage9 38672	Any odd Goldbach number (strong version) is greater than or equal to 9. Because of 9gboa 38682, this bound is strict. (Contributed by AV, 26-Jul-2020.)
|- ( Z e. GoldbachOddALTV -> 9 <_ Z )
Theorem	gbege6 38673	Any even Goldbach number is greater than or equal to 6. Because of 6gbe 38679, this bound is strict. (Contributed by AV, 20-Jul-2020.)
|- ( Z e. GoldbachEven -> 6 <_ Z )
Theorem	gbpart6 38674	The Goldbach partition of 6. (Contributed by AV, 20-Jul-2020.)
|- 6 = ( 3 + 3 )
Theorem	gbpart7 38675	The (weak) Goldbach partition of 7. (Contributed by AV, 20-Jul-2020.)
|- 7 = ( ( 2 + 2 ) + 3 )
Theorem	gbpart8 38676	The Goldbach partition of 8. (Contributed by AV, 20-Jul-2020.)
|- 8 = ( 3 + 5 )
Theorem	gbpart9 38677	The (strong) Goldbach partition of 9. (Contributed by AV, 26-Jul-2020.)
|- 9 = ( ( 3 + 3 ) + 3 )
Theorem	gbpart11 38678	The (strong) Goldbach partition of 11. (Contributed by AV, 29-Jul-2020.)
|- ; 1 1 = ( ( 3 + 3 ) + 5 )
Theorem	6gbe 38679	6 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.)
|- 6 e. GoldbachEven
Theorem	7gbo 38680	7 is an odd Goldbach number. (Contributed by AV, 20-Jul-2020.)
|- 7 e. GoldbachOdd
Theorem	8gbe 38681	8 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.)
|- 8 e. GoldbachEven
Theorem	9gboa 38682	9 is an odd Goldbach number. (Contributed by AV, 26-Jul-2020.)
|- 9 e. GoldbachOddALTV
Theorem	11gboa 38683	11 is an odd Goldbach number. (Contributed by AV, 29-Jul-2020.)
|- ; 1 1 e. GoldbachOddALTV
Theorem	stgoldbwt 38684	If the strong ternary Goldbach conjecture is valid, then the weak ternary Goldbach conjecture holds, too. (Contributed by AV, 27-Jul-2020.)
|- ( A. n e. Odd ( 7 < n -> n e. GoldbachOddALTV ) -> A. n e. Odd ( 5 < n -> n e. GoldbachOdd ) )
Theorem	bgoldbwt 38685*	If the binary Goldbach conjecture is valid, then the (weak) ternary Goldbach conjecture holds, too. (Contributed by AV, 20-Jul-2020.)
|- ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> A. m e. Odd ( 5 < m -> m e. GoldbachOdd ) )
Theorem	bgoldbst 38686*	If the binary Goldbach conjecture is valid, then the (strong) ternary Goldbach conjecture holds, too. (Contributed by AV, 26-Jul-2020.)
|- ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> A. m e. Odd ( 7 < m -> m e. GoldbachOddALTV ) )
Theorem	sgoldbaltlem1 38687	Lemma 1 for sgoldbalt 38689: 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.)
|- ( ( P e. Prime /\ Q e. Prime ) -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> Q e. Odd ) )
Theorem	sgoldbaltlem2 38688	Lemma 2 for sgoldbalt 38689: 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.)
|- ( ( P e. Prime /\ Q e. Prime ) -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> ( P e. Odd /\ Q e. Odd ) ) )
Theorem	sgoldbalt 38689*	An alternate (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.)
|- ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) <-> A. n e. Even ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) )
Theorem	nnsum3primes4 38690*	4 is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020.)
|- E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) )
Theorem	nnsum4primes4 38691*	4 is the sum of at most 4 (actually 2) primes. (Contributed by AV, 23-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.)
|- E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) )
Theorem	nnsum3primesprm 38692*	Every prime is "the sum of at most 3" (actually one - the prime itself) primes. (Contributed by AV, 2-Aug-2020.)
|- ( P e. Prime -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ P = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
Theorem	nnsum4primesprm 38693*	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.)
|- ( P e. Prime -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ P = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
Theorem	nnsum3primesgbe 38694*	Any even Goldbach number is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020.)
|- ( N e. GoldbachEven -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
Theorem	nnsum4primesgbe 38695*	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.)
|- ( N e. GoldbachEven -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
Theorem	nnsum3primesle9 38696*	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.)
|- ( ( N e. ( ZZ>= ` 2 ) /\ N <_ 8 ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
Theorem	nnsum4primesle9 38697*	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.)
|- ( ( N e. ( ZZ>= ` 2 ) /\ N <_ 8 ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
Theorem	nnsum4primesodd 38698*	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.)
|- ( A. m e. Odd ( 5 < m -> m e. GoldbachOdd ) -> ( ( N e. ( ZZ>= ` 6 ) /\ N e. Odd ) -> E. f e. ( Prime ^m ( 1 ... 3 ) ) N = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )
Theorem	nnsum4primesoddALTV 38699*	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.)
|- ( A. m e. Odd ( 7 < m -> m e. GoldbachOddALTV ) -> ( ( N e. ( ZZ>= ` 8 ) /\ N e. Odd ) -> E. f e. ( Prime ^m ( 1 ... 3 ) ) N = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )
Theorem	evengpop3 38700*	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.)
|- ( A. m e. Odd ( 5 < m -> m e. GoldbachOdd ) -> ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) -> E. o e. GoldbachOdd N = ( o + 3 ) ) )