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

Metamath Proof Explorer

Theorem dp2ltsuc

Description: Comparing a decimal fraction with the next integer. (Contributed by Thierry Arnoux, 25-Dec-2021)

Ref Expression
Hypotheses dp2lt.a ⊢ A ∈ ℕ 0
dp2lt.b ⊢ B ∈ ℝ +
dp2ltsuc.1 ⊢ B < 10
dp2ltsuc.2 ⊢ A + 1 = C
Assertion dp2ltsuc Could not format assertion : No typesetting found for |- _ A B < C with typecode |-

Proof

Step Hyp Ref Expression
1 dp2lt.a ⊢ A ∈ ℕ 0
2 dp2lt.b ⊢ B ∈ ℝ +
3 dp2ltsuc.1 ⊢ B < 10
4 dp2ltsuc.2 ⊢ A + 1 = C
5 rpre ⊢ B ∈ ℝ + → B ∈ ℝ
6 2 5 ax-mp ⊢ B ∈ ℝ
7 10re ⊢ 10 ∈ ℝ
8 10pos ⊢ 0 < 10
9 6 7 7 8 ltdiv1ii ⊢ B < 10 ↔ B 10 < 10 10
10 3 9 mpbi ⊢ B 10 < 10 10
11 7 recni ⊢ 10 ∈ ℂ
12 10nn ⊢ 10 ∈ ℕ
13 12 nnne0i ⊢ 10 ≠ 0
14 11 13 dividi ⊢ 10 10 = 1
15 10 14 breqtri ⊢ B 10 < 1
16 6 7 13 redivcli ⊢ B 10 ∈ ℝ
17 1re ⊢ 1 ∈ ℝ
18 1 nn0rei ⊢ A ∈ ℝ
19 16 17 18 ltadd2i ⊢ B 10 < 1 ↔ A + B 10 < A + 1
20 15 19 mpbi ⊢ A + B 10 < A + 1
21 df-dp2 Could not format _ A B = ( A + ( B / ; 1 0 ) ) : No typesetting found for |- _ A B = ( A + ( B / ; 1 0 ) ) with typecode |-
22 4 eqcomi ⊢ C = A + 1
23 20 21 22 3brtr4i Could not format _ A B < C : No typesetting found for |- _ A B < C with typecode |-