Metamath Proof Explorer


Theorem gbegt5

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

Ref Expression
Assertion gbegt5 Z GoldbachEven 5 < Z

Proof

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