Theorem declt

Description: Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Hypotheses	declt.a	$$⊢A\in {\mathbb{N}}_0$$
	declt.b	$$⊢B\in {\mathbb{N}}_0$$
	declt.c	$$⊢C\in \mathbb{N}$$
	declt.l	$$⊢B<C$$
Assertion	declt	Could not format assertion : No typesetting found for |- ; A B < ; A C with typecode |-

Proof

Step	Hyp	Ref	Expression
1		declt.a	$$⊢A\in {\mathbb{N}}_0$$
2		declt.b	$$⊢B\in {\mathbb{N}}_0$$
3		declt.c	$$⊢C\in \mathbb{N}$$
4		declt.l	$$⊢B<C$$
5		10nn	$$⊢10\in \mathbb{N}$$
6	5 1 2 3 4	numlt	$$⊢10A+B<10A+C$$
7		dfdec10	Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
8		dfdec10	Could not format ; A C = ( ( ; 1 0 x. A ) + C ) : No typesetting found for |- ; A C = ( ( ; 1 0 x. A ) + C ) with typecode |-
9	6 7 8	3brtr4i	Could not format ; A B < ; A C : No typesetting found for |- ; A B < ; A C with typecode |-