Theorem fourierdlem90

Description: Given a piecewise continuous function, it is still continuous with respect to an open interval of the moved partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem90.p	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
	fourierdlem90.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
	fourierdlem90.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	fourierdlem90.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
	fourierdlem90.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
	fourierdlem90.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
	fourierdlem90.fcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
	fourierdlem90.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	fourierdlem90.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,) +∞ ) )
	fourierdlem90.o	⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
	fourierdlem90.h	⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
	fourierdlem90.n	⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
	fourierdlem90.s	⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
	fourierdlem90.e	⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
	fourierdlem90.J	⊢ 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
	fourierdlem90.17	⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ 𝑁 ) )
	fourierdlem90.u	⊢ 𝑈 = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
	fourierdlem90.g	⊢ 𝐺 = ( 𝐹 ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
	fourierdlem90.r	⊢ 𝑅 = ( 𝑦 ∈ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) ↦ ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) )
	fourierdlem90.i	⊢ 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) )
Assertion	fourierdlem90	⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem90.p	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
2		fourierdlem90.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
3		fourierdlem90.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4		fourierdlem90.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
5		fourierdlem90.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
6		fourierdlem90.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
7		fourierdlem90.fcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
8		fourierdlem90.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
9		fourierdlem90.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,) +∞ ) )
10		fourierdlem90.o	⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
11		fourierdlem90.h	⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
12		fourierdlem90.n	⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
13		fourierdlem90.s	⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
14		fourierdlem90.e	⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
15		fourierdlem90.J	⊢ 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
16		fourierdlem90.17	⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ 𝑁 ) )
17		fourierdlem90.u	⊢ 𝑈 = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
18		fourierdlem90.g	⊢ 𝐺 = ( 𝐹 ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
19		fourierdlem90.r	⊢ 𝑅 = ( 𝑦 ∈ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) ↦ ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) )
20		fourierdlem90.i	⊢ 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) )
21	1 3 4	fourierdlem11	⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) )
22	21	simp1d	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
23	21	simp2d	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
24	22 23	iccssred	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
25	21	simp3d	⊢ ( 𝜑 → 𝐴 < 𝐵 )
26	22 23 25 15	fourierdlem17	⊢ ( 𝜑 → 𝐿 : ( 𝐴 (,] 𝐵 ) ⟶ ( 𝐴 [,] 𝐵 ) )
27	22 23 25 2 14	fourierdlem4	⊢ ( 𝜑 → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
28		elioore	⊢ ( 𝐷 ∈ ( 𝐶 (,) +∞ ) → 𝐷 ∈ ℝ )
29	9 28	syl	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
30		elioo4g	⊢ ( 𝐷 ∈ ( 𝐶 (,) +∞ ) ↔ ( ( 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ℝ ) ∧ ( 𝐶 < 𝐷 ∧ 𝐷 < +∞ ) ) )
31	9 30	sylib	⊢ ( 𝜑 → ( ( 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ℝ ) ∧ ( 𝐶 < 𝐷 ∧ 𝐷 < +∞ ) ) )
32	31	simprd	⊢ ( 𝜑 → ( 𝐶 < 𝐷 ∧ 𝐷 < +∞ ) )
33	32	simpld	⊢ ( 𝜑 → 𝐶 < 𝐷 )
34	2 1 3 4 8 29 33 10 11 12 13	fourierdlem54	⊢ ( 𝜑 → ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) ∧ 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) )
35	34	simpld	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) )
36	35	simprd	⊢ ( 𝜑 → 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) )
37	35	simpld	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
38	10	fourierdlem2	⊢ ( 𝑁 ∈ ℕ → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
39	37 38	syl	⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
40	36 39	mpbid	⊢ ( 𝜑 → ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
41	40	simpld	⊢ ( 𝜑 → 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) )
42		elmapi	⊢ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
43	41 42	syl	⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
44		elfzofz	⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ( 0 ... 𝑁 ) )
45	16 44	syl	⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑁 ) )
46	43 45	ffvelcdmd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ℝ )
47	27 46	ffvelcdmd	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
48	26 47	ffvelcdmd	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( 𝐴 [,] 𝐵 ) )
49	24 48	sseldd	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ )
50	22	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
51		iocssre	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
52	50 23 51	syl2anc	⊢ ( 𝜑 → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
53		fzofzp1	⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
54	16 53	syl	⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
55	43 54	ffvelcdmd	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
56	27 55	ffvelcdmd	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ( 𝐴 (,] 𝐵 ) )
57	52 56	sseldd	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℝ )
58		eqid	⊢ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
59	55 57	resubcld	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∈ ℝ )
60	17 59	eqeltrid	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
61		eqid	⊢ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) = ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) )
62		eleq1	⊢ ( 𝑗 = 𝐽 → ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↔ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) )
63	62	anbi2d	⊢ ( 𝑗 = 𝐽 → ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ↔ ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ) )
64		fveq2	⊢ ( 𝑗 = 𝐽 → ( 𝑆 ‘ 𝑗 ) = ( 𝑆 ‘ 𝐽 ) )
65	64	fveq2d	⊢ ( 𝑗 = 𝐽 → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) )
66	65	fveq2d	⊢ ( 𝑗 = 𝐽 → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
67		oveq1	⊢ ( 𝑗 = 𝐽 → ( 𝑗 + 1 ) = ( 𝐽 + 1 ) )
68	67	fveq2d	⊢ ( 𝑗 = 𝐽 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
69	68	fveq2d	⊢ ( 𝑗 = 𝐽 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
70	66 69	oveq12d	⊢ ( 𝑗 = 𝐽 → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
71	64	fveq2d	⊢ ( 𝑗 = 𝐽 → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) )
72	71	fveq2d	⊢ ( 𝑗 = 𝐽 → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
73	71	oveq1d	⊢ ( 𝑗 = 𝐽 → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) = ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) )
74	73	fveq2d	⊢ ( 𝑗 = 𝐽 → ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
75	72 74	oveq12d	⊢ ( 𝑗 = 𝐽 → ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) = ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
76	70 75	sseq12d	⊢ ( 𝑗 = 𝐽 → ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) ↔ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) )
77	63 76	imbi12d	⊢ ( 𝑗 = 𝐽 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) ) ↔ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ) )
78	2	oveq2i	⊢ ( 𝑘 · 𝑇 ) = ( 𝑘 · ( 𝐵 − 𝐴 ) )
79	78	oveq2i	⊢ ( 𝑦 + ( 𝑘 · 𝑇 ) ) = ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) )
80	79	eleq1i	⊢ ( ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
81	80	rexbii	⊢ ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
82	81	a1i	⊢ ( 𝑦 ∈ ( 𝐶 [,] 𝐷 ) → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) )
83	82	rabbiia	⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 }
84	83	uneq2i	⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } )
85	11 84	eqtri	⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } )
86		id	⊢ ( 𝑦 = 𝑥 → 𝑦 = 𝑥 )
87	2	eqcomi	⊢ ( 𝐵 − 𝐴 ) = 𝑇
88	87	oveq2i	⊢ ( 𝑘 · ( 𝐵 − 𝐴 ) ) = ( 𝑘 · 𝑇 )
89	88	a1i	⊢ ( 𝑦 = 𝑥 → ( 𝑘 · ( 𝐵 − 𝐴 ) ) = ( 𝑘 · 𝑇 ) )
90	86 89	oveq12d	⊢ ( 𝑦 = 𝑥 → ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
91	90	eleq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
92	91	rexbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
93	92	cbvrabv	⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } = { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 }
94	93	uneq2i	⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
95	85 94	eqtri	⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
96		eqid	⊢ ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) = ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) )
97	2 1 3 4 8 29 33 10 95 12 13 14 15 96 20	fourierdlem79	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) )
98	77 97	vtoclg	⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) )
99	98	anabsi7	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
100	16 99	mpdan	⊢ ( 𝜑 → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
101	100	resabs1d	⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( 𝐹 ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
102	101	eqcomd	⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
103	1 3 4 2 14 15 20	fourierdlem37	⊢ ( 𝜑 → ( 𝐼 : ℝ ⟶ ( 0 ..^ 𝑀 ) ∧ ( 𝑥 ∈ ℝ → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ) ) )
104	103	simpld	⊢ ( 𝜑 → 𝐼 : ℝ ⟶ ( 0 ..^ 𝑀 ) )
105	104 46	ffvelcdmd	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) )
106	105	ancli	⊢ ( 𝜑 → ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) )
107		eleq1	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) )
108	107	anbi2d	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) )
109		fveq2	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
110		oveq1	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑖 + 1 ) = ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) )
111	110	fveq2d	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
112	109 111	oveq12d	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
113	112	reseq2d	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) )
114	112	oveq1d	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) = ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) )
115	113 114	eleq12d	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) ↔ ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) ) )
116	108 115	imbi12d	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) ) ↔ ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) ) ) )
117	116 7	vtoclg	⊢ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) → ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) ) )
118	105 106 117	sylc	⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) )
119		rescncf	⊢ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) ∈ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) –cn→ ℂ ) ) )
120	100 118 119	sylc	⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) ∈ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) –cn→ ℂ ) )
121	102 120	eqeltrd	⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) ∈ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) –cn→ ℂ ) )
122	18 121	eqeltrid	⊢ ( 𝜑 → 𝐺 ∈ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) –cn→ ℂ ) )
123	49 57 58 60 61 122 19	cncfshiftioo	⊢ ( 𝜑 → 𝑅 ∈ ( ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) –cn→ ℂ ) )
124	19	a1i	⊢ ( 𝜑 → 𝑅 = ( 𝑦 ∈ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) ↦ ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) ) )
125	17	oveq2i	⊢ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) = ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
126	125	a1i	⊢ ( 𝜑 → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) = ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
127	69 66	oveq12d	⊢ ( 𝑗 = 𝐽 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
128	68 64	oveq12d	⊢ ( 𝑗 = 𝐽 → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) )
129	127 128	eqeq12d	⊢ ( 𝑗 = 𝐽 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ↔ ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
130	63 129	imbi12d	⊢ ( 𝑗 = 𝐽 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) ↔ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) ) )
131	85	fveq2i	⊢ ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
132	131	oveq1i	⊢ ( ( ♯ ‘ 𝐻 ) − 1 ) = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) − 1 )
133	12 132	eqtri	⊢ 𝑁 = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) − 1 )
134		isoeq5	⊢ ( 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) → ( 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ↔ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) ) )
135	85 134	ax-mp	⊢ ( 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ↔ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
136	135	iotabii	⊢ ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
137	13 136	eqtri	⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
138		eqid	⊢ ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
139	1 2 3 4 8 9 10 133 137 14 15 138	fourierdlem65	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
140	130 139	vtoclg	⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
141	140	anabsi7	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) )
142	16 141	mpdan	⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) )
143	57	recnd	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℂ )
144	55	recnd	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℂ )
145	8 29	iccssred	⊢ ( 𝜑 → ( 𝐶 [,] 𝐷 ) ⊆ ℝ )
146		ax-resscn	⊢ ℝ ⊆ ℂ
147	145 146	sstrdi	⊢ ( 𝜑 → ( 𝐶 [,] 𝐷 ) ⊆ ℂ )
148	10 37 36	fourierdlem15	⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐶 [,] 𝐷 ) )
149	148 45	ffvelcdmd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ( 𝐶 [,] 𝐷 ) )
150	147 149	sseldd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ℂ )
151	144 150	subcld	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ∈ ℂ )
152	49	recnd	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℂ )
153	143 151 152	subsub23d	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ↔ ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
154	142 153	mpbird	⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
155	154	eqcomd	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
156	155	oveq1d	⊢ ( 𝜑 → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
157	143 151	subcld	⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℂ )
158	157 144 143	addsub12d	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
159	143 151 143	sub32d	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
160	143	subidd	⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = 0 )
161	160	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) = ( 0 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
162		df-neg	⊢ - ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) = ( 0 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) )
163	144 150	negsubdi2d	⊢ ( 𝜑 → - ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) = ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
164	162 163	eqtr3id	⊢ ( 𝜑 → ( 0 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) = ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
165	159 161 164	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
166	165	oveq2d	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
167	144 150	pncan3d	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( 𝑆 ‘ 𝐽 ) )
168	158 166 167	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( 𝑆 ‘ 𝐽 ) )
169	126 156 168	3eqtrd	⊢ ( 𝜑 → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) = ( 𝑆 ‘ 𝐽 ) )
170	17	oveq2i	⊢ ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
171	143 144	pncan3d	⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
172	170 171	eqtrid	⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
173	169 172	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) = ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
174	173	mpteq1d	⊢ ( 𝜑 → ( 𝑦 ∈ ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) ↦ ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) ) = ( 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) ) )
175	5	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) )
176	175	reseq1d	⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
177		ioossre	⊢ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ℝ
178	177	a1i	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ℝ )
179	178	resmptd	⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ ↦ ( 𝐹 ‘ 𝑦 ) ) ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐹 ‘ 𝑦 ) ) )
180	18	fveq1i	⊢ ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) = ( ( 𝐹 ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) ‘ ( 𝑦 − 𝑈 ) )
181	180	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) = ( ( 𝐹 ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) ‘ ( 𝑦 − 𝑈 ) ) )
182	49	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ )
183	182	rexrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ* )
184	57	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℝ )
185	184	rexrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℝ* )
186	178	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑦 ∈ ℝ )
187	60	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑈 ∈ ℝ )
188	186 187	resubcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑦 − 𝑈 ) ∈ ℝ )
189	46	rexrd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ℝ* )
190	189	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑆 ‘ 𝐽 ) ∈ ℝ* )
191	55	rexrd	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* )
192	191	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* )
193		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
194		ioogtlb	⊢ ( ( ( 𝑆 ‘ 𝐽 ) ∈ ℝ* ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑆 ‘ 𝐽 ) < 𝑦 )
195	190 192 193 194	syl3anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑆 ‘ 𝐽 ) < 𝑦 )
196	169	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) = ( 𝑆 ‘ 𝐽 ) )
197	186	recnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑦 ∈ ℂ )
198	187	recnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑈 ∈ ℂ )
199	197 198	npcand	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑦 − 𝑈 ) + 𝑈 ) = 𝑦 )
200	195 196 199	3brtr4d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) < ( ( 𝑦 − 𝑈 ) + 𝑈 ) )
201	182 188 187	ltadd1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝑦 − 𝑈 ) ↔ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) < ( ( 𝑦 − 𝑈 ) + 𝑈 ) ) )
202	200 201	mpbird	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝑦 − 𝑈 ) )
203		iooltub	⊢ ( ( ( 𝑆 ‘ 𝐽 ) ∈ ℝ* ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑦 < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
204	190 192 193 203	syl3anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑦 < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
205	172	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
206	204 199 205	3brtr4d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑦 − 𝑈 ) + 𝑈 ) < ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) )
207	188 184 187	ltadd1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑦 − 𝑈 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ↔ ( ( 𝑦 − 𝑈 ) + 𝑈 ) < ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) )
208	206 207	mpbird	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑦 − 𝑈 ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
209	183 185 188 202 208	eliood	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑦 − 𝑈 ) ∈ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
210		fvres	⊢ ( ( 𝑦 − 𝑈 ) ∈ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) ‘ ( 𝑦 − 𝑈 ) ) = ( 𝐹 ‘ ( 𝑦 − 𝑈 ) ) )
211	209 210	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) ‘ ( 𝑦 − 𝑈 ) ) = ( 𝐹 ‘ ( 𝑦 − 𝑈 ) ) )
212	17	oveq2i	⊢ ( 𝑦 − 𝑈 ) = ( 𝑦 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
213	212	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑦 − 𝑈 ) = ( 𝑦 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
214	144	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℂ )
215	143	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℂ )
216	197 214 215	subsub2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑦 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( 𝑦 + ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
217	215 214	subcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℂ )
218	23 22	resubcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
219	2 218	eqeltrid	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
220	219	recnd	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
221	220	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑇 ∈ ℂ )
222	22 23	posdifd	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
223	25 222	mpbid	⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
224	223 2	breqtrrdi	⊢ ( 𝜑 → 0 < 𝑇 )
225	224	gt0ne0d	⊢ ( 𝜑 → 𝑇 ≠ 0 )
226	225	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑇 ≠ 0 )
227	217 221 226	divcan1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) · 𝑇 ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
228	227	eqcomd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) · 𝑇 ) )
229	228	oveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑦 + ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( 𝑦 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) · 𝑇 ) ) )
230	213 216 229	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑦 − 𝑈 ) = ( 𝑦 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) · 𝑇 ) ) )
231	230	fveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑦 − 𝑈 ) ) = ( 𝐹 ‘ ( 𝑦 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) · 𝑇 ) ) ) )
232	5	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝐹 : ℝ ⟶ ℂ )
233	219	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑇 ∈ ℝ )
234	14	a1i	⊢ ( 𝜑 → 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
235		id	⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
236		oveq2	⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( 𝐵 − 𝑥 ) = ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
237	236	oveq1d	⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) )
238	237	fveq2d	⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) )
239	238	oveq1d	⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) )
240	235 239	oveq12d	⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
241	240	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
242	23 55	resubcld	⊢ ( 𝜑 → ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℝ )
243	242 219 225	redivcld	⊢ ( 𝜑 → ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ∈ ℝ )
244	243	flcld	⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) ∈ ℤ )
245	244	zred	⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) ∈ ℝ )
246	245 219	remulcld	⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
247	55 246	readdcld	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
248	234 241 55 247	fvmptd	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
249	248	oveq1d	⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
250	245	recnd	⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) ∈ ℂ )
251	250 220	mulcld	⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
252	144 251	pncan2d	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) )
253	249 252	eqtrd	⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) )
254	253	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) = ( ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) )
255	250 220 225	divcan4d	⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) )
256	254 255	eqtrd	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) )
257	256 244	eqeltrd	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ∈ ℤ )
258	257	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ∈ ℤ )
259	6	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
260	232 233 258 186 259	fperiodmul	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑦 + ( ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑦 ) )
261	231 260	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑦 − 𝑈 ) ) = ( 𝐹 ‘ 𝑦 ) )
262	181 211 261	3eqtrrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) )
263	262	mpteq2dva	⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐹 ‘ 𝑦 ) ) = ( 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) ) )
264	176 179 263	3eqtrrd	⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐺 ‘ ( 𝑦 − 𝑈 ) ) ) = ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
265	124 174 264	3eqtrd	⊢ ( 𝜑 → 𝑅 = ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
266	173	oveq1d	⊢ ( 𝜑 → ( ( ( ( 𝐿 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) –cn→ ℂ ) = ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) –cn→ ℂ ) )
267	123 265 266	3eltr3d	⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) –cn→ ℂ ) )