Metamath Proof Explorer


Theorem decltdi

Description: Comparing a digit to a decimal integer. (Contributed by AV, 8-Sep-2021)

Ref Expression
Hypotheses declti.a
|- A e. NN
declti.b
|- B e. NN0
declti.c
|- C e. NN0
decltdi.4
|- C <_ 9
Assertion decltdi
|- C < ; A B

Proof

Step Hyp Ref Expression
1 declti.a
 |-  A e. NN
2 declti.b
 |-  B e. NN0
3 declti.c
 |-  C e. NN0
4 decltdi.4
 |-  C <_ 9
5 3 4 le9lt10
 |-  C < ; 1 0
6 1 2 3 5 declti
 |-  C < ; A B