Metamath Proof Explorer

Theorem gbegt5

Description: Any even Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020)

Ref Expression
Assertion gbegt5 ( 𝑍 ∈ GoldbachEven → 5 < 𝑍 )

Proof

Step Hyp Ref Expression
1 isgbe ⊢ ( 𝑍 ∈ GoldbachEven ↔ ( 𝑍 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = ( 𝑝 + 𝑞 ) ) ) )
2 oddprmuzge3 ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∈ Odd ) → 𝑝 ∈ ( ℤ≥ ‘ 3 ) )
3 2 ancoms ⊢ ( ( 𝑝 ∈ Odd ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ( ℤ≥ ‘ 3 ) )
4 oddprmuzge3 ⊢ ( ( 𝑞 ∈ ℙ ∧ 𝑞 ∈ Odd ) → 𝑞 ∈ ( ℤ≥ ‘ 3 ) )
5 4 ancoms ⊢ ( ( 𝑞 ∈ Odd ∧ 𝑞 ∈ ℙ ) → 𝑞 ∈ ( ℤ≥ ‘ 3 ) )
6 eluz2 ⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 3 ≤ 𝑝 ) )
7 eluz2 ⊢ ( 𝑞 ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 3 ≤ 𝑞 ) )
8 zre ⊢ ( 𝑞 ∈ ℤ → 𝑞 ∈ ℝ )
9 zre ⊢ ( 𝑝 ∈ ℤ → 𝑝 ∈ ℝ )
10 3re ⊢ 3 ∈ ℝ
11 10 10 pm3.2i ⊢ ( 3 ∈ ℝ ∧ 3 ∈ ℝ )
12 pm3.22 ⊢ ( ( 𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → ( 𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ ) )
13 le2add ⊢ ( ( ( 3 ∈ ℝ ∧ 3 ∈ ℝ ) ∧ ( 𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ ) ) → ( ( 3 ≤ 𝑝 ∧ 3 ≤ 𝑞 ) → ( 3 + 3 ) ≤ ( 𝑝 + 𝑞 ) ) )
14 11 12 13 sylancr ⊢ ( ( 𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → ( ( 3 ≤ 𝑝 ∧ 3 ≤ 𝑞 ) → ( 3 + 3 ) ≤ ( 𝑝 + 𝑞 ) ) )
15 14 ancomsd ⊢ ( ( 𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → ( ( 3 ≤ 𝑞 ∧ 3 ≤ 𝑝 ) → ( 3 + 3 ) ≤ ( 𝑝 + 𝑞 ) ) )
16 3p3e6 ⊢ ( 3 + 3 ) = 6
17 16 breq1i ⊢ ( ( 3 + 3 ) ≤ ( 𝑝 + 𝑞 ) ↔ 6 ≤ ( 𝑝 + 𝑞 ) )
18 5lt6 ⊢ 5 < 6
19 5re ⊢ 5 ∈ ℝ
20 19 a1i ⊢ ( ( 𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → 5 ∈ ℝ )
21 6re ⊢ 6 ∈ ℝ
22 21 a1i ⊢ ( ( 𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → 6 ∈ ℝ )
23 readdcl ⊢ ( ( 𝑝 ∈ ℝ ∧ 𝑞 ∈ ℝ ) → ( 𝑝 + 𝑞 ) ∈ ℝ )
24 23 ancoms ⊢ ( ( 𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → ( 𝑝 + 𝑞 ) ∈ ℝ )
25 ltletr ⊢ ( ( 5 ∈ ℝ ∧ 6 ∈ ℝ ∧ ( 𝑝 + 𝑞 ) ∈ ℝ ) → ( ( 5 < 6 ∧ 6 ≤ ( 𝑝 + 𝑞 ) ) → 5 < ( 𝑝 + 𝑞 ) ) )
26 20 22 24 25 syl3anc ⊢ ( ( 𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → ( ( 5 < 6 ∧ 6 ≤ ( 𝑝 + 𝑞 ) ) → 5 < ( 𝑝 + 𝑞 ) ) )
27 18 26 mpani ⊢ ( ( 𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → ( 6 ≤ ( 𝑝 + 𝑞 ) → 5 < ( 𝑝 + 𝑞 ) ) )
28 17 27 biimtrid ⊢ ( ( 𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → ( ( 3 + 3 ) ≤ ( 𝑝 + 𝑞 ) → 5 < ( 𝑝 + 𝑞 ) ) )
29 15 28 syld ⊢ ( ( 𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → ( ( 3 ≤ 𝑞 ∧ 3 ≤ 𝑝 ) → 5 < ( 𝑝 + 𝑞 ) ) )
30 8 9 29 syl2an ⊢ ( ( 𝑞 ∈ ℤ ∧ 𝑝 ∈ ℤ ) → ( ( 3 ≤ 𝑞 ∧ 3 ≤ 𝑝 ) → 5 < ( 𝑝 + 𝑞 ) ) )
31 30 ex ⊢ ( 𝑞 ∈ ℤ → ( 𝑝 ∈ ℤ → ( ( 3 ≤ 𝑞 ∧ 3 ≤ 𝑝 ) → 5 < ( 𝑝 + 𝑞 ) ) ) )
32 31 adantl ⊢ ( ( 3 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( 𝑝 ∈ ℤ → ( ( 3 ≤ 𝑞 ∧ 3 ≤ 𝑝 ) → 5 < ( 𝑝 + 𝑞 ) ) ) )
33 32 com23 ⊢ ( ( 3 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( ( 3 ≤ 𝑞 ∧ 3 ≤ 𝑝 ) → ( 𝑝 ∈ ℤ → 5 < ( 𝑝 + 𝑞 ) ) ) )
34 33 exp4b ⊢ ( 3 ∈ ℤ → ( 𝑞 ∈ ℤ → ( 3 ≤ 𝑞 → ( 3 ≤ 𝑝 → ( 𝑝 ∈ ℤ → 5 < ( 𝑝 + 𝑞 ) ) ) ) ) )
35 34 3imp ⊢ ( ( 3 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 3 ≤ 𝑞 ) → ( 3 ≤ 𝑝 → ( 𝑝 ∈ ℤ → 5 < ( 𝑝 + 𝑞 ) ) ) )
36 35 com13 ⊢ ( 𝑝 ∈ ℤ → ( 3 ≤ 𝑝 → ( ( 3 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 3 ≤ 𝑞 ) → 5 < ( 𝑝 + 𝑞 ) ) ) )
37 36 imp ⊢ ( ( 𝑝 ∈ ℤ ∧ 3 ≤ 𝑝 ) → ( ( 3 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 3 ≤ 𝑞 ) → 5 < ( 𝑝 + 𝑞 ) ) )
38 37 3adant1 ⊢ ( ( 3 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 3 ≤ 𝑝 ) → ( ( 3 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 3 ≤ 𝑞 ) → 5 < ( 𝑝 + 𝑞 ) ) )
39 7 38 biimtrid ⊢ ( ( 3 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ 3 ≤ 𝑝 ) → ( 𝑞 ∈ ( ℤ≥ ‘ 3 ) → 5 < ( 𝑝 + 𝑞 ) ) )
40 6 39 sylbi ⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑞 ∈ ( ℤ≥ ‘ 3 ) → 5 < ( 𝑝 + 𝑞 ) ) )
41 40 imp ⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑞 ∈ ( ℤ≥ ‘ 3 ) ) → 5 < ( 𝑝 + 𝑞 ) )
42 3 5 41 syl2an ⊢ ( ( ( 𝑝 ∈ Odd ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑞 ∈ Odd ∧ 𝑞 ∈ ℙ ) ) → 5 < ( 𝑝 + 𝑞 ) )
43 42 an4s ⊢ ( ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ) → 5 < ( 𝑝 + 𝑞 ) )
44 43 ex ⊢ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) → ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → 5 < ( 𝑝 + 𝑞 ) ) )
45 44 3adant3 ⊢ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = ( 𝑝 + 𝑞 ) ) → ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → 5 < ( 𝑝 + 𝑞 ) ) )
46 45 impcom ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = ( 𝑝 + 𝑞 ) ) ) → 5 < ( 𝑝 + 𝑞 ) )
47 breq2 ⊢ ( 𝑍 = ( 𝑝 + 𝑞 ) → ( 5 < 𝑍 ↔ 5 < ( 𝑝 + 𝑞 ) ) )
48 47 3ad2ant3 ⊢ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = ( 𝑝 + 𝑞 ) ) → ( 5 < 𝑍 ↔ 5 < ( 𝑝 + 𝑞 ) ) )
49 48 adantl ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = ( 𝑝 + 𝑞 ) ) ) → ( 5 < 𝑍 ↔ 5 < ( 𝑝 + 𝑞 ) ) )
50 46 49 mpbird ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = ( 𝑝 + 𝑞 ) ) ) → 5 < 𝑍 )
51 50 ex ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = ( 𝑝 + 𝑞 ) ) → 5 < 𝑍 ) )
52 51 a1i ⊢ ( 𝑍 ∈ Even → ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = ( 𝑝 + 𝑞 ) ) → 5 < 𝑍 ) ) )
53 52 rexlimdvv ⊢ ( 𝑍 ∈ Even → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = ( 𝑝 + 𝑞 ) ) → 5 < 𝑍 ) )
54 53 imp ⊢ ( ( 𝑍 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = ( 𝑝 + 𝑞 ) ) ) → 5 < 𝑍 )
55 1 54 sylbi ⊢ ( 𝑍 ∈ GoldbachEven → 5 < 𝑍 )