This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gbowgt5

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

Ref Expression
Assertion gbowgt5 
|- ( Z e. GoldbachOddW -> 5 < Z )

Proof

Step Hyp Ref Expression
1 isgbow 
 |-  ( Z e. GoldbachOddW <-> ( Z e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime Z = ( ( p + q ) + r ) ) )
2 prmuz2 
 |-  ( p e. Prime -> p e. ( ZZ>= ` 2 ) )
3 eluz2 
 |-  ( p e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ p e. ZZ /\ 2 <_ p ) )
4 2 3 sylib 
 |-  ( p e. Prime -> ( 2 e. ZZ /\ p e. ZZ /\ 2 <_ p ) )
5 prmuz2 
 |-  ( q e. Prime -> q e. ( ZZ>= ` 2 ) )
6 eluz2 
 |-  ( q e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ q e. ZZ /\ 2 <_ q ) )
7 5 6 sylib 
 |-  ( q e. Prime -> ( 2 e. ZZ /\ q e. ZZ /\ 2 <_ q ) )
8 4 7 anim12i 
 |-  ( ( p e. Prime /\ q e. Prime ) -> ( ( 2 e. ZZ /\ p e. ZZ /\ 2 <_ p ) /\ ( 2 e. ZZ /\ q e. ZZ /\ 2 <_ q ) ) )
9 prmuz2 
 |-  ( r e. Prime -> r e. ( ZZ>= ` 2 ) )
10 eluz2 
 |-  ( r e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) )
11 9 10 sylib 
 |-  ( r e. Prime -> ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) )
12 zre 
 |-  ( p e. ZZ -> p e. RR )
13 12 3ad2ant2 
 |-  ( ( 2 e. ZZ /\ p e. ZZ /\ 2 <_ p ) -> p e. RR )
14 zre 
 |-  ( q e. ZZ -> q e. RR )
15 14 3ad2ant2 
 |-  ( ( 2 e. ZZ /\ q e. ZZ /\ 2 <_ q ) -> q e. RR )
16 13 15 anim12i 
 |-  ( ( ( 2 e. ZZ /\ p e. ZZ /\ 2 <_ p ) /\ ( 2 e. ZZ /\ q e. ZZ /\ 2 <_ q ) ) -> ( p e. RR /\ q e. RR ) )
17 2re 
 |-  2 e. RR
18 17 17 pm3.2i 
 |-  ( 2 e. RR /\ 2 e. RR )
19 16 18 jctil 
 |-  ( ( ( 2 e. ZZ /\ p e. ZZ /\ 2 <_ p ) /\ ( 2 e. ZZ /\ q e. ZZ /\ 2 <_ q ) ) -> ( ( 2 e. RR /\ 2 e. RR ) /\ ( p e. RR /\ q e. RR ) ) )
20 simp3 
 |-  ( ( 2 e. ZZ /\ p e. ZZ /\ 2 <_ p ) -> 2 <_ p )
21 simp3 
 |-  ( ( 2 e. ZZ /\ q e. ZZ /\ 2 <_ q ) -> 2 <_ q )
22 20 21 anim12i 
 |-  ( ( ( 2 e. ZZ /\ p e. ZZ /\ 2 <_ p ) /\ ( 2 e. ZZ /\ q e. ZZ /\ 2 <_ q ) ) -> ( 2 <_ p /\ 2 <_ q ) )
23 le2add 
 |-  ( ( ( 2 e. RR /\ 2 e. RR ) /\ ( p e. RR /\ q e. RR ) ) -> ( ( 2 <_ p /\ 2 <_ q ) -> ( 2 + 2 ) <_ ( p + q ) ) )
24 19 22 23 sylc 
 |-  ( ( ( 2 e. ZZ /\ p e. ZZ /\ 2 <_ p ) /\ ( 2 e. ZZ /\ q e. ZZ /\ 2 <_ q ) ) -> ( 2 + 2 ) <_ ( p + q ) )
25 2p2e4 
 |-  ( 2 + 2 ) = 4
26 25 breq1i 
 |-  ( ( 2 + 2 ) <_ ( p + q ) <-> 4 <_ ( p + q ) )
27 zaddcl 
 |-  ( ( p e. ZZ /\ q e. ZZ ) -> ( p + q ) e. ZZ )
28 27 zred 
 |-  ( ( p e. ZZ /\ q e. ZZ ) -> ( p + q ) e. RR )
29 28 adantr 
 |-  ( ( ( p e. ZZ /\ q e. ZZ ) /\ 4 <_ ( p + q ) ) -> ( p + q ) e. RR )
30 zre 
 |-  ( r e. ZZ -> r e. RR )
31 30 3ad2ant2 
 |-  ( ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) -> r e. RR )
32 29 31 anim12i 
 |-  ( ( ( ( p e. ZZ /\ q e. ZZ ) /\ 4 <_ ( p + q ) ) /\ ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) ) -> ( ( p + q ) e. RR /\ r e. RR ) )
33 4re 
 |-  4 e. RR
34 33 17 pm3.2i 
 |-  ( 4 e. RR /\ 2 e. RR )
35 32 34 jctil 
 |-  ( ( ( ( p e. ZZ /\ q e. ZZ ) /\ 4 <_ ( p + q ) ) /\ ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) ) -> ( ( 4 e. RR /\ 2 e. RR ) /\ ( ( p + q ) e. RR /\ r e. RR ) ) )
36 simpr 
 |-  ( ( ( p e. ZZ /\ q e. ZZ ) /\ 4 <_ ( p + q ) ) -> 4 <_ ( p + q ) )
37 simp3 
 |-  ( ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) -> 2 <_ r )
38 36 37 anim12i 
 |-  ( ( ( ( p e. ZZ /\ q e. ZZ ) /\ 4 <_ ( p + q ) ) /\ ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) ) -> ( 4 <_ ( p + q ) /\ 2 <_ r ) )
39 le2add 
 |-  ( ( ( 4 e. RR /\ 2 e. RR ) /\ ( ( p + q ) e. RR /\ r e. RR ) ) -> ( ( 4 <_ ( p + q ) /\ 2 <_ r ) -> ( 4 + 2 ) <_ ( ( p + q ) + r ) ) )
40 35 38 39 sylc 
 |-  ( ( ( ( p e. ZZ /\ q e. ZZ ) /\ 4 <_ ( p + q ) ) /\ ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) ) -> ( 4 + 2 ) <_ ( ( p + q ) + r ) )
41 4p2e6 
 |-  ( 4 + 2 ) = 6
42 41 breq1i 
 |-  ( ( 4 + 2 ) <_ ( ( p + q ) + r ) <-> 6 <_ ( ( p + q ) + r ) )
43 5lt6 
 |-  5 < 6
44 5re 
 |-  5 e. RR
45 44 a1i 
 |-  ( ( ( p e. ZZ /\ q e. ZZ ) /\ r e. ZZ ) -> 5 e. RR )
46 6re 
 |-  6 e. RR
47 46 a1i 
 |-  ( ( ( p e. ZZ /\ q e. ZZ ) /\ r e. ZZ ) -> 6 e. RR )
48 27 adantr 
 |-  ( ( ( p e. ZZ /\ q e. ZZ ) /\ r e. ZZ ) -> ( p + q ) e. ZZ )
49 simpr 
 |-  ( ( ( p e. ZZ /\ q e. ZZ ) /\ r e. ZZ ) -> r e. ZZ )
50 48 49 zaddcld 
 |-  ( ( ( p e. ZZ /\ q e. ZZ ) /\ r e. ZZ ) -> ( ( p + q ) + r ) e. ZZ )
51 50 zred 
 |-  ( ( ( p e. ZZ /\ q e. ZZ ) /\ r e. ZZ ) -> ( ( p + q ) + r ) e. RR )
52 ltletr 
 |-  ( ( 5 e. RR /\ 6 e. RR /\ ( ( p + q ) + r ) e. RR ) -> ( ( 5 < 6 /\ 6 <_ ( ( p + q ) + r ) ) -> 5 < ( ( p + q ) + r ) ) )
53 45 47 51 52 syl3anc 
 |-  ( ( ( p e. ZZ /\ q e. ZZ ) /\ r e. ZZ ) -> ( ( 5 < 6 /\ 6 <_ ( ( p + q ) + r ) ) -> 5 < ( ( p + q ) + r ) ) )
54 43 53 mpani 
 |-  ( ( ( p e. ZZ /\ q e. ZZ ) /\ r e. ZZ ) -> ( 6 <_ ( ( p + q ) + r ) -> 5 < ( ( p + q ) + r ) ) )
55 42 54 biimtrid 
 |-  ( ( ( p e. ZZ /\ q e. ZZ ) /\ r e. ZZ ) -> ( ( 4 + 2 ) <_ ( ( p + q ) + r ) -> 5 < ( ( p + q ) + r ) ) )
56 55 expcom 
 |-  ( r e. ZZ -> ( ( p e. ZZ /\ q e. ZZ ) -> ( ( 4 + 2 ) <_ ( ( p + q ) + r ) -> 5 < ( ( p + q ) + r ) ) ) )
57 56 3ad2ant2 
 |-  ( ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) -> ( ( p e. ZZ /\ q e. ZZ ) -> ( ( 4 + 2 ) <_ ( ( p + q ) + r ) -> 5 < ( ( p + q ) + r ) ) ) )
58 57 com12 
 |-  ( ( p e. ZZ /\ q e. ZZ ) -> ( ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) -> ( ( 4 + 2 ) <_ ( ( p + q ) + r ) -> 5 < ( ( p + q ) + r ) ) ) )
59 58 adantr 
 |-  ( ( ( p e. ZZ /\ q e. ZZ ) /\ 4 <_ ( p + q ) ) -> ( ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) -> ( ( 4 + 2 ) <_ ( ( p + q ) + r ) -> 5 < ( ( p + q ) + r ) ) ) )
60 59 imp 
 |-  ( ( ( ( p e. ZZ /\ q e. ZZ ) /\ 4 <_ ( p + q ) ) /\ ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) ) -> ( ( 4 + 2 ) <_ ( ( p + q ) + r ) -> 5 < ( ( p + q ) + r ) ) )
61 40 60 mpd 
 |-  ( ( ( ( p e. ZZ /\ q e. ZZ ) /\ 4 <_ ( p + q ) ) /\ ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) ) -> 5 < ( ( p + q ) + r ) )
62 61 exp31 
 |-  ( ( p e. ZZ /\ q e. ZZ ) -> ( 4 <_ ( p + q ) -> ( ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) -> 5 < ( ( p + q ) + r ) ) ) )
63 26 62 biimtrid 
 |-  ( ( p e. ZZ /\ q e. ZZ ) -> ( ( 2 + 2 ) <_ ( p + q ) -> ( ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) -> 5 < ( ( p + q ) + r ) ) ) )
64 63 expcom 
 |-  ( q e. ZZ -> ( p e. ZZ -> ( ( 2 + 2 ) <_ ( p + q ) -> ( ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) -> 5 < ( ( p + q ) + r ) ) ) ) )
65 64 3ad2ant2 
 |-  ( ( 2 e. ZZ /\ q e. ZZ /\ 2 <_ q ) -> ( p e. ZZ -> ( ( 2 + 2 ) <_ ( p + q ) -> ( ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) -> 5 < ( ( p + q ) + r ) ) ) ) )
66 65 com12 
 |-  ( p e. ZZ -> ( ( 2 e. ZZ /\ q e. ZZ /\ 2 <_ q ) -> ( ( 2 + 2 ) <_ ( p + q ) -> ( ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) -> 5 < ( ( p + q ) + r ) ) ) ) )
67 66 3ad2ant2 
 |-  ( ( 2 e. ZZ /\ p e. ZZ /\ 2 <_ p ) -> ( ( 2 e. ZZ /\ q e. ZZ /\ 2 <_ q ) -> ( ( 2 + 2 ) <_ ( p + q ) -> ( ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) -> 5 < ( ( p + q ) + r ) ) ) ) )
68 67 imp 
 |-  ( ( ( 2 e. ZZ /\ p e. ZZ /\ 2 <_ p ) /\ ( 2 e. ZZ /\ q e. ZZ /\ 2 <_ q ) ) -> ( ( 2 + 2 ) <_ ( p + q ) -> ( ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) -> 5 < ( ( p + q ) + r ) ) ) )
69 24 68 mpd 
 |-  ( ( ( 2 e. ZZ /\ p e. ZZ /\ 2 <_ p ) /\ ( 2 e. ZZ /\ q e. ZZ /\ 2 <_ q ) ) -> ( ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) -> 5 < ( ( p + q ) + r ) ) )
70 69 imp 
 |-  ( ( ( ( 2 e. ZZ /\ p e. ZZ /\ 2 <_ p ) /\ ( 2 e. ZZ /\ q e. ZZ /\ 2 <_ q ) ) /\ ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) ) -> 5 < ( ( p + q ) + r ) )
71 breq2 
 |-  ( Z = ( ( p + q ) + r ) -> ( 5 < Z <-> 5 < ( ( p + q ) + r ) ) )
72 70 71 syl5ibrcom 
 |-  ( ( ( ( 2 e. ZZ /\ p e. ZZ /\ 2 <_ p ) /\ ( 2 e. ZZ /\ q e. ZZ /\ 2 <_ q ) ) /\ ( 2 e. ZZ /\ r e. ZZ /\ 2 <_ r ) ) -> ( Z = ( ( p + q ) + r ) -> 5 < Z ) )
73 8 11 72 syl2an 
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ r e. Prime ) -> ( Z = ( ( p + q ) + r ) -> 5 < Z ) )
74 73 rexlimdva 
 |-  ( ( p e. Prime /\ q e. Prime ) -> ( E. r e. Prime Z = ( ( p + q ) + r ) -> 5 < Z ) )
75 74 adantl 
 |-  ( ( Z e. Odd /\ ( p e. Prime /\ q e. Prime ) ) -> ( E. r e. Prime Z = ( ( p + q ) + r ) -> 5 < Z ) )
76 75 rexlimdvva 
 |-  ( Z e. Odd -> ( E. p e. Prime E. q e. Prime E. r e. Prime Z = ( ( p + q ) + r ) -> 5 < Z ) )
77 76 imp 
 |-  ( ( Z e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime Z = ( ( p + q ) + r ) ) -> 5 < Z )
78 1 77 sylbi 
 |-  ( Z e. GoldbachOddW -> 5 < Z )