P. 484 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

fppr 48301*

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

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

Theorem

fpprmod 48302*

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 48303

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

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

Theorem

fpprbasnn 48304

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

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

Theorem

fpprnn 48305

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

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

Theorem

fppr2odd 48306

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

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

Theorem

11t31e341 48307

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

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

Theorem

2exp340mod341 48308

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

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

Theorem

341fppr2 48309

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

⊢ ;;341 ∈ ( FPPr ‘2)

Theorem

4fppr1 48310

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

⊢ 4 ∈ ( FPPr ‘1)

Theorem

8exp8mod9 48311

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

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

Theorem

9fppr8 48312

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

⊢ 9 ∈ ( FPPr ‘8)

Theorem

dfwppr 48313

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 48314

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 48315

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 48316

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 48317

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

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

Theorem

nfermltl2rev 48318

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

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

Theorem

nfermltlrev 48319*

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 48323), "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 48356 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 48356): "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 48324, is the basis for "the other formulation", to formulate the weak ternary Goldbach conjecture. Alternately, df-gbo 48325 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 48323), 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 48346, which would be quite a lot...

As proposed in the Google group discussion https://groups.google.com/g/metamath/c/DOXS4pg0h8w 48346, 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 48385, ax-hgprmladder 48389 and ax-tgoldbachgt 48386.

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 48386
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 48323	A positive even integer that can be expressed as the sum of two odd primes.	See https://mathworld.wolfram.com/GoldbachNumber.html 48323
weak odd Goldbach number		gbow	df-gbow 48324	A positive odd integer that can be expressed as the sum of three primes.
odd Goldbach number	strong odd Goldbach number	gbo	df-gbo 48325	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 48357	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 48357, [*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 48351, sbgoldbwt 48352	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, 48352 [*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 48353	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 48353, https://mathworld.wolfram.com/GoldbachConjecture.html 48353 or section 7.4 in [Helfgott] p. 71.
Goldbach's original conjecture (modern version)	the "ternary" Goldbach conjecture	mogoldb, m	sbgoldbm 48359	Every integer greater than 5 can be written as the sum of three primes.	See https://en.wikipedia.org/wiki/Goldbach's_weak_conjecture 48359, and https://mathworld.wolfram.com/GoldbachConjecture.html 48359
Goldbach's original conjecture (original version)		ogoldb, o	sbgoldbo 48362	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 48362, and https://mathworld.wolfram.com/GoldbachConjecture.html 48362

Syntax

cgbe 48320

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

class GoldbachEven

Syntax

cgbow 48321

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 48322

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

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

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

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

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

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

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 48329

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

⊢ (𝑍 ∈ GoldbachEven → 𝑍 ∈ Even )

Theorem

gbowodd 48330

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

⊢ (𝑍 ∈ GoldbachOddW → 𝑍 ∈ Odd )

Theorem

gbogbow 48331

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

⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ GoldbachOddW )

Theorem

gboodd 48332

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

⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ Odd )

Theorem

gbepos 48333

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

⊢ (𝑍 ∈ GoldbachEven → 𝑍 ∈ ℕ)

Theorem

gbowpos 48334

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

⊢ (𝑍 ∈ GoldbachOddW → 𝑍 ∈ ℕ)

Theorem

gbopos 48335

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

⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ ℕ)

Theorem

gbegt5 48336

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

⊢ (𝑍 ∈ GoldbachEven → 5 < 𝑍)

Theorem

gbowgt5 48337

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

⊢ (𝑍 ∈ GoldbachOddW → 5 < 𝑍)

Theorem

gbowge7 48338

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

⊢ (𝑍 ∈ GoldbachOddW → 7 ≤ 𝑍)

Theorem

gboge9 48339

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

⊢ (𝑍 ∈ GoldbachOdd → 9 ≤ 𝑍)

Theorem

gbege6 48340

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

⊢ (𝑍 ∈ GoldbachEven → 6 ≤ 𝑍)

Theorem

gbpart6 48341

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

⊢ 6 = (3 + 3)

Theorem

gbpart7 48342

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

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

Theorem

gbpart8 48343

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

⊢ 8 = (3 + 5)

Theorem

gbpart9 48344

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

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

Theorem

gbpart11 48345

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

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

Theorem

6gbe 48346

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

⊢ 6 ∈ GoldbachEven

Theorem

7gbow 48347

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

⊢ 7 ∈ GoldbachOddW

Theorem

8gbe 48348

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

⊢ 8 ∈ GoldbachEven

Theorem

9gbo 48349

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

⊢ 9 ∈ GoldbachOdd

Theorem

11gbo 48350

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

⊢ ;11 ∈ GoldbachOdd

Theorem

stgoldbwt 48351

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

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

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 48354

Lemma 1 for sbgoldbalt 48356: 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 48355

Lemma 2 for sbgoldbalt 48356: 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 48356*

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

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

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

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

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

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

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

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

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

Theorem

nnsum4primes4 48364*

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

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

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

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

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

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

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

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

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

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

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

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

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

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...𝑑)(𝑓‘𝑘)))

Theorem

stgoldbnnsum4prm 48378*

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

Theorem

bgoldbnnsum3prm 48379*

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

Theorem

bgoldbtbndlem1 48380

Lemma 1 for bgoldbtbnd 48384: the odd numbers between 7 and 13 (exclusive) are odd Goldbach numbers. (Contributed by AV, 29-Jul-2020.)

⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 ∈ (7[,);13)) → 𝑁 ∈ GoldbachOdd )

Theorem

bgoldbtbndlem2 48381*

Lemma 2 for bgoldbtbnd 48384. (Contributed by AV, 1-Aug-2020.)

⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘;11))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘;11))    &   ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ))    &   ⊢ (𝜑 → 𝐷 ∈ (ℤ_≥‘3))    &   ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷))    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))))    &   ⊢ (𝜑 → (𝐹‘0) = 7)    &   ⊢ (𝜑 → (𝐹‘1) = ;13)    &   ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷))    &   ⊢ 𝑆 = (𝑋 − (𝐹‘(𝐼 − 1)))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹‘𝐼)) ≤ 4) → (𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆)))

Theorem

bgoldbtbndlem3 48382*

Lemma 3 for bgoldbtbnd 48384. (Contributed by AV, 1-Aug-2020.)

⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘;11))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘;11))    &   ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ))    &   ⊢ (𝜑 → 𝐷 ∈ (ℤ_≥‘3))    &   ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷))    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))))    &   ⊢ (𝜑 → (𝐹‘0) = 7)    &   ⊢ (𝜑 → (𝐹‘1) = ;13)    &   ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷))    &   ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ)    &   ⊢ 𝑆 = (𝑋 − (𝐹‘𝐼))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ 4 < 𝑆) → (𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆)))

Theorem

bgoldbtbndlem4 48383*

Lemma 4 for bgoldbtbnd 48384. (Contributed by AV, 1-Aug-2020.)

⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘;11))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘;11))    &   ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ))    &   ⊢ (𝜑 → 𝐷 ∈ (ℤ_≥‘3))    &   ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷))    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))))    &   ⊢ (𝜑 → (𝐹‘0) = 7)    &   ⊢ (𝜑 → (𝐹‘1) = ;13)    &   ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷))    &   ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ)    ⇒   ⊢ (((𝜑 ∧ 𝐼 ∈ (1..^𝐷)) ∧ 𝑋 ∈ Odd ) → ((𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹‘𝐼)) ≤ 4) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑋 = ((𝑝 + 𝑞) + 𝑟))))

Theorem

bgoldbtbnd 48384*

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

⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘;11))    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘;11))    &   ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ))    &   ⊢ (𝜑 → 𝐷 ∈ (ℤ_≥‘3))    &   ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷))    &   ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖))))    &   ⊢ (𝜑 → (𝐹‘0) = 7)    &   ⊢ (𝜑 → (𝐹‘1) = ;13)    &   ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷))    &   ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ)    ⇒   ⊢ (𝜑 → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑀) → 𝑛 ∈ GoldbachOdd ))

Axiom

ax-bgbltosilva 48385

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 ∧ 4 < 𝑁 ∧ 𝑁 ≤ (4 · (;10↑;18))) → 𝑁 ∈ GoldbachEven )

Axiom

ax-tgoldbachgt 48386*

Temporary duplicate of tgoldbachgt 34919, provided as "axiom" as long as this theorem is in the mathbox of Thierry Arnoux: Odd integers greater than (;10↑;27) 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.)

⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐺 = {𝑧 ∈ 𝑂 ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}    ⇒   ⊢ ∃𝑚 ∈ ℕ (𝑚 ≤ (;10↑;27) ∧ ∀𝑛 ∈ 𝑂 (𝑚 < 𝑛 → 𝑛 ∈ 𝐺))

Theorem

tgoldbachgtALTV 48387*

Variant of Thierry Arnoux's tgoldbachgt 34919 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.)

⊢ ∃𝑚 ∈ ℕ (𝑚 ≤ (;10↑;27) ∧ ∀𝑛 ∈ Odd (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ))

Theorem

bgoldbachlt 48388*

The binary Goldbach conjecture is valid for small even numbers (i.e. for all even numbers less than or equal to a fixed big 𝑚). This is verified for m = 4 x 10^18 by Oliveira e Silva, see ax-bgbltosilva 48385. (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.)

⊢ ∃𝑚 ∈ ℕ ((4 · (;10↑;18)) ≤ 𝑚 ∧ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven ))

Axiom

ax-hgprmladder 48389

There is a partition ("ladder") of primes from 7 to 8.8 x 10^30 with parts ("rungs") having lengths of at least 4 and at most N - 4, see section 1.2.2 in [Helfgott] p. 4. Temporarily provided as "axiom". (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.)

⊢ ∃𝑑 ∈ (ℤ_≥‘3)∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = ;13 ∧ (𝑓‘𝑑) = (;89 · (;10↑;29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖)) < ((4 · (;10↑;18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓‘𝑖))))

Theorem

tgblthelfgott 48390

The ternary Goldbach conjecture is valid for all odd numbers less than 8.8 x 10^30 (actually 8.875694 x 10^30, see section 1.2.2 in [Helfgott] p. 4, using bgoldbachlt 48388, ax-hgprmladder 48389 and bgoldbtbnd 48384. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.)

⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29))) → 𝑁 ∈ GoldbachOdd )

Theorem

tgoldbachlt 48391*

The ternary Goldbach conjecture is valid for small odd numbers (i.e. for all odd numbers less than a fixed big 𝑚 greater than 8 x 10^30). This is verified for m = 8.875694 x 10^30 by Helfgott, see tgblthelfgott 48390. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.)

⊢ ∃𝑚 ∈ ℕ ((8 · (;10↑;30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ))

Theorem

tgoldbach 48392

The ternary Goldbach conjecture is valid. Main theorem in [Helfgott] p. 2. This follows from tgoldbachlt 48391 and ax-tgoldbachgt 48386. (Contributed by AV, 2-Aug-2020.) (Revised by AV, 9-Sep-2021.)

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

21.48.15  Graph theory (extension)

21.48.15.1  Closed neighborhood of a vertex

Syntax

cclnbgr 48393

Extend class notation with closed neighborhoods (of a vertex in a graph).

class ClNeighbVtx

Definition

df-clnbgr 48394*

Define the closed neighborhood resp. the class of all neighbors of a vertex (in a graph) and the vertex itself, see definition in section I.1 of [Bollobas] p. 3. The closed neighborhood of a vertex is the set of all vertices which are connected with this vertex by an edge and the vertex itself (in contrast to an open neighborhood, see df-nbgr 29478). Alternatively, a closed neighborhood of a vertex could have been defined as its open neighborhood enhanced by the vertex itself, see dfclnbgr4 48399. This definition is applicable even for arbitrary hypergraphs. (Contributed by AV, 7-May-2025.)

⊢ ClNeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}))

Theorem

clnbgrprc0 48395

The closed neighborhood is empty if the graph 𝐺 or the vertex 𝑁 are proper classes. (Contributed by AV, 7-May-2025.)

⊢ (¬ (𝐺 ∈ V ∧ 𝑁 ∈ V) → (𝐺 ClNeighbVtx 𝑁) = ∅)

Theorem

clnbgrcl 48396

If a class 𝑋 has at least one element in its closed neighborhood, this class must be a vertex. (Contributed by AV, 7-May-2025.)

⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ (𝐺 ClNeighbVtx 𝑋) → 𝑋 ∈ 𝑉)

Theorem

clnbgrval 48397*

The closed neighborhood of a vertex 𝑉 in a graph 𝐺. (Contributed by AV, 7-May-2025.)

⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}))

Theorem

dfclnbgr2 48398*

Alternate definition of the closed neighborhood of a vertex breaking up the subset relationship of an unordered pair. (Contributed by AV, 7-May-2025.)

⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)}))

Theorem

dfclnbgr4 48399

Alternate definition of the closed neighborhood of a vertex as union of the vertex with its open neighborhood. (Contributed by AV, 8-May-2025.)

⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ (𝐺 NeighbVtx 𝑁)))

Theorem

elclnbgrelnbgr 48400

An element of the closed neighborhood of a vertex which is not the vertex itself is an element of the open neighborhood of the vertex. (Contributed by AV, 24-Sep-2025.)

⊢ ((𝑋 ∈ (𝐺 ClNeighbVtx 𝑁) ∧ 𝑋 ≠ 𝑁) → 𝑋 ∈ (𝐺 NeighbVtx 𝑁))