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	⊢ ( 𝑍 ∈ GoldbachEven → 6 ≤ 𝑍 )

Proof

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