Definition df-gbo 41638

Description: Define the set of (strong) odd Goldbach numbers, which are positive odd integers that can be expressed as the sum of three odd primes. By this definition, the strong ternary Goldbach conjecture can be expressed as A. m e. Odd ( 7 < m -> m e. GoldbachOdd ). (Contributed by AV, 26-Jul-2020.)

Assertion

Ref	Expression
df-gbo	|- GoldbachOdd = { z e. Odd | E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ z = ( ( p + q ) + r ) ) }

Distinct variable group:   z, p, q, r

Detailed syntax breakdown of Definition df-gbo

Step	Hyp	Ref	Expression
1		cgbo 41635	. 2 class GoldbachOdd
2		vp	. . . . . . . . . 10 setvar p
3	2	cv 1482	. . . . . . . . 9 class p
4		codd 41538	. . . . . . . . 9 class Odd
5	3, 4	wcel 1990	. . . . . . . 8 wff p e. Odd
6		vq	. . . . . . . . . 10 setvar q
7	6	cv 1482	. . . . . . . . 9 class q
8	7, 4	wcel 1990	. . . . . . . 8 wff q e. Odd
9		vr	. . . . . . . . . 10 setvar r
10	9	cv 1482	. . . . . . . . 9 class r
11	10, 4	wcel 1990	. . . . . . . 8 wff r e. Odd
12	5, 8, 11	w3a 1037	. . . . . . 7 wff ( p e. Odd /\ q e. Odd /\ r e. Odd )
13		vz	. . . . . . . . 9 setvar z
14	13	cv 1482	. . . . . . . 8 class z
15		caddc 9939	. . . . . . . . . 10 class +
16	3, 7, 15	co 6650	. . . . . . . . 9 class ( p + q )
17	16, 10, 15	co 6650	. . . . . . . 8 class ( ( p + q ) + r )
18	14, 17	wceq 1483	. . . . . . 7 wff z = ( ( p + q ) + r )
19	12, 18	wa 384	. . . . . 6 wff ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ z = ( ( p + q ) + r ) )
20		cprime 15385	. . . . . 6 class Prime
21	19, 9, 20	wrex 2913	. . . . 5 wff E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ z = ( ( p + q ) + r ) )
22	21, 6, 20	wrex 2913	. . . 4 wff E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ z = ( ( p + q ) + r ) )
23	22, 2, 20	wrex 2913	. . 3 wff E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ z = ( ( p + q ) + r ) )
24	23, 13, 4	crab 2916	. 2 class { z e. Odd | E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ z = ( ( p + q ) + r ) ) }
25	1, 24	wceq 1483	1 wff GoldbachOdd = { z e. Odd | E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ z = ( ( p + q ) + r ) ) }

This definition is referenced by:  isgbo  41641  tgoldbachgtALTV  41700