dpgti

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

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

Metamath Proof Explorer