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