Metamath Proof Explorer

Theorem gbepos

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

Ref Expression
Assertion gbepos 
|- ( Z e. GoldbachEven -> Z e. NN )

Proof

Step Hyp Ref Expression
1 isgbe 
 |-  ( Z e. GoldbachEven <-> ( Z e. Even /\ E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ Z = ( p + q ) ) ) )
2 prmnn 
 |-  ( p e. Prime -> p e. NN )
3 prmnn 
 |-  ( q e. Prime -> q e. NN )
4 nnaddcl 
 |-  ( ( p e. NN /\ q e. NN ) -> ( p + q ) e. NN )
5 2 3 4 syl2an 
 |-  ( ( p e. Prime /\ q e. Prime ) -> ( p + q ) e. NN )
6 eleq1 
 |-  ( Z = ( p + q ) -> ( Z e. NN <-> ( p + q ) e. NN ) )
7 5 6 imbitrrid 
 |-  ( Z = ( p + q ) -> ( ( p e. Prime /\ q e. Prime ) -> Z e. NN ) )
8 7 3ad2ant3 
 |-  ( ( p e. Odd /\ q e. Odd /\ Z = ( p + q ) ) -> ( ( p e. Prime /\ q e. Prime ) -> Z e. NN ) )
9 8 com12 
 |-  ( ( p e. Prime /\ q e. Prime ) -> ( ( p e. Odd /\ q e. Odd /\ Z = ( p + q ) ) -> Z e. NN ) )
10 9 a1i 
 |-  ( Z e. Even -> ( ( p e. Prime /\ q e. Prime ) -> ( ( p e. Odd /\ q e. Odd /\ Z = ( p + q ) ) -> Z e. NN ) ) )
11 10 rexlimdvv 
 |-  ( Z e. Even -> ( E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ Z = ( p + q ) ) -> Z e. NN ) )
12 11 imp 
 |-  ( ( Z e. Even /\ E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ Z = ( p + q ) ) ) -> Z e. NN )
13 1 12 sylbi 
 |-  ( Z e. GoldbachEven -> Z e. NN )