Theorem dp2lt10

Description: Decimal fraction builds real numbers less than 10. (Contributed by Thierry Arnoux, 16-Dec-2021)

	Ref	Expression
Hypotheses	dp2lt10.a	$$⊢A\in {\mathbb{N}}_0$$
	dp2lt10.b	$$⊢B\in {ℝ}^{+}$$
	dp2lt10.1	$$⊢A<10$$
	dp2lt10.2	$$⊢B<10$$
Assertion	dp2lt10	Could not format assertion : No typesetting found for |- _ A B < ; 1 0 with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dp2lt10.a	$$⊢A\in {\mathbb{N}}_0$$
2		dp2lt10.b	$$⊢B\in {ℝ}^{+}$$
3		dp2lt10.1	$$⊢A<10$$
4		dp2lt10.2	$$⊢B<10$$
5		df-dp2	Could not format _ A B = ( A + ( B / ; 1 0 ) ) : No typesetting found for |- _ A B = ( A + ( B / ; 1 0 ) ) with typecode |-
6		9p1e10	$$⊢9+1=10$$
7	3 6	breqtrri	$$⊢A<9+1$$
8	1	nn0zi	$$⊢A\in \mathbb{Z}$$
9		9nn0	$$⊢9\in {\mathbb{N}}_0$$
10	9	nn0zi	$$⊢9\in \mathbb{Z}$$
11		zleltp1	$$⊢\left(A\in \mathbb{Z}\wedge 9\in \mathbb{Z}\right)\to \left(A\le 9\leftrightarrow A<9+1\right)$$
12	8 10 11	mp2an	$$⊢A\le 9\leftrightarrow A<9+1$$
13	7 12	mpbir	$$⊢A\le 9$$
14		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
15	14 2	sselii	$$⊢B\in ℝ$$
16		10re	$$⊢10\in ℝ$$
17		10pos	$$⊢0<10$$
18	16 17	elrpii	$$⊢10\in {ℝ}^{+}$$
19		divlt1lt	$$⊢\left(B\in ℝ\wedge 10\in {ℝ}^{+}\right)\to \left(\frac{B}{10}<1\leftrightarrow B<10\right)$$
20	15 18 19	mp2an	$$⊢\frac{B}{10}<1\leftrightarrow B<10$$
21	4 20	mpbir	$$⊢\frac{B}{10}<1$$
22	1	nn0rei	$$⊢A\in ℝ$$
23		0re	$$⊢0\in ℝ$$
24	23 17	gtneii	$$⊢10\ne 0$$
25	15 16 24	redivcli	$$⊢\frac{B}{10}\in ℝ$$
26	22 25	pm3.2i	$$⊢\left(A\in ℝ\wedge \frac{B}{10}\in ℝ\right)$$
27		9re	$$⊢9\in ℝ$$
28		1re	$$⊢1\in ℝ$$
29	27 28	pm3.2i	$$⊢\left(9\in ℝ\wedge 1\in ℝ\right)$$
30		leltadd	$$⊢\left(\left(A\in ℝ\wedge \frac{B}{10}\in ℝ\right)\wedge \left(9\in ℝ\wedge 1\in ℝ\right)\right)\to \left(\left(A\le 9\wedge \frac{B}{10}<1\right)\to A+\left(\frac{B}{10}\right)<9+1\right)$$
31	26 29 30	mp2an	$$⊢\left(A\le 9\wedge \frac{B}{10}<1\right)\to A+\left(\frac{B}{10}\right)<9+1$$
32	13 21 31	mp2an	$$⊢A+\left(\frac{B}{10}\right)<9+1$$
33	32 6	breqtri	$$⊢A+\left(\frac{B}{10}\right)<10$$
34	5 33	eqbrtri	Could not format _ A B < ; 1 0 : No typesetting found for |- _ A B < ; 1 0 with typecode |-