Metamath Proof Explorer
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 |
|
|
|
declt.b |
|
|
|
decltc.c |
|
|
|
decltc.d |
|
|
|
decltc.s |
|
|
|
decltc.l |
|
|
Assertion |
decltc |
Could not format assertion : No typesetting found for |- ; A C < ; B D with typecode |- |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
declt.a |
|
2 |
|
declt.b |
|
3 |
|
decltc.c |
|
4 |
|
decltc.d |
|
5 |
|
decltc.s |
|
6 |
|
decltc.l |
|
7 |
|
10nn |
|
8 |
7 1 2 3 4 5 6
|
numltc |
|
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 |- |