Definition df-gbo 43935

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

Assertion

Ref	Expression
df-gbo	⊢ GoldbachOdd = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}

Distinct variable group:   𝑧,𝑝,𝑞,𝑟

Detailed syntax breakdown of Definition df-gbo

Step	Hyp	Ref	Expression
1		cgbo 43932	. 2 class GoldbachOdd
2		vp	. . . . . . . . . 10 setvar 𝑝
3	2	cv 1536	. . . . . . . . 9 class 𝑝
4		codd 43810	. . . . . . . . 9 class Odd
5	3, 4	wcel 2114	. . . . . . . 8 wff 𝑝 ∈ Odd
6		vq	. . . . . . . . . 10 setvar 𝑞
7	6	cv 1536	. . . . . . . . 9 class 𝑞
8	7, 4	wcel 2114	. . . . . . . 8 wff 𝑞 ∈ Odd
9		vr	. . . . . . . . . 10 setvar 𝑟
10	9	cv 1536	. . . . . . . . 9 class 𝑟
11	10, 4	wcel 2114	. . . . . . . 8 wff 𝑟 ∈ Odd
12	5, 8, 11	w3a 1083	. . . . . . 7 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd )
13		vz	. . . . . . . . 9 setvar 𝑧
14	13	cv 1536	. . . . . . . 8 class 𝑧
15		caddc 10540	. . . . . . . . . 10 class +
16	3, 7, 15	co 7156	. . . . . . . . 9 class (𝑝 + 𝑞)
17	16, 10, 15	co 7156	. . . . . . . 8 class ((𝑝 + 𝑞) + 𝑟)
18	14, 17	wceq 1537	. . . . . . 7 wff 𝑧 = ((𝑝 + 𝑞) + 𝑟)
19	12, 18	wa 398	. . . . . 6 wff ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
20		cprime 16015	. . . . . 6 class ℙ
21	19, 9, 20	wrex 3139	. . . . 5 wff ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
22	21, 6, 20	wrex 3139	. . . 4 wff ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
23	22, 2, 20	wrex 3139	. . 3 wff ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
24	23, 13, 4	crab 3142	. 2 class {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}
25	1, 24	wceq 1537	1 wff GoldbachOdd = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}

This definition is referenced by:  isgbo  43938  tgoldbachgtALTV  43997