P. 478 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

fpprwppr 47701

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 47702

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 47703

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 47704

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

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

Theorem

nfermltl2rev 47705

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

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

Theorem

nfermltlrev 47706*

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 47710), "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 47743 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 47743): "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 47711, is the basis for "the other formulation", to formulate the weak ternary Goldbach conjecture. Alternately, df-gbo 47712 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 47710), 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 47733, which would be quite a lot...

As proposed in the Google group discussion https://groups.google.com/g/metamath/c/DOXS4pg0h8w 47733, 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 47772, ax-hgprmladder 47776 and ax-tgoldbachgt 47773.

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

Syntax

cgbe 47707

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

class GoldbachEven

Syntax

cgbow 47708

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 47709

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

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

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

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

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

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

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 47716

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

⊢ (𝑍 ∈ GoldbachEven → 𝑍 ∈ Even )

Theorem

gbowodd 47717

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

⊢ (𝑍 ∈ GoldbachOddW → 𝑍 ∈ Odd )

Theorem

gbogbow 47718

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

⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ GoldbachOddW )

Theorem

gboodd 47719

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

⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ Odd )

Theorem

gbepos 47720

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

⊢ (𝑍 ∈ GoldbachEven → 𝑍 ∈ ℕ)

Theorem

gbowpos 47721

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

⊢ (𝑍 ∈ GoldbachOddW → 𝑍 ∈ ℕ)

Theorem

gbopos 47722

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

⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ ℕ)

Theorem

gbegt5 47723

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

⊢ (𝑍 ∈ GoldbachEven → 5 < 𝑍)

Theorem

gbowgt5 47724

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

⊢ (𝑍 ∈ GoldbachOddW → 5 < 𝑍)

Theorem

gbowge7 47725

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

⊢ (𝑍 ∈ GoldbachOddW → 7 ≤ 𝑍)

Theorem

gboge9 47726

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

⊢ (𝑍 ∈ GoldbachOdd → 9 ≤ 𝑍)

Theorem

gbege6 47727

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

⊢ (𝑍 ∈ GoldbachEven → 6 ≤ 𝑍)

Theorem

gbpart6 47728

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

⊢ 6 = (3 + 3)

Theorem

gbpart7 47729

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

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

Theorem

gbpart8 47730

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

⊢ 8 = (3 + 5)

Theorem

gbpart9 47731

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

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

Theorem

gbpart11 47732

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

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

Theorem

6gbe 47733

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

⊢ 6 ∈ GoldbachEven

Theorem

7gbow 47734

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

⊢ 7 ∈ GoldbachOddW

Theorem

8gbe 47735

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

⊢ 8 ∈ GoldbachEven

Theorem

9gbo 47736

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

⊢ 9 ∈ GoldbachOdd

Theorem

11gbo 47737

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

⊢ ;11 ∈ GoldbachOdd

Theorem

stgoldbwt 47738

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

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

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 47741

Lemma 1 for sbgoldbalt 47743: 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 47742

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

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

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

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

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

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

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

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

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

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

Theorem

nnsum4primes4 47751*

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 47767

Lemma 1 for bgoldbtbnd 47771: 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 47768*

Lemma 2 for bgoldbtbnd 47771. (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 47769*

Lemma 3 for bgoldbtbnd 47771. (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 47770*

Lemma 4 for bgoldbtbnd 47771. (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 47771*

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 47772

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

Temporary duplicate of tgoldbachgt 34641, 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 47774*

Variant of Thierry Arnoux's tgoldbachgt 34641 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 47775*

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 47772. (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.)

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

Axiom

ax-hgprmladder 47776

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 47777

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 47775, ax-hgprmladder 47776 and bgoldbtbnd 47771. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.)

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

Theorem

tgoldbachlt 47778*

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 47777. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.)

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

Theorem

tgoldbach 47779

The ternary Goldbach conjecture is valid. Main theorem in [Helfgott] p. 2. This follows from tgoldbachlt 47778 and ax-tgoldbachgt 47773. (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 47780

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

class ClNeighbVtx

Definition

df-clnbgr 47781*

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 29258). Alternatively, a closed neighborhood of a vertex could have been defined as its open neighborhood enhanced by the vertex itself, see dfclnbgr4 47786. This definition is applicable even for arbitrary hypergraphs. (Contributed by AV, 7-May-2025.)

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

Theorem

clnbgrprc0 47782

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 47783

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

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

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

Theorem

dfclnbgr2 47785*

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 47786

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 47787

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

Theorem

dfclnbgr3 47788*

Alternate definition of the closed neighborhood of a vertex using the edge function instead of the edges themselves (see also clnbgrval 47784). (Contributed by AV, 8-May-2025.)

⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ 𝑉 ∧ Fun 𝐼) → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑖 ∈ dom 𝐼{𝑁, 𝑛} ⊆ (𝐼‘𝑖)}))

Theorem

clnbgrnvtx0 47789

If a class 𝑋 is not a vertex of a graph 𝐺, then it has an empty closed neighborhood in 𝐺. (Contributed by AV, 8-May-2025.)

⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑋 ∉ 𝑉 → (𝐺 ClNeighbVtx 𝑋) = ∅)

Theorem

clnbgrel 47790*

Characterization of a member 𝑁 of the closed neighborhood of a vertex 𝑋 in a graph 𝐺. (Contributed by AV, 9-May-2025.)

⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ (𝐺 ClNeighbVtx 𝑋) ↔ ((𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ (𝑁 = 𝑋 ∨ ∃𝑒 ∈ 𝐸 {𝑋, 𝑁} ⊆ 𝑒)))

Theorem

clnbgrvtxel 47791

Every vertex 𝐾 is a member of its closed neighborhood. (Contributed by AV, 10-May-2025.)

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

Theorem

clnbgrisvtx 47792

Every member 𝑁 of the closed neighborhood of a vertex 𝐾 is a vertex. (Contributed by AV, 9-May-2025.)

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

Theorem

clnbgrssvtx 47793

The closed neighborhood of a vertex 𝐾 in a graph is a subset of all vertices of the graph. (Contributed by AV, 9-May-2025.)

⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ClNeighbVtx 𝐾) ⊆ 𝑉

Theorem

clnbgrn0 47794

The closed neighborhood of a vertex is never empty. (Contributed by AV, 16-May-2025.)

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

Theorem

clnbupgr 47795*

The closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025.)

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

Theorem

clnbupgrel 47796

A member of the closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025.)

⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → (𝑁 ∈ (𝐺 ClNeighbVtx 𝐾) ↔ (𝑁 = 𝐾 ∨ {𝑁, 𝐾} ∈ 𝐸)))

Theorem

clnbgr0vtx 47797

In a null graph (with no vertices), all closed neighborhoods are empty. (Contributed by AV, 15-Nov-2020.)

⊢ ((Vtx‘𝐺) = ∅ → (𝐺 ClNeighbVtx 𝐾) = ∅)

Theorem

clnbgr0edg 47798

In an empty graph (with no edges), all closed neighborhoods consists of a single vertex. (Contributed by AV, 10-May-2025.)

⊢ (((Edg‘𝐺) = ∅ ∧ 𝐾 ∈ (Vtx‘𝐺)) → (𝐺 ClNeighbVtx 𝐾) = {𝐾})

Theorem

clnbgrsym 47799

In a graph, the closed neighborhood relation is symmetric: a vertex 𝑁 in a graph 𝐺 is a neighbor of a second vertex 𝐾 iff the second vertex 𝐾 is a neighbor of the first vertex 𝑁. (Contributed by AV, 10-May-2025.)

⊢ (𝑁 ∈ (𝐺 ClNeighbVtx 𝐾) ↔ 𝐾 ∈ (𝐺 ClNeighbVtx 𝑁))

Theorem

predgclnbgrel 47800

If a (not necessarily proper) unordered pair containing a vertex is an edge, the other vertex is in the closed neighborhood of the first vertex. (Contributed by AV, 23-Aug-2025.)

⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ {𝑋, 𝑁} ∈ 𝐸) → 𝑁 ∈ (𝐺 ClNeighbVtx 𝑋))