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 syl5bi ( ( 𝑞 ∈ ℝ ∧ 𝑝 ∈ ℝ ) → ( ( 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 syl5bi ( ( 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 < 𝑍 )