Theorem dp2ltsuc

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

	Ref	Expression
Hypotheses	dp2lt.a	$$⊢A\in {\mathbb{N}}_0$$
	dp2lt.b	$$⊢B\in {ℝ}^{+}$$
	dp2ltsuc.1	$$⊢B<10$$
	dp2ltsuc.2	$$⊢A+1=C$$
Assertion	dp2ltsuc	Could not format assertion : No typesetting found for |- _ A B < C with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dp2lt.a	$$⊢A\in {\mathbb{N}}_0$$
2		dp2lt.b	$$⊢B\in {ℝ}^{+}$$
3		dp2ltsuc.1	$$⊢B<10$$
4		dp2ltsuc.2	$$⊢A+1=C$$
5		rpre	$$⊢B\in {ℝ}^{+}\to B\in ℝ$$
6	2 5	ax-mp	$$⊢B\in ℝ$$
7		10re	$$⊢10\in ℝ$$
8		10pos	$$⊢0<10$$
9	6 7 7 8	ltdiv1ii	$$⊢B<10\leftrightarrow \frac{B}{10}<\frac{10}{10}$$
10	3 9	mpbi	$$⊢\frac{B}{10}<\frac{10}{10}$$
11	7	recni	$$⊢10\in ℂ$$
12		10nn	$$⊢10\in \mathbb{N}$$
13	12	nnne0i	$$⊢10\ne 0$$
14	11 13	dividi	$$⊢\frac{10}{10}=1$$
15	10 14	breqtri	$$⊢\frac{B}{10}<1$$
16	6 7 13	redivcli	$$⊢\frac{B}{10}\in ℝ$$
17		1re	$$⊢1\in ℝ$$
18	1	nn0rei	$$⊢A\in ℝ$$
19	16 17 18	ltadd2i	$$⊢\frac{B}{10}<1\leftrightarrow A+\left(\frac{B}{10}\right)<A+1$$
20	15 19	mpbi	$$⊢A+\left(\frac{B}{10}\right)<A+1$$
21		df-dp2	Could not format _ A B = ( A + ( B / ; 1 0 ) ) : No typesetting found for |- _ A B = ( A + ( B / ; 1 0 ) ) with typecode |-
22	4	eqcomi	$$⊢C=A+1$$
23	20 21 22	3brtr4i	Could not format _ A B < C : No typesetting found for |- _ A B < C with typecode |-