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 ⊢ 𝐴 ∈ ℕ0
dp2lt.b ⊢ 𝐵 ∈ ℝ+
dp2ltsuc.1 ⊢ 𝐵 < 1 0
dp2ltsuc.2 ⊢ ( 𝐴 + 1 ) = 𝐶
Assertion dp2ltsuc 𝐴 𝐵 < 𝐶

Proof

Step Hyp Ref Expression
1 dp2lt.a ⊢ 𝐴 ∈ ℕ0
2 dp2lt.b ⊢ 𝐵 ∈ ℝ+
3 dp2ltsuc.1 ⊢ 𝐵 < 1 0
4 dp2ltsuc.2 ⊢ ( 𝐴 + 1 ) = 𝐶
5 rpre ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ )
6 2 5 ax-mp ⊢ 𝐵 ∈ ℝ
7 10re ⊢ 1 0 ∈ ℝ
8 10pos ⊢ 0 < 1 0
9 6 7 7 8 ltdiv1ii ⊢ ( 𝐵 < 1 0 ↔ ( 𝐵 / 1 0 ) < ( 1 0 / 1 0 ) )
10 3 9 mpbi ⊢ ( 𝐵 / 1 0 ) < ( 1 0 / 1 0 )
11 7 recni ⊢ 1 0 ∈ ℂ
12 10nn ⊢ 1 0 ∈ ℕ
13 12 nnne0i ⊢ 1 0 ≠ 0
14 11 13 dividi ⊢ ( 1 0 / 1 0 ) = 1
15 10 14 breqtri ⊢ ( 𝐵 / 1 0 ) < 1
16 6 7 13 redivcli ⊢ ( 𝐵 / 1 0 ) ∈ ℝ
17 1re ⊢ 1 ∈ ℝ
18 1 nn0rei ⊢ 𝐴 ∈ ℝ
19 16 17 18 ltadd2i ⊢ ( ( 𝐵 / 1 0 ) < 1 ↔ ( 𝐴 + ( 𝐵 / 1 0 ) ) < ( 𝐴 + 1 ) )
20 15 19 mpbi ⊢ ( 𝐴 + ( 𝐵 / 1 0 ) ) < ( 𝐴 + 1 )
21 df-dp2 ⊢ 𝐴 𝐵 = ( 𝐴 + ( 𝐵 / 1 0 ) )
22 4 eqcomi ⊢ 𝐶 = ( 𝐴 + 1 )
23 20 21 22 3brtr4i ⊢ 𝐴 𝐵 < 𝐶