Theorem dnibndlem10

Description: Lemma for dnibnd . (Contributed by Asger C. Ipsen, 4-Apr-2021)

	Ref	Expression
Hypotheses	dnibndlem10.1	$$⊢\phi \to A\in ℝ$$
	dnibndlem10.2	$$⊢\phi \to B\in ℝ$$
	dnibndlem10.3	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋+2\le ⌊B+\left(\frac{1}{2}\right)⌋$$
Assertion	dnibndlem10	$$⊢\phi \to 1\le B-A$$

Proof

Step	Hyp	Ref	Expression
1		dnibndlem10.1	$$⊢\phi \to A\in ℝ$$
2		dnibndlem10.2	$$⊢\phi \to B\in ℝ$$
3		dnibndlem10.3	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋+2\le ⌊B+\left(\frac{1}{2}\right)⌋$$
4		1red	$$⊢\phi \to 1\in ℝ$$
5		halfre	$$⊢\frac{1}{2}\in ℝ$$
6	5	a1i	$$⊢\phi \to \frac{1}{2}\in ℝ$$
7	2 6	readdcld	$$⊢\phi \to B+\left(\frac{1}{2}\right)\in ℝ$$
8		reflcl	$$⊢B+\left(\frac{1}{2}\right)\in ℝ\to ⌊B+\left(\frac{1}{2}\right)⌋\in ℝ$$
9	7 8	syl	$$⊢\phi \to ⌊B+\left(\frac{1}{2}\right)⌋\in ℝ$$
10	9 6	jca	$$⊢\phi \to \left(⌊B+\left(\frac{1}{2}\right)⌋\in ℝ\wedge \frac{1}{2}\in ℝ\right)$$
11		resubcl	$$⊢\left(⌊B+\left(\frac{1}{2}\right)⌋\in ℝ\wedge \frac{1}{2}\in ℝ\right)\to ⌊B+\left(\frac{1}{2}\right)⌋-\left(\frac{1}{2}\right)\in ℝ$$
12	10 11	syl	$$⊢\phi \to ⌊B+\left(\frac{1}{2}\right)⌋-\left(\frac{1}{2}\right)\in ℝ$$
13	1 6	readdcld	$$⊢\phi \to A+\left(\frac{1}{2}\right)\in ℝ$$
14		reflcl	$$⊢A+\left(\frac{1}{2}\right)\in ℝ\to ⌊A+\left(\frac{1}{2}\right)⌋\in ℝ$$
15	13 14	syl	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋\in ℝ$$
16	15 6	readdcld	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\in ℝ$$
17	12 16	jca	$$⊢\phi \to \left(⌊B+\left(\frac{1}{2}\right)⌋-\left(\frac{1}{2}\right)\in ℝ\wedge ⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\in ℝ\right)$$
18		resubcl	$$⊢\left(⌊B+\left(\frac{1}{2}\right)⌋-\left(\frac{1}{2}\right)\in ℝ\wedge ⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\in ℝ\right)\to ⌊B+\left(\frac{1}{2}\right)⌋-\left(\frac{1}{2}\right)-\left(⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\right)\in ℝ$$
19	17 18	syl	$$⊢\phi \to ⌊B+\left(\frac{1}{2}\right)⌋-\left(\frac{1}{2}\right)-\left(⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\right)\in ℝ$$
20	2 1	resubcld	$$⊢\phi \to B-A\in ℝ$$
21	15	recnd	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋\in ℂ$$
22		2cnd	$$⊢\phi \to 2\in ℂ$$
23	6	recnd	$$⊢\phi \to \frac{1}{2}\in ℂ$$
24	21 22 23	addsubassd	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋+2-\left(\frac{1}{2}\right)=⌊A+\left(\frac{1}{2}\right)⌋+2-\left(\frac{1}{2}\right)$$
25	24	oveq1d	$$⊢\phi \to \left(⌊A+\left(\frac{1}{2}\right)⌋+2\right)-\left(\frac{1}{2}\right)-\left(⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\right)=⌊A+\left(\frac{1}{2}\right)⌋+\left(2-\left(\frac{1}{2}\right)\right)-\left(⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\right)$$
26	22 23	subcld	$$⊢\phi \to 2-\left(\frac{1}{2}\right)\in ℂ$$
27	21 26 23	pnpcand	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋+\left(2-\left(\frac{1}{2}\right)\right)-\left(⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\right)=2-\left(\frac{1}{2}\right)-\left(\frac{1}{2}\right)$$
28	22 23 23	subsub4d	$$⊢\phi \to 2-\left(\frac{1}{2}\right)-\left(\frac{1}{2}\right)=2-\left(\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)\right)$$
29		ax-1cn	$$⊢1\in ℂ$$
30		2halves	$$⊢1\in ℂ\to \left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=1$$
31	29 30	ax-mp	$$⊢\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=1$$
32	31	a1i	$$⊢\phi \to \left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=1$$
33	32	oveq2d	$$⊢\phi \to 2-\left(\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)\right)=2-1$$
34		2m1e1	$$⊢2-1=1$$
35	34	a1i	$$⊢\phi \to 2-1=1$$
36	28 33 35	3eqtrd	$$⊢\phi \to 2-\left(\frac{1}{2}\right)-\left(\frac{1}{2}\right)=1$$
37	25 27 36	3eqtrd	$$⊢\phi \to \left(⌊A+\left(\frac{1}{2}\right)⌋+2\right)-\left(\frac{1}{2}\right)-\left(⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\right)=1$$
38	37	eqcomd	$$⊢\phi \to 1=\left(⌊A+\left(\frac{1}{2}\right)⌋+2\right)-\left(\frac{1}{2}\right)-\left(⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\right)$$
39		2re	$$⊢2\in ℝ$$
40	39	a1i	$$⊢\phi \to 2\in ℝ$$
41	15 40	readdcld	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋+2\in ℝ$$
42	41 6	jca	$$⊢\phi \to \left(⌊A+\left(\frac{1}{2}\right)⌋+2\in ℝ\wedge \frac{1}{2}\in ℝ\right)$$
43		resubcl	$$⊢\left(⌊A+\left(\frac{1}{2}\right)⌋+2\in ℝ\wedge \frac{1}{2}\in ℝ\right)\to ⌊A+\left(\frac{1}{2}\right)⌋+2-\left(\frac{1}{2}\right)\in ℝ$$
44	42 43	syl	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋+2-\left(\frac{1}{2}\right)\in ℝ$$
45	41 9 6 3	lesub1dd	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋+2-\left(\frac{1}{2}\right)\le ⌊B+\left(\frac{1}{2}\right)⌋-\left(\frac{1}{2}\right)$$
46	44 12 16 45	lesub1dd	$$⊢\phi \to \left(⌊A+\left(\frac{1}{2}\right)⌋+2\right)-\left(\frac{1}{2}\right)-\left(⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\right)\le ⌊B+\left(\frac{1}{2}\right)⌋-\left(\frac{1}{2}\right)-\left(⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\right)$$
47	38 46	eqbrtrd	$$⊢\phi \to 1\le ⌊B+\left(\frac{1}{2}\right)⌋-\left(\frac{1}{2}\right)-\left(⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\right)$$
48		flle	$$⊢B+\left(\frac{1}{2}\right)\in ℝ\to ⌊B+\left(\frac{1}{2}\right)⌋\le B+\left(\frac{1}{2}\right)$$
49	7 48	syl	$$⊢\phi \to ⌊B+\left(\frac{1}{2}\right)⌋\le B+\left(\frac{1}{2}\right)$$
50	9 6 2	lesubaddd	$$⊢\phi \to \left(⌊B+\left(\frac{1}{2}\right)⌋-\left(\frac{1}{2}\right)\le B\leftrightarrow ⌊B+\left(\frac{1}{2}\right)⌋\le B+\left(\frac{1}{2}\right)\right)$$
51	49 50	mpbird	$$⊢\phi \to ⌊B+\left(\frac{1}{2}\right)⌋-\left(\frac{1}{2}\right)\le B$$
52		fllep1	$$⊢A+\left(\frac{1}{2}\right)\in ℝ\to A+\left(\frac{1}{2}\right)\le ⌊A+\left(\frac{1}{2}\right)⌋+1$$
53	13 52	syl	$$⊢\phi \to A+\left(\frac{1}{2}\right)\le ⌊A+\left(\frac{1}{2}\right)⌋+1$$
54	21 23 23	addassd	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)$$
55	32	oveq2d	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=⌊A+\left(\frac{1}{2}\right)⌋+1$$
56	54 55	eqtrd	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=⌊A+\left(\frac{1}{2}\right)⌋+1$$
57	56	eqcomd	$$⊢\phi \to ⌊A+\left(\frac{1}{2}\right)⌋+1=⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)$$
58	53 57	breqtrd	$$⊢\phi \to A+\left(\frac{1}{2}\right)\le ⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)$$
59	1 16 6	leadd1d	$$⊢\phi \to \left(A\le ⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\leftrightarrow A+\left(\frac{1}{2}\right)\le ⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)\right)$$
60	58 59	mpbird	$$⊢\phi \to A\le ⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)$$
61	12 1 2 16 51 60	le2subd	$$⊢\phi \to ⌊B+\left(\frac{1}{2}\right)⌋-\left(\frac{1}{2}\right)-\left(⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\right)\le B-A$$
62	4 19 20 47 61	letrd	$$⊢\phi \to 1\le B-A$$