Definition df-gbe 47735

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 47732	. 2 class GoldbachEven
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1539	. . . . . . 7 class 𝑝
4		codd 47612	. . . . . . 7 class Odd
5	3, 4	wcel 2108	. . . . . 6 wff 𝑝 ∈ Odd
6		vq	. . . . . . . 8 setvar 𝑞
7	6	cv 1539	. . . . . . 7 class 𝑞
8	7, 4	wcel 2108	. . . . . 6 wff 𝑞 ∈ Odd
9		vz	. . . . . . . 8 setvar 𝑧
10	9	cv 1539	. . . . . . 7 class 𝑧
11		caddc 11158	. . . . . . . 8 class +
12	3, 7, 11	co 7431	. . . . . . 7 class (𝑝 + 𝑞)
13	10, 12	wceq 1540	. . . . . 6 wff 𝑧 = (𝑝 + 𝑞)
14	5, 8, 13	w3a 1087	. . . . 5 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
15		cprime 16708	. . . . 5 class ℙ
16	14, 6, 15	wrex 3070	. . . 4 wff ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
17	16, 2, 15	wrex 3070	. . 3 wff ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
18		ceven 47611	. . 3 class Even
19	17, 9, 18	crab 3436	. 2 class {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}
20	1, 19	wceq 1540	1 wff GoldbachEven = {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}

This definition is referenced by:  isgbe  47738