Metamath Proof Explorer


Theorem le9lt10

Description: A "decimal digit" (i.e. a nonnegative integer less than or equal to 9) is less then 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