fourierdlem102

Description: For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem102.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem102.t	$⊢ T = 2 π$
	fourierdlem102.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fourierdlem102.g	$⊢ G = {F_{ℝ}^{'} ↾}_{(- π, π)}$
	fourierdlem102.dmdv	$⊢ φ \to (- π, π) ∖ dom G \in Fin$
	fourierdlem102.gcn	$⊢ φ \to G : dom G \underset{cn}{⟶} ℂ$
	fourierdlem102.rlim	$⊢ (φ \land x \in ([- π, π) ∖ dom G)) \to ({G ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
	fourierdlem102.llim	$⊢ (φ \land x \in ((- π, π] ∖ dom G)) \to ({G ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
	fourierdlem102.x	$⊢ φ \to X \in ℝ$
	fourierdlem102.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))\})$
	fourierdlem102.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{π - x}{T}⌋ T)$
	fourierdlem102.h	$⊢ H = \{- π, π, E (X)\} \cup ([- π, π] ∖ dom G)$
	fourierdlem102.m	$⊢ M = \|H\| - 1$
	fourierdlem102.q	$⊢ Q = (ι g \| g {Isom}_{<, <} ((0 \dots M), H))$
Assertion	fourierdlem102	$⊢ φ \to (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X \neq \emptyset \land ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset)$

Proof

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

Metamath Proof Explorer

Theorem fourierdlem102

Proof