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 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