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