Definition df-gbe

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 A. n e. Even ( 4 < n -> n e. GoldbachEven ) . (Contributed by AV, 14-Jun-2020)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgbe	⊢ GoldbachEven
1		vz	⊢ 𝑧
2		ceven	⊢ Even
3		vp	⊢ 𝑝
4		cprime	⊢ ℙ
5		vq	⊢ 𝑞
6	3	cv	⊢ 𝑝
7		codd	⊢ Odd
8	6 7	wcel	⊢ 𝑝 ∈ Odd
9	5	cv	⊢ 𝑞
10	9 7	wcel	⊢ 𝑞 ∈ Odd
11	1	cv	⊢ 𝑧
12		caddc	⊢ +
13	6 9 12	co	⊢ ( 𝑝 + 𝑞 )
14	11 13	wceq	⊢ 𝑧 = ( 𝑝 + 𝑞 )
15	8 10 14	w3a	⊢ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = ( 𝑝 + 𝑞 ) )
16	15 5 4	wrex	⊢ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = ( 𝑝 + 𝑞 ) )
17	16 3 4	wrex	⊢ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = ( 𝑝 + 𝑞 ) )
18	17 1 2	crab	⊢ { 𝑧 ∈ Even ∣ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = ( 𝑝 + 𝑞 ) ) }
19	0 18	wceq	⊢ GoldbachEven = { 𝑧 ∈ Even ∣ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = ( 𝑝 + 𝑞 ) ) }