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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	fourierdlem6.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	fourierdlem6.altb	⊢ ( 𝜑 → 𝐴 < 𝐵 )
	fourierdlem6.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
	fourierdlem6.5	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	fourierdlem6.i	⊢ ( 𝜑 → 𝐼 ∈ ℤ )
	fourierdlem6.j	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
	fourierdlem6.iltj	⊢ ( 𝜑 → 𝐼 < 𝐽 )
	fourierdlem6.iel	⊢ ( 𝜑 → ( 𝑋 + ( 𝐼 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
	fourierdlem6.jel	⊢ ( 𝜑 → ( 𝑋 + ( 𝐽 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
Assertion	fourierdlem6	⊢ ( 𝜑 → 𝐽 = ( 𝐼 + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem6.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		fourierdlem6.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		fourierdlem6.altb	⊢ ( 𝜑 → 𝐴 < 𝐵 )
4		fourierdlem6.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
5		fourierdlem6.5	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
6		fourierdlem6.i	⊢ ( 𝜑 → 𝐼 ∈ ℤ )
7		fourierdlem6.j	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
8		fourierdlem6.iltj	⊢ ( 𝜑 → 𝐼 < 𝐽 )
9		fourierdlem6.iel	⊢ ( 𝜑 → ( 𝑋 + ( 𝐼 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
10		fourierdlem6.jel	⊢ ( 𝜑 → ( 𝑋 + ( 𝐽 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
11	7	zred	⊢ ( 𝜑 → 𝐽 ∈ ℝ )
12	6	zred	⊢ ( 𝜑 → 𝐼 ∈ ℝ )
13	11 12	resubcld	⊢ ( 𝜑 → ( 𝐽 − 𝐼 ) ∈ ℝ )
14	2 1	resubcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
15	4 14	eqeltrid	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
16	13 15	remulcld	⊢ ( 𝜑 → ( ( 𝐽 − 𝐼 ) · 𝑇 ) ∈ ℝ )
17	1 2	posdifd	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
18	3 17	mpbid	⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
19	18 4	breqtrrdi	⊢ ( 𝜑 → 0 < 𝑇 )
20	15 19	elrpd	⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
21	1 2 10 9	iccsuble	⊢ ( 𝜑 → ( ( 𝑋 + ( 𝐽 · 𝑇 ) ) − ( 𝑋 + ( 𝐼 · 𝑇 ) ) ) ≤ ( 𝐵 − 𝐴 ) )
22	11	recnd	⊢ ( 𝜑 → 𝐽 ∈ ℂ )
23	12	recnd	⊢ ( 𝜑 → 𝐼 ∈ ℂ )
24	15	recnd	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
25	22 23 24	subdird	⊢ ( 𝜑 → ( ( 𝐽 − 𝐼 ) · 𝑇 ) = ( ( 𝐽 · 𝑇 ) − ( 𝐼 · 𝑇 ) ) )
26	5	recnd	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
27	11 15	remulcld	⊢ ( 𝜑 → ( 𝐽 · 𝑇 ) ∈ ℝ )
28	27	recnd	⊢ ( 𝜑 → ( 𝐽 · 𝑇 ) ∈ ℂ )
29	12 15	remulcld	⊢ ( 𝜑 → ( 𝐼 · 𝑇 ) ∈ ℝ )
30	29	recnd	⊢ ( 𝜑 → ( 𝐼 · 𝑇 ) ∈ ℂ )
31	26 28 30	pnpcand	⊢ ( 𝜑 → ( ( 𝑋 + ( 𝐽 · 𝑇 ) ) − ( 𝑋 + ( 𝐼 · 𝑇 ) ) ) = ( ( 𝐽 · 𝑇 ) − ( 𝐼 · 𝑇 ) ) )
32	25 31	eqtr4d	⊢ ( 𝜑 → ( ( 𝐽 − 𝐼 ) · 𝑇 ) = ( ( 𝑋 + ( 𝐽 · 𝑇 ) ) − ( 𝑋 + ( 𝐼 · 𝑇 ) ) ) )
33	4	a1i	⊢ ( 𝜑 → 𝑇 = ( 𝐵 − 𝐴 ) )
34	21 32 33	3brtr4d	⊢ ( 𝜑 → ( ( 𝐽 − 𝐼 ) · 𝑇 ) ≤ 𝑇 )
35	16 15 20 34	lediv1dd	⊢ ( 𝜑 → ( ( ( 𝐽 − 𝐼 ) · 𝑇 ) / 𝑇 ) ≤ ( 𝑇 / 𝑇 ) )
36	13	recnd	⊢ ( 𝜑 → ( 𝐽 − 𝐼 ) ∈ ℂ )
37	19	gt0ne0d	⊢ ( 𝜑 → 𝑇 ≠ 0 )
38	36 24 37	divcan4d	⊢ ( 𝜑 → ( ( ( 𝐽 − 𝐼 ) · 𝑇 ) / 𝑇 ) = ( 𝐽 − 𝐼 ) )
39	24 37	dividd	⊢ ( 𝜑 → ( 𝑇 / 𝑇 ) = 1 )
40	35 38 39	3brtr3d	⊢ ( 𝜑 → ( 𝐽 − 𝐼 ) ≤ 1 )
41		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
42	11 12 41	lesubadd2d	⊢ ( 𝜑 → ( ( 𝐽 − 𝐼 ) ≤ 1 ↔ 𝐽 ≤ ( 𝐼 + 1 ) ) )
43	40 42	mpbid	⊢ ( 𝜑 → 𝐽 ≤ ( 𝐼 + 1 ) )
44		zltp1le	⊢ ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝐼 < 𝐽 ↔ ( 𝐼 + 1 ) ≤ 𝐽 ) )
45	6 7 44	syl2anc	⊢ ( 𝜑 → ( 𝐼 < 𝐽 ↔ ( 𝐼 + 1 ) ≤ 𝐽 ) )
46	8 45	mpbid	⊢ ( 𝜑 → ( 𝐼 + 1 ) ≤ 𝐽 )
47	12 41	readdcld	⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ℝ )
48	11 47	letri3d	⊢ ( 𝜑 → ( 𝐽 = ( 𝐼 + 1 ) ↔ ( 𝐽 ≤ ( 𝐼 + 1 ) ∧ ( 𝐼 + 1 ) ≤ 𝐽 ) ) )
49	43 46 48	mpbir2and	⊢ ( 𝜑 → 𝐽 = ( 𝐼 + 1 ) )