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 biimtrrdi ⊢ 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