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=zEven|pqpOddqOddz=p+q

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgbe classGoldbachEven
1 vz setvarz
2 ceven classEven
3 vp setvarp
4 cprime class
5 vq setvarq
6 3 cv setvarp
7 codd classOdd
8 6 7 wcel wffpOdd
9 5 cv setvarq
10 9 7 wcel wffqOdd
11 1 cv setvarz
12 caddc class+
13 6 9 12 co classp+q
14 11 13 wceq wffz=p+q
15 8 10 14 w3a wffpOddqOddz=p+q
16 15 5 4 wrex wffqpOddqOddz=p+q
17 16 3 4 wrex wffpqpOddqOddz=p+q
18 17 1 2 crab classzEven|pqpOddqOddz=p+q
19 0 18 wceq wffGoldbachEven=zEven|pqpOddqOddz=p+q