Theorem dplti

Description: Comparing a decimal expansions with the next higher integer. (Contributed by Thierry Arnoux, 16-Dec-2021)

	Ref	Expression
Hypotheses	dplti.a	$$⊢A\in {\mathbb{N}}_0$$
	dplti.b	$$⊢B\in {ℝ}^{+}$$
	dplti.c	$$⊢C\in {\mathbb{N}}_0$$
	dplti.1	$$⊢B<10$$
	dplti.2	$$⊢A+1=C$$
Assertion	dplti	$$⊢A.B<C$$

Proof

Step	Hyp	Ref	Expression
1		dplti.a	$$⊢A\in {\mathbb{N}}_0$$
2		dplti.b	$$⊢B\in {ℝ}^{+}$$
3		dplti.c	$$⊢C\in {\mathbb{N}}_0$$
4		dplti.1	$$⊢B<10$$
5		dplti.2	$$⊢A+1=C$$
6		rpre	$$⊢B\in {ℝ}^{+}\to B\in ℝ$$
7	2 6	ax-mp	$$⊢B\in ℝ$$
8	1 7	dpval2	$$⊢A.B=A+\left(\frac{B}{10}\right)$$
9		10re	$$⊢10\in ℝ$$
10		10pos	$$⊢0<10$$
11	9 10	pm3.2i	$$⊢\left(10\in ℝ\wedge 0<10\right)$$
12		elrp	$$⊢10\in {ℝ}^{+}\leftrightarrow \left(10\in ℝ\wedge 0<10\right)$$
13	11 12	mpbir	$$⊢10\in {ℝ}^{+}$$
14		divlt1lt	$$⊢\left(B\in ℝ\wedge 10\in {ℝ}^{+}\right)\to \left(\frac{B}{10}<1\leftrightarrow B<10\right)$$
15	7 13 14	mp2an	$$⊢\frac{B}{10}<1\leftrightarrow B<10$$
16	4 15	mpbir	$$⊢\frac{B}{10}<1$$
17		0re	$$⊢0\in ℝ$$
18	17 10	gtneii	$$⊢10\ne 0$$
19	7 9 18	redivcli	$$⊢\frac{B}{10}\in ℝ$$
20		1re	$$⊢1\in ℝ$$
21		nn0ssre	$$⊢{\mathbb{N}}_0\subseteq ℝ$$
22	21 1	sselii	$$⊢A\in ℝ$$
23	19 20 22	ltadd2i	$$⊢\frac{B}{10}<1\leftrightarrow A+\left(\frac{B}{10}\right)<A+1$$
24	16 23	mpbi	$$⊢A+\left(\frac{B}{10}\right)<A+1$$
25	8 24	eqbrtri	$$⊢A.B<A+1$$
26	25 5	breqtri	$$⊢A.B<C$$