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	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem76.xre	$⊢ φ \to X \in ℝ$
	fourierdlem76.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π + X \land p (m) = π + X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem76.m	$⊢ φ \to M \in ℕ$
	fourierdlem76.v	$⊢ φ \to V \in P (M)$
	fourierdlem76.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem76.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i))$
	fourierdlem76.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i + 1))$
	fourierdlem76.a	$⊢ φ \to A \in ℝ$
	fourierdlem76.b	$⊢ φ \to B \in ℝ$
	fourierdlem76.altb	$⊢ φ \to A < B$
	fourierdlem76.ab	$⊢ φ \to [A, B] \subseteq [- π, π]$
	fourierdlem76.n0	$⊢ φ \to \neg 0 \in [A, B]$
	fourierdlem76.c	$⊢ φ \to C \in ℝ$
	fourierdlem76.o	$⊢ O = (s \in [A, B] ⟼ (\frac{F (X + s) - C}{s}) (\frac{s}{2 \sin (\frac{s}{2})}))$
	fourierdlem76.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
	fourierdlem76.t	$⊢ T = \{A, B\} \cup (ran Q \cap (A, B))$
	fourierdlem76.n	$⊢ N = \|T\| - 1$
	fourierdlem76.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), T))$
	fourierdlem76.d	$⊢ D = (\frac{if (S (j + 1) = Q (i + 1), L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})})$
	fourierdlem76.e	$⊢ E = (\frac{if (S (j) = Q (i), R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})})$
	fourierdlem76.ch	$⊢ χ \leftrightarrow (((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \land (S (j), S (j + 1)) \subseteq (Q (i), Q (i + 1)))$
Assertion	fourierdlem76	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \land (S (j), S (j + 1)) \subseteq (Q (i), Q (i + 1))) \to ((D \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)) \land E \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))) \land ({O ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ)$

Proof

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

Metamath Proof Explorer

Theorem fourierdlem76

Proof