Metamath Proof Explorer

Theorem dp2ltc

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

Ref Expression
Hypotheses dp2lt.a ⊢ 𝐴 ∈ ℕ0
dp2lt.b ⊢ 𝐵 ∈ ℝ+
dp2ltc.c ⊢ 𝐶 ∈ ℕ0
dp2ltc.d ⊢ 𝐷 ∈ ℝ+
dp2ltc.s ⊢ 𝐵 < 1 0
dp2ltc.l ⊢ 𝐴 < 𝐶
Assertion dp2ltc 𝐴 𝐵 < 𝐶 𝐷

Proof

Step Hyp Ref Expression
1 dp2lt.a ⊢ 𝐴 ∈ ℕ0
2 dp2lt.b ⊢ 𝐵 ∈ ℝ+
3 dp2ltc.c ⊢ 𝐶 ∈ ℕ0
4 dp2ltc.d ⊢ 𝐷 ∈ ℝ+
5 dp2ltc.s ⊢ 𝐵 < 1 0
6 dp2ltc.l ⊢ 𝐴 < 𝐶
7 rpssre ⊢ ℝ+ ⊆ ℝ
8 7 2 sselii ⊢ 𝐵 ∈ ℝ
9 10re ⊢ 1 0 ∈ ℝ
10 10pos ⊢ 0 < 1 0
11 elrp ⊢ ( 1 0 ∈ ℝ+ ↔ ( 1 0 ∈ ℝ ∧ 0 < 1 0 ) )
12 9 10 11 mpbir2an ⊢ 1 0 ∈ ℝ+
13 divlt1lt ⊢ ( ( 𝐵 ∈ ℝ ∧ 1 0 ∈ ℝ+ ) → ( ( 𝐵 / 1 0 ) < 1 ↔ 𝐵 < 1 0 ) )
14 8 12 13 mp2an ⊢ ( ( 𝐵 / 1 0 ) < 1 ↔ 𝐵 < 1 0 )
15 5 14 mpbir ⊢ ( 𝐵 / 1 0 ) < 1
16 9 10 gt0ne0ii ⊢ 1 0 ≠ 0
17 8 9 16 redivcli ⊢ ( 𝐵 / 1 0 ) ∈ ℝ
18 1re ⊢ 1 ∈ ℝ
19 1 nn0rei ⊢ 𝐴 ∈ ℝ
20 ltadd2 ⊢ ( ( ( 𝐵 / 1 0 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝐵 / 1 0 ) < 1 ↔ ( 𝐴 + ( 𝐵 / 1 0 ) ) < ( 𝐴 + 1 ) ) )
21 17 18 19 20 mp3an ⊢ ( ( 𝐵 / 1 0 ) < 1 ↔ ( 𝐴 + ( 𝐵 / 1 0 ) ) < ( 𝐴 + 1 ) )
22 15 21 mpbi ⊢ ( 𝐴 + ( 𝐵 / 1 0 ) ) < ( 𝐴 + 1 )
23 1 nn0zi ⊢ 𝐴 ∈ ℤ
24 3 nn0zi ⊢ 𝐶 ∈ ℤ
25 zltp1le ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 < 𝐶 ↔ ( 𝐴 + 1 ) ≤ 𝐶 ) )
26 23 24 25 mp2an ⊢ ( 𝐴 < 𝐶 ↔ ( 𝐴 + 1 ) ≤ 𝐶 )
27 6 26 mpbi ⊢ ( 𝐴 + 1 ) ≤ 𝐶
28 19 17 readdcli ⊢ ( 𝐴 + ( 𝐵 / 1 0 ) ) ∈ ℝ
29 19 18 readdcli ⊢ ( 𝐴 + 1 ) ∈ ℝ
30 3 nn0rei ⊢ 𝐶 ∈ ℝ
31 28 29 30 ltletri ⊢ ( ( ( 𝐴 + ( 𝐵 / 1 0 ) ) < ( 𝐴 + 1 ) ∧ ( 𝐴 + 1 ) ≤ 𝐶 ) → ( 𝐴 + ( 𝐵 / 1 0 ) ) < 𝐶 )
32 22 27 31 mp2an ⊢ ( 𝐴 + ( 𝐵 / 1 0 ) ) < 𝐶
33 4 12 pm3.2i ⊢ ( 𝐷 ∈ ℝ+ ∧ 1 0 ∈ ℝ+ )
34 rpdivcl ⊢ ( ( 𝐷 ∈ ℝ+ ∧ 1 0 ∈ ℝ+ ) → ( 𝐷 / 1 0 ) ∈ ℝ+ )
35 33 34 ax-mp ⊢ ( 𝐷 / 1 0 ) ∈ ℝ+
36 ltaddrp ⊢ ( ( 𝐶 ∈ ℝ ∧ ( 𝐷 / 1 0 ) ∈ ℝ+ ) → 𝐶 < ( 𝐶 + ( 𝐷 / 1 0 ) ) )
37 30 35 36 mp2an ⊢ 𝐶 < ( 𝐶 + ( 𝐷 / 1 0 ) )
38 7 4 sselii ⊢ 𝐷 ∈ ℝ
39 38 9 16 redivcli ⊢ ( 𝐷 / 1 0 ) ∈ ℝ
40 30 39 readdcli ⊢ ( 𝐶 + ( 𝐷 / 1 0 ) ) ∈ ℝ
41 28 30 40 lttri ⊢ ( ( ( 𝐴 + ( 𝐵 / 1 0 ) ) < 𝐶 ∧ 𝐶 < ( 𝐶 + ( 𝐷 / 1 0 ) ) ) → ( 𝐴 + ( 𝐵 / 1 0 ) ) < ( 𝐶 + ( 𝐷 / 1 0 ) ) )
42 32 37 41 mp2an ⊢ ( 𝐴 + ( 𝐵 / 1 0 ) ) < ( 𝐶 + ( 𝐷 / 1 0 ) )
43 df-dp2 ⊢ 𝐴 𝐵 = ( 𝐴 + ( 𝐵 / 1 0 ) )
44 df-dp2 ⊢ 𝐶 𝐷 = ( 𝐶 + ( 𝐷 / 1 0 ) )
45 42 43 44 3brtr4i ⊢ 𝐴 𝐵 < 𝐶 𝐷