Metamath Proof Explorer

Theorem 8gbe

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

Ref Expression
Assertion 8gbe 
|- 8 e. GoldbachEven

Proof

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