This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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