Metamath Proof Explorer

Theorem eluz4eluz2

Description: An integer greater than or equal to 4 is an integer greater than or equal to 2. (Contributed by AV, 30-May-2023)

Ref Expression
Assertion eluz4eluz2 
|- ( X e. ( ZZ>= ` 4 ) -> X e. ( ZZ>= ` 2 ) )

Proof

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