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∈GoldbachOddW→7≤Z

Proof

Step Hyp Ref Expression
1 gbowgt5 ⊢Z∈GoldbachOddW→5<Z
2 gbowpos ⊢Z∈GoldbachOddW→Z∈ℕ
3 5nn ⊢5∈ℕ
4 3 nnzi ⊢5∈ℤ
5 nnz ⊢Z∈ℕ→Z∈ℤ
6 zltp1le ⊢5∈ℤ∧Z∈ℤ→5<Z↔5+1≤Z
7 4 5 6 sylancr ⊢Z∈ℕ→5<Z↔5+1≤Z
8 7 biimpd ⊢Z∈ℕ→5<Z→5+1≤Z
9 2 8 syl ⊢Z∈GoldbachOddW→5<Z→5+1≤Z
10 5p1e6 ⊢5+1=6
11 10 breq1i ⊢5+1≤Z↔6≤Z
12 6re ⊢6∈ℝ
13 2 nnred ⊢Z∈GoldbachOddW→Z∈ℝ
14 leloe ⊢6∈ℝ∧Z∈ℝ→6≤Z↔6<Z∨6=Z
15 12 13 14 sylancr ⊢Z∈GoldbachOddW→6≤Z↔6<Z∨6=Z
16 11 15 bitrid ⊢Z∈GoldbachOddW→5+1≤Z↔6<Z∨6=Z
17 6nn ⊢6∈ℕ
18 17 nnzi ⊢6∈ℤ
19 2 nnzd ⊢Z∈GoldbachOddW→Z∈ℤ
20 zltp1le ⊢6∈ℤ∧Z∈ℤ→6<Z↔6+1≤Z
21 20 biimpd ⊢6∈ℤ∧Z∈ℤ→6<Z→6+1≤Z
22 18 19 21 sylancr ⊢Z∈GoldbachOddW→6<Z→6+1≤Z
23 6p1e7 ⊢6+1=7
24 23 breq1i ⊢6+1≤Z↔7≤Z
25 22 24 imbitrdi ⊢Z∈GoldbachOddW→6<Z→7≤Z
26 isgbow ⊢Z∈GoldbachOddW↔Z∈Odd∧∃p∈ℙ∃q∈ℙ∃r∈ℙZ=p+q+r
27 eleq1 ⊢6=Z→6∈Odd↔Z∈Odd
28 6even ⊢6∈Even
29 evennodd ⊢6∈Even→¬6∈Odd
30 pm2.21 ⊢¬6∈Odd→6∈Odd→7≤Z
31 28 29 30 mp2b ⊢6∈Odd→7≤Z
32 27 31 syl6bir ⊢6=Z→Z∈Odd→7≤Z
33 32 com12 ⊢Z∈Odd→6=Z→7≤Z
34 33 adantr ⊢Z∈Odd∧∃p∈ℙ∃q∈ℙ∃r∈ℙZ=p+q+r→6=Z→7≤Z
35 26 34 sylbi ⊢Z∈GoldbachOddW→6=Z→7≤Z
36 25 35 jaod ⊢Z∈GoldbachOddW→6<Z∨6=Z→7≤Z
37 16 36 sylbid ⊢Z∈GoldbachOddW→5+1≤Z→7≤Z
38 9 37 syld ⊢Z∈GoldbachOddW→5<Z→7≤Z
39 1 38 mpd ⊢Z∈GoldbachOddW→7≤Z