dp2lt10

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

	Ref	Expression
Hypotheses	dp2lt10.a	$⊢ A \in ℕ_{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 ℕ_{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 ℤ$
9		9nn0	$⊢ 9 \in ℕ_{0}$
10	9	nn0zi	$⊢ 9 \in ℤ$
11		zleltp1	$⊢ (A \in ℤ \land 9 \in ℤ) \to (A \leq 9 \leftrightarrow A < 9 + 1)$
12	8 10 11	mp2an	$⊢ A \leq 9 \leftrightarrow A < 9 + 1$
13	7 12	mpbir	$⊢ A \leq 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	$⊢ (B \in ℝ \land 10 \in ℝ^{+}) \to (\frac{B}{10} < 1 \leftrightarrow B < 10)$
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 \neq 0$
25	15 16 24	redivcli	$⊢ \frac{B}{10} \in ℝ$
26	22 25	pm3.2i	$⊢ (A \in ℝ \land \frac{B}{10} \in ℝ)$
27		9re	$⊢ 9 \in ℝ$
28		1re	$⊢ 1 \in ℝ$
29	27 28	pm3.2i	$⊢ (9 \in ℝ \land 1 \in ℝ)$
30		leltadd	$⊢ ((A \in ℝ \land \frac{B}{10} \in ℝ) \land (9 \in ℝ \land 1 \in ℝ)) \to ((A \leq 9 \land \frac{B}{10} < 1) \to A + (\frac{B}{10}) < 9 + 1)$
31	26 29 30	mp2an	$⊢ (A \leq 9 \land \frac{B}{10} < 1) \to A + (\frac{B}{10}) < 9 + 1$
32	13 21 31	mp2an	$⊢ A + (\frac{B}{10}) < 9 + 1$
33	32 6	breqtri	$⊢ A + (\frac{B}{10}) < 10$
34	5 33	eqbrtri	Could not format _ A B < ; 1 0 : No typesetting found for \|- _ A B < ; 1 0 with typecode \|-

Metamath Proof Explorer

Theorem dp2lt10

Proof