Theorem dp2ltc

Description: Comparing two decimal expansions (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021)

	Ref	Expression
Hypotheses	dp2lt.a	$$⊢A\in {\mathbb{N}}_0$$
	dp2lt.b	$$⊢B\in {ℝ}^{+}$$
	dp2ltc.c	$$⊢C\in {\mathbb{N}}_0$$
	dp2ltc.d	$$⊢D\in {ℝ}^{+}$$
	dp2ltc.s	$$⊢B<10$$
	dp2ltc.l	$$⊢A<C$$
Assertion	dp2ltc	Could not format assertion : No typesetting found for |- _ A B < _ C D with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dp2lt.a	$$⊢A\in {\mathbb{N}}_0$$
2		dp2lt.b	$$⊢B\in {ℝ}^{+}$$
3		dp2ltc.c	$$⊢C\in {\mathbb{N}}_0$$
4		dp2ltc.d	$$⊢D\in {ℝ}^{+}$$
5		dp2ltc.s	$$⊢B<10$$
6		dp2ltc.l	$$⊢A<C$$
7		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
8	7 2	sselii	$$⊢B\in ℝ$$
9		10re	$$⊢10\in ℝ$$
10		10pos	$$⊢0<10$$
11		elrp	$$⊢10\in {ℝ}^{+}\leftrightarrow \left(10\in ℝ\wedge 0<10\right)$$
12	9 10 11	mpbir2an	$$⊢10\in {ℝ}^{+}$$
13		divlt1lt	$$⊢\left(B\in ℝ\wedge 10\in {ℝ}^{+}\right)\to \left(\frac{B}{10}<1\leftrightarrow B<10\right)$$
14	8 12 13	mp2an	$$⊢\frac{B}{10}<1\leftrightarrow B<10$$
15	5 14	mpbir	$$⊢\frac{B}{10}<1$$
16	9 10	gt0ne0ii	$$⊢10\ne 0$$
17	8 9 16	redivcli	$$⊢\frac{B}{10}\in ℝ$$
18		1re	$$⊢1\in ℝ$$
19	1	nn0rei	$$⊢A\in ℝ$$
20		ltadd2	$$⊢\left(\frac{B}{10}\in ℝ\wedge 1\in ℝ\wedge A\in ℝ\right)\to \left(\frac{B}{10}<1\leftrightarrow A+\left(\frac{B}{10}\right)<A+1\right)$$
21	17 18 19 20	mp3an	$$⊢\frac{B}{10}<1\leftrightarrow A+\left(\frac{B}{10}\right)<A+1$$
22	15 21	mpbi	$$⊢A+\left(\frac{B}{10}\right)<A+1$$
23	1	nn0zi	$$⊢A\in \mathbb{Z}$$
24	3	nn0zi	$$⊢C\in \mathbb{Z}$$
25		zltp1le	$$⊢\left(A\in \mathbb{Z}\wedge C\in \mathbb{Z}\right)\to \left(A<C\leftrightarrow A+1\le C\right)$$
26	23 24 25	mp2an	$$⊢A<C\leftrightarrow A+1\le C$$
27	6 26	mpbi	$$⊢A+1\le C$$
28	19 17	readdcli	$$⊢A+\left(\frac{B}{10}\right)\in ℝ$$
29	19 18	readdcli	$$⊢A+1\in ℝ$$
30	3	nn0rei	$$⊢C\in ℝ$$
31	28 29 30	ltletri	$$⊢\left(A+\left(\frac{B}{10}\right)<A+1\wedge A+1\le C\right)\to A+\left(\frac{B}{10}\right)<C$$
32	22 27 31	mp2an	$$⊢A+\left(\frac{B}{10}\right)<C$$
33	4 12	pm3.2i	$$⊢\left(D\in {ℝ}^{+}\wedge 10\in {ℝ}^{+}\right)$$
34		rpdivcl	$$⊢\left(D\in {ℝ}^{+}\wedge 10\in {ℝ}^{+}\right)\to \frac{D}{10}\in {ℝ}^{+}$$
35	33 34	ax-mp	$$⊢\frac{D}{10}\in {ℝ}^{+}$$
36		ltaddrp	$$⊢\left(C\in ℝ\wedge \frac{D}{10}\in {ℝ}^{+}\right)\to C<C+\left(\frac{D}{10}\right)$$
37	30 35 36	mp2an	$$⊢C<C+\left(\frac{D}{10}\right)$$
38	7 4	sselii	$$⊢D\in ℝ$$
39	38 9 16	redivcli	$$⊢\frac{D}{10}\in ℝ$$
40	30 39	readdcli	$$⊢C+\left(\frac{D}{10}\right)\in ℝ$$
41	28 30 40	lttri	$$⊢\left(A+\left(\frac{B}{10}\right)<C\wedge C<C+\left(\frac{D}{10}\right)\right)\to A+\left(\frac{B}{10}\right)<C+\left(\frac{D}{10}\right)$$
42	32 37 41	mp2an	$$⊢A+\left(\frac{B}{10}\right)<C+\left(\frac{D}{10}\right)$$
43		df-dp2	Could not format _ A B = ( A + ( B / ; 1 0 ) ) : No typesetting found for |- _ A B = ( A + ( B / ; 1 0 ) ) with typecode |-
44		df-dp2	Could not format _ C D = ( C + ( D / ; 1 0 ) ) : No typesetting found for |- _ C D = ( C + ( D / ; 1 0 ) ) with typecode |-
45	42 43 44	3brtr4i	Could not format _ A B < _ C D : No typesetting found for |- _ A B < _ C D with typecode |-