Metamath Proof Explorer

Theorem uzuzle35

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

Ref Expression
Assertion uzuzle35 
|- ( A e. ( ZZ>= ` 5 ) -> A e. ( ZZ>= ` 3 ) )

Proof

Step Hyp Ref Expression
1 5eluz3 
 |-  5 e. ( ZZ>= ` 3 )
2 uzss 
 |-  ( 5 e. ( ZZ>= ` 3 ) -> ( ZZ>= ` 5 ) C_ ( ZZ>= ` 3 ) )
3 1 2 ax-mp 
 |-  ( ZZ>= ` 5 ) C_ ( ZZ>= ` 3 )
4 3 sseli 
 |-  ( A e. ( ZZ>= ` 5 ) -> A e. ( ZZ>= ` 3 ) )