Theorem decle

Description: Comparing two decimal integers (equal higher places). (Contributed by AV, 17-Aug-2021) (Revised by AV, 8-Sep-2021)

	Ref	Expression
Hypotheses	decle.1	$$⊢A\in {\mathbb{N}}_0$$
	decle.2	$$⊢B\in {\mathbb{N}}_0$$
	decle.3	$$⊢C\in {\mathbb{N}}_0$$
	decle.4	$$⊢B\le C$$
Assertion	decle	Could not format assertion : No typesetting found for |- ; A B <_ ; A C with typecode |-

Proof

Step	Hyp	Ref	Expression
1		decle.1	$$⊢A\in {\mathbb{N}}_0$$
2		decle.2	$$⊢B\in {\mathbb{N}}_0$$
3		decle.3	$$⊢C\in {\mathbb{N}}_0$$
4		decle.4	$$⊢B\le C$$
5	2	nn0rei	$$⊢B\in ℝ$$
6	3	nn0rei	$$⊢C\in ℝ$$
7		10nn0	$$⊢10\in {\mathbb{N}}_0$$
8	7 1	nn0mulcli	$$⊢10A\in {\mathbb{N}}_0$$
9	8	nn0rei	$$⊢10A\in ℝ$$
10	5 6 9	leadd2i	$$⊢B\le C\leftrightarrow 10A+B\le 10A+C$$
11	4 10	mpbi	$$⊢10A+B\le 10A+C$$
12		dfdec10	Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
13		dfdec10	Could not format ; A C = ( ( ; 1 0 x. A ) + C ) : No typesetting found for |- ; A C = ( ( ; 1 0 x. A ) + C ) with typecode |-
14	11 12 13	3brtr4i	Could not format ; A B <_ ; A C : No typesetting found for |- ; A B <_ ; A C with typecode |-