Definition df-gbe 45200

Description: Define the set of (even) Goldbach numbers, which are positive even integers that can be expressed as the sum of two odd primes. By this definition, the binary Goldbach conjecture can be expressed as ∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ). (Contributed by AV, 14-Jun-2020.)

Assertion

Ref	Expression
df-gbe	⊢ GoldbachEven = {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}

Distinct variable group:   𝑧,𝑝,𝑞

Detailed syntax breakdown of Definition df-gbe

Step	Hyp	Ref	Expression
1		cgbe 45197	. 2 class GoldbachEven
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1538	. . . . . . 7 class 𝑝
4		codd 45077	. . . . . . 7 class Odd
5	3, 4	wcel 2106	. . . . . 6 wff 𝑝 ∈ Odd
6		vq	. . . . . . . 8 setvar 𝑞
7	6	cv 1538	. . . . . . 7 class 𝑞
8	7, 4	wcel 2106	. . . . . 6 wff 𝑞 ∈ Odd
9		vz	. . . . . . . 8 setvar 𝑧
10	9	cv 1538	. . . . . . 7 class 𝑧
11		caddc 10874	. . . . . . . 8 class +
12	3, 7, 11	co 7275	. . . . . . 7 class (𝑝 + 𝑞)
13	10, 12	wceq 1539	. . . . . 6 wff 𝑧 = (𝑝 + 𝑞)
14	5, 8, 13	w3a 1086	. . . . 5 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
15		cprime 16376	. . . . 5 class ℙ
16	14, 6, 15	wrex 3065	. . . 4 wff ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
17	16, 2, 15	wrex 3065	. . 3 wff ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
18		ceven 45076	. . 3 class Even
19	17, 9, 18	crab 3068	. 2 class {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}
20	1, 19	wceq 1539	1 wff GoldbachEven = {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}

This definition is referenced by:  isgbe  45203