P. 481 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48001-48100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	gbowpos 48001	Any weak odd Goldbach number is positive. (Contributed by AV, 20-Jul-2020.)
⊢ (𝑍 ∈ GoldbachOddW → 𝑍 ∈ ℕ)
Theorem	gbopos 48002	Any odd Goldbach number is positive. (Contributed by AV, 26-Jul-2020.)
⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ ℕ)
Theorem	gbegt5 48003	Any even Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.)
⊢ (𝑍 ∈ GoldbachEven → 5 < 𝑍)
Theorem	gbowgt5 48004	Any weak odd Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.)
⊢ (𝑍 ∈ GoldbachOddW → 5 < 𝑍)
Theorem	gbowge7 48005	Any weak odd Goldbach number is greater than or equal to 7. Because of 7gbow 48014, this bound is strict. (Contributed by AV, 20-Jul-2020.)
⊢ (𝑍 ∈ GoldbachOddW → 7 ≤ 𝑍)
Theorem	gboge9 48006	Any odd Goldbach number is greater than or equal to 9. Because of 9gbo 48016, this bound is strict. (Contributed by AV, 26-Jul-2020.)
⊢ (𝑍 ∈ GoldbachOdd → 9 ≤ 𝑍)
Theorem	gbege6 48007	Any even Goldbach number is greater than or equal to 6. Because of 6gbe 48013, this bound is strict. (Contributed by AV, 20-Jul-2020.)
⊢ (𝑍 ∈ GoldbachEven → 6 ≤ 𝑍)
Theorem	gbpart6 48008	The Goldbach partition of 6. (Contributed by AV, 20-Jul-2020.)
⊢ 6 = (3 + 3)
Theorem	gbpart7 48009	The (weak) Goldbach partition of 7. (Contributed by AV, 20-Jul-2020.)
⊢ 7 = ((2 + 2) + 3)
Theorem	gbpart8 48010	The Goldbach partition of 8. (Contributed by AV, 20-Jul-2020.)
⊢ 8 = (3 + 5)
Theorem	gbpart9 48011	The (strong) Goldbach partition of 9. (Contributed by AV, 26-Jul-2020.)
⊢ 9 = ((3 + 3) + 3)
Theorem	gbpart11 48012	The (strong) Goldbach partition of 11. (Contributed by AV, 29-Jul-2020.)
⊢ ;11 = ((3 + 3) + 5)
Theorem	6gbe 48013	6 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.)
⊢ 6 ∈ GoldbachEven
Theorem	7gbow 48014	7 is a weak odd Goldbach number. (Contributed by AV, 20-Jul-2020.)
⊢ 7 ∈ GoldbachOddW
Theorem	8gbe 48015	8 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.)
⊢ 8 ∈ GoldbachEven
Theorem	9gbo 48016	9 is an odd Goldbach number. (Contributed by AV, 26-Jul-2020.)
⊢ 9 ∈ GoldbachOdd
Theorem	11gbo 48017	11 is an odd Goldbach number. (Contributed by AV, 29-Jul-2020.)
⊢ ;11 ∈ GoldbachOdd
Theorem	stgoldbwt 48018	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 48019*	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 48020*	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 48021	Lemma 1 for sbgoldbalt 48023: 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 48022	Lemma 2 for sbgoldbalt 48023: 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 48023*	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 48024*	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 48025*	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 48026*	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 48027*	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 48028*	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 48029*	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 48030*	4 is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020.)
⊢ ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m (1...𝑑))(𝑑 ≤ 3 ∧ 4 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))
Theorem	nnsum4primes4 48031*	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 48032*	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 48033*	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 48034*	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 48035*	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 48036*	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 48037*	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 48038*	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 48039*	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 48040*	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 48041*	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 48042*	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 48043*	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 48044*	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 48045*	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 48046*	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 48047	Lemma 1 for bgoldbtbnd 48051: 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 48048*	Lemma 2 for bgoldbtbnd 48051. (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 48049*	Lemma 3 for bgoldbtbnd 48051. (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 48050*	Lemma 4 for bgoldbtbnd 48051. (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 48051*	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 48052	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 48053*	Temporary duplicate of tgoldbachgt 34820, 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 48054*	Variant of Thierry Arnoux's tgoldbachgt 34820 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 48055*	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 48052. (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.)
⊢ ∃𝑚 ∈ ℕ ((4 · (;10↑;18)) ≤ 𝑚 ∧ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven ))
Axiom	ax-hgprmladder 48056	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 48057	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 48055, ax-hgprmladder 48056 and bgoldbtbnd 48051. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.)
⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 < (;88 · (;10↑;29))) → 𝑁 ∈ GoldbachOdd )
Theorem	tgoldbachlt 48058*	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 48057. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.)
⊢ ∃𝑚 ∈ ℕ ((8 · (;10↑;30)) < 𝑚 ∧ ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachOdd ))
Theorem	tgoldbach 48059	The ternary Goldbach conjecture is valid. Main theorem in [Helfgott] p. 2. This follows from tgoldbachlt 48058 and ax-tgoldbachgt 48053. (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 48060	Extend class notation with closed neighborhoods (of a vertex in a graph).
class ClNeighbVtx
Definition	df-clnbgr 48061*	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 29406). Alternatively, a closed neighborhood of a vertex could have been defined as its open neighborhood enhanced by the vertex itself, see dfclnbgr4 48066. This definition is applicable even for arbitrary hypergraphs. (Contributed by AV, 7-May-2025.)
⊢ ClNeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ ({𝑣} ∪ {𝑛 ∈ (Vtx‘𝑔) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}))
Theorem	clnbgrprc0 48062	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 48063	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 48064*	The closed neighborhood of a vertex 𝑉 in a graph 𝐺. (Contributed by AV, 7-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}))
Theorem	dfclnbgr2 48065*	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 48066	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 48067	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 48068*	Alternate definition of the closed neighborhood of a vertex using the edge function instead of the edges themselves (see also clnbgrval 48064). (Contributed by AV, 8-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ 𝑉 ∧ Fun 𝐼) → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ ∃𝑖 ∈ dom 𝐼{𝑁, 𝑛} ⊆ (𝐼‘𝑖)}))
Theorem	clnbgrnvtx0 48069	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 48070*	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 48071	Every vertex 𝐾 is a member of its closed neighborhood. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ (𝐺 ClNeighbVtx 𝐾))
Theorem	clnbgrisvtx 48072	Every member 𝑁 of the closed neighborhood of a vertex 𝐾 is a vertex. (Contributed by AV, 9-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ (𝐺 ClNeighbVtx 𝐾) → 𝑁 ∈ 𝑉)
Theorem	clnbgrssvtx 48073	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 48074	The closed neighborhood of a vertex is never empty. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) ≠ ∅)
Theorem	clnbupgr 48075*	The closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸}))
Theorem	clnbupgrel 48076	A member of the closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) → (𝑁 ∈ (𝐺 ClNeighbVtx 𝐾) ↔ (𝑁 = 𝐾 ∨ {𝑁, 𝐾} ∈ 𝐸)))
Theorem	clnbupgreli 48077	A member of the closed neighborhood of a vertex in a pseudograph. (Contributed by AV, 28-Dec-2025.)
⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ (𝐺 ClNeighbVtx 𝐾)) → (𝑁 = 𝐾 ∨ {𝑁, 𝐾} ∈ 𝐸))
Theorem	clnbgr0vtx 48078	In a null graph (with no vertices), all closed neighborhoods are empty. (Contributed by AV, 15-Nov-2020.)
⊢ ((Vtx‘𝐺) = ∅ → (𝐺 ClNeighbVtx 𝐾) = ∅)
Theorem	clnbgr0edg 48079	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 48080	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 48081	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 𝑋))
Theorem	clnbgredg 48082	A vertex connected by an edge with another vertex is a neighbor of that vertex. (Contributed by AV, 24-Aug-2025.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑋)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ (𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾)) → 𝑌 ∈ 𝑁)
Theorem	clnbgrssedg 48083	The vertices connected by an edge are a subset of the neighborhood of each of these vertices. (Contributed by AV, 26-May-2025.) (Proof shortened by AV, 24-Aug-2025.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑁 = (𝐺 ClNeighbVtx 𝑋)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝐾 ∈ 𝐸 ∧ 𝑋 ∈ 𝐾) → 𝐾 ⊆ 𝑁)
Theorem	edgusgrclnbfin 48084*	The size of the closed neighborhood of a vertex in a simple graph is finite iff the number of edges having this vertex as endpoint is finite. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ((𝐺 ClNeighbVtx 𝑈) ∈ Fin ↔ {𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒} ∈ Fin))
Theorem	clnbusgrfi 48085	The closed neighborhood of a vertex in a simple graph with a finite number of edges is a finite set. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐸 ∈ Fin ∧ 𝑈 ∈ 𝑉) → (𝐺 ClNeighbVtx 𝑈) ∈ Fin)
Theorem	clnbfiusgrfi 48086	The closed neighborhood of a vertex in a finite simple graph is a finite set. (Contributed by AV, 10-May-2025.)
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ (Vtx‘𝐺)) → (𝐺 ClNeighbVtx 𝑁) ∈ Fin)
Theorem	clnbgrlevtx 48087	The size of the closed neighborhood of a vertex is at most the number of vertices of a graph. (Contributed by AV, 10-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (♯‘(𝐺 ClNeighbVtx 𝑈)) ≤ (♯‘𝑉)
21.48.15.2  Semiclosed and semiopen neighborhoods (experimental) We have already definitions for open and closed neighborhoods of a vertex, which differs only in the fact that the first never contains the vertex, and the latter always contains the vertex. One of these definitions, however, cannot be simply derived from the other. This would be possible if a definition of a semiclosed neighborhood was available, see dfsclnbgr2 48088. The definitions for open and closed neighborhoods could be derived from such a more simple, but otherwise probably useless definition, see dfnbgr5 48093 and dfclnbgr5 48092. Depending on the existence of certain edges, a vertex belongs to its semiclosed neighborhood or not. An alternate approach is to introduce semiopen neighborhoods, see dfvopnbgr2 48095. The definitions for open and closed neighborhoods could also be derived from such a definition, see dfnbgr6 48099 and dfclnbgr6 48098. Like with semiclosed neighborhood, depending on the existence of certain edges, a vertex belongs to its semiopen neighborhood or not. It is unclear if either definition is/will be useful, and in contrast to dfsclnbgr2 48088, the definition of semiopen neighborhoods is much more complex.
Theorem	dfsclnbgr2 48088*	Alternate definition of the semiclosed neighborhood of a vertex breaking up the subset relationship of an unordered pair. A semiclosed neighborhood 𝑆 of a vertex 𝑁 is the set of all vertices incident with edges which join the vertex 𝑁 with a vertex. Therefore, a vertex is contained in its semiclosed neighborhood if it is connected with any vertex by an edge (see sclnbgrelself 48090), even only with itself (i.e., by a loop). (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)})
Theorem	sclnbgrel 48089*	Characterization of a member 𝑋 of the semiclosed neighborhood of a vertex 𝑁 in a graph 𝐺. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑆 ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝑋} ⊆ 𝑒))
Theorem	sclnbgrelself 48090*	A vertex 𝑁 is a member of its semiclosed neighborhood iff there is an edge joining the vertex with a vertex. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑆 ↔ (𝑁 ∈ 𝑉 ∧ ∃𝑒 ∈ 𝐸 𝑁 ∈ 𝑒))
Theorem	sclnbgrisvtx 48091*	Every member 𝑋 of the semiclosed neighborhood of a vertex 𝑁 is a vertex. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑆 → 𝑋 ∈ 𝑉)
Theorem	dfclnbgr5 48092*	Alternate definition of the closed neighborhood of a vertex as union of the vertex with its semiclosed neighborhood. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ 𝑆))
Theorem	dfnbgr5 48093*	Alternate definition of the (open) neighborhood of a vertex as a semiclosed neighborhood without itself. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 NeighbVtx 𝑁) = (𝑆 ∖ {𝑁}))
Theorem	dfnbgrss 48094*	Subset chain for different kinds of neighborhoods of a vertex. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝑁 ∈ 𝑉 → ((𝐺 NeighbVtx 𝑁) ⊆ 𝑆 ∧ 𝑆 ⊆ (𝐺 ClNeighbVtx 𝑁)))
Theorem	dfvopnbgr2 48095*	Alternate definition of the semiopen neighborhood of a vertex breaking up the subset relationship of an unordered pair. A semiopen neighborhood 𝑈 of a vertex 𝑁 is its open neighborhood together with itself if there is a loop at this vertex. (Contributed by AV, 15-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))}    ⇒   ⊢ (𝑁 ∈ 𝑉 → 𝑈 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 ((𝑛 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒) ∨ (𝑛 = 𝑁 ∧ 𝑒 = {𝑛}))})
Theorem	vopnbgrel 48096*	Characterization of a member 𝑋 of the semiopen neighborhood of a vertex 𝑁 in a graph 𝐺. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))}    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝑉 ∧ ∃𝑒 ∈ 𝐸 ((𝑋 ≠ 𝑁 ∧ 𝑁 ∈ 𝑒 ∧ 𝑋 ∈ 𝑒) ∨ (𝑋 = 𝑁 ∧ 𝑒 = {𝑋})))))
Theorem	vopnbgrelself 48097*	A vertex 𝑁 is a member of its semiopen neighborhood iff there is a loop joining the vertex with itself. (Contributed by AV, 16-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))}    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝑁 ∈ 𝑈 ↔ ∃𝑒 ∈ 𝐸 𝑒 = {𝑁}))
Theorem	dfclnbgr6 48098*	Alternate definition of the closed neighborhood of a vertex as union of the vertex with its semiopen neighborhood. (Contributed by AV, 17-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))}    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 ClNeighbVtx 𝑁) = ({𝑁} ∪ 𝑈))
Theorem	dfnbgr6 48099*	Alternate definition of the (open) neighborhood of a vertex as a difference of its semiopen neighborhood and the singleton of itself. (Contributed by AV, 17-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))}    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝐺 NeighbVtx 𝑁) = (𝑈 ∖ {𝑁}))
Theorem	dfsclnbgr6 48100*	Alternate definition of a semiclosed neighborhood of a vertex as a union of a semiopen neighborhood and the vertex itself if there is a loop at this vertex. (Contributed by AV, 17-May-2025.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝑈 = {𝑛 ∈ 𝑉 ∣ (𝑛 ∈ (𝐺 NeighbVtx 𝑁) ∨ ∃𝑒 ∈ 𝐸 (𝑁 = 𝑛 ∧ 𝑒 = {𝑁}))}    &   ⊢ 𝑆 = {𝑛 ∈ 𝑉 ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}    ⇒   ⊢ (𝑁 ∈ 𝑉 → 𝑆 = (𝑈 ∪ {𝑛 ∈ {𝑁} ∣ ∃𝑒 ∈ 𝐸 𝑛 ∈ 𝑒}))