Theorem dpgti

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

	Ref	Expression
Hypotheses	dpgti.a	$$⊢A\in {\mathbb{N}}_0$$
	dpgti.b	$$⊢B\in {ℝ}^{+}$$
Assertion	dpgti	$$⊢A<A.B$$

Proof

Step	Hyp	Ref	Expression
1		dpgti.a	$$⊢A\in {\mathbb{N}}_0$$
2		dpgti.b	$$⊢B\in {ℝ}^{+}$$
3	1	nn0rei	$$⊢A\in ℝ$$
4		10re	$$⊢10\in ℝ$$
5		10pos	$$⊢0<10$$
6	4 5	pm3.2i	$$⊢\left(10\in ℝ\wedge 0<10\right)$$
7		elrp	$$⊢10\in {ℝ}^{+}\leftrightarrow \left(10\in ℝ\wedge 0<10\right)$$
8	6 7	mpbir	$$⊢10\in {ℝ}^{+}$$
9		rpdivcl	$$⊢\left(B\in {ℝ}^{+}\wedge 10\in {ℝ}^{+}\right)\to \frac{B}{10}\in {ℝ}^{+}$$
10	2 8 9	mp2an	$$⊢\frac{B}{10}\in {ℝ}^{+}$$
11		ltaddrp	$$⊢\left(A\in ℝ\wedge \frac{B}{10}\in {ℝ}^{+}\right)\to A<A+\left(\frac{B}{10}\right)$$
12	3 10 11	mp2an	$$⊢A<A+\left(\frac{B}{10}\right)$$
13		rpre	$$⊢B\in {ℝ}^{+}\to B\in ℝ$$
14	2 13	ax-mp	$$⊢B\in ℝ$$
15	1 14	dpval2	$$⊢A.B=A+\left(\frac{B}{10}\right)$$
16	12 15	breqtrri	$$⊢A<A.B$$