Metamath Proof Explorer

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 = z ∈ Even | ∃ p ∈ ℙ ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ z = p + q

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgbe class GoldbachEven
1 vz setvar z
2 ceven class Even
3 vp setvar p
4 cprime class ℙ
5 vq setvar q
6 3 cv setvar p
7 codd class Odd
8 6 7 wcel wff p ∈ Odd
9 5 cv setvar q
10 9 7 wcel wff q ∈ Odd
11 1 cv setvar z
12 caddc class +
13 6 9 12 co class p + q
14 11 13 wceq wff z = p + q
15 8 10 14 w3a wff p ∈ Odd ∧ q ∈ Odd ∧ z = p + q
16 15 5 4 wrex wff ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ z = p + q
17 16 3 4 wrex wff ∃ p ∈ ℙ ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ z = p + q
18 17 1 2 crab class z ∈ Even | ∃ p ∈ ℙ ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ z = p + q
19 0 18 wceq wff GoldbachEven = z ∈ Even | ∃ p ∈ ℙ ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ z = p + q