Theorem dpgti

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

	Ref	Expression
Hypotheses	dpgti.a	⊢ 𝐴 ∈ ℕ0
	dpgti.b	⊢ 𝐵 ∈ ℝ+
Assertion	dpgti	⊢ 𝐴 < ( 𝐴 . 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dpgti.a	⊢ 𝐴 ∈ ℕ0
2		dpgti.b	⊢ 𝐵 ∈ ℝ+
3	1	nn0rei	⊢ 𝐴 ∈ ℝ
4		10re	⊢ ; 1 0 ∈ ℝ
5		10pos	⊢ 0 < ; 1 0
6	4 5	pm3.2i	⊢ ( ; 1 0 ∈ ℝ ∧ 0 < ; 1 0 )
7		elrp	⊢ ( ; 1 0 ∈ ℝ+ ↔ ( ; 1 0 ∈ ℝ ∧ 0 < ; 1 0 ) )
8	6 7	mpbir	⊢ ; 1 0 ∈ ℝ+
9		rpdivcl	⊢ ( ( 𝐵 ∈ ℝ+ ∧ ; 1 0 ∈ ℝ+ ) → ( 𝐵 / ; 1 0 ) ∈ ℝ+ )
10	2 8 9	mp2an	⊢ ( 𝐵 / ; 1 0 ) ∈ ℝ+
11		ltaddrp	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 / ; 1 0 ) ∈ ℝ+ ) → 𝐴 < ( 𝐴 + ( 𝐵 / ; 1 0 ) ) )
12	3 10 11	mp2an	⊢ 𝐴 < ( 𝐴 + ( 𝐵 / ; 1 0 ) )
13		rpre	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ )
14	2 13	ax-mp	⊢ 𝐵 ∈ ℝ
15	1 14	dpval2	⊢ ( 𝐴 . 𝐵 ) = ( 𝐴 + ( 𝐵 / ; 1 0 ) )
16	12 15	breqtrri	⊢ 𝐴 < ( 𝐴 . 𝐵 )