Theorem numltc

Description: Comparing two decimal integers (unequal 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$$
	numltc.3	$$⊢C\in {\mathbb{N}}_0$$
	numltc.4	$$⊢D\in {\mathbb{N}}_0$$
	numltc.5	$$⊢C<T$$
	numltc.6	$$⊢A<B$$
Assertion	numltc	$$⊢TA+C<TB+D$$

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		numltc.3	$$⊢C\in {\mathbb{N}}_0$$
5		numltc.4	$$⊢D\in {\mathbb{N}}_0$$
6		numltc.5	$$⊢C<T$$
7		numltc.6	$$⊢A<B$$
8	1 2 4 1 6	numlt	$$⊢TA+C<TA+T$$
9	1	nnrei	$$⊢T\in ℝ$$
10	9	recni	$$⊢T\in ℂ$$
11	2	nn0rei	$$⊢A\in ℝ$$
12	11	recni	$$⊢A\in ℂ$$
13		ax-1cn	$$⊢1\in ℂ$$
14	10 12 13	adddii	$$⊢T\left(A+1\right)=TA+T\cdot 1$$
15	10	mulridi	$$⊢T\cdot 1=T$$
16	15	oveq2i	$$⊢TA+T\cdot 1=TA+T$$
17	14 16	eqtri	$$⊢T\left(A+1\right)=TA+T$$
18	8 17	breqtrri	$$⊢TA+C<T\left(A+1\right)$$
19		nn0ltp1le	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(A<B\leftrightarrow A+1\le B\right)$$
20	2 3 19	mp2an	$$⊢A<B\leftrightarrow A+1\le B$$
21	7 20	mpbi	$$⊢A+1\le B$$
22	1	nngt0i	$$⊢0<T$$
23		peano2re	$$⊢A\in ℝ\to A+1\in ℝ$$
24	11 23	ax-mp	$$⊢A+1\in ℝ$$
25	3	nn0rei	$$⊢B\in ℝ$$
26	24 25 9	lemul2i	$$⊢0<T\to \left(A+1\le B\leftrightarrow T\left(A+1\right)\le TB\right)$$
27	22 26	ax-mp	$$⊢A+1\le B\leftrightarrow T\left(A+1\right)\le TB$$
28	21 27	mpbi	$$⊢T\left(A+1\right)\le TB$$
29	9 11	remulcli	$$⊢TA\in ℝ$$
30	4	nn0rei	$$⊢C\in ℝ$$
31	29 30	readdcli	$$⊢TA+C\in ℝ$$
32	9 24	remulcli	$$⊢T\left(A+1\right)\in ℝ$$
33	9 25	remulcli	$$⊢TB\in ℝ$$
34	31 32 33	ltletri	$$⊢\left(TA+C<T\left(A+1\right)\wedge T\left(A+1\right)\le TB\right)\to TA+C<TB$$
35	18 28 34	mp2an	$$⊢TA+C<TB$$
36	33 5	nn0addge1i	$$⊢TB\le TB+D$$
37	5	nn0rei	$$⊢D\in ℝ$$
38	33 37	readdcli	$$⊢TB+D\in ℝ$$
39	31 33 38	ltletri	$$⊢\left(TA+C<TB\wedge TB\le TB+D\right)\to TA+C<TB+D$$
40	35 36 39	mp2an	$$⊢TA+C<TB+D$$