Definition df-gbow 48514

Description: Define the set of weak odd Goldbach numbers, which are positive odd integers that can be expressed as the sum of three primes. By this definition, the weak ternary Goldbach conjecture can be expressed as ∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ). (Contributed by AV, 14-Jun-2020.)

Assertion

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

Distinct variable group:   𝑧,𝑝,𝑞,𝑟

Detailed syntax breakdown of Definition df-gbow

Step	Hyp	Ref	Expression
1		cgbow 48511	. 2 class GoldbachOddW
2		vz	. . . . . . . 8 setvar 𝑧
3	2	cv 1569	. . . . . . 7 class 𝑧
4		vp	. . . . . . . . . 10 setvar 𝑝
5	4	cv 1569	. . . . . . . . 9 class 𝑝
6		vq	. . . . . . . . . 10 setvar 𝑞
7	6	cv 1569	. . . . . . . . 9 class 𝑞
8		caddc 11098	. . . . . . . . 9 class +
9	5, 7, 8	co 7410	. . . . . . . 8 class (𝑝 + 𝑞)
10		vr	. . . . . . . . 9 setvar 𝑟
11	10	cv 1569	. . . . . . . 8 class 𝑟
12	9, 11, 8	co 7410	. . . . . . 7 class ((𝑝 + 𝑞) + 𝑟)
13	3, 12	wceq 1570	. . . . . 6 wff 𝑧 = ((𝑝 + 𝑞) + 𝑟)
14		cprime 16724	. . . . . 6 class ℙ
15	13, 10, 14	wrex 3089	. . . . 5 wff ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)
16	15, 6, 14	wrex 3089	. . . 4 wff ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)
17	16, 4, 14	wrex 3089	. . 3 wff ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)
18		codd 48390	. . 3 class Odd
19	17, 2, 18	crab 3416	. 2 class {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)}
20	1, 19	wceq 1570	1 wff GoldbachOddW = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)}

This definition is referenced by:  isgbow  48517