Metamath Proof Explorer

Theorem zabs0b

Description: An integer has an absolute value less than 1 iff it is 0. (Contributed by AV, 21-Nov-2025)

Ref Expression
Assertion zabs0b 
|- ( X e. ZZ -> ( ( abs ` X ) < 1 <-> X = 0 ) )

Proof

Step Hyp Ref Expression
1 nn0abscl 
 |-  ( X e. ZZ -> ( abs ` X ) e. NN0 )
2 nn0lt10b 
 |-  ( ( abs ` X ) e. NN0 -> ( ( abs ` X ) < 1 <-> ( abs ` X ) = 0 ) )
3 1 2 syl 
 |-  ( X e. ZZ -> ( ( abs ` X ) < 1 <-> ( abs ` X ) = 0 ) )
4 zcn 
 |-  ( X e. ZZ -> X e. CC )
5 4 abs00ad 
 |-  ( X e. ZZ -> ( ( abs ` X ) = 0 <-> X = 0 ) )
6 3 5 bitrd 
 |-  ( X e. ZZ -> ( ( abs ` X ) < 1 <-> X = 0 ) )