P. 390 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38901-39000   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-odd 38901	Define the set of odd numbers. (Contributed by AV, 14-Jun-2020.)
|- Odd = { z e. ZZ | ( ( z + 1 ) / 2 ) e. ZZ }
Theorem	iseven 38902	The predicate "is an even number". An even number is an integer which is divisible by 2, i.e. the result of dividing the even integer by 2 is still an integer. (Contributed by AV, 14-Jun-2020.)
|- ( Z e. Even <-> ( Z e. ZZ /\ ( Z / 2 ) e. ZZ ) )
Theorem	isodd 38903	The predicate "is an odd number". An odd number is an integer which is not divisible by 2, i.e. the result of dividing the odd integer increased by 1 and then divided by 2 is still an integer. (Contributed by AV, 14-Jun-2020.)
|- ( Z e. Odd <-> ( Z e. ZZ /\ ( ( Z + 1 ) / 2 ) e. ZZ ) )
Theorem	evenz 38904	An even number is an integer. (Contributed by AV, 14-Jun-2020.)
|- ( Z e. Even -> Z e. ZZ )
Theorem	oddz 38905	An odd number is an integer. (Contributed by AV, 14-Jun-2020.)
|- ( Z e. Odd -> Z e. ZZ )
Theorem	evendiv2z 38906	The result of dividing an even number by 2 is an integer. (Contributed by AV, 15-Jun-2020.)
|- ( Z e. Even -> ( Z / 2 ) e. ZZ )
Theorem	oddp1div2z 38907	The result of dividing an odd number increased by 1 and then divided by 2 is an integer. (Contributed by AV, 15-Jun-2020.)
|- ( Z e. Odd -> ( ( Z + 1 ) / 2 ) e. ZZ )
Theorem	zob 38908	Alternate characterizations of an odd number. (Contributed by AV, 7-Jun-2020.)
|- ( N e. ZZ -> ( ( ( N + 1 ) / 2 ) e. ZZ <-> ( ( N - 1 ) / 2 ) e. ZZ ) )
Theorem	oddm1div2z 38909	The result of dividing an odd number decreased by 1 and then divided by 2 is an integer. (Contributed by AV, 15-Jun-2020.)
|- ( Z e. Odd -> ( ( Z - 1 ) / 2 ) e. ZZ )
Theorem	isodd2 38910	The predicate "is an odd number". An odd number is an integer which is not divisible by 2, i.e. the result of dividing the odd number decreased by 1 and then divided by 2 is still an integer. (Contributed by AV, 15-Jun-2020.)
|- ( Z e. Odd <-> ( Z e. ZZ /\ ( ( Z - 1 ) / 2 ) e. ZZ ) )
Theorem	dfodd2 38911	Alternate definition for odd numbers. (Contributed by AV, 15-Jun-2020.)
|- Odd = { z e. ZZ | ( ( z - 1 ) / 2 ) e. ZZ }
Theorem	dfodd6 38912*	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
|- Odd = { z e. ZZ | E. i e. ZZ z = ( ( 2 x. i ) + 1 ) }
Theorem	dfeven4 38913*	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
|- Even = { z e. ZZ | E. i e. ZZ z = ( 2 x. i ) }
Theorem	evenm1odd 38914	The predecessor of an even number is odd. (Contributed by AV, 16-Jun-2020.)
|- ( Z e. Even -> ( Z - 1 ) e. Odd )
Theorem	evenp1odd 38915	The successor of an even number is odd. (Contributed by AV, 16-Jun-2020.)
|- ( Z e. Even -> ( Z + 1 ) e. Odd )
Theorem	oddp1eveni 38916	The successor of an odd number is even. (Contributed by AV, 16-Jun-2020.)
|- ( Z e. Odd -> ( Z + 1 ) e. Even )
Theorem	oddm1eveni 38917	The predecessor of an odd number is even. (Contributed by AV, 6-Jul-2020.)
|- ( Z e. Odd -> ( Z - 1 ) e. Even )
Theorem	evennodd 38918	An even number is not an odd number. (Contributed by AV, 16-Jun-2020.)
|- ( Z e. Even -> -. Z e. Odd )
Theorem	oddneven 38919	An odd number is not an even number. (Contributed by AV, 16-Jun-2020.)
|- ( Z e. Odd -> -. Z e. Even )
Theorem	enege 38920	The negative of an even number is even. (Contributed by AV, 20-Jun-2020.)
|- ( A e. Even -> -u A e. Even )
Theorem	onego 38921	The negative of an odd number is odd. (Contributed by AV, 20-Jun-2020.)
|- ( A e. Odd -> -u A e. Odd )
Theorem	m1expevenALTV 38922	Exponentiation of -1 by an even power. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 6-Jul-2020.)
|- ( N e. Even -> ( -u 1 ^ N ) = 1 )
Theorem	m1expoddALTV 38923	Exponentiation of -1 by an odd power. (Contributed by AV, 6-Jul-2020.)
|- ( N e. Odd -> ( -u 1 ^ N ) = -u 1 )
21.33.4.2  Alternate definitions using the "divides" relation
Theorem	dfeven2 38924	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
|- Even = { z e. ZZ | 2 || z }
Theorem	dfodd3 38925	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
|- Odd = { z e. ZZ | -. 2 || z }
Theorem	iseven2 38926	The predicate "is an even number". An even number is an integer which is divisible by 2. (Contributed by AV, 18-Jun-2020.)
|- ( Z e. Even <-> ( Z e. ZZ /\ 2 || Z ) )
Theorem	isodd3 38927	The predicate "is an odd number". An odd number is an integer which is not divisible by 2. (Contributed by AV, 18-Jun-2020.)
|- ( Z e. Odd <-> ( Z e. ZZ /\ -. 2 || Z ) )
Theorem	2dvdseven 38928	2 divides an even number. (Contributed by AV, 18-Jun-2020.)
|- ( Z e. Even -> 2 || Z )
Theorem	2ndvdsodd 38929	2 does not divide an odd number. (Contributed by AV, 18-Jun-2020.)
|- ( Z e. Odd -> -. 2 || Z )
Theorem	2dvdsoddp1 38930	2 divides an odd number increased by 1. (Contributed by AV, 18-Jun-2020.)
|- ( Z e. Odd -> 2 || ( Z + 1 ) )
Theorem	2dvdsoddm1 38931	2 divides an odd number decreased by 1. (Contributed by AV, 18-Jun-2020.)
|- ( Z e. Odd -> 2 || ( Z - 1 ) )
21.33.4.3  Alternate definitions using the "modulo" operation
Theorem	dfeven3 38932	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
|- Even = { z e. ZZ | ( z mod 2 ) = 0 }
Theorem	dfodd4 38933	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
|- Odd = { z e. ZZ | ( z mod 2 ) = 1 }
Theorem	dfodd5 38934	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
|- Odd = { z e. ZZ | ( z mod 2 ) =/= 0 }
Theorem	zefldiv2ALTV 38935	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.)
|- ( N e. Even -> ( |_ ` ( N / 2 ) ) = ( N / 2 ) )
Theorem	zofldiv2ALTV 38936	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.)
|- ( N e. Odd -> ( |_ ` ( N / 2 ) ) = ( ( N - 1 ) / 2 ) )
Theorem	oddflALTV 38937	Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 18-Jun-2020.)
|- ( K e. Odd -> K = ( ( 2 x. ( |_ ` ( K / 2 ) ) ) + 1 ) )
21.33.4.4  Alternate definitions using the "gcd" operation
Theorem	gcdzeq 38938	A positive integer A is equal to its gcd with an integer B if and only if A divides B. Generalization of gcdeq 14599. (Contributed by AV, 1-Jul-2020.)
|- ( ( A e. NN /\ B e. ZZ ) -> ( ( A gcd B ) = A <-> A || B ) )
Theorem	iseven5 38939	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 38940	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 38941	Alternate definition for even numbers. (Contributed by AV, 1-Jul-2020.)
|- Even = { z e. ZZ | ( 2 gcd z ) = 2 }
Theorem	dfodd7 38942	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 38943	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 38944	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 38945	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 38946	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 38947	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 38948*	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 38949	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 38950	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 38951	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 38952	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 38953	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 38954	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 38955	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 38956	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 38957	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 38958	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 38959	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 38960	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 38961	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 38962	0 is an even number. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 17-Jun-2020.)
|- 0 e. Even
Theorem	0noddALTV 38963	0 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 17-Jun-2020.)
|- 0 e/ Odd
Theorem	1oddALTV 38964	1 is an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.)
|- 1 e. Odd
Theorem	1nevenALTV 38965	1 is not an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.)
|- 1 e/ Even
Theorem	2evenALTV 38966	2 is an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.)
|- 2 e. Even
Theorem	2noddALTV 38967	2 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.)
|- 2 e/ Odd
Theorem	nn0o1gt2ALTV 38968	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 38969	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 38970	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 38971	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 38972*	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 38973*	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 38974	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 38975	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 38976	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 38977	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 38978	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 38979	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 38980	3 is an odd number. (Contributed by AV, 20-Jul-2020.)
|- 3 e. Odd
Theorem	4even 38981	4 is an even number. (Contributed by AV, 23-Jul-2020.)
|- 4 e. Even
Theorem	5odd 38982	5 is an odd number. (Contributed by AV, 23-Jul-2020.)
|- 5 e. Odd
Theorem	6even 38983	6 is an even number. (Contributed by AV, 20-Jul-2020.)
|- 6 e. Even
Theorem	7odd 38984	7 is an odd number. (Contributed by AV, 20-Jul-2020.)
|- 7 e. Odd
Theorem	8even 38985	8 is an even number. (Contributed by AV, 23-Jul-2020.)
|- 8 e. Even
Theorem	oddprmuzge3 38986	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 38987	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 38988	Lemma for perfectALTV 38990. (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 38989	Lemma for perfectALTV 38990. (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 38990*	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 38994), "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 39027 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 38995, is the basis for "the other formulation", to formulate the weak ternary Goldbach conjecture. Alternatively, df-gboa 38996 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 39017, 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 39050, ax-hgprmladder 39052 and ax-tgoldbachgt 39055.
Syntax	cgbe 38991	Extend the definition of a class to include the set of even numbers which have a Goldbach partition.
class GoldbachEven
Syntax	cgbo 38992	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 38993	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 38994*	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 38995*	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 38996*	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 38997*	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 38998*	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 38999*	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 39000	An even Goldbach number is even. (Contributed by AV, 25-Jul-2020.)
|- ( Z e. GoldbachEven -> Z e. Even )