Theorem numlt

Description: Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 18-Feb-2014)

	Ref	Expression
Hypotheses	numlt.1	$$⊢T\in \mathbb{N}$$
	numlt.2	$$⊢A\in {\mathbb{N}}_0$$
	numlt.3	$$⊢B\in {\mathbb{N}}_0$$
	numlt.4	$$⊢C\in \mathbb{N}$$
	numlt.5	$$⊢B<C$$
Assertion	numlt	$$⊢TA+B<TA+C$$

Proof

Step	Hyp	Ref	Expression
1		numlt.1	$$⊢T\in \mathbb{N}$$
2		numlt.2	$$⊢A\in {\mathbb{N}}_0$$
3		numlt.3	$$⊢B\in {\mathbb{N}}_0$$
4		numlt.4	$$⊢C\in \mathbb{N}$$
5		numlt.5	$$⊢B<C$$
6	3	nn0rei	$$⊢B\in ℝ$$
7	4	nnrei	$$⊢C\in ℝ$$
8	1	nnnn0i	$$⊢T\in {\mathbb{N}}_0$$
9	8 2	nn0mulcli	$$⊢TA\in {\mathbb{N}}_0$$
10	9	nn0rei	$$⊢TA\in ℝ$$
11	6 7 10	ltadd2i	$$⊢B<C\leftrightarrow TA+B<TA+C$$
12	5 11	mpbi	$$⊢TA+B<TA+C$$