Theorem fourierdlem6

Description: X is in the periodic partition, when the considered interval is centered at X . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem6.a	$$⊢\phi \to A\in ℝ$$
	fourierdlem6.b	$$⊢\phi \to B\in ℝ$$
	fourierdlem6.altb	$$⊢\phi \to A<B$$
	fourierdlem6.t	$$⊢T=B-A$$
	fourierdlem6.5	$$⊢\phi \to X\in ℝ$$
	fourierdlem6.i	$$⊢\phi \to I\in \mathbb{Z}$$
	fourierdlem6.j	$$⊢\phi \to J\in \mathbb{Z}$$
	fourierdlem6.iltj	$$⊢\phi \to I<J$$
	fourierdlem6.iel	$$⊢\phi \to X+IT\in \left[A,B\right]$$
	fourierdlem6.jel	$$⊢\phi \to X+JT\in \left[A,B\right]$$
Assertion	fourierdlem6	$$⊢\phi \to J=I+1$$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem6.a	$$⊢\phi \to A\in ℝ$$
2		fourierdlem6.b	$$⊢\phi \to B\in ℝ$$
3		fourierdlem6.altb	$$⊢\phi \to A<B$$
4		fourierdlem6.t	$$⊢T=B-A$$
5		fourierdlem6.5	$$⊢\phi \to X\in ℝ$$
6		fourierdlem6.i	$$⊢\phi \to I\in \mathbb{Z}$$
7		fourierdlem6.j	$$⊢\phi \to J\in \mathbb{Z}$$
8		fourierdlem6.iltj	$$⊢\phi \to I<J$$
9		fourierdlem6.iel	$$⊢\phi \to X+IT\in \left[A,B\right]$$
10		fourierdlem6.jel	$$⊢\phi \to X+JT\in \left[A,B\right]$$
11	7	zred	$$⊢\phi \to J\in ℝ$$
12	6	zred	$$⊢\phi \to I\in ℝ$$
13	11 12	resubcld	$$⊢\phi \to J-I\in ℝ$$
14	2 1	resubcld	$$⊢\phi \to B-A\in ℝ$$
15	4 14	eqeltrid	$$⊢\phi \to T\in ℝ$$
16	13 15	remulcld	$$⊢\phi \to \left(J-I\right)T\in ℝ$$
17	1 2	posdifd	$$⊢\phi \to \left(A<B\leftrightarrow 0<B-A\right)$$
18	3 17	mpbid	$$⊢\phi \to 0<B-A$$
19	18 4	breqtrrdi	$$⊢\phi \to 0<T$$
20	15 19	elrpd	$$⊢\phi \to T\in {ℝ}^{+}$$
21	1 2 10 9	iccsuble	$$⊢\phi \to X+JT-\left(X+IT\right)\le B-A$$
22	11	recnd	$$⊢\phi \to J\in ℂ$$
23	12	recnd	$$⊢\phi \to I\in ℂ$$
24	15	recnd	$$⊢\phi \to T\in ℂ$$
25	22 23 24	subdird	$$⊢\phi \to \left(J-I\right)T=JT-IT$$
26	5	recnd	$$⊢\phi \to X\in ℂ$$
27	11 15	remulcld	$$⊢\phi \to JT\in ℝ$$
28	27	recnd	$$⊢\phi \to JT\in ℂ$$
29	12 15	remulcld	$$⊢\phi \to IT\in ℝ$$
30	29	recnd	$$⊢\phi \to IT\in ℂ$$
31	26 28 30	pnpcand	$$⊢\phi \to X+JT-\left(X+IT\right)=JT-IT$$
32	25 31	eqtr4d	$$⊢\phi \to \left(J-I\right)T=X+JT-\left(X+IT\right)$$
33	4	a1i	$$⊢\phi \to T=B-A$$
34	21 32 33	3brtr4d	$$⊢\phi \to \left(J-I\right)T\le T$$
35	16 15 20 34	lediv1dd	$$⊢\phi \to \frac{\left(J-I\right)T}{T}\le \frac{T}{T}$$
36	13	recnd	$$⊢\phi \to J-I\in ℂ$$
37	19	gt0ne0d	$$⊢\phi \to T\ne 0$$
38	36 24 37	divcan4d	$$⊢\phi \to \frac{\left(J-I\right)T}{T}=J-I$$
39	24 37	dividd	$$⊢\phi \to \frac{T}{T}=1$$
40	35 38 39	3brtr3d	$$⊢\phi \to J-I\le 1$$
41		1red	$$⊢\phi \to 1\in ℝ$$
42	11 12 41	lesubadd2d	$$⊢\phi \to \left(J-I\le 1\leftrightarrow J\le I+1\right)$$
43	40 42	mpbid	$$⊢\phi \to J\le I+1$$
44		zltp1le	$$⊢\left(I\in \mathbb{Z}\wedge J\in \mathbb{Z}\right)\to \left(I<J\leftrightarrow I+1\le J\right)$$
45	6 7 44	syl2anc	$$⊢\phi \to \left(I<J\leftrightarrow I+1\le J\right)$$
46	8 45	mpbid	$$⊢\phi \to I+1\le J$$
47	12 41	readdcld	$$⊢\phi \to I+1\in ℝ$$
48	11 47	letri3d	$$⊢\phi \to \left(J=I+1\leftrightarrow \left(J\le I+1\wedge I+1\le J\right)\right)$$
49	43 46 48	mpbir2and	$$⊢\phi \to J=I+1$$