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 ⊢ A ∈ ℕ 0
dplti.b ⊢ B ∈ ℝ +
dplti.c ⊢ C ∈ ℕ 0
dplti.1 ⊢ B < 10
dplti.2 ⊢ A + 1 = C
Assertion dplti ⊢ A . B < C

Proof

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