Metamath Proof Explorer

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 
|- ( X e. ( ZZ>= ` 4 ) -> X e. ( ZZ>= ` 3 ) )

Proof

Step Hyp Ref Expression
1 3z 
 |-  3 e. ZZ
2 3re 
 |-  3 e. RR
3 4re 
 |-  4 e. RR
4 3lt4 
 |-  3 < 4
5 2 3 4 ltleii 
 |-  3 <_ 4
6 eluzuzle 
 |-  ( ( 3 e. ZZ /\ 3 <_ 4 ) -> ( X e. ( ZZ>= ` 4 ) -> X e. ( ZZ>= ` 3 ) ) )
7 1 5 6 mp2an 
 |-  ( X e. ( ZZ>= ` 4 ) -> X e. ( ZZ>= ` 3 ) )