Metamath Proof Explorer

Theorem gbowge7

Description: Any weak odd Goldbach number is greater than or equal to 7. Because of 7gbow , this bound is strict. (Contributed by AV, 20-Jul-2020)

Ref Expression
Assertion gbowge7 
|- ( Z e. GoldbachOddW -> 7 <_ Z )

Proof

Step Hyp Ref Expression
1 gbowgt5 
 |-  ( Z e. GoldbachOddW -> 5 < Z )
2 gbowpos 
 |-  ( Z e. GoldbachOddW -> Z e. NN )
3 5nn 
 |-  5 e. NN
4 3 nnzi 
 |-  5 e. ZZ
5 nnz 
 |-  ( Z e. NN -> Z e. ZZ )
6 zltp1le 
 |-  ( ( 5 e. ZZ /\ Z e. ZZ ) -> ( 5 < Z <-> ( 5 + 1 ) <_ Z ) )
7 4 5 6 sylancr 
 |-  ( Z e. NN -> ( 5 < Z <-> ( 5 + 1 ) <_ Z ) )
8 7 biimpd 
 |-  ( Z e. NN -> ( 5 < Z -> ( 5 + 1 ) <_ Z ) )
9 2 8 syl 
 |-  ( Z e. GoldbachOddW -> ( 5 < Z -> ( 5 + 1 ) <_ Z ) )
10 5p1e6 
 |-  ( 5 + 1 ) = 6
11 10 breq1i 
 |-  ( ( 5 + 1 ) <_ Z <-> 6 <_ Z )
12 6re 
 |-  6 e. RR
13 2 nnred 
 |-  ( Z e. GoldbachOddW -> Z e. RR )
14 leloe 
 |-  ( ( 6 e. RR /\ Z e. RR ) -> ( 6 <_ Z <-> ( 6 < Z \/ 6 = Z ) ) )
15 12 13 14 sylancr 
 |-  ( Z e. GoldbachOddW -> ( 6 <_ Z <-> ( 6 < Z \/ 6 = Z ) ) )
16 11 15 bitrid 
 |-  ( Z e. GoldbachOddW -> ( ( 5 + 1 ) <_ Z <-> ( 6 < Z \/ 6 = Z ) ) )
17 6nn 
 |-  6 e. NN
18 17 nnzi 
 |-  6 e. ZZ
19 2 nnzd 
 |-  ( Z e. GoldbachOddW -> Z e. ZZ )
20 zltp1le 
 |-  ( ( 6 e. ZZ /\ Z e. ZZ ) -> ( 6 < Z <-> ( 6 + 1 ) <_ Z ) )
21 20 biimpd 
 |-  ( ( 6 e. ZZ /\ Z e. ZZ ) -> ( 6 < Z -> ( 6 + 1 ) <_ Z ) )
22 18 19 21 sylancr 
 |-  ( Z e. GoldbachOddW -> ( 6 < Z -> ( 6 + 1 ) <_ Z ) )
23 6p1e7 
 |-  ( 6 + 1 ) = 7
24 23 breq1i 
 |-  ( ( 6 + 1 ) <_ Z <-> 7 <_ Z )
25 22 24 imbitrdi 
 |-  ( Z e. GoldbachOddW -> ( 6 < Z -> 7 <_ Z ) )
26 isgbow 
 |-  ( Z e. GoldbachOddW <-> ( Z e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime Z = ( ( p + q ) + r ) ) )
27 eleq1 
 |-  ( 6 = Z -> ( 6 e. Odd <-> Z e. Odd ) )
28 6even 
 |-  6 e. Even
29 evennodd 
 |-  ( 6 e. Even -> -. 6 e. Odd )
30 pm2.21 
 |-  ( -. 6 e. Odd -> ( 6 e. Odd -> 7 <_ Z ) )
31 28 29 30 mp2b 
 |-  ( 6 e. Odd -> 7 <_ Z )
32 27 31 biimtrrdi 
 |-  ( 6 = Z -> ( Z e. Odd -> 7 <_ Z ) )
33 32 com12 
 |-  ( Z e. Odd -> ( 6 = Z -> 7 <_ Z ) )
34 33 adantr 
 |-  ( ( Z e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime Z = ( ( p + q ) + r ) ) -> ( 6 = Z -> 7 <_ Z ) )
35 26 34 sylbi 
 |-  ( Z e. GoldbachOddW -> ( 6 = Z -> 7 <_ Z ) )
36 25 35 jaod 
 |-  ( Z e. GoldbachOddW -> ( ( 6 < Z \/ 6 = Z ) -> 7 <_ Z ) )
37 16 36 sylbid 
 |-  ( Z e. GoldbachOddW -> ( ( 5 + 1 ) <_ Z -> 7 <_ Z ) )
38 9 37 syld 
 |-  ( Z e. GoldbachOddW -> ( 5 < Z -> 7 <_ Z ) )
39 1 38 mpd 
 |-  ( Z e. GoldbachOddW -> 7 <_ Z )