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

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 ( 𝑍 ∈ GoldbachOddW → 7 ≤ 𝑍 )

Proof

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