Metamath Proof Explorer

Theorem 11gbo

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

Ref Expression
Assertion 11gbo 
|- ; 1 1 e. GoldbachOdd

Proof

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