Metamath Proof Explorer

Theorem 6gbe

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

Ref Expression
Assertion 6gbe 
|- 6 e. GoldbachEven

Proof

Step Hyp Ref Expression
1 6even 
 |-  6 e. Even
2 3prm 
 |-  3 e. Prime
3 3odd 
 |-  3 e. Odd
4 gbpart6 
 |-  6 = ( 3 + 3 )
5 3 3 4 3pm3.2i 
 |-  ( 3 e. Odd /\ 3 e. Odd /\ 6 = ( 3 + 3 ) )
6 eleq1 
 |-  ( p = 3 -> ( p e. Odd <-> 3 e. Odd ) )
7 biidd 
 |-  ( p = 3 -> ( q e. Odd <-> q e. Odd ) )
8 oveq1 
 |-  ( p = 3 -> ( p + q ) = ( 3 + q ) )
9 8 eqeq2d 
 |-  ( p = 3 -> ( 6 = ( p + q ) <-> 6 = ( 3 + q ) ) )
10 6 7 9 3anbi123d 
 |-  ( p = 3 -> ( ( p e. Odd /\ q e. Odd /\ 6 = ( p + q ) ) <-> ( 3 e. Odd /\ q e. Odd /\ 6 = ( 3 + q ) ) ) )
11 biidd 
 |-  ( q = 3 -> ( 3 e. Odd <-> 3 e. Odd ) )
12 eleq1 
 |-  ( q = 3 -> ( q e. Odd <-> 3 e. Odd ) )
13 oveq2 
 |-  ( q = 3 -> ( 3 + q ) = ( 3 + 3 ) )
14 13 eqeq2d 
 |-  ( q = 3 -> ( 6 = ( 3 + q ) <-> 6 = ( 3 + 3 ) ) )
15 11 12 14 3anbi123d 
 |-  ( q = 3 -> ( ( 3 e. Odd /\ q e. Odd /\ 6 = ( 3 + q ) ) <-> ( 3 e. Odd /\ 3 e. Odd /\ 6 = ( 3 + 3 ) ) ) )
16 10 15 rspc2ev 
 |-  ( ( 3 e. Prime /\ 3 e. Prime /\ ( 3 e. Odd /\ 3 e. Odd /\ 6 = ( 3 + 3 ) ) ) -> E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ 6 = ( p + q ) ) )
17 2 2 5 16 mp3an 
 |-  E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ 6 = ( p + q ) )
18 isgbe 
 |-  ( 6 e. GoldbachEven <-> ( 6 e. Even /\ E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ 6 = ( p + q ) ) ) )
19 1 17 18 mpbir2an 
 |-  6 e. GoldbachEven