Metamath Proof Explorer


Theorem decltc

Description: Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)

Ref Expression
Hypotheses declt.a A0
declt.b B0
decltc.c C0
decltc.d D0
decltc.s C<10
decltc.l A<B
Assertion decltc Could not format assertion : No typesetting found for |- ; A C < ; B D with typecode |-

Proof

Step Hyp Ref Expression
1 declt.a A0
2 declt.b B0
3 decltc.c C0
4 decltc.d D0
5 decltc.s C<10
6 decltc.l A<B
7 10nn 10
8 7 1 2 3 4 5 6 numltc 10A+C<10B+D
9 dfdec10 Could not format ; A C = ( ( ; 1 0 x. A ) + C ) : No typesetting found for |- ; A C = ( ( ; 1 0 x. A ) + C ) with typecode |-
10 dfdec10 Could not format ; B D = ( ( ; 1 0 x. B ) + D ) : No typesetting found for |- ; B D = ( ( ; 1 0 x. B ) + D ) with typecode |-
11 8 9 10 3brtr4i Could not format ; A C < ; B D : No typesetting found for |- ; A C < ; B D with typecode |-