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