Metamath Proof Explorer

Theorem gbowpos

Description: Any weak odd Goldbach number is positive. (Contributed by AV, 20-Jul-2020)

Ref Expression
Assertion gbowpos 
|- ( Z e. GoldbachOddW -> Z e. NN )

Proof

Step Hyp Ref Expression
1 isgbow 
 |-  ( Z e. GoldbachOddW <-> ( Z e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime Z = ( ( p + q ) + r ) ) )
2 prmnn 
 |-  ( p e. Prime -> p e. NN )
3 prmnn 
 |-  ( q e. Prime -> q e. NN )
4 2 3 anim12i 
 |-  ( ( p e. Prime /\ q e. Prime ) -> ( p e. NN /\ q e. NN ) )
5 4 adantr 
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> ( p e. NN /\ q e. NN ) )
6 nnaddcl 
 |-  ( ( p e. NN /\ q e. NN ) -> ( p + q ) e. NN )
7 5 6 syl 
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> ( p + q ) e. NN )
8 prmnn 
 |-  ( r e. Prime -> r e. NN )
9 8 adantl 
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> r e. NN )
10 7 9 nnaddcld 
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> ( ( p + q ) + r ) e. NN )
11 eleq1 
 |-  ( Z = ( ( p + q ) + r ) -> ( Z e. NN <-> ( ( p + q ) + r ) e. NN ) )
12 10 11 syl5ibrcom 
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> ( Z = ( ( p + q ) + r ) -> Z e. NN ) )
13 12 rexlimdva 
 |-  ( ( p e. Prime /\ q e. Prime ) -> ( E. r e. Prime Z = ( ( p + q ) + r ) -> Z e. NN ) )
14 13 a1i 
 |-  ( Z e. Odd -> ( ( p e. Prime /\ q e. Prime ) -> ( E. r e. Prime Z = ( ( p + q ) + r ) -> Z e. NN ) ) )
15 14 rexlimdvv 
 |-  ( Z e. Odd -> ( E. p e. Prime E. q e. Prime E. r e. Prime Z = ( ( p + q ) + r ) -> Z e. NN ) )
16 15 imp 
 |-  ( ( Z e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime Z = ( ( p + q ) + r ) ) -> Z e. NN )
17 1 16 sylbi 
 |-  ( Z e. GoldbachOddW -> Z e. NN )