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

Metamath Proof Explorer

Theorem le9lt10

Description: A "decimal digit" (i.e. a nonnegative integer less than or equal to 9) is less than 10. (Contributed by AV, 8-Sep-2021)

Ref Expression
Hypotheses le9lt10.c ⊢ 𝐴 ∈ ℕ0
le9lt10.e ⊢ 𝐴 ≤ 9
Assertion le9lt10 𝐴 < 1 0

Proof

Step Hyp Ref Expression
1 le9lt10.c ⊢ 𝐴 ∈ ℕ0
2 le9lt10.e ⊢ 𝐴 ≤ 9
3 1 nn0zi ⊢ 𝐴 ∈ ℤ
4 9nn0 ⊢ 9 ∈ ℕ0
5 4 nn0zi ⊢ 9 ∈ ℤ
6 zleltp1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 9 ∈ ℤ ) → ( 𝐴 ≤ 9 ↔ 𝐴 < ( 9 + 1 ) ) )
7 3 5 6 mp2an ⊢ ( 𝐴 ≤ 9 ↔ 𝐴 < ( 9 + 1 ) )
8 2 7 mpbi ⊢ 𝐴 < ( 9 + 1 )
9 9p1e10 ⊢ ( 9 + 1 ) = 1 0
10 8 9 breqtri ⊢ 𝐴 < 1 0