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 ⊢ A ∈ ℕ 0
dp2lt.b ⊢ B ∈ ℝ +
dp2lt.c ⊢ C ∈ ℝ +
dp2lt.l ⊢ B < C
Assertion dp2lt Could not format assertion : No typesetting found for |- _ A B < _ A C with typecode |-

Proof

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