Theorem dp2lt

Description: Comparing two decimal fractions (equal unit places). (Contributed by Thierry Arnoux, 16-Dec-2021)

	Ref	Expression
Hypotheses	dp2lt.a	⊢ 𝐴 ∈ ℕ0
	dp2lt.b	⊢ 𝐵 ∈ ℝ+
	dp2lt.c	⊢ 𝐶 ∈ ℝ+
	dp2lt.l	⊢ 𝐵 < 𝐶
Assertion	dp2lt	⊢ _ 𝐴 𝐵 < _ 𝐴 𝐶

Proof

Step	Hyp	Ref	Expression
1		dp2lt.a	⊢ 𝐴 ∈ ℕ0
2		dp2lt.b	⊢ 𝐵 ∈ ℝ+
3		dp2lt.c	⊢ 𝐶 ∈ ℝ+
4		dp2lt.l	⊢ 𝐵 < 𝐶
5		rpssre	⊢ ℝ+ ⊆ ℝ
6	5 2	sselii	⊢ 𝐵 ∈ ℝ
7		10re	⊢ ; 1 0 ∈ ℝ
8		0re	⊢ 0 ∈ ℝ
9		10pos	⊢ 0 < ; 1 0
10	8 9	gtneii	⊢ ; 1 0 ≠ 0
11		redivcl	⊢ ( ( 𝐵 ∈ ℝ ∧ ; 1 0 ∈ ℝ ∧ ; 1 0 ≠ 0 ) → ( 𝐵 / ; 1 0 ) ∈ ℝ )
12	6 7 10 11	mp3an	⊢ ( 𝐵 / ; 1 0 ) ∈ ℝ
13	5 3	sselii	⊢ 𝐶 ∈ ℝ
14		redivcl	⊢ ( ( 𝐶 ∈ ℝ ∧ ; 1 0 ∈ ℝ ∧ ; 1 0 ≠ 0 ) → ( 𝐶 / ; 1 0 ) ∈ ℝ )
15	13 7 10 14	mp3an	⊢ ( 𝐶 / ; 1 0 ) ∈ ℝ
16	1	nn0rei	⊢ 𝐴 ∈ ℝ
17	12 15 16	3pm3.2i	⊢ ( ( 𝐵 / ; 1 0 ) ∈ ℝ ∧ ( 𝐶 / ; 1 0 ) ∈ ℝ ∧ 𝐴 ∈ ℝ )
18	7 9	pm3.2i	⊢ ( ; 1 0 ∈ ℝ ∧ 0 < ; 1 0 )
19		ltdiv1	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ ( ; 1 0 ∈ ℝ ∧ 0 < ; 1 0 ) ) → ( 𝐵 < 𝐶 ↔ ( 𝐵 / ; 1 0 ) < ( 𝐶 / ; 1 0 ) ) )
20	6 13 18 19	mp3an	⊢ ( 𝐵 < 𝐶 ↔ ( 𝐵 / ; 1 0 ) < ( 𝐶 / ; 1 0 ) )
21	4 20	mpbi	⊢ ( 𝐵 / ; 1 0 ) < ( 𝐶 / ; 1 0 )
22		axltadd	⊢ ( ( ( 𝐵 / ; 1 0 ) ∈ ℝ ∧ ( 𝐶 / ; 1 0 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 / ; 1 0 ) < ( 𝐶 / ; 1 0 ) → ( 𝐴 + ( 𝐵 / ; 1 0 ) ) < ( 𝐴 + ( 𝐶 / ; 1 0 ) ) ) )
23	22	imp	⊢ ( ( ( ( 𝐵 / ; 1 0 ) ∈ ℝ ∧ ( 𝐶 / ; 1 0 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 / ; 1 0 ) < ( 𝐶 / ; 1 0 ) ) → ( 𝐴 + ( 𝐵 / ; 1 0 ) ) < ( 𝐴 + ( 𝐶 / ; 1 0 ) ) )
24	17 21 23	mp2an	⊢ ( 𝐴 + ( 𝐵 / ; 1 0 ) ) < ( 𝐴 + ( 𝐶 / ; 1 0 ) )
25		df-dp2	⊢ _ 𝐴 𝐵 = ( 𝐴 + ( 𝐵 / ; 1 0 ) )
26		df-dp2	⊢ _ 𝐴 𝐶 = ( 𝐴 + ( 𝐶 / ; 1 0 ) )
27	24 25 26	3brtr4i	⊢ _ 𝐴 𝐵 < _ 𝐴 𝐶