This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ 𝐴 𝐵 < 𝐴 𝐶