This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℤ → X < 1 ↔ X = 0

Proof

Step Hyp Ref Expression
1 nn0abscl ⊢ X ∈ ℤ → X ∈ ℕ 0
2 nn0lt10b ⊢ X ∈ ℕ 0 → X < 1 ↔ X = 0
3 1 2 syl ⊢ X ∈ ℤ → X < 1 ↔ X = 0
4 zcn ⊢ X ∈ ℤ → X ∈ ℂ
5 4 abs00ad ⊢ X ∈ ℤ → X = 0 ↔ X = 0
6 3 5 bitrd ⊢ X ∈ ℤ → X < 1 ↔ X = 0