dp2ltc

Description: Comparing two decimal expansions (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021)

	Ref	Expression
Hypotheses	dp2lt.a	$⊢ A \in ℕ_{0}$
	dp2lt.b	$⊢ B \in ℝ^{+}$
	dp2ltc.c	$⊢ C \in ℕ_{0}$
	dp2ltc.d	$⊢ D \in ℝ^{+}$
	dp2ltc.s	$⊢ B < 10$
	dp2ltc.l	$⊢ A < C$
Assertion	dp2ltc	Could not format assertion : No typesetting found for \|- _ A B < _ C D with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		dp2lt.a	$⊢ A \in ℕ_{0}$
2		dp2lt.b	$⊢ B \in ℝ^{+}$
3		dp2ltc.c	$⊢ C \in ℕ_{0}$
4		dp2ltc.d	$⊢ D \in ℝ^{+}$
5		dp2ltc.s	$⊢ B < 10$
6		dp2ltc.l	$⊢ A < C$
7		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
8	7 2	sselii	$⊢ B \in ℝ$
9		10re	$⊢ 10 \in ℝ$
10		10pos	$⊢ 0 < 10$
11		elrp	$⊢ 10 \in ℝ^{+} \leftrightarrow (10 \in ℝ \land 0 < 10)$
12	9 10 11	mpbir2an	$⊢ 10 \in ℝ^{+}$
13		divlt1lt	$⊢ (B \in ℝ \land 10 \in ℝ^{+}) \to (\frac{B}{10} < 1 \leftrightarrow B < 10)$
14	8 12 13	mp2an	$⊢ \frac{B}{10} < 1 \leftrightarrow B < 10$
15	5 14	mpbir	$⊢ \frac{B}{10} < 1$
16	9 10	gt0ne0ii	$⊢ 10 \neq 0$
17	8 9 16	redivcli	$⊢ \frac{B}{10} \in ℝ$
18		1re	$⊢ 1 \in ℝ$
19	1	nn0rei	$⊢ A \in ℝ$
20		ltadd2	$⊢ (\frac{B}{10} \in ℝ \land 1 \in ℝ \land A \in ℝ) \to (\frac{B}{10} < 1 \leftrightarrow A + (\frac{B}{10}) < A + 1)$
21	17 18 19 20	mp3an	$⊢ \frac{B}{10} < 1 \leftrightarrow A + (\frac{B}{10}) < A + 1$
22	15 21	mpbi	$⊢ A + (\frac{B}{10}) < A + 1$
23	1	nn0zi	$⊢ A \in ℤ$
24	3	nn0zi	$⊢ C \in ℤ$
25		zltp1le	$⊢ (A \in ℤ \land C \in ℤ) \to (A < C \leftrightarrow A + 1 \leq C)$
26	23 24 25	mp2an	$⊢ A < C \leftrightarrow A + 1 \leq C$
27	6 26	mpbi	$⊢ A + 1 \leq C$
28	19 17	readdcli	$⊢ A + (\frac{B}{10}) \in ℝ$
29	19 18	readdcli	$⊢ A + 1 \in ℝ$
30	3	nn0rei	$⊢ C \in ℝ$
31	28 29 30	ltletri	$⊢ (A + (\frac{B}{10}) < A + 1 \land A + 1 \leq C) \to A + (\frac{B}{10}) < C$
32	22 27 31	mp2an	$⊢ A + (\frac{B}{10}) < C$
33	4 12	pm3.2i	$⊢ (D \in ℝ^{+} \land 10 \in ℝ^{+})$
34		rpdivcl	$⊢ (D \in ℝ^{+} \land 10 \in ℝ^{+}) \to \frac{D}{10} \in ℝ^{+}$
35	33 34	ax-mp	$⊢ \frac{D}{10} \in ℝ^{+}$
36		ltaddrp	$⊢ (C \in ℝ \land \frac{D}{10} \in ℝ^{+}) \to C < C + (\frac{D}{10})$
37	30 35 36	mp2an	$⊢ C < C + (\frac{D}{10})$
38	7 4	sselii	$⊢ D \in ℝ$
39	38 9 16	redivcli	$⊢ \frac{D}{10} \in ℝ$
40	30 39	readdcli	$⊢ C + (\frac{D}{10}) \in ℝ$
41	28 30 40	lttri	$⊢ (A + (\frac{B}{10}) < C \land C < C + (\frac{D}{10})) \to A + (\frac{B}{10}) < C + (\frac{D}{10})$
42	32 37 41	mp2an	$⊢ A + (\frac{B}{10}) < C + (\frac{D}{10})$
43		df-dp2	Could not format _ A B = ( A + ( B / ; 1 0 ) ) : No typesetting found for \|- _ A B = ( A + ( B / ; 1 0 ) ) with typecode \|-
44		df-dp2	Could not format _ C D = ( C + ( D / ; 1 0 ) ) : No typesetting found for \|- _ C D = ( C + ( D / ; 1 0 ) ) with typecode \|-
45	42 43 44	3brtr4i	Could not format _ A B < _ C D : No typesetting found for \|- _ A B < _ C D with typecode \|-

Metamath Proof Explorer

Theorem dp2ltc

Proof