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	⊢ _ 𝐴 𝐵 < 𝐶