Metamath Proof Explorer

Theorem 9gbo

Description: 9 is an odd Goldbach number. (Contributed by AV, 26-Jul-2020)

Ref Expression
Assertion 9gbo 
|- 9 e. GoldbachOdd

Proof

Step Hyp Ref Expression
1 df-9 
 |-  9 = ( 8 + 1 )
2 8even 
 |-  8 e. Even
3 evenp1odd 
 |-  ( 8 e. Even -> ( 8 + 1 ) e. Odd )
4 2 3 ax-mp 
 |-  ( 8 + 1 ) e. Odd
5 1 4 eqeltri 
 |-  9 e. Odd
6 3prm 
 |-  3 e. Prime
7 3odd 
 |-  3 e. Odd
8 7 7 7 3pm3.2i 
 |-  ( 3 e. Odd /\ 3 e. Odd /\ 3 e. Odd )
9 gbpart9 
 |-  9 = ( ( 3 + 3 ) + 3 )
10 8 9 pm3.2i 
 |-  ( ( 3 e. Odd /\ 3 e. Odd /\ 3 e. Odd ) /\ 9 = ( ( 3 + 3 ) + 3 ) )
11 eleq1 
 |-  ( r = 3 -> ( r e. Odd <-> 3 e. Odd ) )
12 11 3anbi3d 
 |-  ( r = 3 -> ( ( 3 e. Odd /\ 3 e. Odd /\ r e. Odd ) <-> ( 3 e. Odd /\ 3 e. Odd /\ 3 e. Odd ) ) )
13 oveq2 
 |-  ( r = 3 -> ( ( 3 + 3 ) + r ) = ( ( 3 + 3 ) + 3 ) )
14 13 eqeq2d 
 |-  ( r = 3 -> ( 9 = ( ( 3 + 3 ) + r ) <-> 9 = ( ( 3 + 3 ) + 3 ) ) )
15 12 14 anbi12d 
 |-  ( r = 3 -> ( ( ( 3 e. Odd /\ 3 e. Odd /\ r e. Odd ) /\ 9 = ( ( 3 + 3 ) + r ) ) <-> ( ( 3 e. Odd /\ 3 e. Odd /\ 3 e. Odd ) /\ 9 = ( ( 3 + 3 ) + 3 ) ) ) )
16 15 rspcev 
 |-  ( ( 3 e. Prime /\ ( ( 3 e. Odd /\ 3 e. Odd /\ 3 e. Odd ) /\ 9 = ( ( 3 + 3 ) + 3 ) ) ) -> E. r e. Prime ( ( 3 e. Odd /\ 3 e. Odd /\ r e. Odd ) /\ 9 = ( ( 3 + 3 ) + r ) ) )
17 6 10 16 mp2an 
 |-  E. r e. Prime ( ( 3 e. Odd /\ 3 e. Odd /\ r e. Odd ) /\ 9 = ( ( 3 + 3 ) + r ) )
18 eleq1 
 |-  ( p = 3 -> ( p e. Odd <-> 3 e. Odd ) )
19 18 3anbi1d 
 |-  ( p = 3 -> ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) <-> ( 3 e. Odd /\ q e. Odd /\ r e. Odd ) ) )
20 oveq1 
 |-  ( p = 3 -> ( p + q ) = ( 3 + q ) )
21 20 oveq1d 
 |-  ( p = 3 -> ( ( p + q ) + r ) = ( ( 3 + q ) + r ) )
22 21 eqeq2d 
 |-  ( p = 3 -> ( 9 = ( ( p + q ) + r ) <-> 9 = ( ( 3 + q ) + r ) ) )
23 19 22 anbi12d 
 |-  ( p = 3 -> ( ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ 9 = ( ( p + q ) + r ) ) <-> ( ( 3 e. Odd /\ q e. Odd /\ r e. Odd ) /\ 9 = ( ( 3 + q ) + r ) ) ) )
24 23 rexbidv 
 |-  ( p = 3 -> ( E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ 9 = ( ( p + q ) + r ) ) <-> E. r e. Prime ( ( 3 e. Odd /\ q e. Odd /\ r e. Odd ) /\ 9 = ( ( 3 + q ) + r ) ) ) )
25 eleq1 
 |-  ( q = 3 -> ( q e. Odd <-> 3 e. Odd ) )
26 25 3anbi2d 
 |-  ( q = 3 -> ( ( 3 e. Odd /\ q e. Odd /\ r e. Odd ) <-> ( 3 e. Odd /\ 3 e. Odd /\ r e. Odd ) ) )
27 oveq2 
 |-  ( q = 3 -> ( 3 + q ) = ( 3 + 3 ) )
28 27 oveq1d 
 |-  ( q = 3 -> ( ( 3 + q ) + r ) = ( ( 3 + 3 ) + r ) )
29 28 eqeq2d 
 |-  ( q = 3 -> ( 9 = ( ( 3 + q ) + r ) <-> 9 = ( ( 3 + 3 ) + r ) ) )
30 26 29 anbi12d 
 |-  ( q = 3 -> ( ( ( 3 e. Odd /\ q e. Odd /\ r e. Odd ) /\ 9 = ( ( 3 + q ) + r ) ) <-> ( ( 3 e. Odd /\ 3 e. Odd /\ r e. Odd ) /\ 9 = ( ( 3 + 3 ) + r ) ) ) )
31 30 rexbidv 
 |-  ( q = 3 -> ( E. r e. Prime ( ( 3 e. Odd /\ q e. Odd /\ r e. Odd ) /\ 9 = ( ( 3 + q ) + r ) ) <-> E. r e. Prime ( ( 3 e. Odd /\ 3 e. Odd /\ r e. Odd ) /\ 9 = ( ( 3 + 3 ) + r ) ) ) )
32 24 31 rspc2ev 
 |-  ( ( 3 e. Prime /\ 3 e. Prime /\ E. r e. Prime ( ( 3 e. Odd /\ 3 e. Odd /\ r e. Odd ) /\ 9 = ( ( 3 + 3 ) + r ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ 9 = ( ( p + q ) + r ) ) )
33 6 6 17 32 mp3an 
 |-  E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ 9 = ( ( p + q ) + r ) )
34 isgbo 
 |-  ( 9 e. GoldbachOdd <-> ( 9 e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ 9 = ( ( p + q ) + r ) ) ) )
35 5 33 34 mpbir2an 
 |-  9 e. GoldbachOdd