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