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	⊢ ( 𝐴 . 𝐵 ) < 𝐶