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