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