Definition df-gbo 48573

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 48570	. 2 class GoldbachOdd
2		vp	. . . . . . . . . 10 setvar 𝑝
3	2	cv 1569	. . . . . . . . 9 class 𝑝
4		codd 48448	. . . . . . . . 9 class Odd
5	3, 4	wcel 2146	. . . . . . . 8 wff 𝑝 ∈ Odd
6		vq	. . . . . . . . . 10 setvar 𝑞
7	6	cv 1569	. . . . . . . . 9 class 𝑞
8	7, 4	wcel 2146	. . . . . . . 8 wff 𝑞 ∈ Odd
9		vr	. . . . . . . . . 10 setvar 𝑟
10	9	cv 1569	. . . . . . . . 9 class 𝑟
11	10, 4	wcel 2146	. . . . . . . 8 wff 𝑟 ∈ Odd
12	5, 8, 11	w3a 1103	. . . . . . 7 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd )
13		vz	. . . . . . . . 9 setvar 𝑧
14	13	cv 1569	. . . . . . . 8 class 𝑧
15		caddc 11118	. . . . . . . . . 10 class +
16	3, 7, 15	co 7419	. . . . . . . . 9 class (𝑝 + 𝑞)
17	16, 10, 15	co 7419	. . . . . . . 8 class ((𝑝 + 𝑞) + 𝑟)
18	14, 17	wceq 1570	. . . . . . 7 wff 𝑧 = ((𝑝 + 𝑞) + 𝑟)
19	12, 18	wa 401	. . . . . 6 wff ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
20		cprime 16751	. . . . . 6 class ℙ
21	19, 9, 20	wrex 3091	. . . . 5 wff ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
22	21, 6, 20	wrex 3091	. . . 4 wff ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
23	22, 2, 20	wrex 3091	. . 3 wff ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
24	23, 13, 4	crab 3418	. 2 class {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}
25	1, 24	wceq 1570	1 wff GoldbachOdd = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}

This definition is used by:  isgbo  48576  tgoldbachgtALTV  48635