Definition df-gbe 41636

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.)

Assertion

Ref	Expression
df-gbe	|- GoldbachEven = { z e. Even | E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ z = ( p + q ) ) }

Distinct variable group:   z, p, q

Detailed syntax breakdown of Definition df-gbe

Step	Hyp	Ref	Expression
1		cgbe 41633	. 2 class GoldbachEven
2		vp	. . . . . . . 8 setvar p
3	2	cv 1482	. . . . . . 7 class p
4		codd 41538	. . . . . . 7 class Odd
5	3, 4	wcel 1990	. . . . . 6 wff p e. Odd
6		vq	. . . . . . . 8 setvar q
7	6	cv 1482	. . . . . . 7 class q
8	7, 4	wcel 1990	. . . . . 6 wff q e. Odd
9		vz	. . . . . . . 8 setvar z
10	9	cv 1482	. . . . . . 7 class z
11		caddc 9939	. . . . . . . 8 class +
12	3, 7, 11	co 6650	. . . . . . 7 class ( p + q )
13	10, 12	wceq 1483	. . . . . 6 wff z = ( p + q )
14	5, 8, 13	w3a 1037	. . . . 5 wff ( p e. Odd /\ q e. Odd /\ z = ( p + q ) )
15		cprime 15385	. . . . 5 class Prime
16	14, 6, 15	wrex 2913	. . . 4 wff E. q e. Prime ( p e. Odd /\ q e. Odd /\ z = ( p + q ) )
17	16, 2, 15	wrex 2913	. . 3 wff E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ z = ( p + q ) )
18		ceven 41537	. . 3 class Even
19	17, 9, 18	crab 2916	. 2 class { z e. Even | E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ z = ( p + q ) ) }
20	1, 19	wceq 1483	1 wff GoldbachEven = { z e. Even | E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ z = ( p + q ) ) }

This definition is referenced by:  isgbe  41639