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 ⊢ A ∈ ℕ 0
le9lt10.e ⊢ A ≤ 9
Assertion le9lt10 ⊢ A < 10

Proof

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