Theorem fourierdlem89

Description: Given a piecewise continuous function and changing the interval and the partition, the limit at the lower bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		fourierdlem89.p	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
2		fourierdlem89.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
3		fourierdlem89.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4		fourierdlem89.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
5		fourierdlem89.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
6		fourierdlem89.per	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
7		fourierdlem89.fcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
8		fourierdlem89.limc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
9		fourierdlem89.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
10		fourierdlem89.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,) +∞ ) )
11		fourierdlem89.o	⊢ 𝑂 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
12		fourierdlem89.12	⊢ 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
13		fourierdlem89.n	⊢ 𝑁 = ( ( ♯ ‘ 𝐻 ) − 1 )
14		fourierdlem89.s	⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) )
15		fourierdlem89.e	⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
16		fourierdlem89.z	⊢ 𝑍 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
17		fourierdlem89.j	⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ 𝑁 ) )
18		fourierdlem89.u	⊢ 𝑈 = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
19		fourierdlem89.20	⊢ 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑍 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) )
20		fourierdlem89.21	⊢ 𝑉 = ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝑅 )
21	1	fourierdlem2	⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
22	3 21	syl	⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
23	4 22	mpbid	⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
24	23	simpld	⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
25		elmapi	⊢ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
26	24 25	syl	⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
27		fzossfz	⊢ ( 0 ..^ 𝑀 ) ⊆ ( 0 ... 𝑀 )
28	1 3 4 2 15 16 19	fourierdlem37	⊢ ( 𝜑 → ( 𝐼 : ℝ ⟶ ( 0 ..^ 𝑀 ) ∧ ( 𝑥 ∈ ℝ → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑍 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑍 ‘ ( 𝐸 ‘ 𝑥 ) ) } ) ) )
29	28	simpld	⊢ ( 𝜑 → 𝐼 : ℝ ⟶ ( 0 ..^ 𝑀 ) )
30		elioore	⊢ ( 𝐷 ∈ ( 𝐶 (,) +∞ ) → 𝐷 ∈ ℝ )
31	10 30	syl	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
32		elioo4g	⊢ ( 𝐷 ∈ ( 𝐶 (,) +∞ ) ↔ ( ( 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ℝ ) ∧ ( 𝐶 < 𝐷 ∧ 𝐷 < +∞ ) ) )
33	10 32	sylib	⊢ ( 𝜑 → ( ( 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ℝ ) ∧ ( 𝐶 < 𝐷 ∧ 𝐷 < +∞ ) ) )
34	33	simprd	⊢ ( 𝜑 → ( 𝐶 < 𝐷 ∧ 𝐷 < +∞ ) )
35	34	simpld	⊢ ( 𝜑 → 𝐶 < 𝐷 )
36		oveq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 + ( 𝑘 · 𝑇 ) ) = ( 𝑥 + ( 𝑘 · 𝑇 ) ) )
37	36	eleq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
38	37	rexbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ) )
39	38	cbvrabv	⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 }
40	39	uneq2i	⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } )
41	12	fveq2i	⊢ ( ♯ ‘ 𝐻 ) = ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) )
42	41	oveq1i	⊢ ( ( ♯ ‘ 𝐻 ) − 1 ) = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 )
43	13 42	eqtri	⊢ 𝑁 = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 )
44		isoeq5	⊢ ( 𝐻 = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) → ( 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ↔ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
45	12 44	ax-mp	⊢ ( 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ↔ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
46	45	iotabii	⊢ ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝐻 ) ) = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
47	14 46	eqtri	⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
48	2 1 3 4 9 31 35 11 40 43 47	fourierdlem54	⊢ ( 𝜑 → ( ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) ∧ 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
49	48	simpld	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ∧ 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ) )
50	49	simprd	⊢ ( 𝜑 → 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) )
51	49	simpld	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
52	11	fourierdlem2	⊢ ( 𝑁 ∈ ℕ → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
53	51 52	syl	⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝑂 ‘ 𝑁 ) ↔ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
54	50 53	mpbid	⊢ ( 𝜑 → ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) ∧ ( ( ( 𝑆 ‘ 0 ) = 𝐶 ∧ ( 𝑆 ‘ 𝑁 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
55	54	simpld	⊢ ( 𝜑 → 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) )
56		elmapi	⊢ ( 𝑆 ∈ ( ℝ ↑m ( 0 ... 𝑁 ) ) → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
57	55 56	syl	⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
58		elfzofz	⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ( 0 ... 𝑁 ) )
59	17 58	syl	⊢ ( 𝜑 → 𝐽 ∈ ( 0 ... 𝑁 ) )
60	57 59	ffvelcdmd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ℝ )
61	29 60	ffvelcdmd	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) )
62	27 61	sselid	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ... 𝑀 ) )
63	26 62	ffvelcdmd	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ )
64	63	rexrd	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ* )
65	64	adantr	⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ* )
66		fzofzp1	⊢ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ∈ ( 0 ... 𝑀 ) )
67	61 66	syl	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ∈ ( 0 ... 𝑀 ) )
68	26 67	ffvelcdmd	⊢ ( 𝜑 → ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ∈ ℝ )
69	68	rexrd	⊢ ( 𝜑 → ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ∈ ℝ* )
70	69	adantr	⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ∈ ℝ* )
71	1 3 4	fourierdlem11	⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) )
72	71	simp1d	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
73	71	simp2d	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
74	72 73	iccssred	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
75	71	simp3d	⊢ ( 𝜑 → 𝐴 < 𝐵 )
76	72 73 75 16	fourierdlem17	⊢ ( 𝜑 → 𝑍 : ( 𝐴 (,] 𝐵 ) ⟶ ( 𝐴 [,] 𝐵 ) )
77	72 73 75 2 15	fourierdlem4	⊢ ( 𝜑 → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
78	77 60	ffvelcdmd	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
79	76 78	ffvelcdmd	⊢ ( 𝜑 → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( 𝐴 [,] 𝐵 ) )
80	74 79	sseldd	⊢ ( 𝜑 → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ )
81	80	adantr	⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ )
82	63	adantr	⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℝ )
83	72	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
84		iocssre	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
85	83 73 84	syl2anc	⊢ ( 𝜑 → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
86		fzofzp1	⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
87	17 86	syl	⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
88	57 87	ffvelcdmd	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
89	77 88	ffvelcdmd	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ( 𝐴 (,] 𝐵 ) )
90	85 89	sseldd	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℝ )
91	54	simprrd	⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
92		fveq2	⊢ ( 𝑖 = 𝐽 → ( 𝑆 ‘ 𝑖 ) = ( 𝑆 ‘ 𝐽 ) )
93		oveq1	⊢ ( 𝑖 = 𝐽 → ( 𝑖 + 1 ) = ( 𝐽 + 1 ) )
94	93	fveq2d	⊢ ( 𝑖 = 𝐽 → ( 𝑆 ‘ ( 𝑖 + 1 ) ) = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
95	92 94	breq12d	⊢ ( 𝑖 = 𝐽 → ( ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
96	95	rspccva	⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑆 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
97	91 17 96	syl2anc	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
98	60 88	posdifd	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ↔ 0 < ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
99	97 98	mpbid	⊢ ( 𝜑 → 0 < ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) )
100	17	ancli	⊢ ( 𝜑 → ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) )
101		eleq1	⊢ ( 𝑗 = 𝐽 → ( 𝑗 ∈ ( 0 ..^ 𝑁 ) ↔ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) )
102	101	anbi2d	⊢ ( 𝑗 = 𝐽 → ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ↔ ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) ) )
103		oveq1	⊢ ( 𝑗 = 𝐽 → ( 𝑗 + 1 ) = ( 𝐽 + 1 ) )
104	103	fveq2d	⊢ ( 𝑗 = 𝐽 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
105	104	fveq2d	⊢ ( 𝑗 = 𝐽 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
106		fveq2	⊢ ( 𝑗 = 𝐽 → ( 𝑆 ‘ 𝑗 ) = ( 𝑆 ‘ 𝐽 ) )
107	106	fveq2d	⊢ ( 𝑗 = 𝐽 → ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) )
108	107	fveq2d	⊢ ( 𝑗 = 𝐽 → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
109	105 108	oveq12d	⊢ ( 𝑗 = 𝐽 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
110	104 106	oveq12d	⊢ ( 𝑗 = 𝐽 → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) )
111	109 110	eqeq12d	⊢ ( 𝑗 = 𝐽 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ↔ ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
112	102 111	imbi12d	⊢ ( 𝑗 = 𝐽 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) ) ↔ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) ) )
113	2	oveq2i	⊢ ( 𝑘 · 𝑇 ) = ( 𝑘 · ( 𝐵 − 𝐴 ) )
114	113	oveq2i	⊢ ( 𝑦 + ( 𝑘 · 𝑇 ) ) = ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) )
115	114	eleq1i	⊢ ( ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
116	115	rexbii	⊢ ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
117	116	rgenw	⊢ ∀ 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 )
118		rabbi	⊢ ( ∀ 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 ) ↔ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } )
119	117 118	mpbi	⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 }
120	119	uneq2i	⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } )
121	120	fveq2i	⊢ ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) = ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) )
122	121	oveq1i	⊢ ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) − 1 )
123	43 122	eqtri	⊢ 𝑁 = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) − 1 )
124		isoeq5	⊢ ( ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) → ( 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) ) )
125	120 124	ax-mp	⊢ ( 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
126	125	iotabii	⊢ ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
127	47 126	eqtri	⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · ( 𝐵 − 𝐴 ) ) ) ∈ ran 𝑄 } ) ) )
128		eqid	⊢ ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ 𝑗 ) + ( 𝐵 − ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) )
129	1 2 3 4 9 10 11 123 127 15 16 128	fourierdlem65	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) )
130	112 129	vtoclg	⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
131	17 100 130	sylc	⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) )
132	99 131	breqtrrd	⊢ ( 𝜑 → 0 < ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
133	80 90	posdifd	⊢ ( 𝜑 → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ↔ 0 < ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) )
134	132 133	mpbird	⊢ ( 𝜑 → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
135		id	⊢ ( 𝜑 → 𝜑 )
136	108 105	oveq12d	⊢ ( 𝑗 = 𝐽 → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
137	106	fveq2d	⊢ ( 𝑗 = 𝐽 → ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) )
138	137	fveq2d	⊢ ( 𝑗 = 𝐽 → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
139	137	oveq1d	⊢ ( 𝑗 = 𝐽 → ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) = ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) )
140	139	fveq2d	⊢ ( 𝑗 = 𝐽 → ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
141	138 140	oveq12d	⊢ ( 𝑗 = 𝐽 → ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) = ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
142	136 141	sseq12d	⊢ ( 𝑗 = 𝐽 → ( ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) ↔ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) )
143	102 142	imbi12d	⊢ ( 𝑗 = 𝐽 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) ) ↔ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ) )
144		eqid	⊢ ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) ) = ( ( 𝑆 ‘ 𝑗 ) + if ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) < ( ( 𝑄 ‘ 1 ) − 𝐴 ) , ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) − ( 𝑆 ‘ 𝑗 ) ) / 2 ) , ( ( ( 𝑄 ‘ 1 ) − 𝐴 ) / 2 ) ) )
145	2 1 3 4 9 31 35 11 40 43 47 15 16 144 19	fourierdlem79	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝑗 ) ) + 1 ) ) ) )
146	143 145	vtoclg	⊢ ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) )
147	146	anabsi7	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
148	135 17 147	syl2anc	⊢ ( 𝜑 → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
149	63 68 80 90 134 148	fourierdlem10	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ≤ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∧ ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ≤ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
150	149	simpld	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ≤ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
151	150	adantr	⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ≤ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
152		neqne	⊢ ( ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ≠ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
153	152	adantl	⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ≠ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
154	82 81 151 153	leneltd	⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
155	149	simprd	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ≤ ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
156	80 90 68 134 155	ltletrd	⊢ ( 𝜑 → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
157	156	adantr	⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
158	65 70 81 154 157	eliood	⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
159		fvres	⊢ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( 𝐹 ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
160	158 159	syl	⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( 𝐹 ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
161	160	eqcomd	⊢ ( ( 𝜑 ∧ ¬ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) → ( 𝐹 ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
162	161	ifeq2da	⊢ ( 𝜑 → if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝐹 ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) = if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) )
163		fdm	⊢ ( 𝐹 : ℝ ⟶ ℂ → dom 𝐹 = ℝ )
164	5 163	syl	⊢ ( 𝜑 → dom 𝐹 = ℝ )
165	164	feq2d	⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ ℂ ↔ 𝐹 : ℝ ⟶ ℂ ) )
166	5 165	mpbird	⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℂ )
167		ioosscn	⊢ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ℂ
168	167	a1i	⊢ ( 𝜑 → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ℂ )
169		ioossre	⊢ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ ℝ
170	169 164	sseqtrrid	⊢ ( 𝜑 → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ⊆ dom 𝐹 )
171	88 90	resubcld	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ∈ ℝ )
172	18 171	eqeltrid	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
173	172	recnd	⊢ ( 𝜑 → 𝑈 ∈ ℂ )
174		eqid	⊢ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } = { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) }
175	80 90 172	iooshift	⊢ ( 𝜑 → ( ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) = { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } )
176		ioossre	⊢ ( ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) ⊆ ℝ
177	176 164	sseqtrrid	⊢ ( 𝜑 → ( ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) ⊆ dom 𝐹 )
178	175 177	eqsstrrd	⊢ ( 𝜑 → { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } ⊆ dom 𝐹 )
179		elioore	⊢ ( 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑦 ∈ ℝ )
180	73 72	resubcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
181	2 180	eqeltrid	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
182	181	recnd	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
183	72 73	posdifd	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
184	75 183	mpbid	⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
185	184 2	breqtrrdi	⊢ ( 𝜑 → 0 < 𝑇 )
186	185	gt0ne0d	⊢ ( 𝜑 → 𝑇 ≠ 0 )
187	173 182 186	divcan1d	⊢ ( 𝜑 → ( ( 𝑈 / 𝑇 ) · 𝑇 ) = 𝑈 )
188	187	eqcomd	⊢ ( 𝜑 → 𝑈 = ( ( 𝑈 / 𝑇 ) · 𝑇 ) )
189	188	oveq2d	⊢ ( 𝜑 → ( 𝑦 + 𝑈 ) = ( 𝑦 + ( ( 𝑈 / 𝑇 ) · 𝑇 ) ) )
190	189	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 + 𝑈 ) = ( 𝑦 + ( ( 𝑈 / 𝑇 ) · 𝑇 ) ) )
191	190	fveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + 𝑈 ) ) = ( 𝐹 ‘ ( 𝑦 + ( ( 𝑈 / 𝑇 ) · 𝑇 ) ) ) )
192	5	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐹 : ℝ ⟶ ℂ )
193	181	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑇 ∈ ℝ )
194	90	recnd	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℂ )
195	88	recnd	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℂ )
196	194 195	negsubdi2d	⊢ ( 𝜑 → - ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
197	196	eqcomd	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = - ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
198	197	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) / 𝑇 ) = ( - ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) )
199	18	oveq1i	⊢ ( 𝑈 / 𝑇 ) = ( ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) / 𝑇 )
200	199	a1i	⊢ ( 𝜑 → ( 𝑈 / 𝑇 ) = ( ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) / 𝑇 ) )
201	15	a1i	⊢ ( 𝜑 → 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
202		id	⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
203		oveq2	⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( 𝐵 − 𝑥 ) = ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
204	203	oveq1d	⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) )
205	204	fveq2d	⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) )
206	205	oveq1d	⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) )
207	202 206	oveq12d	⊢ ( 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
208	207	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
209	73 88	resubcld	⊢ ( 𝜑 → ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℝ )
210	209 181 186	redivcld	⊢ ( 𝜑 → ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ∈ ℝ )
211	210	flcld	⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) ∈ ℤ )
212	211	zred	⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) ∈ ℝ )
213	212 181	remulcld	⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
214	88 213	readdcld	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
215	201 208 88 214	fvmptd	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) )
216	215	oveq1d	⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
217	212	recnd	⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) ∈ ℂ )
218	217 182	mulcld	⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
219	195 218	pncan2d	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) )
220	216 219	eqtrd	⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) = ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) )
221	220 218	eqeltrd	⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∈ ℂ )
222	221 182 186	divnegd	⊢ ( 𝜑 → - ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) = ( - ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) )
223	198 200 222	3eqtr4d	⊢ ( 𝜑 → ( 𝑈 / 𝑇 ) = - ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) )
224	220	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) = ( ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) )
225	217 182 186	divcan4d	⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) · 𝑇 ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) )
226	224 225	eqtrd	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) = ( ⌊ ‘ ( ( 𝐵 − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ) )
227	226 211	eqeltrd	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ∈ ℤ )
228	227	znegcld	⊢ ( 𝜑 → - ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) / 𝑇 ) ∈ ℤ )
229	223 228	eqeltrd	⊢ ( 𝜑 → ( 𝑈 / 𝑇 ) ∈ ℤ )
230	229	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑈 / 𝑇 ) ∈ ℤ )
231		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
232	6	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
233	192 193 230 231 232	fperiodmul	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + ( ( 𝑈 / 𝑇 ) · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑦 ) )
234	191 233	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + 𝑈 ) ) = ( 𝐹 ‘ 𝑦 ) )
235	179 234	sylan2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) → ( 𝐹 ‘ ( 𝑦 + 𝑈 ) ) = ( 𝐹 ‘ 𝑦 ) )
236	23	simprrd	⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
237		fveq2	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
238		oveq1	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑖 + 1 ) = ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) )
239	238	fveq2d	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
240	237 239	breq12d	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
241	240	rspccva	⊢ ( ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
242	236 61 241	syl2anc	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) < ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) )
243	61	ancli	⊢ ( 𝜑 → ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) )
244		eleq1	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) )
245	244	anbi2d	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) )
246	237 239	oveq12d	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
247	246	reseq2d	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) )
248	246	oveq1d	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) = ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) )
249	247 248	eleq12d	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) ↔ ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) ) )
250	245 249	imbi12d	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) ) ↔ ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) ) ) )
251	250 7	vtoclg	⊢ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) → ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) ) )
252	61 243 251	sylc	⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) –cn→ ℂ ) )
253		nfv	⊢ Ⅎ 𝑖 ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) )
254		nfmpt1	⊢ Ⅎ 𝑖 ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ 𝑅 )
255	20 254	nfcxfr	⊢ Ⅎ 𝑖 𝑉
256		nfcv	⊢ Ⅎ 𝑖 ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) )
257	255 256	nffv	⊢ Ⅎ 𝑖 ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) )
258	257	nfel1	⊢ Ⅎ 𝑖 ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
259	253 258	nfim	⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
260	245	biimpar	⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) )
261	260	3adant2	⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) )
262	261 8	syl	⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
263		fveq2	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
264	263	eqcomd	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑉 ‘ 𝑖 ) )
265	264	adantr	⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑉 ‘ 𝑖 ) )
266	260	simprd	⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
267		elex	⊢ ( 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) → 𝑅 ∈ V )
268	260 8 267	3syl	⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → 𝑅 ∈ V )
269	20	fvmpt2	⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑅 ∈ V ) → ( 𝑉 ‘ 𝑖 ) = 𝑅 )
270	266 268 269	syl2anc	⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑉 ‘ 𝑖 ) = 𝑅 )
271	265 270	eqtrd	⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = 𝑅 )
272	271	3adant2	⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = 𝑅 )
273	247 237	oveq12d	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
274	273	eqcomd	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
275	274	3ad2ant1	⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
276	262 272 275	3eltr4d	⊢ ( ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∧ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ∧ ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
277	276	3exp	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) → ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) ) )
278	8	2a1i	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ) )
279	277 278	impbid	⊢ ( 𝑖 = ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ↔ ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) ) )
280	259 279 8	vtoclg1f	⊢ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) → ( ( 𝜑 ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) )
281	61 243 280	sylc	⊢ ( 𝜑 → ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
282		eqid	⊢ if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) = if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
283		eqid	⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) [,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) [,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) )
284	63 68 242 252 281 80 90 134 148 282 283	fourierdlem32	⊢ ( 𝜑 → if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) ∈ ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ↾ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) limℂ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
285	148	resabs1d	⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ↾ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( 𝐹 ↾ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
286	285	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ↾ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) limℂ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝐹 ↾ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) limℂ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
287	284 286	eleqtrd	⊢ ( 𝜑 → if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) limℂ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) )
288	166 168 170 173 174 178 235 287	limcperiod	⊢ ( 𝜑 → if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) ∈ ( ( 𝐹 ↾ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } ) limℂ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) ) )
289	18	oveq2i	⊢ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) = ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
290	289	a1i	⊢ ( 𝜑 → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) = ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
291	9 31	iccssred	⊢ ( 𝜑 → ( 𝐶 [,] 𝐷 ) ⊆ ℝ )
292		ax-resscn	⊢ ℝ ⊆ ℂ
293	291 292	sstrdi	⊢ ( 𝜑 → ( 𝐶 [,] 𝐷 ) ⊆ ℂ )
294	11 51 50	fourierdlem15	⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐶 [,] 𝐷 ) )
295	294 59	ffvelcdmd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ( 𝐶 [,] 𝐷 ) )
296	293 295	sseldd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐽 ) ∈ ℂ )
297	195 296	subcld	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ∈ ℂ )
298	80	recnd	⊢ ( 𝜑 → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℂ )
299	194 297 298	subsub23d	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ↔ ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
300	131 299	mpbird	⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) )
301	300	eqcomd	⊢ ( 𝜑 → ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
302	301	oveq1d	⊢ ( 𝜑 → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
303	194 297	subcld	⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) ∈ ℂ )
304	303 195 194	addsub12d	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) )
305	194 297 194	sub32d	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
306	194	subidd	⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = 0 )
307	306	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) = ( 0 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) )
308		df-neg	⊢ - ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) = ( 0 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) )
309	195 296	negsubdi2d	⊢ ( 𝜑 → - ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) = ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
310	308 309	eqtr3id	⊢ ( 𝜑 → ( 0 − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) = ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
311	305 307 310	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
312	311	oveq2d	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
313	195 296	pncan3d	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) + ( ( 𝑆 ‘ 𝐽 ) − ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) = ( 𝑆 ‘ 𝐽 ) )
314	304 312 313	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) − ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝑆 ‘ 𝐽 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( 𝑆 ‘ 𝐽 ) )
315	290 302 314	3eqtrd	⊢ ( 𝜑 → ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) = ( 𝑆 ‘ 𝐽 ) )
316	315	oveq2d	⊢ ( 𝜑 → ( ( 𝐹 ↾ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } ) limℂ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) ) = ( ( 𝐹 ↾ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } ) limℂ ( 𝑆 ‘ 𝐽 ) ) )
317	288 316	eleqtrd	⊢ ( 𝜑 → if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) ∈ ( ( 𝐹 ↾ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } ) limℂ ( 𝑆 ‘ 𝐽 ) ) )
318	18	oveq2i	⊢ ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) = ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
319	194 195	pncan3d	⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + ( ( 𝑆 ‘ ( 𝐽 + 1 ) ) − ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
320	318 319	eqtrid	⊢ ( 𝜑 → ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) = ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
321	315 320	oveq12d	⊢ ( 𝜑 → ( ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) + 𝑈 ) (,) ( ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) + 𝑈 ) ) = ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
322	175 321	eqtr3d	⊢ ( 𝜑 → { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } = ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
323	322	reseq2d	⊢ ( 𝜑 → ( 𝐹 ↾ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } ) = ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) )
324	323	oveq1d	⊢ ( 𝜑 → ( ( 𝐹 ↾ { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝐸 ‘ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) 𝑥 = ( 𝑦 + 𝑈 ) } ) limℂ ( 𝑆 ‘ 𝐽 ) ) = ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝐽 ) ) )
325	317 324	eleqtrd	⊢ ( 𝜑 → if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( ( 𝐹 ↾ ( ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) (,) ( 𝑄 ‘ ( ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) + 1 ) ) ) ) ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝐽 ) ) )
326	162 325	eqeltrd	⊢ ( 𝜑 → if ( ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) = ( 𝑄 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝑉 ‘ ( 𝐼 ‘ ( 𝑆 ‘ 𝐽 ) ) ) , ( 𝐹 ‘ ( 𝑍 ‘ ( 𝐸 ‘ ( 𝑆 ‘ 𝐽 ) ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑆 ‘ 𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝐽 ) ) )