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

Metamath Proof Explorer

Theorem gbege6

Description: Any even Goldbach number is greater than or equal to 6. Because of 6gbe , this bound is strict. (Contributed by AV, 20-Jul-2020)

Ref Expression
Assertion gbege6 ⊢ Z ∈ GoldbachEven → 6 ≤ Z

Proof

Step Hyp Ref Expression
1 gbepos ⊢ Z ∈ GoldbachEven → Z ∈ ℕ
2 gbegt5 ⊢ Z ∈ GoldbachEven → 5 < 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 5p1e6 ⊢ 5 + 1 = 6
10 9 breq1i ⊢ 5 + 1 ≤ Z ↔ 6 ≤ Z
11 8 10 imbitrdi ⊢ Z ∈ ℕ → 5 < Z → 6 ≤ Z
12 1 2 11 sylc ⊢ Z ∈ GoldbachEven → 6 ≤ Z