Theorem dp2lt

Description: Comparing two decimal fractions (equal unit places). (Contributed by Thierry Arnoux, 16-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		dp2lt.a	$$⊢A\in {\mathbb{N}}_0$$
2		dp2lt.b	$$⊢B\in {ℝ}^{+}$$
3		dp2lt.c	$$⊢C\in {ℝ}^{+}$$
4		dp2lt.l	$$⊢B<C$$
5		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
6	5 2	sselii	$$⊢B\in ℝ$$
7		10re	$$⊢10\in ℝ$$
8		0re	$$⊢0\in ℝ$$
9		10pos	$$⊢0<10$$
10	8 9	gtneii	$$⊢10\ne 0$$
11		redivcl	$$⊢\left(B\in ℝ\wedge 10\in ℝ\wedge 10\ne 0\right)\to \frac{B}{10}\in ℝ$$
12	6 7 10 11	mp3an	$$⊢\frac{B}{10}\in ℝ$$
13	5 3	sselii	$$⊢C\in ℝ$$
14		redivcl	$$⊢\left(C\in ℝ\wedge 10\in ℝ\wedge 10\ne 0\right)\to \frac{C}{10}\in ℝ$$
15	13 7 10 14	mp3an	$$⊢\frac{C}{10}\in ℝ$$
16	1	nn0rei	$$⊢A\in ℝ$$
17	12 15 16	3pm3.2i	$$⊢\left(\frac{B}{10}\in ℝ\wedge \frac{C}{10}\in ℝ\wedge A\in ℝ\right)$$
18	7 9	pm3.2i	$$⊢\left(10\in ℝ\wedge 0<10\right)$$
19		ltdiv1	$$⊢\left(B\in ℝ\wedge C\in ℝ\wedge \left(10\in ℝ\wedge 0<10\right)\right)\to \left(B<C\leftrightarrow \frac{B}{10}<\frac{C}{10}\right)$$
20	6 13 18 19	mp3an	$$⊢B<C\leftrightarrow \frac{B}{10}<\frac{C}{10}$$
21	4 20	mpbi	$$⊢\frac{B}{10}<\frac{C}{10}$$
22		axltadd	$$⊢\left(\frac{B}{10}\in ℝ\wedge \frac{C}{10}\in ℝ\wedge A\in ℝ\right)\to \left(\frac{B}{10}<\frac{C}{10}\to A+\left(\frac{B}{10}\right)<A+\left(\frac{C}{10}\right)\right)$$
23	22	imp	$$⊢\left(\left(\frac{B}{10}\in ℝ\wedge \frac{C}{10}\in ℝ\wedge A\in ℝ\right)\wedge \frac{B}{10}<\frac{C}{10}\right)\to A+\left(\frac{B}{10}\right)<A+\left(\frac{C}{10}\right)$$
24	17 21 23	mp2an	$$⊢A+\left(\frac{B}{10}\right)<A+\left(\frac{C}{10}\right)$$
25		df-dp2	Could not format _ A B = ( A + ( B / ; 1 0 ) ) : No typesetting found for |- _ A B = ( A + ( B / ; 1 0 ) ) with typecode |-
26		df-dp2	Could not format _ A C = ( A + ( C / ; 1 0 ) ) : No typesetting found for |- _ A C = ( A + ( C / ; 1 0 ) ) with typecode |-
27	24 25 26	3brtr4i	Could not format _ A B < _ A C : No typesetting found for |- _ A B < _ A C with typecode |-