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

Metamath Proof Explorer

Theorem dplti

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

Ref Expression
Hypotheses dplti.a ⊢ 𝐴 ∈ ℕ0
dplti.b ⊢ 𝐵 ∈ ℝ+
dplti.c ⊢ 𝐶 ∈ ℕ0
dplti.1 ⊢ 𝐵 < 1 0
dplti.2 ⊢ ( 𝐴 + 1 ) = 𝐶
Assertion dplti ( 𝐴 . 𝐵 ) < 𝐶

Proof

Step Hyp Ref Expression
1 dplti.a ⊢ 𝐴 ∈ ℕ0
2 dplti.b ⊢ 𝐵 ∈ ℝ+
3 dplti.c ⊢ 𝐶 ∈ ℕ0
4 dplti.1 ⊢ 𝐵 < 1 0
5 dplti.2 ⊢ ( 𝐴 + 1 ) = 𝐶
6 rpre ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ )
7 2 6 ax-mp ⊢ 𝐵 ∈ ℝ
8 1 7 dpval2 ⊢ ( 𝐴 . 𝐵 ) = ( 𝐴 + ( 𝐵 / 1 0 ) )
9 10re ⊢ 1 0 ∈ ℝ
10 10pos ⊢ 0 < 1 0
11 9 10 pm3.2i ⊢ ( 1 0 ∈ ℝ ∧ 0 < 1 0 )
12 elrp ⊢ ( 1 0 ∈ ℝ+ ↔ ( 1 0 ∈ ℝ ∧ 0 < 1 0 ) )
13 11 12 mpbir ⊢ 1 0 ∈ ℝ+
14 divlt1lt ⊢ ( ( 𝐵 ∈ ℝ ∧ 1 0 ∈ ℝ+ ) → ( ( 𝐵 / 1 0 ) < 1 ↔ 𝐵 < 1 0 ) )
15 7 13 14 mp2an ⊢ ( ( 𝐵 / 1 0 ) < 1 ↔ 𝐵 < 1 0 )
16 4 15 mpbir ⊢ ( 𝐵 / 1 0 ) < 1
17 0re ⊢ 0 ∈ ℝ
18 17 10 gtneii ⊢ 1 0 ≠ 0
19 7 9 18 redivcli ⊢ ( 𝐵 / 1 0 ) ∈ ℝ
20 1re ⊢ 1 ∈ ℝ
21 nn0ssre ⊢ ℕ0 ⊆ ℝ
22 21 1 sselii ⊢ 𝐴 ∈ ℝ
23 19 20 22 ltadd2i ⊢ ( ( 𝐵 / 1 0 ) < 1 ↔ ( 𝐴 + ( 𝐵 / 1 0 ) ) < ( 𝐴 + 1 ) )
24 16 23 mpbi ⊢ ( 𝐴 + ( 𝐵 / 1 0 ) ) < ( 𝐴 + 1 )
25 8 24 eqbrtri ⊢ ( 𝐴 . 𝐵 ) < ( 𝐴 + 1 )
26 25 5 breqtri ⊢ ( 𝐴 . 𝐵 ) < 𝐶