Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Number theory (extension 2)
Goldbach's conjectures
df-gbow
Metamath Proof Explorer
Description: Define the set of weak odd Goldbach numbers, which are positive odd
integers that can be expressed as the sum of three primes. By this
definition, the weak ternary Goldbach conjecture can be expressed as
A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) . (Contributed by AV , 14-Jun-2020)
Ref
Expression
Assertion
df-gbow
|- GoldbachOddW = { z e. Odd | E. p e. Prime E. q e. Prime E. r e. Prime z = ( ( p + q ) + r ) }
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cgbow
|- GoldbachOddW
1
vz
|- z
2
codd
|- Odd
3
vp
|- p
4
cprime
|- Prime
5
vq
|- q
6
vr
|- r
7
1
cv
|- z
8
3
cv
|- p
9
caddc
|- +
10
5
cv
|- q
11
8 10 9
co
|- ( p + q )
12
6
cv
|- r
13
11 12 9
co
|- ( ( p + q ) + r )
14
7 13
wceq
|- z = ( ( p + q ) + r )
15
14 6 4
wrex
|- E. r e. Prime z = ( ( p + q ) + r )
16
15 5 4
wrex
|- E. q e. Prime E. r e. Prime z = ( ( p + q ) + r )
17
16 3 4
wrex
|- E. p e. Prime E. q e. Prime E. r e. Prime z = ( ( p + q ) + r )
18
17 1 2
crab
|- { z e. Odd | E. p e. Prime E. q e. Prime E. r e. Prime z = ( ( p + q ) + r ) }
19
0 18
wceq
|- GoldbachOddW = { z e. Odd | E. p e. Prime E. q e. Prime E. r e. Prime z = ( ( p + q ) + r ) }