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 A0
le9lt10.e A9
Assertion le9lt10 A<10

Proof

Step Hyp Ref Expression
1 le9lt10.c A0
2 le9lt10.e A9
3 1 nn0zi A
4 9nn0 90
5 4 nn0zi 9
6 zleltp1 A9A9A<9+1
7 3 5 6 mp2an A9A<9+1
8 2 7 mpbi A<9+1
9 9p1e10 9+1=10
10 8 9 breqtri A<10