Theorem fourierdlem76

Description: Continuity of O and its limits with respect to the S partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem76.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
	fourierdlem76.xre	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	fourierdlem76.p	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
	fourierdlem76.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	fourierdlem76.v	⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
	fourierdlem76.fcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
	fourierdlem76.r	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) )
	fourierdlem76.l	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
	fourierdlem76.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	fourierdlem76.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	fourierdlem76.altb	⊢ ( 𝜑 → 𝐴 < 𝐵 )
	fourierdlem76.ab	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ( - π [,] π ) )
	fourierdlem76.n0	⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐴 [,] 𝐵 ) )
	fourierdlem76.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	fourierdlem76.o	⊢ 𝑂 = ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
	fourierdlem76.q	⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
	fourierdlem76.t	⊢ 𝑇 = ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) )
	fourierdlem76.n	⊢ 𝑁 = ( ( ♯ ‘ 𝑇 ) − 1 )
	fourierdlem76.s	⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
	fourierdlem76.d	⊢ 𝐷 = ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) )
	fourierdlem76.e	⊢ 𝐸 = ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) )
	fourierdlem76.ch	⊢ ( 𝜒 ↔ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
Assertion	fourierdlem76	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐷 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ 𝐸 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) ∧ ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem76.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2		fourierdlem76.xre	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
3		fourierdlem76.p	⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑝 ‘ 𝑚 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
4		fourierdlem76.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
5		fourierdlem76.v	⊢ ( 𝜑 → 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) )
6		fourierdlem76.fcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
7		fourierdlem76.r	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) )
8		fourierdlem76.l	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
9		fourierdlem76.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
10		fourierdlem76.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
11		fourierdlem76.altb	⊢ ( 𝜑 → 𝐴 < 𝐵 )
12		fourierdlem76.ab	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ( - π [,] π ) )
13		fourierdlem76.n0	⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐴 [,] 𝐵 ) )
14		fourierdlem76.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
15		fourierdlem76.o	⊢ 𝑂 = ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
16		fourierdlem76.q	⊢ 𝑄 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
17		fourierdlem76.t	⊢ 𝑇 = ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) )
18		fourierdlem76.n	⊢ 𝑁 = ( ( ♯ ‘ 𝑇 ) − 1 )
19		fourierdlem76.s	⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
20		fourierdlem76.d	⊢ 𝐷 = ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) )
21		fourierdlem76.e	⊢ 𝐸 = ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) )
22		fourierdlem76.ch	⊢ ( 𝜒 ↔ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
23		eqid	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) )
24		eqid	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) )
25		eqid	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) )
26		simplll	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝜑 )
27	22 26	sylbi	⊢ ( 𝜒 → 𝜑 )
28	27	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝜑 )
29		ioossicc	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
30	9	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
31	27 30	syl	⊢ ( 𝜒 → 𝐴 ∈ ℝ* )
32	31	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝐴 ∈ ℝ* )
33	10	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
34	27 33	syl	⊢ ( 𝜒 → 𝐵 ∈ ℝ* )
35	34	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝐵 ∈ ℝ* )
36		elioore	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → 𝑠 ∈ ℝ )
37	36	adantl	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
38	27 9	syl	⊢ ( 𝜒 → 𝐴 ∈ ℝ )
39	38	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝐴 ∈ ℝ )
40		prfi	⊢ { 𝐴 , 𝐵 } ∈ Fin
41	40	a1i	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ Fin )
42		fzfid	⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
43	16	rnmptfi	⊢ ( ( 0 ... 𝑀 ) ∈ Fin → ran 𝑄 ∈ Fin )
44		infi	⊢ ( ran 𝑄 ∈ Fin → ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ∈ Fin )
45	42 43 44	3syl	⊢ ( 𝜑 → ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ∈ Fin )
46		unfi	⊢ ( ( { 𝐴 , 𝐵 } ∈ Fin ∧ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ∈ Fin ) → ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) ∈ Fin )
47	41 45 46	syl2anc	⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) ∈ Fin )
48	17 47	eqeltrid	⊢ ( 𝜑 → 𝑇 ∈ Fin )
49		prssg	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ↔ { 𝐴 , 𝐵 } ⊆ ℝ ) )
50	9 10 49	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ↔ { 𝐴 , 𝐵 } ⊆ ℝ ) )
51	9 10 50	mpbi2and	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ ℝ )
52		inss2	⊢ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ( 𝐴 (,) 𝐵 )
53		ioossre	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
54	52 53	sstri	⊢ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ℝ
55	54	a1i	⊢ ( 𝜑 → ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ℝ )
56	51 55	unssd	⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) ⊆ ℝ )
57	17 56	eqsstrid	⊢ ( 𝜑 → 𝑇 ⊆ ℝ )
58	48 57 19 18	fourierdlem36	⊢ ( 𝜑 → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
59	27 58	syl	⊢ ( 𝜒 → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
60		isof1o	⊢ ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) → 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝑇 )
61		f1of	⊢ ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝑇 → 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝑇 )
62	59 60 61	3syl	⊢ ( 𝜒 → 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝑇 )
63	27 57	syl	⊢ ( 𝜒 → 𝑇 ⊆ ℝ )
64	62 63	fssd	⊢ ( 𝜒 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
65	64	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ )
66		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑗 ∈ ( 0 ..^ 𝑁 ) )
67	22 66	sylbi	⊢ ( 𝜒 → 𝑗 ∈ ( 0 ..^ 𝑁 ) )
68		elfzofz	⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
69	67 68	syl	⊢ ( 𝜒 → 𝑗 ∈ ( 0 ... 𝑁 ) )
70	69	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
71	65 70	ffvelcdmd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
72	58 60 61	3syl	⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝑇 )
73		frn	⊢ ( 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝑇 → ran 𝑆 ⊆ 𝑇 )
74	72 73	syl	⊢ ( 𝜑 → ran 𝑆 ⊆ 𝑇 )
75	9	leidd	⊢ ( 𝜑 → 𝐴 ≤ 𝐴 )
76	9 10 11	ltled	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
77	9 10 9 75 76	eliccd	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
78	10	leidd	⊢ ( 𝜑 → 𝐵 ≤ 𝐵 )
79	9 10 10 76 78	eliccd	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
80		prssg	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ { 𝐴 , 𝐵 } ⊆ ( 𝐴 [,] 𝐵 ) ) )
81	9 10 80	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ { 𝐴 , 𝐵 } ⊆ ( 𝐴 [,] 𝐵 ) ) )
82	77 79 81	mpbi2and	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ ( 𝐴 [,] 𝐵 ) )
83	52 29	sstri	⊢ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 )
84	83	a1i	⊢ ( 𝜑 → ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
85	82 84	unssd	⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
86	17 85	eqsstrid	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐴 [,] 𝐵 ) )
87	74 86	sstrd	⊢ ( 𝜑 → ran 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) )
88	27 87	syl	⊢ ( 𝜒 → ran 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) )
89		ffun	⊢ ( 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ → Fun 𝑆 )
90	64 89	syl	⊢ ( 𝜒 → Fun 𝑆 )
91		fdm	⊢ ( 𝑆 : ( 0 ... 𝑁 ) ⟶ ℝ → dom 𝑆 = ( 0 ... 𝑁 ) )
92	64 91	syl	⊢ ( 𝜒 → dom 𝑆 = ( 0 ... 𝑁 ) )
93	92	eqcomd	⊢ ( 𝜒 → ( 0 ... 𝑁 ) = dom 𝑆 )
94	69 93	eleqtrd	⊢ ( 𝜒 → 𝑗 ∈ dom 𝑆 )
95		fvelrn	⊢ ( ( Fun 𝑆 ∧ 𝑗 ∈ dom 𝑆 ) → ( 𝑆 ‘ 𝑗 ) ∈ ran 𝑆 )
96	90 94 95	syl2anc	⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ∈ ran 𝑆 )
97	88 96	sseldd	⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) )
98		iccgelb	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ ( 𝑆 ‘ 𝑗 ) )
99	31 34 97 98	syl3anc	⊢ ( 𝜒 → 𝐴 ≤ ( 𝑆 ‘ 𝑗 ) )
100	99	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝐴 ≤ ( 𝑆 ‘ 𝑗 ) )
101	71	rexrd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ* )
102		fzofzp1	⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) )
103	67 102	syl	⊢ ( 𝜒 → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) )
104	64 103	ffvelcdmd	⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
105	104	rexrd	⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* )
106	105	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* )
107		simpr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
108		ioogtlb	⊢ ( ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ* ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑆 ‘ 𝑗 ) < 𝑠 )
109	101 106 107 108	syl3anc	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑆 ‘ 𝑗 ) < 𝑠 )
110	39 71 37 100 109	lelttrd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝐴 < 𝑠 )
111	104	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
112	27 10	syl	⊢ ( 𝜒 → 𝐵 ∈ ℝ )
113	112	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝐵 ∈ ℝ )
114		iooltub	⊢ ( ( ( 𝑆 ‘ 𝑗 ) ∈ ℝ* ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ* ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
115	101 106 107 114	syl3anc	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
116	103 93	eleqtrd	⊢ ( 𝜒 → ( 𝑗 + 1 ) ∈ dom 𝑆 )
117		fvelrn	⊢ ( ( Fun 𝑆 ∧ ( 𝑗 + 1 ) ∈ dom 𝑆 ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ran 𝑆 )
118	90 116 117	syl2anc	⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ran 𝑆 )
119	88 118	sseldd	⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
120		iccleub	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐵 )
121	31 34 119 120	syl3anc	⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐵 )
122	121	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐵 )
123	37 111 113 115 122	ltletrd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 < 𝐵 )
124	32 35 37 110 123	eliood	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ( 𝐴 (,) 𝐵 ) )
125	29 124	sselid	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
126	1	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐹 : ℝ ⟶ ℝ )
127	2	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑋 ∈ ℝ )
128	9 10	iccssred	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
129	128	sselda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑠 ∈ ℝ )
130	127 129	readdcld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
131	126 130	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
132	28 125 131	syl2anc	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℝ )
133	132	recnd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ∈ ℂ )
134	14	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
135	27 134	syl	⊢ ( 𝜒 → 𝐶 ∈ ℂ )
136	135	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝐶 ∈ ℂ )
137	133 136	subcld	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ∈ ℂ )
138		ioossre	⊢ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ℝ
139	138	a1i	⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ℝ )
140	139	sselda	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
141	140	recnd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ℂ )
142		nne	⊢ ( ¬ 𝑠 ≠ 0 ↔ 𝑠 = 0 )
143	142	biimpi	⊢ ( ¬ 𝑠 ≠ 0 → 𝑠 = 0 )
144	143	eqcomd	⊢ ( ¬ 𝑠 ≠ 0 → 0 = 𝑠 )
145	144	adantl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑠 ≠ 0 ) → 0 = 𝑠 )
146		simpr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
147	146	adantr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑠 ≠ 0 ) → 𝑠 ∈ ( 𝐴 [,] 𝐵 ) )
148	145 147	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑠 ≠ 0 ) → 0 ∈ ( 𝐴 [,] 𝐵 ) )
149	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ¬ 𝑠 ≠ 0 ) → ¬ 0 ∈ ( 𝐴 [,] 𝐵 ) )
150	148 149	condan	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑠 ≠ 0 )
151	28 125 150	syl2anc	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ≠ 0 )
152	137 141 151	divcld	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) ∈ ℂ )
153		2cnd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 2 ∈ ℂ )
154	141	halfcld	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑠 / 2 ) ∈ ℂ )
155	154	sincld	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
156	153 155	mulcld	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ )
157	36	recnd	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → 𝑠 ∈ ℂ )
158	157	adantl	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ℂ )
159	158	halfcld	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑠 / 2 ) ∈ ℂ )
160	159	sincld	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℂ )
161		2ne0	⊢ 2 ≠ 0
162	161	a1i	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 2 ≠ 0 )
163	27 12	syl	⊢ ( 𝜒 → ( 𝐴 [,] 𝐵 ) ⊆ ( - π [,] π ) )
164	163	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ( - π [,] π ) )
165	164 125	sseldd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ( - π [,] π ) )
166		fourierdlem44	⊢ ( ( 𝑠 ∈ ( - π [,] π ) ∧ 𝑠 ≠ 0 ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
167	165 151 166	syl2anc	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ≠ 0 )
168	153 160 162 167	mulne0d	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ≠ 0 )
169	141 156 168	divcld	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ℂ )
170		eqid	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) )
171		eqid	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝑠 ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝑠 )
172	151	neneqd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ¬ 𝑠 = 0 )
173		velsn	⊢ ( 𝑠 ∈ { 0 } ↔ 𝑠 = 0 )
174	172 173	sylnibr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ¬ 𝑠 ∈ { 0 } )
175	141 174	eldifd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ( ℂ ∖ { 0 } ) )
176		eqid	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
177		eqid	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝐶 ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝐶 )
178		elfzofz	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
179	178	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
180		pire	⊢ π ∈ ℝ
181	180	renegcli	⊢ - π ∈ ℝ
182	181	a1i	⊢ ( 𝜑 → - π ∈ ℝ )
183	182 2	readdcld	⊢ ( 𝜑 → ( - π + 𝑋 ) ∈ ℝ )
184	180	a1i	⊢ ( 𝜑 → π ∈ ℝ )
185	184 2	readdcld	⊢ ( 𝜑 → ( π + 𝑋 ) ∈ ℝ )
186	183 185	iccssred	⊢ ( 𝜑 → ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ⊆ ℝ )
187	186	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) ⊆ ℝ )
188	3 4 5	fourierdlem15	⊢ ( 𝜑 → 𝑉 : ( 0 ... 𝑀 ) ⟶ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) )
189	188	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑉 : ( 0 ... 𝑀 ) ⟶ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) )
190	189 179	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) )
191	187 190	sseldd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
192	2	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑋 ∈ ℝ )
193	191 192	resubcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ )
194	16	fvmpt2	⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ∈ ℝ ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
195	179 193 194	syl2anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
196	195 193	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
197	196	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
198	197	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
199	22 198	sylbi	⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
200		fveq2	⊢ ( 𝑖 = 𝑗 → ( 𝑉 ‘ 𝑖 ) = ( 𝑉 ‘ 𝑗 ) )
201	200	oveq1d	⊢ ( 𝑖 = 𝑗 → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) = ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
202	201	cbvmptv	⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
203	16 202	eqtri	⊢ 𝑄 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) )
204	203	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) ) )
205		fveq2	⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( 𝑉 ‘ 𝑗 ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
206	205	oveq1d	⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
207	206	adantl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 = ( 𝑖 + 1 ) ) → ( ( 𝑉 ‘ 𝑗 ) − 𝑋 ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
208		fzofzp1	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
209	208	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
210	189 209	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ( ( - π + 𝑋 ) [,] ( π + 𝑋 ) ) )
211	187 210	sseldd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
212	211 192	resubcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ∈ ℝ )
213	204 207 209 212	fvmptd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
214	213 212	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
215	214	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
216	215	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
217	22 216	sylbi	⊢ ( 𝜒 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
218	3	fourierdlem2	⊢ ( 𝑀 ∈ ℕ → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
219	4 218	syl	⊢ ( 𝜑 → ( 𝑉 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ) )
220	5 219	mpbid	⊢ ( 𝜑 → ( 𝑉 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑉 ‘ 0 ) = ( - π + 𝑋 ) ∧ ( 𝑉 ‘ 𝑀 ) = ( π + 𝑋 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) )
221	220	simprrd	⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
222	221	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑉 ‘ 𝑖 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
223	191 211 192 222	ltsub1dd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) < ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
224	223 195 213	3brtr4d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
225	224	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
226	225	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
227	22 226	sylbi	⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
228	22	biimpi	⊢ ( 𝜒 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
229	228	simplrd	⊢ ( 𝜒 → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
230	27 229 191	syl2anc	⊢ ( 𝜒 → ( 𝑉 ‘ 𝑖 ) ∈ ℝ )
231	230	rexrd	⊢ ( 𝜒 → ( 𝑉 ‘ 𝑖 ) ∈ ℝ* )
232	231	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ* )
233	27 229 211	syl2anc	⊢ ( 𝜒 → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
234	233	rexrd	⊢ ( 𝜒 → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
235	234	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
236	27 2	syl	⊢ ( 𝜒 → 𝑋 ∈ ℝ )
237	236	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑋 ∈ ℝ )
238		elioore	⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ℝ )
239	238	adantl	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
240	237 239	readdcld	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
241	27 229 195	syl2anc	⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) = ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) )
242	241	oveq2d	⊢ ( 𝜒 → ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) = ( 𝑋 + ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) )
243	236	recnd	⊢ ( 𝜒 → 𝑋 ∈ ℂ )
244	230	recnd	⊢ ( 𝜒 → ( 𝑉 ‘ 𝑖 ) ∈ ℂ )
245	243 244	pncan3d	⊢ ( 𝜒 → ( 𝑋 + ( ( 𝑉 ‘ 𝑖 ) − 𝑋 ) ) = ( 𝑉 ‘ 𝑖 ) )
246	242 245	eqtr2d	⊢ ( 𝜒 → ( 𝑉 ‘ 𝑖 ) = ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) )
247	246	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) = ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) )
248	199	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
249	199	rexrd	⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
250	249	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
251	217	rexrd	⊢ ( 𝜒 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
252	251	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
253		simpr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
254		ioogtlb	⊢ ( ( ( 𝑄 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) < 𝑠 )
255	250 252 253 254	syl3anc	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) < 𝑠 )
256	248 239 237 255	ltadd2dd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) < ( 𝑋 + 𝑠 ) )
257	247 256	eqbrtrd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) < ( 𝑋 + 𝑠 ) )
258	217	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
259		iooltub	⊢ ( ( ( 𝑄 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
260	250 252 253 259	syl3anc	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
261	239 258 237 260	ltadd2dd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) < ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
262	27 229 213	syl2anc	⊢ ( 𝜒 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) )
263	262	oveq2d	⊢ ( 𝜒 → ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑋 + ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) )
264	233	recnd	⊢ ( 𝜒 → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
265	243 264	pncan3d	⊢ ( 𝜒 → ( 𝑋 + ( ( 𝑉 ‘ ( 𝑖 + 1 ) ) − 𝑋 ) ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
266	263 265	eqtrd	⊢ ( 𝜒 → ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
267	266	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
268	261 267	breqtrd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
269	232 235 240 257 268	eliood	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
270		fvres	⊢ ( ( 𝑋 + 𝑠 ) ∈ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
271	269 270	syl	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
272	271	eqcomd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) )
273	272	mpteq2dva	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
274		ioosscn	⊢ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ
275	274	a1i	⊢ ( 𝜒 → ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ )
276	27 229 6	syl2anc	⊢ ( 𝜒 → ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
277		ioosscn	⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ
278	277	a1i	⊢ ( 𝜒 → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ )
279	275 276 278 243 269	fourierdlem23	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
280	273 279	eqeltrd	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
281	27 1	syl	⊢ ( 𝜒 → 𝐹 : ℝ ⟶ ℝ )
282		ioossre	⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ
283	282	a1i	⊢ ( 𝜒 → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
284		eqid	⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) )
285		ioossre	⊢ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ
286	285	a1i	⊢ ( 𝜒 → ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
287	239 260	ltned	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ≠ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
288	27 229 8	syl2anc	⊢ ( 𝜒 → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
289	266	eqcomd	⊢ ( 𝜒 → ( 𝑉 ‘ ( 𝑖 + 1 ) ) = ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
290	289	oveq2d	⊢ ( 𝜒 → ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
291	288 290	eleqtrd	⊢ ( 𝜒 → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
292	217	recnd	⊢ ( 𝜒 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
293	281 236 283 284 269 286 287 291 292	fourierdlem53	⊢ ( 𝜒 → 𝐿 ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
294	64 69	ffvelcdmd	⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
295		elfzoelz	⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 ∈ ℤ )
296		zre	⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ℝ )
297	67 295 296	3syl	⊢ ( 𝜒 → 𝑗 ∈ ℝ )
298	297	ltp1d	⊢ ( 𝜒 → 𝑗 < ( 𝑗 + 1 ) )
299		isorel	⊢ ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑗 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑗 < ( 𝑗 + 1 ) ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
300	59 69 103 299	syl12anc	⊢ ( 𝜒 → ( 𝑗 < ( 𝑗 + 1 ) ↔ ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
301	298 300	mpbid	⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
302	22	simprbi	⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
303		eqid	⊢ if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
304		eqid	⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∪ { ( 𝑄 ‘ ( 𝑖 + 1 ) ) } ) )
305	199 217 227 280 293 294 104 301 302 303 304	fourierdlem33	⊢ ( 𝜒 → if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
306		eqidd	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) )
307		simpr	⊢ ( ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → 𝑠 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
308	307	oveq2d	⊢ ( ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑋 + 𝑠 ) = ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
309	308	fveq2d	⊢ ( ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑠 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
310	249	adantr	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
311	251	adantr	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
312	104	adantr	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
313	199 217 294 104 301 302	fourierdlem10	⊢ ( 𝜒 → ( ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
314	313	simpld	⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑆 ‘ 𝑗 ) )
315	199 294 104 314 301	lelttrd	⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
316	315	adantr	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
317	217	adantr	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
318	313	simprd	⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
319	318	adantr	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
320		neqne	⊢ ( ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≠ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
321	320	necomd	⊢ ( ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≠ ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
322	321	adantl	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≠ ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
323	312 317 319 322	leneltd	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
324	310 311 312 316 323	eliood	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
325	236 104	readdcld	⊢ ( 𝜒 → ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
326	281 325	ffvelcdmd	⊢ ( 𝜒 → ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ℝ )
327	326	adantr	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ℝ )
328	306 309 324 327	fvmptd	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) )
329	328	ifeq2da	⊢ ( 𝜒 → if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) )
330	302	resmptd	⊢ ( 𝜒 → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) )
331	330	oveq1d	⊢ ( 𝜒 → ( ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
332	305 329 331	3eltr3d	⊢ ( 𝜒 → if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
333		ax-resscn	⊢ ℝ ⊆ ℂ
334	139 333	sstrdi	⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ℂ )
335	104	recnd	⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℂ )
336	177 334 135 335	constlimc	⊢ ( 𝜒 → 𝐶 ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝐶 ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
337	176 177 170 133 136 332 336	sublimc	⊢ ( 𝜒 → ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
338	334 171 335	idlimc	⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝑠 ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
339	27 119	jca	⊢ ( 𝜒 → ( 𝜑 ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) )
340		eleq1	⊢ ( 𝑠 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) )
341	340	anbi2d	⊢ ( 𝑠 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝜑 ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) ) )
342		neeq1	⊢ ( 𝑠 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( 𝑠 ≠ 0 ↔ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≠ 0 ) )
343	341 342	imbi12d	⊢ ( 𝑠 = ( 𝑆 ‘ ( 𝑗 + 1 ) ) → ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑠 ≠ 0 ) ↔ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≠ 0 ) ) )
344	343 150	vtoclg	⊢ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ → ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≠ 0 ) )
345	104 339 344	sylc	⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≠ 0 )
346	170 171 23 137 175 337 338 345 151	divlimc	⊢ ( 𝜒 → ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
347		eqid	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) )
348	153 160	mulcld	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℂ )
349	168	neneqd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ¬ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) = 0 )
350		2re	⊢ 2 ∈ ℝ
351	350	a1i	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 2 ∈ ℝ )
352	36	rehalfcld	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( 𝑠 / 2 ) ∈ ℝ )
353	352	resincld	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℝ )
354	353	adantl	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( sin ‘ ( 𝑠 / 2 ) ) ∈ ℝ )
355	351 354	remulcld	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℝ )
356		elsng	⊢ ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ℝ → ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ { 0 } ↔ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) = 0 ) )
357	355 356	syl	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ { 0 } ↔ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) = 0 ) )
358	349 357	mtbird	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ¬ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ { 0 } )
359	348 358	eldifd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ( ℂ ∖ { 0 } ) )
360		eqid	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 2 ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 2 )
361		eqid	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( sin ‘ ( 𝑠 / 2 ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( sin ‘ ( 𝑠 / 2 ) ) )
362		2cnd	⊢ ( 𝜒 → 2 ∈ ℂ )
363	360 334 362 335	constlimc	⊢ ( 𝜒 → 2 ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 2 ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
364	352	ad2antrl	⊢ ( ( 𝜒 ∧ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( 𝑠 / 2 ) ≠ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) → ( 𝑠 / 2 ) ∈ ℝ )
365		recn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
366	365	sincld	⊢ ( 𝑥 ∈ ℝ → ( sin ‘ 𝑥 ) ∈ ℂ )
367	366	adantl	⊢ ( ( 𝜒 ∧ 𝑥 ∈ ℝ ) → ( sin ‘ 𝑥 ) ∈ ℂ )
368		eqid	⊢ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / 2 ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / 2 ) )
369		2cn	⊢ 2 ∈ ℂ
370		eldifsn	⊢ ( 2 ∈ ( ℂ ∖ { 0 } ) ↔ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
371	369 161 370	mpbir2an	⊢ 2 ∈ ( ℂ ∖ { 0 } )
372	371	a1i	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 2 ∈ ( ℂ ∖ { 0 } ) )
373	161	a1i	⊢ ( 𝜒 → 2 ≠ 0 )
374	171 360 368 158 372 338 363 373 162	divlimc	⊢ ( 𝜒 → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / 2 ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
375		sinf	⊢ sin : ℂ ⟶ ℂ
376	375	a1i	⊢ ( ⊤ → sin : ℂ ⟶ ℂ )
377	333	a1i	⊢ ( ⊤ → ℝ ⊆ ℂ )
378	376 377	feqresmpt	⊢ ( ⊤ → ( sin ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ ( sin ‘ 𝑥 ) ) )
379	378	mptru	⊢ ( sin ↾ ℝ ) = ( 𝑥 ∈ ℝ ↦ ( sin ‘ 𝑥 ) )
380		resincncf	⊢ ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℝ )
381	379 380	eqeltrri	⊢ ( 𝑥 ∈ ℝ ↦ ( sin ‘ 𝑥 ) ) ∈ ( ℝ –cn→ ℝ )
382	381	a1i	⊢ ( 𝜒 → ( 𝑥 ∈ ℝ ↦ ( sin ‘ 𝑥 ) ) ∈ ( ℝ –cn→ ℝ ) )
383	104	rehalfcld	⊢ ( 𝜒 → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ∈ ℝ )
384		fveq2	⊢ ( 𝑥 = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) → ( sin ‘ 𝑥 ) = ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) )
385	382 383 384	cnmptlimc	⊢ ( 𝜒 → ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ∈ ( ( 𝑥 ∈ ℝ ↦ ( sin ‘ 𝑥 ) ) limℂ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) )
386		fveq2	⊢ ( 𝑥 = ( 𝑠 / 2 ) → ( sin ‘ 𝑥 ) = ( sin ‘ ( 𝑠 / 2 ) ) )
387		fveq2	⊢ ( ( 𝑠 / 2 ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) → ( sin ‘ ( 𝑠 / 2 ) ) = ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) )
388	387	ad2antll	⊢ ( ( 𝜒 ∧ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( 𝑠 / 2 ) = ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) → ( sin ‘ ( 𝑠 / 2 ) ) = ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) )
389	364 367 374 385 386 388	limcco	⊢ ( 𝜒 → ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( sin ‘ ( 𝑠 / 2 ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
390	360 361 347 153 160 363 389	mullimc	⊢ ( 𝜒 → ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
391	335	halfcld	⊢ ( 𝜒 → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ∈ ℂ )
392	391	sincld	⊢ ( 𝜒 → ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ∈ ℂ )
393	163 119	sseldd	⊢ ( 𝜒 → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( - π [,] π ) )
394		fourierdlem44	⊢ ( ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ( - π [,] π ) ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≠ 0 ) → ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ≠ 0 )
395	393 345 394	syl2anc	⊢ ( 𝜒 → ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ≠ 0 )
396	362 392 373 395	mulne0d	⊢ ( 𝜒 → ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ≠ 0 )
397	171 347 24 158 359 338 390 396 168	divlimc	⊢ ( 𝜒 → ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
398	23 24 25 152 169 346 397	mullimc	⊢ ( 𝜒 → ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
399	20	a1i	⊢ ( 𝜒 → 𝐷 = ( ( ( if ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) · ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ ( 𝑗 + 1 ) ) / 2 ) ) ) ) ) )
400	15	reseq1i	⊢ ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
401		ioossicc	⊢ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑆 ‘ 𝑗 ) [,] ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
402		iccss	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≤ ( 𝑆 ‘ 𝑗 ) ∧ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ 𝐵 ) ) → ( ( 𝑆 ‘ 𝑗 ) [,] ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
403	38 112 99 121 402	syl22anc	⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) [,] ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
404	401 403	sstrid	⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
405	404	resmptd	⊢ ( 𝜒 → ( ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
406	400 405	eqtrid	⊢ ( 𝜒 → ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) )
407	406	oveq1d	⊢ ( 𝜒 → ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) = ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
408	398 399 407	3eltr4d	⊢ ( 𝜒 → 𝐷 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
409	22 408	sylbir	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐷 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) )
410	248 255	gtned	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ≠ ( 𝑄 ‘ 𝑖 ) )
411	27 229 7	syl2anc	⊢ ( 𝜒 → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) )
412	246	oveq2d	⊢ ( 𝜒 → ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑉 ‘ 𝑖 ) ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) ) )
413	411 412	eleqtrd	⊢ ( 𝜒 → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) ) )
414	199	recnd	⊢ ( 𝜒 → ( 𝑄 ‘ 𝑖 ) ∈ ℂ )
415	281 236 283 284 269 286 410 413 414	fourierdlem53	⊢ ( 𝜒 → 𝑅 ∈ ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
416		eqid	⊢ if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ 𝑗 ) ) ) = if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ 𝑗 ) ) )
417		eqid	⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝑄 ‘ 𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝑄 ‘ 𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
418	199 217 227 280 415 294 104 301 302 416 417	fourierdlem32	⊢ ( 𝜒 → if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ 𝑗 ) ) ) ∈ ( ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
419		eqidd	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) )
420		oveq2	⊢ ( 𝑠 = ( 𝑆 ‘ 𝑗 ) → ( 𝑋 + 𝑠 ) = ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) )
421	420	fveq2d	⊢ ( 𝑠 = ( 𝑆 ‘ 𝑗 ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) )
422	421	adantl	⊢ ( ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) ∧ 𝑠 = ( 𝑆 ‘ 𝑗 ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) )
423	249	adantr	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
424	251	adantr	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
425	294	adantr	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ℝ )
426	199	adantr	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
427	314	adantr	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑆 ‘ 𝑗 ) )
428		neqne	⊢ ( ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) → ( 𝑆 ‘ 𝑗 ) ≠ ( 𝑄 ‘ 𝑖 ) )
429	428	adantl	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑗 ) ≠ ( 𝑄 ‘ 𝑖 ) )
430	426 425 427 429	leneltd	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑆 ‘ 𝑗 ) )
431	104	adantr	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
432	217	adantr	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
433	301	adantr	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑆 ‘ ( 𝑗 + 1 ) ) )
434	318	adantr	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑆 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
435	425 431 432 433 434	ltletrd	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑗 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
436	423 424 425 430 435	eliood	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝑆 ‘ 𝑗 ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
437	236 294	readdcld	⊢ ( 𝜒 → ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ∈ ℝ )
438	281 437	ffvelcdmd	⊢ ( 𝜒 → ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ )
439	438	adantr	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ∈ ℝ )
440	419 422 436 439	fvmptd	⊢ ( ( 𝜒 ∧ ¬ ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) ) → ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ 𝑗 ) ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) )
441	440	ifeq2da	⊢ ( 𝜒 → if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ‘ ( 𝑆 ‘ 𝑗 ) ) ) = if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) )
442	330	oveq1d	⊢ ( 𝜒 → ( ( ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) = ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
443	418 441 442	3eltr3d	⊢ ( 𝜒 → if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
444	294	recnd	⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ∈ ℂ )
445	177 334 135 444	constlimc	⊢ ( 𝜒 → 𝐶 ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝐶 ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
446	176 177 170 133 136 443 445	sublimc	⊢ ( 𝜒 → ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
447	334 171 444	idlimc	⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝑠 ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
448	27 97	jca	⊢ ( 𝜒 → ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) ) )
449		eleq1	⊢ ( 𝑠 = ( 𝑆 ‘ 𝑗 ) → ( 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) ) )
450	449	anbi2d	⊢ ( 𝑠 = ( 𝑆 ‘ 𝑗 ) → ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) ) ) )
451		neeq1	⊢ ( 𝑠 = ( 𝑆 ‘ 𝑗 ) → ( 𝑠 ≠ 0 ↔ ( 𝑆 ‘ 𝑗 ) ≠ 0 ) )
452	450 451	imbi12d	⊢ ( 𝑠 = ( 𝑆 ‘ 𝑗 ) → ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑠 ≠ 0 ) ↔ ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑆 ‘ 𝑗 ) ≠ 0 ) ) )
453	452 150	vtoclg	⊢ ( ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) → ( ( 𝜑 ∧ ( 𝑆 ‘ 𝑗 ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑆 ‘ 𝑗 ) ≠ 0 ) )
454	97 448 453	sylc	⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ≠ 0 )
455	170 171 23 137 175 446 447 454 151	divlimc	⊢ ( 𝜒 → ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
456	360 334 362 444	constlimc	⊢ ( 𝜒 → 2 ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 2 ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
457	352	ad2antrl	⊢ ( ( 𝜒 ∧ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( 𝑠 / 2 ) ≠ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) → ( 𝑠 / 2 ) ∈ ℝ )
458	171 360 368 158 372 447 456 373 162	divlimc	⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) / 2 ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / 2 ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
459	294	rehalfcld	⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) / 2 ) ∈ ℝ )
460		fveq2	⊢ ( 𝑥 = ( ( 𝑆 ‘ 𝑗 ) / 2 ) → ( sin ‘ 𝑥 ) = ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) )
461	382 459 460	cnmptlimc	⊢ ( 𝜒 → ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ∈ ( ( 𝑥 ∈ ℝ ↦ ( sin ‘ 𝑥 ) ) limℂ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) )
462		fveq2	⊢ ( ( 𝑠 / 2 ) = ( ( 𝑆 ‘ 𝑗 ) / 2 ) → ( sin ‘ ( 𝑠 / 2 ) ) = ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) )
463	462	ad2antll	⊢ ( ( 𝜒 ∧ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ ( 𝑠 / 2 ) = ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) → ( sin ‘ ( 𝑠 / 2 ) ) = ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) )
464	457 367 458 461 386 463	limcco	⊢ ( 𝜒 → ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( sin ‘ ( 𝑠 / 2 ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
465	360 361 347 153 160 456 464	mullimc	⊢ ( 𝜒 → ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
466	444	halfcld	⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) / 2 ) ∈ ℂ )
467	466	sincld	⊢ ( 𝜒 → ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ∈ ℂ )
468	163 97	sseldd	⊢ ( 𝜒 → ( 𝑆 ‘ 𝑗 ) ∈ ( - π [,] π ) )
469		fourierdlem44	⊢ ( ( ( 𝑆 ‘ 𝑗 ) ∈ ( - π [,] π ) ∧ ( 𝑆 ‘ 𝑗 ) ≠ 0 ) → ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ≠ 0 )
470	468 454 469	syl2anc	⊢ ( 𝜒 → ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ≠ 0 )
471	362 467 373 470	mulne0d	⊢ ( 𝜒 → ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ≠ 0 )
472	171 347 24 158 359 447 465 471 168	divlimc	⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
473	23 24 25 152 169 455 472	mullimc	⊢ ( 𝜒 → ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) ∈ ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
474	21	a1i	⊢ ( 𝜒 → 𝐸 = ( ( ( if ( ( 𝑆 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) , 𝑅 , ( 𝐹 ‘ ( 𝑋 + ( 𝑆 ‘ 𝑗 ) ) ) ) − 𝐶 ) / ( 𝑆 ‘ 𝑗 ) ) · ( ( 𝑆 ‘ 𝑗 ) / ( 2 · ( sin ‘ ( ( 𝑆 ‘ 𝑗 ) / 2 ) ) ) ) ) )
475	406	oveq1d	⊢ ( 𝜒 → ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) = ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
476	473 474 475	3eltr4d	⊢ ( 𝜒 → 𝐸 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
477	22 476	sylbir	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐸 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) )
478	302	sselda	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
479	478 272	syldan	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) = ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) )
480	479	mpteq2dva	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) = ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) )
481	231	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) ∈ ℝ* )
482	234	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑉 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
483	236	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑋 ∈ ℝ )
484	483 140	readdcld	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ℝ )
485	246	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) = ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) )
486	199	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
487	249	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
488	251	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
489	487 488 478 254	syl3anc	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) < 𝑠 )
490	486 37 483 489	ltadd2dd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑋 + ( 𝑄 ‘ 𝑖 ) ) < ( 𝑋 + 𝑠 ) )
491	485 490	eqbrtrd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑉 ‘ 𝑖 ) < ( 𝑋 + 𝑠 ) )
492	217	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
493	487 488 478 259	syl3anc	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → 𝑠 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
494	37 492 483 493	ltadd2dd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) < ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
495	266	adantr	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑋 + ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
496	494 495	breqtrd	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) < ( 𝑉 ‘ ( 𝑖 + 1 ) ) )
497	481 482 484 491 496	eliood	⊢ ( ( 𝜒 ∧ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) → ( 𝑋 + 𝑠 ) ∈ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) )
498	275 276 334 243 497	fourierdlem23	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( 𝐹 ↾ ( ( 𝑉 ‘ 𝑖 ) (,) ( 𝑉 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑋 + 𝑠 ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
499	480 498	eqeltrd	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
500		ssid	⊢ ℂ ⊆ ℂ
501	500	a1i	⊢ ( 𝜒 → ℂ ⊆ ℂ )
502	334 135 501	constcncfg	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝐶 ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
503	499 502	subcncf	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
504	175	ralrimiva	⊢ ( 𝜒 → ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) 𝑠 ∈ ( ℂ ∖ { 0 } ) )
505		dfss3	⊢ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ℂ ∖ { 0 } ) ↔ ∀ 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) 𝑠 ∈ ( ℂ ∖ { 0 } ) )
506	504 505	sylibr	⊢ ( 𝜒 → ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ℂ ∖ { 0 } ) )
507		difssd	⊢ ( 𝜒 → ( ℂ ∖ { 0 } ) ⊆ ℂ )
508	506 507	idcncfg	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝑠 ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ( ℂ ∖ { 0 } ) ) )
509	503 508	divcncf	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
510	334 501	idcncfg	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 𝑠 ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
511	359 347	fmptd	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) : ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⟶ ( ℂ ∖ { 0 } ) )
512	334 362 501	constcncfg	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 2 ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
513		sincn	⊢ sin ∈ ( ℂ –cn→ ℂ )
514	513	a1i	⊢ ( 𝜒 → sin ∈ ( ℂ –cn→ ℂ ) )
515	371	a1i	⊢ ( 𝜒 → 2 ∈ ( ℂ ∖ { 0 } ) )
516	334 515 507	constcncfg	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ 2 ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ( ℂ ∖ { 0 } ) ) )
517	510 516	divcncf	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / 2 ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
518	514 517	cncfmpt1f	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( sin ‘ ( 𝑠 / 2 ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
519	512 518	mulcncf	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
520		cncfcdm	⊢ ( ( ( ℂ ∖ { 0 } ) ⊆ ℂ ∧ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) ) → ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) : ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⟶ ( ℂ ∖ { 0 } ) ) )
521	507 519 520	syl2anc	⊢ ( 𝜒 → ( ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) : ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⟶ ( ℂ ∖ { 0 } ) ) )
522	511 521	mpbird	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ( ℂ ∖ { 0 } ) ) )
523	510 522	divcncf	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
524	509 523	mulcncf	⊢ ( 𝜒 → ( 𝑠 ∈ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ↦ ( ( ( ( 𝐹 ‘ ( 𝑋 + 𝑠 ) ) − 𝐶 ) / 𝑠 ) · ( 𝑠 / ( 2 · ( sin ‘ ( 𝑠 / 2 ) ) ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
525	406 524	eqeltrd	⊢ ( 𝜒 → ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
526	22 525	sylbir	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) )
527	409 477 526	jca31	⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐷 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ∧ 𝐸 ∈ ( ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) limℂ ( 𝑆 ‘ 𝑗 ) ) ) ∧ ( 𝑂 ↾ ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) ) ∈ ( ( ( 𝑆 ‘ 𝑗 ) (,) ( 𝑆 ‘ ( 𝑗 + 1 ) ) ) –cn→ ℂ ) ) )