Metamath Proof Explorer


Theorem declei

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

Ref Expression
Hypotheses declei.1
|- A e. NN
declei.2
|- B e. NN0
declei.3
|- C e. NN0
declei.4
|- C <_ 9
Assertion declei
|- C <_ ; A B

Proof

Step Hyp Ref Expression
1 declei.1
 |-  A e. NN
2 declei.2
 |-  B e. NN0
3 declei.3
 |-  C e. NN0
4 declei.4
 |-  C <_ 9
5 3 dec0h
 |-  C = ; 0 C
6 0nn0
 |-  0 e. NN0
7 1 nnnn0i
 |-  A e. NN0
8 1 nngt0i
 |-  0 < A
9 6 7 3 2 4 8 decleh
 |-  ; 0 C <_ ; A B
10 5 9 eqbrtri
 |-  C <_ ; A B