fourierdlem114

Description: Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem114.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem114.t	$⊢ T = 2 π$
	fourierdlem114.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fourierdlem114.g	$⊢ G = {F_{ℝ}^{'} ↾}_{(- π, π)}$
	fourierdlem114.dmdv	$⊢ φ \to (- π, π) ∖ dom G \in Fin$
	fourierdlem114.gcn	$⊢ φ \to G : dom G \underset{cn}{⟶} ℂ$
	fourierdlem114.rlim	$⊢ (φ \land x \in ([- π, π) ∖ dom G)) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
	fourierdlem114.llim	$⊢ (φ \land x \in ((- π, π] ∖ dom G)) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
	fourierdlem114.x	$⊢ φ \to X \in ℝ$
	fourierdlem114.l	$⊢ φ \to L \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
	fourierdlem114.r	$⊢ φ \to R \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
	fourierdlem114.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
	fourierdlem114.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
	fourierdlem114.s	$⊢ S = (n \in ℕ ⟼ A (n) \cos n X + B (n) \sin n X)$
	fourierdlem114.p	$⊢ P = (n \in ℕ ⟼ \{p \in (ℝ^{(0 \dots n)}) \| ((p (0) = - π \land p (n) = π) \land \forall i \in (0 ..^n) p (i) < p (i + 1))\})$
	fourierdlem114.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{π - x}{T}⌋ T)$
	fourierdlem114.h	$⊢ H = \{- π, π, E (X)\} \cup ([- π, π] ∖ dom G)$
	fourierdlem114.m	$⊢ M = \|H\| - 1$
	fourierdlem114.q	$⊢ Q = (ι g \| g {Isom}_{<, <} ((0 \dots M), H))$
Assertion	fourierdlem114	$⊢ φ \to (seq 1 (+ S) ⇝ ((\frac{L + R}{2}) - (\frac{A (0)}{2})) \land (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{L + R}{2})$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem114.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem114.t	$⊢ T = 2 π$
3		fourierdlem114.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
4		fourierdlem114.g	$⊢ G = {F_{ℝ}^{'} ↾}_{(- π, π)}$
5		fourierdlem114.dmdv	$⊢ φ \to (- π, π) ∖ dom G \in Fin$
6		fourierdlem114.gcn	$⊢ φ \to G : dom G \underset{cn}{⟶} ℂ$
7		fourierdlem114.rlim	$⊢ (φ \land x \in ([- π, π) ∖ dom G)) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
8		fourierdlem114.llim	$⊢ (φ \land x \in ((- π, π] ∖ dom G)) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
9		fourierdlem114.x	$⊢ φ \to X \in ℝ$
10		fourierdlem114.l	$⊢ φ \to L \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
11		fourierdlem114.r	$⊢ φ \to R \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
12		fourierdlem114.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
13		fourierdlem114.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
14		fourierdlem114.s	$⊢ S = (n \in ℕ ⟼ A (n) \cos n X + B (n) \sin n X)$
15		fourierdlem114.p	$⊢ P = (n \in ℕ ⟼ \{p \in (ℝ^{(0 \dots n)}) \| ((p (0) = - π \land p (n) = π) \land \forall i \in (0 ..^n) p (i) < p (i + 1))\})$
16		fourierdlem114.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{π - x}{T}⌋ T)$
17		fourierdlem114.h	$⊢ H = \{- π, π, E (X)\} \cup ([- π, π] ∖ dom G)$
18		fourierdlem114.m	$⊢ M = \|H\| - 1$
19		fourierdlem114.q	$⊢ Q = (ι g \| g {Isom}_{<, <} ((0 \dots M), H))$
20		2z	$⊢ 2 \in ℤ$
21	20	a1i	$⊢ φ \to 2 \in ℤ$
22		tpfi	$⊢ \{- π, π, E (X)\} \in Fin$
23	22	a1i	$⊢ φ \to \{- π, π, E (X)\} \in Fin$
24		pire	$⊢ π \in ℝ$
25	24	renegcli	$⊢ - π \in ℝ$
26	25	rexri	$⊢ - π \in ℝ^{*}$
27	24	rexri	$⊢ π \in ℝ^{*}$
28		negpilt0	$⊢ - π < 0$
29		pipos	$⊢ 0 < π$
30		0re	$⊢ 0 \in ℝ$
31	25 30 24	lttri	$⊢ (- π < 0 \land 0 < π) \to - π < π$
32	28 29 31	mp2an	$⊢ - π < π$
33	25 24 32	ltleii	$⊢ - π \leq π$
34		prunioo	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land - π \leq π) \to (- π, π) \cup \{- π, π\} = [- π, π]$
35	26 27 33 34	mp3an	$⊢ (- π, π) \cup \{- π, π\} = [- π, π]$
36	35	difeq1i	$⊢ ((- π, π) \cup \{- π, π\}) ∖ dom G = [- π, π] ∖ dom G$
37		difundir	$⊢ ((- π, π) \cup \{- π, π\}) ∖ dom G = ((- π, π) ∖ dom G) \cup (\{- π, π\} ∖ dom G)$
38	36 37	eqtr3i	$⊢ [- π, π] ∖ dom G = ((- π, π) ∖ dom G) \cup (\{- π, π\} ∖ dom G)$
39		prfi	$⊢ \{- π, π\} \in Fin$
40		diffi	$⊢ \{- π, π\} \in Fin \to \{- π, π\} ∖ dom G \in Fin$
41	39 40	mp1i	$⊢ φ \to \{- π, π\} ∖ dom G \in Fin$
42		unfi	$⊢ ((- π, π) ∖ dom G \in Fin \land \{- π, π\} ∖ dom G \in Fin) \to ((- π, π) ∖ dom G) \cup (\{- π, π\} ∖ dom G) \in Fin$
43	5 41 42	syl2anc	$⊢ φ \to ((- π, π) ∖ dom G) \cup (\{- π, π\} ∖ dom G) \in Fin$
44	38 43	eqeltrid	$⊢ φ \to [- π, π] ∖ dom G \in Fin$
45		unfi	$⊢ (\{- π, π, E (X)\} \in Fin \land [- π, π] ∖ dom G \in Fin) \to \{- π, π, E (X)\} \cup ([- π, π] ∖ dom G) \in Fin$
46	23 44 45	syl2anc	$⊢ φ \to \{- π, π, E (X)\} \cup ([- π, π] ∖ dom G) \in Fin$
47	17 46	eqeltrid	$⊢ φ \to H \in Fin$
48		hashcl	$⊢ H \in Fin \to \|H\| \in ℕ_{0}$
49	47 48	syl	$⊢ φ \to \|H\| \in ℕ_{0}$
50	49	nn0zd	$⊢ φ \to \|H\| \in ℤ$
51	25 32	ltneii	$⊢ - π \neq π$
52		hashprg	$⊢ (- π \in ℝ \land π \in ℝ) \to (- π \neq π \leftrightarrow \|\{- π, π\}\| = 2)$
53	25 24 52	mp2an	$⊢ - π \neq π \leftrightarrow \|\{- π, π\}\| = 2$
54	51 53	mpbi	$⊢ \|\{- π, π\}\| = 2$
55	22	elexi	$⊢ \{- π, π, E (X)\} \in V$
56		ovex	$⊢ [- π, π] \in V$
57		difexg	$⊢ [- π, π] \in V \to [- π, π] ∖ dom G \in V$
58	56 57	ax-mp	$⊢ [- π, π] ∖ dom G \in V$
59	55 58	unex	$⊢ \{- π, π, E (X)\} \cup ([- π, π] ∖ dom G) \in V$
60	17 59	eqeltri	$⊢ H \in V$
61		negex	$⊢ - π \in V$
62	61	tpid1	$⊢ - π \in \{- π, π, E (X)\}$
63	24	elexi	$⊢ π \in V$
64	63	tpid2	$⊢ π \in \{- π, π, E (X)\}$
65		prssi	$⊢ (- π \in \{- π, π, E (X)\} \land π \in \{- π, π, E (X)\}) \to \{- π, π\} \subseteq \{- π, π, E (X)\}$
66	62 64 65	mp2an	$⊢ \{- π, π\} \subseteq \{- π, π, E (X)\}$
67		ssun1	$⊢ \{- π, π, E (X)\} \subseteq \{- π, π, E (X)\} \cup ([- π, π] ∖ dom G)$
68	67 17	sseqtrri	$⊢ \{- π, π, E (X)\} \subseteq H$
69	66 68	sstri	$⊢ \{- π, π\} \subseteq H$
70		hashss	$⊢ (H \in V \land \{- π, π\} \subseteq H) \to \|\{- π, π\}\| \leq \|H\|$
71	60 69 70	mp2an	$⊢ \|\{- π, π\}\| \leq \|H\|$
72	71	a1i	$⊢ φ \to \|\{- π, π\}\| \leq \|H\|$
73	54 72	eqbrtrrid	$⊢ φ \to 2 \leq \|H\|$
74		eluz2	$⊢ \|H\| \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land \|H\| \in ℤ \land 2 \leq \|H\|)$
75	21 50 73 74	syl3anbrc	$⊢ φ \to \|H\| \in ℤ_{\geq 2}$
76		uz2m1nn	$⊢ \|H\| \in ℤ_{\geq 2} \to \|H\| - 1 \in ℕ$
77	75 76	syl	$⊢ φ \to \|H\| - 1 \in ℕ$
78	18 77	eqeltrid	$⊢ φ \to M \in ℕ$
79	25	a1i	$⊢ φ \to - π \in ℝ$
80	24	a1i	$⊢ φ \to π \in ℝ$
81		negpitopissre	$⊢ (- π, π] \subseteq ℝ$
82	32	a1i	$⊢ φ \to - π < π$
83		picn	$⊢ π \in ℂ$
84	83	2timesi	$⊢ 2 π = π + π$
85	83 83	subnegi	$⊢ π - (- π) = π + π$
86	84 2 85	3eqtr4i	$⊢ T = π - (- π)$
87	79 80 82 86 16	fourierdlem4	$⊢ φ \to E : ℝ ⟶ (- π, π]$
88	87 9	ffvelrnd	$⊢ φ \to E (X) \in (- π, π]$
89	81 88	sseldi	$⊢ φ \to E (X) \in ℝ$
90	79 80 89	3jca	$⊢ φ \to (- π \in ℝ \land π \in ℝ \land E (X) \in ℝ)$
91		fvex	$⊢ E (X) \in V$
92	61 63 91	tpss	$⊢ (- π \in ℝ \land π \in ℝ \land E (X) \in ℝ) \leftrightarrow \{- π, π, E (X)\} \subseteq ℝ$
93	90 92	sylib	$⊢ φ \to \{- π, π, E (X)\} \subseteq ℝ$
94		iccssre	$⊢ (- π \in ℝ \land π \in ℝ) \to [- π, π] \subseteq ℝ$
95	25 24 94	mp2an	$⊢ [- π, π] \subseteq ℝ$
96		ssdifss	$⊢ [- π, π] \subseteq ℝ \to [- π, π] ∖ dom G \subseteq ℝ$
97	95 96	mp1i	$⊢ φ \to [- π, π] ∖ dom G \subseteq ℝ$
98	93 97	unssd	$⊢ φ \to \{- π, π, E (X)\} \cup ([- π, π] ∖ dom G) \subseteq ℝ$
99	17 98	eqsstrid	$⊢ φ \to H \subseteq ℝ$
100	47 99 19 18	fourierdlem36	$⊢ φ \to Q {Isom}_{<, <} ((0 \dots M), H)$
101		isof1o	$⊢ Q {Isom}_{<, <} ((0 \dots M), H) \to Q : (0 \dots M) \underset{1-1 onto}{⟶} H$
102		f1of	$⊢ Q : (0 \dots M) \underset{1-1 onto}{⟶} H \to Q : (0 \dots M) ⟶ H$
103	100 101 102	3syl	$⊢ φ \to Q : (0 \dots M) ⟶ H$
104	103 99	fssd	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
105		reex	$⊢ ℝ \in V$
106		ovex	$⊢ (0 \dots M) \in V$
107	105 106	elmap	$⊢ Q \in (ℝ^{(0 \dots M)}) \leftrightarrow Q : (0 \dots M) ⟶ ℝ$
108	104 107	sylibr	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
109		fveq2	$⊢ 0 = i \to Q (0) = Q (i)$
110	109	adantl	$⊢ ((φ \land i \in (0 \dots M)) \land 0 = i) \to Q (0) = Q (i)$
111	104	ffvelrnda	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \in ℝ$
112	111	leidd	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \leq Q (i)$
113	112	adantr	$⊢ ((φ \land i \in (0 \dots M)) \land 0 = i) \to Q (i) \leq Q (i)$
114	110 113	eqbrtrd	$⊢ ((φ \land i \in (0 \dots M)) \land 0 = i) \to Q (0) \leq Q (i)$
115		elfzelz	$⊢ i \in (0 \dots M) \to i \in ℤ$
116	115	zred	$⊢ i \in (0 \dots M) \to i \in ℝ$
117	116	ad2antlr	$⊢ ((φ \land i \in (0 \dots M)) \land \neg 0 = i) \to i \in ℝ$
118		elfzle1	$⊢ i \in (0 \dots M) \to 0 \leq i$
119	118	ad2antlr	$⊢ ((φ \land i \in (0 \dots M)) \land \neg 0 = i) \to 0 \leq i$
120		neqne	$⊢ \neg 0 = i \to 0 \neq i$
121	120	necomd	$⊢ \neg 0 = i \to i \neq 0$
122	121	adantl	$⊢ ((φ \land i \in (0 \dots M)) \land \neg 0 = i) \to i \neq 0$
123	117 119 122	ne0gt0d	$⊢ ((φ \land i \in (0 \dots M)) \land \neg 0 = i) \to 0 < i$
124		nnssnn0	$⊢ ℕ \subseteq ℕ_{0}$
125		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
126	124 125	sseqtri	$⊢ ℕ \subseteq ℤ_{\geq 0}$
127	126 78	sseldi	$⊢ φ \to M \in ℤ_{\geq 0}$
128		eluzfz1	$⊢ M \in ℤ_{\geq 0} \to 0 \in (0 \dots M)$
129	127 128	syl	$⊢ φ \to 0 \in (0 \dots M)$
130	103 129	ffvelrnd	$⊢ φ \to Q (0) \in H$
131	99 130	sseldd	$⊢ φ \to Q (0) \in ℝ$
132	131	ad2antrr	$⊢ ((φ \land i \in (0 \dots M)) \land 0 < i) \to Q (0) \in ℝ$
133	111	adantr	$⊢ ((φ \land i \in (0 \dots M)) \land 0 < i) \to Q (i) \in ℝ$
134		simpr	$⊢ ((φ \land i \in (0 \dots M)) \land 0 < i) \to 0 < i$
135	100	ad2antrr	$⊢ ((φ \land i \in (0 \dots M)) \land 0 < i) \to Q {Isom}_{<, <} ((0 \dots M), H)$
136	129	anim1i	$⊢ (φ \land i \in (0 \dots M)) \to (0 \in (0 \dots M) \land i \in (0 \dots M))$
137	136	adantr	$⊢ ((φ \land i \in (0 \dots M)) \land 0 < i) \to (0 \in (0 \dots M) \land i \in (0 \dots M))$
138		isorel	$⊢ (Q {Isom}_{<, <} ((0 \dots M), H) \land (0 \in (0 \dots M) \land i \in (0 \dots M))) \to (0 < i \leftrightarrow Q (0) < Q (i))$
139	135 137 138	syl2anc	$⊢ ((φ \land i \in (0 \dots M)) \land 0 < i) \to (0 < i \leftrightarrow Q (0) < Q (i))$
140	134 139	mpbid	$⊢ ((φ \land i \in (0 \dots M)) \land 0 < i) \to Q (0) < Q (i)$
141	132 133 140	ltled	$⊢ ((φ \land i \in (0 \dots M)) \land 0 < i) \to Q (0) \leq Q (i)$
142	123 141	syldan	$⊢ ((φ \land i \in (0 \dots M)) \land \neg 0 = i) \to Q (0) \leq Q (i)$
143	114 142	pm2.61dan	$⊢ (φ \land i \in (0 \dots M)) \to Q (0) \leq Q (i)$
144	143	adantr	$⊢ ((φ \land i \in (0 \dots M)) \land Q (i) = - π) \to Q (0) \leq Q (i)$
145		simpr	$⊢ ((φ \land i \in (0 \dots M)) \land Q (i) = - π) \to Q (i) = - π$
146	144 145	breqtrd	$⊢ ((φ \land i \in (0 \dots M)) \land Q (i) = - π) \to Q (0) \leq - π$
147	79	rexrd	$⊢ φ \to - π \in ℝ^{*}$
148	80	rexrd	$⊢ φ \to π \in ℝ^{*}$
149		lbicc2	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land - π \leq π) \to - π \in [- π, π]$
150	26 27 33 149	mp3an	$⊢ - π \in [- π, π]$
151	150	a1i	$⊢ φ \to - π \in [- π, π]$
152		ubicc2	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land - π \leq π) \to π \in [- π, π]$
153	26 27 33 152	mp3an	$⊢ π \in [- π, π]$
154	153	a1i	$⊢ φ \to π \in [- π, π]$
155		iocssicc	$⊢ (- π, π] \subseteq [- π, π]$
156	155 88	sseldi	$⊢ φ \to E (X) \in [- π, π]$
157		tpssi	$⊢ (- π \in [- π, π] \land π \in [- π, π] \land E (X) \in [- π, π]) \to \{- π, π, E (X)\} \subseteq [- π, π]$
158	151 154 156 157	syl3anc	$⊢ φ \to \{- π, π, E (X)\} \subseteq [- π, π]$
159		difssd	$⊢ φ \to [- π, π] ∖ dom G \subseteq [- π, π]$
160	158 159	unssd	$⊢ φ \to \{- π, π, E (X)\} \cup ([- π, π] ∖ dom G) \subseteq [- π, π]$
161	17 160	eqsstrid	$⊢ φ \to H \subseteq [- π, π]$
162	161 130	sseldd	$⊢ φ \to Q (0) \in [- π, π]$
163		iccgelb	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land Q (0) \in [- π, π]) \to - π \leq Q (0)$
164	147 148 162 163	syl3anc	$⊢ φ \to - π \leq Q (0)$
165	164	ad2antrr	$⊢ ((φ \land i \in (0 \dots M)) \land Q (i) = - π) \to - π \leq Q (0)$
166	131	ad2antrr	$⊢ ((φ \land i \in (0 \dots M)) \land Q (i) = - π) \to Q (0) \in ℝ$
167	25	a1i	$⊢ ((φ \land i \in (0 \dots M)) \land Q (i) = - π) \to - π \in ℝ$
168	166 167	letri3d	$⊢ ((φ \land i \in (0 \dots M)) \land Q (i) = - π) \to (Q (0) = - π \leftrightarrow (Q (0) \leq - π \land - π \leq Q (0)))$
169	146 165 168	mpbir2and	$⊢ ((φ \land i \in (0 \dots M)) \land Q (i) = - π) \to Q (0) = - π$
170	68 62	sselii	$⊢ - π \in H$
171		f1ofo	$⊢ Q : (0 \dots M) \underset{1-1 onto}{⟶} H \to Q : (0 \dots M) \underset{onto}{⟶} H$
172	101 171	syl	$⊢ Q {Isom}_{<, <} ((0 \dots M), H) \to Q : (0 \dots M) \underset{onto}{⟶} H$
173		forn	$⊢ Q : (0 \dots M) \underset{onto}{⟶} H \to ran Q = H$
174	100 172 173	3syl	$⊢ φ \to ran Q = H$
175	170 174	eleqtrrid	$⊢ φ \to - π \in ran Q$
176		ffn	$⊢ Q : (0 \dots M) ⟶ H \to Q Fn (0 \dots M)$
177		fvelrnb	$⊢ Q Fn (0 \dots M) \to (- π \in ran Q \leftrightarrow \exists i \in (0 \dots M) Q (i) = - π)$
178	103 176 177	3syl	$⊢ φ \to (- π \in ran Q \leftrightarrow \exists i \in (0 \dots M) Q (i) = - π)$
179	175 178	mpbid	$⊢ φ \to \exists i \in (0 \dots M) Q (i) = - π$
180	169 179	r19.29a	$⊢ φ \to Q (0) = - π$
181	68 64	sselii	$⊢ π \in H$
182	181 174	eleqtrrid	$⊢ φ \to π \in ran Q$
183		fvelrnb	$⊢ Q Fn (0 \dots M) \to (π \in ran Q \leftrightarrow \exists i \in (0 \dots M) Q (i) = π)$
184	103 176 183	3syl	$⊢ φ \to (π \in ran Q \leftrightarrow \exists i \in (0 \dots M) Q (i) = π)$
185	182 184	mpbid	$⊢ φ \to \exists i \in (0 \dots M) Q (i) = π$
186	103 161	fssd	$⊢ φ \to Q : (0 \dots M) ⟶ [- π, π]$
187		eluzfz2	$⊢ M \in ℤ_{\geq 0} \to M \in (0 \dots M)$
188	127 187	syl	$⊢ φ \to M \in (0 \dots M)$
189	186 188	ffvelrnd	$⊢ φ \to Q (M) \in [- π, π]$
190		iccleub	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land Q (M) \in [- π, π]) \to Q (M) \leq π$
191	147 148 189 190	syl3anc	$⊢ φ \to Q (M) \leq π$
192	191	3ad2ant1	$⊢ (φ \land i \in (0 \dots M) \land Q (i) = π) \to Q (M) \leq π$
193		id	$⊢ Q (i) = π \to Q (i) = π$
194	193	eqcomd	$⊢ Q (i) = π \to π = Q (i)$
195	194	3ad2ant3	$⊢ (φ \land i \in (0 \dots M) \land Q (i) = π) \to π = Q (i)$
196	112	adantr	$⊢ ((φ \land i \in (0 \dots M)) \land i = M) \to Q (i) \leq Q (i)$
197		fveq2	$⊢ i = M \to Q (i) = Q (M)$
198	197	adantl	$⊢ ((φ \land i \in (0 \dots M)) \land i = M) \to Q (i) = Q (M)$
199	196 198	breqtrd	$⊢ ((φ \land i \in (0 \dots M)) \land i = M) \to Q (i) \leq Q (M)$
200	116	ad2antlr	$⊢ ((φ \land i \in (0 \dots M)) \land \neg i = M) \to i \in ℝ$
201		elfzel2	$⊢ i \in (0 \dots M) \to M \in ℤ$
202	201	zred	$⊢ i \in (0 \dots M) \to M \in ℝ$
203	202	ad2antlr	$⊢ ((φ \land i \in (0 \dots M)) \land \neg i = M) \to M \in ℝ$
204		elfzle2	$⊢ i \in (0 \dots M) \to i \leq M$
205	204	ad2antlr	$⊢ ((φ \land i \in (0 \dots M)) \land \neg i = M) \to i \leq M$
206		neqne	$⊢ \neg i = M \to i \neq M$
207	206	necomd	$⊢ \neg i = M \to M \neq i$
208	207	adantl	$⊢ ((φ \land i \in (0 \dots M)) \land \neg i = M) \to M \neq i$
209	200 203 205 208	leneltd	$⊢ ((φ \land i \in (0 \dots M)) \land \neg i = M) \to i < M$
210	111	adantr	$⊢ ((φ \land i \in (0 \dots M)) \land i < M) \to Q (i) \in ℝ$
211	95 189	sseldi	$⊢ φ \to Q (M) \in ℝ$
212	211	ad2antrr	$⊢ ((φ \land i \in (0 \dots M)) \land i < M) \to Q (M) \in ℝ$
213		simpr	$⊢ ((φ \land i \in (0 \dots M)) \land i < M) \to i < M$
214	100	ad2antrr	$⊢ ((φ \land i \in (0 \dots M)) \land i < M) \to Q {Isom}_{<, <} ((0 \dots M), H)$
215		simpr	$⊢ (φ \land i \in (0 \dots M)) \to i \in (0 \dots M)$
216	188	adantr	$⊢ (φ \land i \in (0 \dots M)) \to M \in (0 \dots M)$
217	215 216	jca	$⊢ (φ \land i \in (0 \dots M)) \to (i \in (0 \dots M) \land M \in (0 \dots M))$
218	217	adantr	$⊢ ((φ \land i \in (0 \dots M)) \land i < M) \to (i \in (0 \dots M) \land M \in (0 \dots M))$
219		isorel	$⊢ (Q {Isom}_{<, <} ((0 \dots M), H) \land (i \in (0 \dots M) \land M \in (0 \dots M))) \to (i < M \leftrightarrow Q (i) < Q (M))$
220	214 218 219	syl2anc	$⊢ ((φ \land i \in (0 \dots M)) \land i < M) \to (i < M \leftrightarrow Q (i) < Q (M))$
221	213 220	mpbid	$⊢ ((φ \land i \in (0 \dots M)) \land i < M) \to Q (i) < Q (M)$
222	210 212 221	ltled	$⊢ ((φ \land i \in (0 \dots M)) \land i < M) \to Q (i) \leq Q (M)$
223	209 222	syldan	$⊢ ((φ \land i \in (0 \dots M)) \land \neg i = M) \to Q (i) \leq Q (M)$
224	199 223	pm2.61dan	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \leq Q (M)$
225	224	3adant3	$⊢ (φ \land i \in (0 \dots M) \land Q (i) = π) \to Q (i) \leq Q (M)$
226	195 225	eqbrtrd	$⊢ (φ \land i \in (0 \dots M) \land Q (i) = π) \to π \leq Q (M)$
227	211	3ad2ant1	$⊢ (φ \land i \in (0 \dots M) \land Q (i) = π) \to Q (M) \in ℝ$
228	24	a1i	$⊢ (φ \land i \in (0 \dots M) \land Q (i) = π) \to π \in ℝ$
229	227 228	letri3d	$⊢ (φ \land i \in (0 \dots M) \land Q (i) = π) \to (Q (M) = π \leftrightarrow (Q (M) \leq π \land π \leq Q (M)))$
230	192 226 229	mpbir2and	$⊢ (φ \land i \in (0 \dots M) \land Q (i) = π) \to Q (M) = π$
231	230	rexlimdv3a	$⊢ φ \to (\exists i \in (0 \dots M) Q (i) = π \to Q (M) = π)$
232	185 231	mpd	$⊢ φ \to Q (M) = π$
233		elfzoelz	$⊢ i \in (0 ..^M) \to i \in ℤ$
234	233	zred	$⊢ i \in (0 ..^M) \to i \in ℝ$
235	234	ltp1d	$⊢ i \in (0 ..^M) \to i < i + 1$
236	235	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i < i + 1$
237		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
238		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
239	237 238	jca	$⊢ i \in (0 ..^M) \to (i \in (0 \dots M) \land i + 1 \in (0 \dots M))$
240		isorel	$⊢ (Q {Isom}_{<, <} ((0 \dots M), H) \land (i \in (0 \dots M) \land i + 1 \in (0 \dots M))) \to (i < i + 1 \leftrightarrow Q (i) < Q (i + 1))$
241	100 239 240	syl2an	$⊢ (φ \land i \in (0 ..^M)) \to (i < i + 1 \leftrightarrow Q (i) < Q (i + 1))$
242	236 241	mpbid	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
243	242	ralrimiva	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
244	180 232 243	jca31	$⊢ φ \to ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))$
245	15	fourierdlem2	$⊢ M \in ℕ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
246	78 245	syl	$⊢ φ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
247	108 244 246	mpbir2and	$⊢ φ \to Q \in P (M)$
248	4	reseq1i	$⊢ {G ↾}_{(Q (i), Q (i + 1))} = {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(Q (i), Q (i + 1))}$
249	26	a1i	$⊢ (φ \land i \in (0 ..^M)) \to - π \in ℝ^{*}$
250	27	a1i	$⊢ (φ \land i \in (0 ..^M)) \to π \in ℝ^{*}$
251	186	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ [- π, π]$
252		simpr	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 ..^M)$
253	249 250 251 252	fourierdlem27	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq (- π, π)$
254	253	resabs1d	$⊢ (φ \land i \in (0 ..^M)) \to {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(Q (i), Q (i + 1))} = {F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}$
255	248 254	eqtr2id	$⊢ (φ \land i \in (0 ..^M)) \to {F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))} = {G ↾}_{(Q (i), Q (i + 1))}$
256	6 15 78 247 17 174	fourierdlem38	$⊢ (φ \land i \in (0 ..^M)) \to ({G ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
257	255 256	eqeltrd	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
258	255	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = ({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i)$
259	6	adantr	$⊢ (φ \land i \in (0 ..^M)) \to G : dom G \underset{cn}{⟶} ℂ$
260	7	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in ([- π, π) ∖ dom G)) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
261	8	adantlr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in ((- π, π] ∖ dom G)) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
262	100	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q {Isom}_{<, <} ((0 \dots M), H)$
263	262 101 102	3syl	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ H$
264	89	adantr	$⊢ (φ \land i \in (0 ..^M)) \to E (X) \in ℝ$
265	262 172 173	3syl	$⊢ (φ \land i \in (0 ..^M)) \to ran Q = H$
266	259 260 261 262 263 252 242 253 264 17 265	fourierdlem46	$⊢ (φ \land i \in (0 ..^M)) \to (({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) \neq \emptyset \land ({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) \neq \emptyset)$
267	266	simpld	$⊢ (φ \land i \in (0 ..^M)) \to ({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) \neq \emptyset$
268	258 267	eqnetrd	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) \neq \emptyset$
269	255	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) = ({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1)$
270	266	simprd	$⊢ (φ \land i \in (0 ..^M)) \to ({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) \neq \emptyset$
271	269 270	eqnetrd	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) \neq \emptyset$
272	91	tpid3	$⊢ E (X) \in \{- π, π, E (X)\}$
273		elun1	$⊢ E (X) \in \{- π, π, E (X)\} \to E (X) \in (\{- π, π, E (X)\} \cup ([- π, π] ∖ dom G))$
274	272 273	mp1i	$⊢ φ \to E (X) \in (\{- π, π, E (X)\} \cup ([- π, π] ∖ dom G))$
275	274 17	eleqtrrdi	$⊢ φ \to E (X) \in H$
276	275 174	eleqtrrd	$⊢ φ \to E (X) \in ran Q$
277	1 2 3 9 10 11 15 78 247 257 268 271 12 13 14 16 276	fourierdlem113	$⊢ φ \to (seq 1 (+ S) ⇝ ((\frac{L + R}{2}) - (\frac{A (0)}{2})) \land (\frac{A (0)}{2}) + \sum_{n \in ℕ} (A (n) \cos n X + B (n) \sin n X) = \frac{L + R}{2})$

Metamath Proof Explorer

Theorem fourierdlem114

Proof