Theorem eluz4eluz3

Description: An integer greater than or equal to 4 is an integer greater than or equal to 3. (Contributed by AV, 5-Sep-2025)

	Ref	Expression
Assertion	eluz4eluz3	⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ( ℤ≥ ‘ 3 ) )

Proof

Step	Hyp	Ref	Expression
1		3z	⊢ 3 ∈ ℤ
2		3re	⊢ 3 ∈ ℝ
3		4re	⊢ 4 ∈ ℝ
4		3lt4	⊢ 3 < 4
5	2 3 4	ltleii	⊢ 3 ≤ 4
6		eluzuzle	⊢ ( ( 3 ∈ ℤ ∧ 3 ≤ 4 ) → ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ( ℤ≥ ‘ 3 ) ) )
7	1 5 6	mp2an	⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ( ℤ≥ ‘ 3 ) )