Metamath Proof Explorer


Theorem 11gbo

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

Ref Expression
Assertion 11gbo 11 GoldbachOdd

Proof

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