This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 11gbo

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

Ref Expression
Assertion 11gbo 1 1 ∈ GoldbachOdd

Proof

Step Hyp Ref Expression
1 6p5e11 ⊢ ( 6 + 5 ) = 1 1
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 ⊢ 1 1 ∈ 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 ⊢ 1 1 = ( ( 3 + 3 ) + 5 )
12 10 11 pm3.2i ⊢ ( ( 3 ∈ Odd ∧ 3 ∈ Odd ∧ 5 ∈ Odd ) ∧ 1 1 = ( ( 3 + 3 ) + 5 ) )
13 eleq1 ⊢ ( 𝑟 = 5 → ( 𝑟 ∈ Odd ↔ 5 ∈ Odd ) )
14 13 3anbi3d ⊢ ( 𝑟 = 5 → ( ( 3 ∈ Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd ) ↔ ( 3 ∈ Odd ∧ 3 ∈ Odd ∧ 5 ∈ Odd ) ) )
15 oveq2 ⊢ ( 𝑟 = 5 → ( ( 3 + 3 ) + 𝑟 ) = ( ( 3 + 3 ) + 5 ) )
16 15 eqeq2d ⊢ ( 𝑟 = 5 → ( 1 1 = ( ( 3 + 3 ) + 𝑟 ) ↔ 1 1 = ( ( 3 + 3 ) + 5 ) ) )
17 14 16 anbi12d ⊢ ( 𝑟 = 5 → ( ( ( 3 ∈ Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 1 1 = ( ( 3 + 3 ) + 𝑟 ) ) ↔ ( ( 3 ∈ Odd ∧ 3 ∈ Odd ∧ 5 ∈ Odd ) ∧ 1 1 = ( ( 3 + 3 ) + 5 ) ) ) )
18 17 rspcev ⊢ ( ( 5 ∈ ℙ ∧ ( ( 3 ∈ Odd ∧ 3 ∈ Odd ∧ 5 ∈ Odd ) ∧ 1 1 = ( ( 3 + 3 ) + 5 ) ) ) → ∃ 𝑟 ∈ ℙ ( ( 3 ∈ Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 1 1 = ( ( 3 + 3 ) + 𝑟 ) ) )
19 8 12 18 mp2an ⊢ ∃ 𝑟 ∈ ℙ ( ( 3 ∈ Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 1 1 = ( ( 3 + 3 ) + 𝑟 ) )
20 eleq1 ⊢ ( 𝑝 = 3 → ( 𝑝 ∈ Odd ↔ 3 ∈ Odd ) )
21 20 3anbi1d ⊢ ( 𝑝 = 3 → ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ↔ ( 3 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ) )
22 oveq1 ⊢ ( 𝑝 = 3 → ( 𝑝 + 𝑞 ) = ( 3 + 𝑞 ) )
23 22 oveq1d ⊢ ( 𝑝 = 3 → ( ( 𝑝 + 𝑞 ) + 𝑟 ) = ( ( 3 + 𝑞 ) + 𝑟 ) )
24 23 eqeq2d ⊢ ( 𝑝 = 3 → ( 1 1 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ 1 1 = ( ( 3 + 𝑞 ) + 𝑟 ) ) )
25 21 24 anbi12d ⊢ ( 𝑝 = 3 → ( ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 1 1 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ↔ ( ( 3 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 1 1 = ( ( 3 + 𝑞 ) + 𝑟 ) ) ) )
26 25 rexbidv ⊢ ( 𝑝 = 3 → ( ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 1 1 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ↔ ∃ 𝑟 ∈ ℙ ( ( 3 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 1 1 = ( ( 3 + 𝑞 ) + 𝑟 ) ) ) )
27 eleq1 ⊢ ( 𝑞 = 3 → ( 𝑞 ∈ Odd ↔ 3 ∈ Odd ) )
28 27 3anbi2d ⊢ ( 𝑞 = 3 → ( ( 3 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ↔ ( 3 ∈ Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd ) ) )
29 oveq2 ⊢ ( 𝑞 = 3 → ( 3 + 𝑞 ) = ( 3 + 3 ) )
30 29 oveq1d ⊢ ( 𝑞 = 3 → ( ( 3 + 𝑞 ) + 𝑟 ) = ( ( 3 + 3 ) + 𝑟 ) )
31 30 eqeq2d ⊢ ( 𝑞 = 3 → ( 1 1 = ( ( 3 + 𝑞 ) + 𝑟 ) ↔ 1 1 = ( ( 3 + 3 ) + 𝑟 ) ) )
32 28 31 anbi12d ⊢ ( 𝑞 = 3 → ( ( ( 3 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 1 1 = ( ( 3 + 𝑞 ) + 𝑟 ) ) ↔ ( ( 3 ∈ Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 1 1 = ( ( 3 + 3 ) + 𝑟 ) ) ) )
33 32 rexbidv ⊢ ( 𝑞 = 3 → ( ∃ 𝑟 ∈ ℙ ( ( 3 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 1 1 = ( ( 3 + 𝑞 ) + 𝑟 ) ) ↔ ∃ 𝑟 ∈ ℙ ( ( 3 ∈ Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 1 1 = ( ( 3 + 3 ) + 𝑟 ) ) ) )
34 26 33 rspc2ev ⊢ ( ( 3 ∈ ℙ ∧ 3 ∈ ℙ ∧ ∃ 𝑟 ∈ ℙ ( ( 3 ∈ Odd ∧ 3 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 1 1 = ( ( 3 + 3 ) + 𝑟 ) ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 1 1 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
35 7 7 19 34 mp3an ⊢ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 1 1 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
36 isgbo ⊢ ( 1 1 ∈ GoldbachOdd ↔ ( 1 1 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 1 1 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
37 6 35 36 mpbir2an ⊢ 1 1 ∈ GoldbachOdd