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	$$⊢A\in {\mathbb{N}}_0$$
	declt.b	$$⊢B\in {\mathbb{N}}_0$$
	decltc.c	$$⊢C\in {\mathbb{N}}_0$$
	decltc.d	$$⊢D\in {\mathbb{N}}_0$$
	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	$$⊢A\in {\mathbb{N}}_0$$
2		declt.b	$$⊢B\in {\mathbb{N}}_0$$
3		decltc.c	$$⊢C\in {\mathbb{N}}_0$$
4		decltc.d	$$⊢D\in {\mathbb{N}}_0$$
5		decltc.s	$$⊢C<10$$
6		decltc.l	$$⊢A<B$$
7		10nn	$$⊢10\in \mathbb{N}$$
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 |-