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