Definition df-gbo 48403

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 48400	. 2 class GoldbachOdd
2		vp	. . . . . . . . . 10 setvar 𝑝
3	2	cv 1566	. . . . . . . . 9 class 𝑝
4		codd 48278	. . . . . . . . 9 class Odd
5	3, 4	wcel 2149	. . . . . . . 8 wff 𝑝 ∈ Odd
6		vq	. . . . . . . . . 10 setvar 𝑞
7	6	cv 1566	. . . . . . . . 9 class 𝑞
8	7, 4	wcel 2149	. . . . . . . 8 wff 𝑞 ∈ Odd
9		vr	. . . . . . . . . 10 setvar 𝑟
10	9	cv 1566	. . . . . . . . 9 class 𝑟
11	10, 4	wcel 2149	. . . . . . . 8 wff 𝑟 ∈ Odd
12	5, 8, 11	w3a 1101	. . . . . . 7 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd )
13		vz	. . . . . . . . 9 setvar 𝑧
14	13	cv 1566	. . . . . . . 8 class 𝑧
15		caddc 11102	. . . . . . . . . 10 class +
16	3, 7, 15	co 7411	. . . . . . . . 9 class (𝑝 + 𝑞)
17	16, 10, 15	co 7411	. . . . . . . 8 class ((𝑝 + 𝑞) + 𝑟)
18	14, 17	wceq 1567	. . . . . . 7 wff 𝑧 = ((𝑝 + 𝑞) + 𝑟)
19	12, 18	wa 400	. . . . . 6 wff ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
20		cprime 16728	. . . . . 6 class ℙ
21	19, 9, 20	wrex 3095	. . . . 5 wff ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
22	21, 6, 20	wrex 3095	. . . 4 wff ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
23	22, 2, 20	wrex 3095	. . 3 wff ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
24	23, 13, 4	crab 3423	. 2 class {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}
25	1, 24	wceq 1567	1 wff GoldbachOdd = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}

This definition is referenced by:  isgbo  48406  tgoldbachgtALTV  48465