Definition df-gbo 47090

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 47087	. 2 class GoldbachOdd
2		vp	. . . . . . . . . 10 setvar 𝑝
3	2	cv 1533	. . . . . . . . 9 class 𝑝
4		codd 46965	. . . . . . . . 9 class Odd
5	3, 4	wcel 2099	. . . . . . . 8 wff 𝑝 ∈ Odd
6		vq	. . . . . . . . . 10 setvar 𝑞
7	6	cv 1533	. . . . . . . . 9 class 𝑞
8	7, 4	wcel 2099	. . . . . . . 8 wff 𝑞 ∈ Odd
9		vr	. . . . . . . . . 10 setvar 𝑟
10	9	cv 1533	. . . . . . . . 9 class 𝑟
11	10, 4	wcel 2099	. . . . . . . 8 wff 𝑟 ∈ Odd
12	5, 8, 11	w3a 1085	. . . . . . 7 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd )
13		vz	. . . . . . . . 9 setvar 𝑧
14	13	cv 1533	. . . . . . . 8 class 𝑧
15		caddc 11142	. . . . . . . . . 10 class +
16	3, 7, 15	co 7420	. . . . . . . . 9 class (𝑝 + 𝑞)
17	16, 10, 15	co 7420	. . . . . . . 8 class ((𝑝 + 𝑞) + 𝑟)
18	14, 17	wceq 1534	. . . . . . 7 wff 𝑧 = ((𝑝 + 𝑞) + 𝑟)
19	12, 18	wa 395	. . . . . 6 wff ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
20		cprime 16642	. . . . . 6 class ℙ
21	19, 9, 20	wrex 3067	. . . . 5 wff ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
22	21, 6, 20	wrex 3067	. . . 4 wff ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
23	22, 2, 20	wrex 3067	. . 3 wff ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
24	23, 13, 4	crab 3429	. 2 class {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}
25	1, 24	wceq 1534	1 wff GoldbachOdd = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}

This definition is referenced by:  isgbo  47093  tgoldbachgtALTV  47152