Metamath Proof Explorer

Theorem gboge9

Description: Any odd Goldbach number is greater than or equal to 9. Because of 9gbo , this bound is strict. (Contributed by AV, 26-Jul-2020)

Ref Expression
Assertion gboge9 ( 𝑍 ∈ GoldbachOdd → 9 ≤ 𝑍 )

Proof

Step Hyp Ref Expression
1 isgbo ⊢ ( 𝑍 ∈ GoldbachOdd ↔ ( 𝑍 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
2 df-3an ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ ) ↔ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) )
3 an6 ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ) ↔ ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∈ Odd ) ∧ ( 𝑞 ∈ ℙ ∧ 𝑞 ∈ Odd ) ∧ ( 𝑟 ∈ ℙ ∧ 𝑟 ∈ Odd ) ) )
4 oddprmuzge3 ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∈ Odd ) → 𝑝 ∈ ( ℤ≥ ‘ 3 ) )
5 oddprmuzge3 ⊢ ( ( 𝑞 ∈ ℙ ∧ 𝑞 ∈ Odd ) → 𝑞 ∈ ( ℤ≥ ‘ 3 ) )
6 oddprmuzge3 ⊢ ( ( 𝑟 ∈ ℙ ∧ 𝑟 ∈ Odd ) → 𝑟 ∈ ( ℤ≥ ‘ 3 ) )
7 6p3e9 ⊢ ( 6 + 3 ) = 9
8 eluzelz ⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) → 𝑝 ∈ ℤ )
9 eluzelz ⊢ ( 𝑞 ∈ ( ℤ≥ ‘ 3 ) → 𝑞 ∈ ℤ )
10 zaddcl ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( 𝑝 + 𝑞 ) ∈ ℤ )
11 8 9 10 syl2an ⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑝 + 𝑞 ) ∈ ℤ )
12 11 zred ⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑝 + 𝑞 ) ∈ ℝ )
13 eluzelre ⊢ ( 𝑟 ∈ ( ℤ≥ ‘ 3 ) → 𝑟 ∈ ℝ )
14 12 13 anim12i ⊢ ( ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) ∧ 𝑟 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑝 + 𝑞 ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) )
15 14 3impa ⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑝 + 𝑞 ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) )
16 6re ⊢ 6 ∈ ℝ
17 3re ⊢ 3 ∈ ℝ
18 16 17 pm3.2i ⊢ ( 6 ∈ ℝ ∧ 3 ∈ ℝ )
19 15 18 jctil ⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 6 ∈ ℝ ∧ 3 ∈ ℝ ) ∧ ( ( 𝑝 + 𝑞 ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) ) )
20 3p3e6 ⊢ ( 3 + 3 ) = 6
21 eluzelre ⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) → 𝑝 ∈ ℝ )
22 eluzelre ⊢ ( 𝑞 ∈ ( ℤ≥ ‘ 3 ) → 𝑞 ∈ ℝ )
23 21 22 anim12i ⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ ) )
24 17 17 pm3.2i ⊢ ( 3 ∈ ℝ ∧ 3 ∈ ℝ )
25 23 24 jctil ⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 3 ∈ ℝ ∧ 3 ∈ ℝ ) ∧ ( 𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ ) ) )
26 eluzle ⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑝 )
27 eluzle ⊢ ( 𝑞 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑞 )
28 26 27 anim12i ⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) → ( 3 ≤ 𝑝 ∧ 3 ≤ 𝑞 ) )
29 le2add ⊢ ( ( ( 3 ∈ ℝ ∧ 3 ∈ ℝ ) ∧ ( 𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ ) ) → ( ( 3 ≤ 𝑝 ∧ 3 ≤ 𝑞 ) → ( 3 + 3 ) ≤ ( 𝑝 + 𝑞 ) ) )
30 25 28 29 sylc ⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) → ( 3 + 3 ) ≤ ( 𝑝 + 𝑞 ) )
31 20 30 eqbrtrrid ⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) → 6 ≤ ( 𝑝 + 𝑞 ) )
32 31 3adant3 ⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ ( ℤ≥ ‘ 3 ) ) → 6 ≤ ( 𝑝 + 𝑞 ) )
33 eluzle ⊢ ( 𝑟 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑟 )
34 33 3ad2ant3 ⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ ( ℤ≥ ‘ 3 ) ) → 3 ≤ 𝑟 )
35 32 34 jca ⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ ( ℤ≥ ‘ 3 ) ) → ( 6 ≤ ( 𝑝 + 𝑞 ) ∧ 3 ≤ 𝑟 ) )
36 le2add ⊢ ( ( ( 6 ∈ ℝ ∧ 3 ∈ ℝ ) ∧ ( ( 𝑝 + 𝑞 ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) ) → ( ( 6 ≤ ( 𝑝 + 𝑞 ) ∧ 3 ≤ 𝑟 ) → ( 6 + 3 ) ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
37 19 35 36 sylc ⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ ( ℤ≥ ‘ 3 ) ) → ( 6 + 3 ) ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
38 7 37 eqbrtrrid ⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑟 ∈ ( ℤ≥ ‘ 3 ) ) → 9 ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
39 4 5 6 38 syl3an ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∈ Odd ) ∧ ( 𝑞 ∈ ℙ ∧ 𝑞 ∈ Odd ) ∧ ( 𝑟 ∈ ℙ ∧ 𝑟 ∈ Odd ) ) → 9 ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
40 3 39 sylbi ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ) → 9 ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
41 2 40 sylanbr ⊢ ( ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ) → 9 ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
42 breq2 ⊢ ( 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ( 9 ≤ 𝑍 ↔ 9 ≤ ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
43 41 42 syl5ibrcom ⊢ ( ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ) → ( 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → 9 ≤ 𝑍 ) )
44 43 expimpd ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → ( ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → 9 ≤ 𝑍 ) )
45 44 rexlimdva ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → 9 ≤ 𝑍 ) )
46 45 a1i ⊢ ( 𝑍 ∈ Odd → ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → 9 ≤ 𝑍 ) ) )
47 46 rexlimdvv ⊢ ( 𝑍 ∈ Odd → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → 9 ≤ 𝑍 ) )
48 47 imp ⊢ ( ( 𝑍 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) → 9 ≤ 𝑍 )
49 1 48 sylbi ⊢ ( 𝑍 ∈ GoldbachOdd → 9 ≤ 𝑍 )