P. 483 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

21.48.13.8  Additional theorems

Theorem

epoo 48201

The sum of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.)

⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → (𝐴 + 𝐵) ∈ Odd )

Theorem

emoo 48202

The difference of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.)

⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → (𝐴 − 𝐵) ∈ Odd )

Theorem

epee 48203

The sum of two even numbers is even. (Contributed by AV, 21-Jul-2020.)

⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → (𝐴 + 𝐵) ∈ Even )

Theorem

emee 48204

The difference of two even numbers is even. (Contributed by AV, 21-Jul-2020.)

⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → (𝐴 − 𝐵) ∈ Even )

Theorem

evensumeven 48205

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 48206

3 is an odd number. (Contributed by AV, 20-Jul-2020.)

⊢ 3 ∈ Odd

Theorem

4even 48207

4 is an even number. (Contributed by AV, 23-Jul-2020.)

⊢ 4 ∈ Even

Theorem

5odd 48208

5 is an odd number. (Contributed by AV, 23-Jul-2020.)

⊢ 5 ∈ Odd

Theorem

6even 48209

6 is an even number. (Contributed by AV, 20-Jul-2020.)

⊢ 6 ∈ Even

Theorem

7odd 48210

7 is an odd number. (Contributed by AV, 20-Jul-2020.)

⊢ 7 ∈ Odd

Theorem

8even 48211

8 is an even number. (Contributed by AV, 23-Jul-2020.)

⊢ 8 ∈ Even

Theorem

evenprm2 48212

A prime number is even iff it is 2. (Contributed by AV, 21-Jul-2020.)

⊢ (𝑃 ∈ ℙ → (𝑃 ∈ Even ↔ 𝑃 = 2))

Theorem

oddprmne2 48213

Every prime number not being 2 is an odd prime number. (Contributed by AV, 21-Aug-2021.)

⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ∈ Odd ) ↔ 𝑃 ∈ (ℙ ∖ {2}))

Theorem

oddprmuzge3 48214

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 48215

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 48216

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 48217

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 48218*

Lemma for mogoldbb 48283. (Contributed by AV, 26-Dec-2021.)

⊢ (((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ) ∧ 𝑁 ∈ Even ∧ (𝑁 + 2) = ((𝑃 + 𝑄) + 𝑅)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑁 = (𝑝 + 𝑞))

21.48.13.9  Perfect Number Theorem (revised)

Theorem

perfectALTVlem1 48219

Lemma for perfectALTV 48221. (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 48220

Lemma for perfectALTV 48221. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by AV, 1-Jul-2020.)

⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ Odd )    &   ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵)))    ⇒   ⊢ (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1)))

Theorem

perfectALTV 48221*

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)))))

21.48.14  Number theory (extension 2)

21.48.14.1  Fermat pseudoprimes

"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 16752].

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 48241] 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 48241, 29-May-2023.

Syntax

cfppr 48222

Extend class notation with the Fermat pseudoprimes.

class FPPr

Definition

df-fppr 48223*

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 48224*

The set of Fermat pseudoprimes to the base 𝑁. (Contributed by AV, 29-May-2023.)

⊢ (𝑁 ∈ ℕ → ( FPPr ‘𝑁) = {𝑥 ∈ (ℤ_≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑁↑(𝑥 − 1)) − 1))})

Theorem

fpprmod 48225*

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 48226

A Fermat pseudoprime to the base 𝑁. (Contributed by AV, 30-May-2023.)

⊢ (𝑁 ∈ ℕ → (𝑋 ∈ ( FPPr ‘𝑁) ↔ (𝑋 ∈ (ℤ_≥‘4) ∧ 𝑋 ∉ ℙ ∧ ((𝑁↑(𝑋 − 1)) mod 𝑋) = 1)))

Theorem

fpprbasnn 48227

The base of a Fermat pseudoprime is a positive integer. (Contributed by AV, 30-May-2023.)

⊢ (𝑋 ∈ ( FPPr ‘𝑁) → 𝑁 ∈ ℕ)

Theorem

fpprnn 48228

A Fermat pseudoprime to the base 𝑁 is a positive integer. (Contributed by AV, 30-May-2023.)

⊢ (𝑋 ∈ ( FPPr ‘𝑁) → 𝑋 ∈ ℕ)

Theorem

fppr2odd 48229

A Fermat pseudoprime to the base 2 is odd. (Contributed by AV, 5-Jun-2023.)

⊢ (𝑋 ∈ ( FPPr ‘2) → 𝑋 ∈ Odd )

Theorem

11t31e341 48230

341 is the product of 11 and 31. (Contributed by AV, 3-Jun-2023.)

⊢ (;11 · ;31) = ;;341

Theorem

2exp340mod341 48231

Eight to the eighth power modulo nine is one. (Contributed by AV, 3-Jun-2023.)

⊢ ((2↑;;340) mod ;;341) = 1

Theorem

341fppr2 48232

341 is the (smallest) Poulet number (Fermat pseudoprime to the base 2). (Contributed by AV, 3-Jun-2023.)

⊢ ;;341 ∈ ( FPPr ‘2)

Theorem

4fppr1 48233

4 is the (smallest) Fermat pseudoprime to the base 1. (Contributed by AV, 3-Jun-2023.)

⊢ 4 ∈ ( FPPr ‘1)

Theorem

8exp8mod9 48234

Eight to the eighth power modulo nine is one. (Contributed by AV, 2-Jun-2023.)

⊢ ((8↑8) mod 9) = 1

Theorem

9fppr8 48235

9 is the (smallest) Fermat pseudoprime to the base 8. (Contributed by AV, 2-Jun-2023.)

⊢ 9 ∈ ( FPPr ‘8)

Theorem

dfwppr 48236

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 48237

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 48238

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 48239

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 48240

Fermat's little theorem with base 8 reversed is not generally true: There is an integer 𝑝 (for example 9, see 9fppr8 48235) so that "𝑝 is prime" does not follow from 8↑𝑝≡8 (mod 𝑝). (Contributed by AV, 3-Jun-2023.)

⊢ ∃𝑝 ∈ (ℤ_≥‘3) ¬ (((8↑𝑝) mod 𝑝) = (8 mod 𝑝) → 𝑝 ∈ ℙ)

Theorem

nfermltl2rev 48241

Fermat's little theorem with base 2 reversed is not generally true: There is an integer 𝑝 (for example 341, see 341fppr2 48232) so that "𝑝 is prime" does not follow from 2↑𝑝≡2 (mod 𝑝). (Contributed by AV, 3-Jun-2023.)

⊢ ∃𝑝 ∈ (ℤ_≥‘3) ¬ (((2↑𝑝) mod 𝑝) = (2 mod 𝑝) → 𝑝 ∈ ℙ)

Theorem

nfermltlrev 48242*

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 𝑝) → 𝑝 ∈ ℙ)

21.48.14.2  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 (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.

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 48246), "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. sbgoldbalt 48279 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 48279): "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." The definition of "weak odd Goldbach numbers", see df-gbow 48247, is the basis for "the other formulation", to formulate the weak ternary Goldbach conjecture. Alternately, df-gbo 48248 provides a definition of "(strong) odd Goldbach numbers" allowing for stating the strong ternary Goldbach conjecture. In literature, the term "Goldbach number" is used for "even Goldbach numbers" (according to definition df-gbe 48246), whereas there seems to be no explicit names and definitions for "odd Goldbach numbers". Since there are more theorems for "strong odd Goldbach numbers", "odd Goldbach numbers" refers to "strong odd Goldbach numbers" in the following. Otherwise, the term "weak odd Goldbach numbers" is explicitly used.

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 was 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). 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 binary Goldbach conjecture (see section 2 in [OeSilva] p. 2042, called "even Goldbach conjecture" here) resp. about 9 x 10^30 for the ternary Goldbach conjecture (see section 1.2.2 in [Helfgott] p. 4) or 8 x 10^26 (see theorem 2.1 in [OeSilva] p. 2057, called "odd Goldbach conjecture" here). Maybe each of the results must be provided as theorem, like 6gbe 48269, which would be quite a lot...

As proposed in the Google group discussion https://groups.google.com/g/metamath/c/DOXS4pg0h8w 48269, 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 48308, ax-hgprmladder 48312 and ax-tgoldbachgt 48309.

Summary/glossary:

Term	Synonyms	Label fragment	Definition/Theorem	Remarks
binary Goldbach partition	simply "Goldbach partition"			A pair of primes (p,q) that sum to an even integer 2n=p+q	See https://mathworld.wolfram.com/GoldbachPartition.html 48309
weak Goldbach partition		gbpart		A sum of two resp. three primes resulting in an even resp. odd number without further specialization.
Goldbach partition		gbpart		A sum of two resp. three odd primes resulting in an even resp. odd number without further specialization.
even Goldbach number	simply "Goldbach number"	gbe	df-gbe 48246	A positive even integer that can be expressed as the sum of two odd primes.	See https://mathworld.wolfram.com/GoldbachNumber.html 48246
weak odd Goldbach number		gbow	df-gbow 48247	A positive odd integer that can be expressed as the sum of three primes.
odd Goldbach number	strong odd Goldbach number	gbo	df-gbo 48248	A positive odd integer that can be expressed as the sum of three odd primes.
strong binary Goldbach conjecture	"the" Goldbach conjecture" [*1], even Goldbach conjecture [*2]	sbgoldb		Every even integer greater than 4 can be expressed as the sum of two odd primes.	[*1] Equation (1) in [ApostolNT] p. 304 or [*2] introduction of [OeSilva] p. 2033.
binary Goldbach conjecture[*1][*3]	strong Goldbach conjecture [*1], even Goldbach conjecture [*1], or simply "the Goldbach conjecture" [*1][*2]	bgoldb, b	sbgoldbb 48280	Every even integer greater than 2 can be expressed as the sum of two primes.	See [*1] https://en.wikipedia.org/wiki/Goldbach's_conjecture 48280, [*2] statement in [ApostolNT] p. 9 or [*3] section 1.1 in [Helfgott] p. 2.
weak ternary Goldbach conjecture	Goldbach's weak conjecture [*1], odd Goldbach conjecture [*1][*3], ternary Goldbach conjecture [*2], ternary Goldbach problem[*1], three-primes problem [*1][*2]	wtgoldb, wt	stgoldbwt 48274, sbgoldbwt 48275	Every odd number greater than 5 can be expressed as the sum of three primes.	See [*1] https://en.wikipedia.org/wiki/Goldbach's_weak_conjecture, 48275 [*2] section 1.1 in [Helfgott] p. 2 or [*3] section 2.4 in [OeSilva] p. 2057.
ternary Goldbach conjecture	strong ternary Goldbach conjecture, the "weak" Goldbach conjecture	tgoldb, stgoldb, st	sbgoldbst 48276	Every odd number greater than 7 can be expressed as the sum of three odd primes.	See https://en.wikipedia.org/wiki/Goldbach's_weak_conjecture 48276, https://mathworld.wolfram.com/GoldbachConjecture.html 48276 or section 7.4 in [Helfgott] p. 71.
Goldbach's original conjecture (modern version)	the "ternary" Goldbach conjecture	mogoldb, m	sbgoldbm 48282	Every integer greater than 5 can be written as the sum of three primes.	See https://en.wikipedia.org/wiki/Goldbach's_weak_conjecture 48282, and https://mathworld.wolfram.com/GoldbachConjecture.html 48282
Goldbach's original conjecture (original version)		ogoldb, o	sbgoldbo 48285	Every integer greater than 2 can be written as the sum of three "primes" (considered the number 1 to be a "prime").	See https://en.wikipedia.org/wiki/Goldbach's_weak_conjecture 48285, and https://mathworld.wolfram.com/GoldbachConjecture.html 48285

Syntax

cgbe 48243

Extend the definition of a class to include the set of even numbers which have a Goldbach partition.

class GoldbachEven

Syntax

cgbow 48244

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 48245

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 48246*

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 48247*

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 48248*

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 48249*

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 48250*

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 48251*

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 48252

An even Goldbach number is even. (Contributed by AV, 25-Jul-2020.)

⊢ (𝑍 ∈ GoldbachEven → 𝑍 ∈ Even )

Theorem

gbowodd 48253

A weak odd Goldbach number is odd. (Contributed by AV, 25-Jul-2020.)

⊢ (𝑍 ∈ GoldbachOddW → 𝑍 ∈ Odd )

Theorem

gbogbow 48254

A (strong) odd Goldbach number is a weak Goldbach number. (Contributed by AV, 26-Jul-2020.)

⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ GoldbachOddW )

Theorem

gboodd 48255

An odd Goldbach number is odd. (Contributed by AV, 26-Jul-2020.)

⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ Odd )

Theorem

gbepos 48256

Any even Goldbach number is positive. (Contributed by AV, 20-Jul-2020.)

⊢ (𝑍 ∈ GoldbachEven → 𝑍 ∈ ℕ)

Theorem

gbowpos 48257

Any weak odd Goldbach number is positive. (Contributed by AV, 20-Jul-2020.)

⊢ (𝑍 ∈ GoldbachOddW → 𝑍 ∈ ℕ)

Theorem

gbopos 48258

Any odd Goldbach number is positive. (Contributed by AV, 26-Jul-2020.)

⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ ℕ)

Theorem

gbegt5 48259

Any even Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.)

⊢ (𝑍 ∈ GoldbachEven → 5 < 𝑍)

Theorem

gbowgt5 48260

Any weak odd Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.)

⊢ (𝑍 ∈ GoldbachOddW → 5 < 𝑍)

Theorem

gbowge7 48261

Any weak odd Goldbach number is greater than or equal to 7. Because of 7gbow 48270, this bound is strict. (Contributed by AV, 20-Jul-2020.)

⊢ (𝑍 ∈ GoldbachOddW → 7 ≤ 𝑍)

Theorem

gboge9 48262

Any odd Goldbach number is greater than or equal to 9. Because of 9gbo 48272, this bound is strict. (Contributed by AV, 26-Jul-2020.)

⊢ (𝑍 ∈ GoldbachOdd → 9 ≤ 𝑍)

Theorem

gbege6 48263

Any even Goldbach number is greater than or equal to 6. Because of 6gbe 48269, this bound is strict. (Contributed by AV, 20-Jul-2020.)

⊢ (𝑍 ∈ GoldbachEven → 6 ≤ 𝑍)

Theorem

gbpart6 48264

The Goldbach partition of 6. (Contributed by AV, 20-Jul-2020.)

⊢ 6 = (3 + 3)

Theorem

gbpart7 48265

The (weak) Goldbach partition of 7. (Contributed by AV, 20-Jul-2020.)

⊢ 7 = ((2 + 2) + 3)

Theorem

gbpart8 48266

The Goldbach partition of 8. (Contributed by AV, 20-Jul-2020.)

⊢ 8 = (3 + 5)

Theorem

gbpart9 48267

The (strong) Goldbach partition of 9. (Contributed by AV, 26-Jul-2020.)

⊢ 9 = ((3 + 3) + 3)

Theorem

gbpart11 48268

The (strong) Goldbach partition of 11. (Contributed by AV, 29-Jul-2020.)

⊢ ;11 = ((3 + 3) + 5)

Theorem

6gbe 48269

6 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.)

⊢ 6 ∈ GoldbachEven

Theorem

7gbow 48270

7 is a weak odd Goldbach number. (Contributed by AV, 20-Jul-2020.)

⊢ 7 ∈ GoldbachOddW

Theorem

8gbe 48271

8 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.)

⊢ 8 ∈ GoldbachEven

Theorem

9gbo 48272

9 is an odd Goldbach number. (Contributed by AV, 26-Jul-2020.)

⊢ 9 ∈ GoldbachOdd

Theorem

11gbo 48273

11 is an odd Goldbach number. (Contributed by AV, 29-Jul-2020.)

⊢ ;11 ∈ GoldbachOdd

Theorem

stgoldbwt 48274

If the strong ternary Goldbach conjecture is valid, then the weak ternary Goldbach conjecture holds, too. (Contributed by AV, 27-Jul-2020.)

⊢ (∀𝑛 ∈ Odd (7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → ∀𝑛 ∈ Odd (5 < 𝑛 → 𝑛 ∈ GoldbachOddW ))

Theorem

sbgoldbwt 48275*

If the strong binary Goldbach conjecture is valid, then the (weak) ternary Goldbach conjecture holds, too. (Contributed by AV, 20-Jul-2020.)

⊢ (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ))

Theorem

sbgoldbst 48276*

If the strong binary Goldbach conjecture is valid, then the (strong) ternary Goldbach conjecture holds, too. (Contributed by AV, 26-Jul-2020.)

⊢ (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀𝑚 ∈ Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOdd ))

Theorem

sbgoldbaltlem1 48277

Lemma 1 for sbgoldbalt 48279: 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 ∧ 4 < 𝑁 ∧ 𝑁 = (𝑃 + 𝑄)) → 𝑄 ∈ Odd ))

Theorem

sbgoldbaltlem2 48278

Lemma 2 for sbgoldbalt 48279: 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 ∧ 4 < 𝑁 ∧ 𝑁 = (𝑃 + 𝑄)) → (𝑃 ∈ Odd ∧ 𝑄 ∈ Odd )))

Theorem

sbgoldbalt 48279*

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 (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ ∀𝑛 ∈ Even (2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))

Theorem

sbgoldbb 48280*

If the strong binary Goldbach conjecture is valid, the binary Goldbach conjecture is valid. (Contributed by AV, 23-Dec-2021.)

⊢ (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀𝑛 ∈ Even (2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))

Theorem

sgoldbeven3prm 48281*

If the binary Goldbach conjecture is valid, then an even integer greater than 5 can be expressed as the sum of three primes: Since (𝑁 − 2) is even iff 𝑁 is even, there would be primes 𝑝 and 𝑞 with (𝑁 − 2) = (𝑝 + 𝑞), and therefore 𝑁 = ((𝑝 + 𝑞) + 2). (Contributed by AV, 24-Dec-2021.)

⊢ (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ((𝑁 ∈ Even ∧ 6 ≤ 𝑁) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑁 = ((𝑝 + 𝑞) + 𝑟)))

Theorem

sbgoldbm 48282*

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 (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀𝑛 ∈ (ℤ_≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟))

Theorem

mogoldbb 48283*

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.)

⊢ (∀𝑛 ∈ (ℤ_≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) → ∀𝑛 ∈ Even (2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞)))

Theorem

sbgoldbmb 48284*

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 (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ ∀𝑛 ∈ (ℤ_≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟))

Theorem

sbgoldbo 48285*

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.)

⊢ 𝑃 = ({1} ∪ ℙ)    ⇒   ⊢ (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀𝑛 ∈ (ℤ_≥‘3)∃𝑝 ∈ 𝑃 ∃𝑞 ∈ 𝑃 ∃𝑟 ∈ 𝑃 𝑛 = ((𝑝 + 𝑞) + 𝑟))

Theorem

nnsum3primes4 48286*

4 is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020.)

⊢ ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑_m (1...𝑑))(𝑑 ≤ 3 ∧ 4 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))

Theorem

nnsum4primes4 48287*

4 is the sum of at most 4 (actually 2) primes. (Contributed by AV, 23-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.)

⊢ ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑_m (1...𝑑))(𝑑 ≤ 4 ∧ 4 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))

Theorem

nnsum3primesprm 48288*

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.)

⊢ (𝑃 ∈ ℙ → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑_m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑃 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))

Theorem

nnsum4primesprm 48289*

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.)

⊢ (𝑃 ∈ ℙ → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑_m (1...𝑑))(𝑑 ≤ 4 ∧ 𝑃 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))

Theorem

nnsum3primesgbe 48290*

Any even Goldbach number is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020.)

⊢ (𝑁 ∈ GoldbachEven → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑_m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))

Theorem

nnsum4primesgbe 48291*

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 → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑_m (1...𝑑))(𝑑 ≤ 4 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))

Theorem

nnsum3primesle9 48292*

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.)

⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑁 ≤ 8) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑_m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))

Theorem

nnsum4primesle9 48293*

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.)

⊢ ((𝑁 ∈ (ℤ_≥‘2) ∧ 𝑁 ≤ 8) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑_m (1...𝑑))(𝑑 ≤ 4 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))

Theorem

nnsum4primesodd 48294*

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 (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ((𝑁 ∈ (ℤ_≥‘6) ∧ 𝑁 ∈ Odd ) → ∃𝑓 ∈ (ℙ ↑_m (1...3))𝑁 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘)))

Theorem

nnsum4primesoddALTV 48295*

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 (7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ((𝑁 ∈ (ℤ_≥‘8) ∧ 𝑁 ∈ Odd ) → ∃𝑓 ∈ (ℙ ↑_m (1...3))𝑁 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘)))

Theorem

evengpop3 48296*

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 (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even ) → ∃𝑜 ∈ GoldbachOddW 𝑁 = (𝑜 + 3)))

Theorem

evengpoap3 48297*

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 (7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ((𝑁 ∈ (ℤ_≥‘;12) ∧ 𝑁 ∈ Even ) → ∃𝑜 ∈ GoldbachOdd 𝑁 = (𝑜 + 3)))

Theorem

nnsum4primeseven 48298*

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 (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ((𝑁 ∈ (ℤ_≥‘9) ∧ 𝑁 ∈ Even ) → ∃𝑓 ∈ (ℙ ↑_m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))

Theorem

nnsum4primesevenALTV 48299*

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 (7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ((𝑁 ∈ (ℤ_≥‘;12) ∧ 𝑁 ∈ Even ) → ∃𝑓 ∈ (ℙ ↑_m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘)))

Theorem

wtgoldbnnsum4prm 48300*

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 (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ∀𝑛 ∈ (ℤ_≥‘2)∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑_m (1...𝑑))(𝑑 ≤ 4 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))