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 ≤ 𝑍 )