Metamath Proof Explorer


Theorem 9gbo

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

Ref Expression
Assertion 9gbo 9 GoldbachOdd

Proof

Step Hyp Ref Expression
1 df-9 9 = 8 + 1
2 8even 8 Even
3 evenp1odd 8 Even 8 + 1 Odd
4 2 3 ax-mp 8 + 1 Odd
5 1 4 eqeltri 9 Odd
6 3prm 3
7 3odd 3 Odd
8 7 7 7 3pm3.2i 3 Odd 3 Odd 3 Odd
9 gbpart9 9 = 3 + 3 + 3
10 8 9 pm3.2i 3 Odd 3 Odd 3 Odd 9 = 3 + 3 + 3
11 eleq1 r = 3 r Odd 3 Odd
12 11 3anbi3d r = 3 3 Odd 3 Odd r Odd 3 Odd 3 Odd 3 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 Odd 3 Odd r Odd 9 = 3 + 3 + r 3 Odd 3 Odd 3 Odd 9 = 3 + 3 + 3
16 15 rspcev 3 3 Odd 3 Odd 3 Odd 9 = 3 + 3 + 3 r 3 Odd 3 Odd r Odd 9 = 3 + 3 + r
17 6 10 16 mp2an r 3 Odd 3 Odd r Odd 9 = 3 + 3 + r
18 eleq1 p = 3 p Odd 3 Odd
19 18 3anbi1d p = 3 p Odd q Odd r Odd 3 Odd q Odd r 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 Odd q Odd r Odd 9 = p + q + r 3 Odd q Odd r Odd 9 = 3 + q + r
24 23 rexbidv p = 3 r p Odd q Odd r Odd 9 = p + q + r r 3 Odd q Odd r Odd 9 = 3 + q + r
25 eleq1 q = 3 q Odd 3 Odd
26 25 3anbi2d q = 3 3 Odd q Odd r Odd 3 Odd 3 Odd r 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 Odd q Odd r Odd 9 = 3 + q + r 3 Odd 3 Odd r Odd 9 = 3 + 3 + r
31 30 rexbidv q = 3 r 3 Odd q Odd r Odd 9 = 3 + q + r r 3 Odd 3 Odd r Odd 9 = 3 + 3 + r
32 24 31 rspc2ev 3 3 r 3 Odd 3 Odd r Odd 9 = 3 + 3 + r p q r p Odd q Odd r Odd 9 = p + q + r
33 6 6 17 32 mp3an p q r p Odd q Odd r Odd 9 = p + q + r
34 isgbo 9 GoldbachOdd 9 Odd p q r p Odd q Odd r Odd 9 = p + q + r
35 5 33 34 mpbir2an 9 GoldbachOdd