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 e. GoldbachEven -> 5 < Z )

Proof

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