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