fourierdlem113

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

	Ref	Expression
Hypotheses	fourierdlem113.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem113.t	$⊢ T = 2 π$
	fourierdlem113.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fourierdlem113.x	$⊢ φ \to X \in ℝ$
	fourierdlem113.l	$⊢ φ \to L \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
	fourierdlem113.r	$⊢ φ \to R \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
	fourierdlem113.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))\})$
	fourierdlem113.m	$⊢ φ \to M \in ℕ$
	fourierdlem113.q	$⊢ φ \to Q \in P (M)$
	fourierdlem113.dvcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem113.dvlb	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) \neq \emptyset$
	fourierdlem113.dvub	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) \neq \emptyset$
	fourierdlem113.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
	fourierdlem113.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
	fourierdlem113.15	$⊢ S = (n \in ℕ ⟼ A (n) \cos n X + B (n) \sin n X)$
	fourierdlem113.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{π - x}{T}⌋ T)$
	fourierdlem113.exq	$⊢ φ \to E (X) \in ran Q$
Assertion	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})$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem113.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem113.t	$⊢ T = 2 π$
3		fourierdlem113.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
4		fourierdlem113.x	$⊢ φ \to X \in ℝ$
5		fourierdlem113.l	$⊢ φ \to L \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
6		fourierdlem113.r	$⊢ φ \to R \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
7		fourierdlem113.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))\})$
8		fourierdlem113.m	$⊢ φ \to M \in ℕ$
9		fourierdlem113.q	$⊢ φ \to Q \in P (M)$
10		fourierdlem113.dvcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
11		fourierdlem113.dvlb	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) \neq \emptyset$
12		fourierdlem113.dvub	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) \neq \emptyset$
13		fourierdlem113.a	$⊢ A = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
14		fourierdlem113.b	$⊢ B = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
15		fourierdlem113.15	$⊢ S = (n \in ℕ ⟼ A (n) \cos n X + B (n) \sin n X)$
16		fourierdlem113.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{π - x}{T}⌋ T)$
17		fourierdlem113.exq	$⊢ φ \to E (X) \in ran Q$
18		oveq1	$⊢ w = y \to w \mod 2 π = y \mod 2 π$
19	18	eqeq1d	$⊢ w = y \to (w \mod 2 π = 0 \leftrightarrow y \mod 2 π = 0)$
20		oveq2	$⊢ w = y \to (k + (\frac{1}{2})) w = (k + (\frac{1}{2})) y$
21	20	fveq2d	$⊢ w = y \to \sin (k + (\frac{1}{2})) w = \sin (k + (\frac{1}{2})) y$
22		fvoveq1	$⊢ w = y \to \sin (\frac{w}{2}) = \sin (\frac{y}{2})$
23	22	oveq2d	$⊢ w = y \to 2 π \sin (\frac{w}{2}) = 2 π \sin (\frac{y}{2})$
24	21 23	oveq12d	$⊢ w = y \to \frac{\sin (k + (\frac{1}{2})) w}{2 π \sin (\frac{w}{2})} = \frac{\sin (k + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})}$
25	19 24	ifbieq2d	$⊢ w = y \to if (w \mod 2 π = 0, \frac{2 k + 1}{2 π}, \frac{\sin (k + (\frac{1}{2})) w}{2 π \sin (\frac{w}{2})}) = if (y \mod 2 π = 0, \frac{2 k + 1}{2 π}, \frac{\sin (k + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})$
26	25	cbvmptv	$⊢ (w \in ℝ ⟼ if (w \mod 2 π = 0, \frac{2 k + 1}{2 π}, \frac{\sin (k + (\frac{1}{2})) w}{2 π \sin (\frac{w}{2})})) = (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 k + 1}{2 π}, \frac{\sin (k + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})}))$
27		oveq2	$⊢ k = m \to 2 k = 2 m$
28	27	oveq1d	$⊢ k = m \to 2 k + 1 = 2 m + 1$
29	28	oveq1d	$⊢ k = m \to \frac{2 k + 1}{2 π} = \frac{2 m + 1}{2 π}$
30		oveq1	$⊢ k = m \to k + (\frac{1}{2}) = m + (\frac{1}{2})$
31	30	fvoveq1d	$⊢ k = m \to \sin (k + (\frac{1}{2})) y = \sin (m + (\frac{1}{2})) y$
32	31	oveq1d	$⊢ k = m \to \frac{\sin (k + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})} = \frac{\sin (m + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})}$
33	29 32	ifeq12d	$⊢ k = m \to if (y \mod 2 π = 0, \frac{2 k + 1}{2 π}, \frac{\sin (k + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})}) = if (y \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})$
34	33	mpteq2dv	$⊢ k = m \to (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 k + 1}{2 π}, \frac{\sin (k + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})) = (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})}))$
35	26 34	eqtrid	$⊢ k = m \to (w \in ℝ ⟼ if (w \mod 2 π = 0, \frac{2 k + 1}{2 π}, \frac{\sin (k + (\frac{1}{2})) w}{2 π \sin (\frac{w}{2})})) = (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})}))$
36	35	cbvmptv	$⊢ (k \in ℕ ⟼ (w \in ℝ ⟼ if (w \mod 2 π = 0, \frac{2 k + 1}{2 π}, \frac{\sin (k + (\frac{1}{2})) w}{2 π \sin (\frac{w}{2})}))) = (m \in ℕ ⟼ (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 m + 1}{2 π}, \frac{\sin (m + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})))$
37		oveq1	$⊢ w = y \to w + j T = y + j T$
38	37	eleq1d	$⊢ w = y \to (w + j T \in ran Q \leftrightarrow y + j T \in ran Q)$
39	38	rexbidv	$⊢ w = y \to (\exists j \in ℤ w + j T \in ran Q \leftrightarrow \exists j \in ℤ y + j T \in ran Q)$
40	39	cbvrabv	$⊢ \{w \in [- π + X, π + X] \| \exists j \in ℤ w + j T \in ran Q\} = \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\}$
41	40	uneq2i	$⊢ \{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists j \in ℤ w + j T \in ran Q\} = \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\}$
42	41	fveq2i	$⊢ \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists j \in ℤ w + j T \in ran Q\}\| = \|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\}\|$
43	42	oveq1i	$⊢ \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists j \in ℤ w + j T \in ran Q\}\| - 1 = \|\{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\}\| - 1$
44		oveq1	$⊢ k = j \to k T = j T$
45	44	oveq2d	$⊢ k = j \to y + k T = y + j T$
46	45	eleq1d	$⊢ k = j \to (y + k T \in ran Q \leftrightarrow y + j T \in ran Q)$
47	46	cbvrexvw	$⊢ \exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists j \in ℤ y + j T \in ran Q$
48	47	rabbii	$⊢ \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\} = \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\}$
49	48	uneq2i	$⊢ \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\} = \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\}$
50		isoeq5	$⊢ \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\} = \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\} \to (g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}) \leftrightarrow g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\}))$
51	49 50	ax-mp	$⊢ g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}) \leftrightarrow g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\})$
52	51	a1i	$⊢ g = f \to (g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}) \leftrightarrow g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\}))$
53	44	oveq2d	$⊢ k = j \to w + k T = w + j T$
54	53	eleq1d	$⊢ k = j \to (w + k T \in ran Q \leftrightarrow w + j T \in ran Q)$
55	54	cbvrexvw	$⊢ \exists k \in ℤ w + k T \in ran Q \leftrightarrow \exists j \in ℤ w + j T \in ran Q$
56	55	rabbii	$⊢ \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\} = \{w \in [- π + X, π + X] \| \exists j \in ℤ w + j T \in ran Q\}$
57	56	uneq2i	$⊢ \{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\} = \{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists j \in ℤ w + j T \in ran Q\}$
58	57	fveq2i	$⊢ \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| = \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists j \in ℤ w + j T \in ran Q\}\|$
59	58	oveq1i	$⊢ \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1 = \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists j \in ℤ w + j T \in ran Q\}\| - 1$
60	59	oveq2i	$⊢ (0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1) = (0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists j \in ℤ w + j T \in ran Q\}\| - 1)$
61		isoeq4	$⊢ (0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1) = (0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists j \in ℤ w + j T \in ran Q\}\| - 1) \to (g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\}) \leftrightarrow g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists j \in ℤ w + j T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\}))$
62	60 61	ax-mp	$⊢ g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\}) \leftrightarrow g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists j \in ℤ w + j T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\})$
63	62	a1i	$⊢ g = f \to (g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\}) \leftrightarrow g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists j \in ℤ w + j T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\}))$
64		isoeq1	$⊢ g = f \to (g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists j \in ℤ w + j T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\}) \leftrightarrow f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists j \in ℤ w + j T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\}))$
65	52 63 64	3bitrd	$⊢ g = f \to (g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}) \leftrightarrow f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists j \in ℤ w + j T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\}))$
66	65	cbviotavw	$⊢ (ι g \| g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\})) = (ι f \| f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists j \in ℤ w + j T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists j \in ℤ y + j T \in ran Q\}))$
67		pire	$⊢ π \in ℝ$
68	67	renegcli	$⊢ - π \in ℝ$
69	68	a1i	$⊢ φ \to - π \in ℝ$
70	67	a1i	$⊢ φ \to π \in ℝ$
71		negpilt0	$⊢ - π < 0$
72	71	a1i	$⊢ φ \to - π < 0$
73		pipos	$⊢ 0 < π$
74	73	a1i	$⊢ φ \to 0 < π$
75		picn	$⊢ π \in ℂ$
76	75	2timesi	$⊢ 2 π = π + π$
77	75 75	subnegi	$⊢ π - (- π) = π + π$
78	76 2 77	3eqtr4i	$⊢ T = π - (- π)$
79	7	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))))$
80	8 79	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))))$
81	9 80	mpbid	$⊢ φ \to (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1)))$
82	81	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
83		elmapi	$⊢ Q \in (ℝ^{(0 \dots M)}) \to Q : (0 \dots M) ⟶ ℝ$
84	82 83	syl	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
85		fzfid	$⊢ φ \to (0 \dots M) \in Fin$
86		rnffi	$⊢ (Q : (0 \dots M) ⟶ ℝ \land (0 \dots M) \in Fin) \to ran Q \in Fin$
87	84 85 86	syl2anc	$⊢ φ \to ran Q \in Fin$
88	7 8 9	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [- π, π]$
89	88	frnd	$⊢ φ \to ran Q \subseteq [- π, π]$
90	81	simprd	$⊢ φ \to ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))$
91	90	simplrd	$⊢ φ \to Q (M) = π$
92	88	ffund	$⊢ φ \to Fun Q$
93	8	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
94		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
95	93 94	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
96		eluzfz2	$⊢ M \in ℤ_{\geq 0} \to M \in (0 \dots M)$
97	95 96	syl	$⊢ φ \to M \in (0 \dots M)$
98	88	fdmd	$⊢ φ \to dom Q = (0 \dots M)$
99	98	eqcomd	$⊢ φ \to (0 \dots M) = dom Q$
100	97 99	eleqtrd	$⊢ φ \to M \in dom Q$
101		fvelrn	$⊢ (Fun Q \land M \in dom Q) \to Q (M) \in ran Q$
102	92 100 101	syl2anc	$⊢ φ \to Q (M) \in ran Q$
103	91 102	eqeltrrd	$⊢ φ \to π \in ran Q$
104		eqid	$⊢ \{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\} = \{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}$
105		isoeq1	$⊢ g = f \to (g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}) \leftrightarrow f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}))$
106	41 57 49	3eqtr4ri	$⊢ \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\} = \{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}$
107		isoeq5	$⊢ \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\} = \{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\} \to (f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}) \leftrightarrow f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}))$
108	106 107	ax-mp	$⊢ f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}) \leftrightarrow f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\})$
109	105 108	bitrdi	$⊢ g = f \to (g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}) \leftrightarrow f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}))$
110	109	cbviotavw	$⊢ (ι g \| g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\})) = (ι f \| f {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}))$
111		eqid	$⊢ \{w \in (- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\} = \{w \in (- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}$
112	69 70 72 74 78 87 89 103 16 4 17 104 110 111	fourierdlem51	$⊢ φ \to X \in ran (ι g \| g {Isom}_{<, <} ((0 \dots \|\{- π + X, π + X\} \cup \{w \in [- π + X, π + X] \| \exists k \in ℤ w + k T \in ran Q\}\| - 1), \{- π + X, π + X\} \cup \{y \in [- π + X, π + X] \| \exists k \in ℤ y + k T \in ran Q\}))$
113		ax-resscn	$⊢ ℝ \subseteq ℂ$
114	113	a1i	$⊢ (φ \land i \in (0 ..^M)) \to ℝ \subseteq ℂ$
115		ioossre	$⊢ (Q (i), Q (i + 1)) \subseteq ℝ$
116	115	a1i	$⊢ φ \to (Q (i), Q (i + 1)) \subseteq ℝ$
117	1 116	fssresd	$⊢ φ \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℝ$
118	113	a1i	$⊢ φ \to ℝ \subseteq ℂ$
119	117 118	fssd	$⊢ φ \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
120	119	adantr	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
121	115	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℝ$
122	1 118	fssd	$⊢ φ \to F : ℝ ⟶ ℂ$
123	122	adantr	$⊢ (φ \land i \in (0 ..^M)) \to F : ℝ ⟶ ℂ$
124		ssidd	$⊢ (φ \land i \in (0 ..^M)) \to ℝ \subseteq ℝ$
125		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
126		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
127	125 126	dvres	$⊢ ((ℝ \subseteq ℂ \land F : ℝ ⟶ ℂ) \land (ℝ \subseteq ℝ \land (Q (i), Q (i + 1)) \subseteq ℝ)) \to ℝ D ({F ↾}_{(Q (i), Q (i + 1))}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((Q (i), Q (i + 1)))}$
128	114 123 124 121 127	syl22anc	$⊢ (φ \land i \in (0 ..^M)) \to ℝ D ({F ↾}_{(Q (i), Q (i + 1))}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((Q (i), Q (i + 1)))}$
129	128	dmeqd	$⊢ (φ \land i \in (0 ..^M)) \to dom {({F ↾}_{(Q (i), Q (i + 1))})}_{ℝ}^{'} = dom ({F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((Q (i), Q (i + 1)))})$
130		ioontr	$⊢ int (topGen (ran (.))) ((Q (i), Q (i + 1))) = (Q (i), Q (i + 1))$
131	130	reseq2i	$⊢ {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((Q (i), Q (i + 1)))} = {F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}$
132	131	dmeqi	$⊢ dom ({F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((Q (i), Q (i + 1)))}) = dom ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))})$
133	132	a1i	$⊢ (φ \land i \in (0 ..^M)) \to dom ({F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((Q (i), Q (i + 1)))}) = dom ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))})$
134		cncff	$⊢ ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
135		fdm	$⊢ ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ \to dom ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1))$
136	10 134 135	3syl	$⊢ (φ \land i \in (0 ..^M)) \to dom ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1))$
137	129 133 136	3eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to dom {({F ↾}_{(Q (i), Q (i + 1))})}_{ℝ}^{'} = (Q (i), Q (i + 1))$
138		dvcn	$⊢ ((ℝ \subseteq ℂ \land ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ \land (Q (i), Q (i + 1)) \subseteq ℝ) \land dom {({F ↾}_{(Q (i), Q (i + 1))})}_{ℝ}^{'} = (Q (i), Q (i + 1))) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
139	114 120 121 137 138	syl31anc	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
140	121 114	sstrd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℂ$
141	84	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
142		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
143	142	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
144	141 143	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
145	144	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ^{*}$
146		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
147	146	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
148	141 147	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
149	81	simprrd	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
150	149	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
151	125 145 148 150	lptioo1cn	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in limPt (TopOpen (ℂ_{fld})) ((Q (i), Q (i + 1)))$
152	117	adantr	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℝ$
153		ssidd	$⊢ φ \to ℝ \subseteq ℝ$
154	118 122 153	dvbss	$⊢ φ \to dom F_{ℝ}^{'} \subseteq ℝ$
155		dvfre	$⊢ (F : ℝ ⟶ ℝ \land ℝ \subseteq ℝ) \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
156	1 153 155	syl2anc	$⊢ φ \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
157		0re	$⊢ 0 \in ℝ$
158	68 157 67	lttri	$⊢ (- π < 0 \land 0 < π) \to - π < π$
159	71 73 158	mp2an	$⊢ - π < π$
160	159	a1i	$⊢ φ \to - π < π$
161	90	simplld	$⊢ φ \to Q (0) = - π$
162	10 134	syl	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
163	162 140 151 11 125	ellimciota	$⊢ (φ \land i \in (0 ..^M)) \to (ι x \| x \in (({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))) \in (({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
164	148	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ^{*}$
165	125 164 144 150	lptioo2cn	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in limPt (TopOpen (ℂ_{fld})) ((Q (i), Q (i + 1)))$
166	162 140 165 12 125	ellimciota	$⊢ (φ \land i \in (0 ..^M)) \to (ι x \| x \in (({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))) \in (({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
167	122	adantr	$⊢ (φ \land k \in ℤ) \to F : ℝ ⟶ ℂ$
168		zre	$⊢ k \in ℤ \to k \in ℝ$
169	168	adantl	$⊢ (φ \land k \in ℤ) \to k \in ℝ$
170		2pire	$⊢ 2 π \in ℝ$
171	170	a1i	$⊢ φ \to 2 π \in ℝ$
172	2 171	eqeltrid	$⊢ φ \to T \in ℝ$
173	172	adantr	$⊢ (φ \land k \in ℤ) \to T \in ℝ$
174	169 173	remulcld	$⊢ (φ \land k \in ℤ) \to k T \in ℝ$
175	167	adantr	$⊢ ((φ \land k \in ℤ) \land t \in ℝ) \to F : ℝ ⟶ ℂ$
176	173	adantr	$⊢ ((φ \land k \in ℤ) \land t \in ℝ) \to T \in ℝ$
177		simplr	$⊢ ((φ \land k \in ℤ) \land t \in ℝ) \to k \in ℤ$
178		simpr	$⊢ ((φ \land k \in ℤ) \land t \in ℝ) \to t \in ℝ$
179	3	ad4ant14	$⊢ (((φ \land k \in ℤ) \land t \in ℝ) \land x \in ℝ) \to F (x + T) = F (x)$
180	175 176 177 178 179	fperiodmul	$⊢ ((φ \land k \in ℤ) \land t \in ℝ) \to F (t + k T) = F (t)$
181		eqid	$⊢ ℝ D F = ℝ D F$
182	167 174 180 181	fperdvper	$⊢ ((φ \land k \in ℤ) \land t \in dom F_{ℝ}^{'}) \to (t + k T \in dom F_{ℝ}^{'} \land F_{ℝ}^{'} (t + k T) = F_{ℝ}^{'} (t))$
183	182	an32s	$⊢ ((φ \land t \in dom F_{ℝ}^{'}) \land k \in ℤ) \to (t + k T \in dom F_{ℝ}^{'} \land F_{ℝ}^{'} (t + k T) = F_{ℝ}^{'} (t))$
184	183	simpld	$⊢ ((φ \land t \in dom F_{ℝ}^{'}) \land k \in ℤ) \to t + k T \in dom F_{ℝ}^{'}$
185	183	simprd	$⊢ ((φ \land t \in dom F_{ℝ}^{'}) \land k \in ℤ) \to F_{ℝ}^{'} (t + k T) = F_{ℝ}^{'} (t)$
186		fveq2	$⊢ j = i \to Q (j) = Q (i)$
187		fvoveq1	$⊢ j = i \to Q (j + 1) = Q (i + 1)$
188	186 187	oveq12d	$⊢ j = i \to (Q (j), Q (j + 1)) = (Q (i), Q (i + 1))$
189	188	cbvmptv	$⊢ (j \in (0 ..^M) ⟼ (Q (j), Q (j + 1))) = (i \in (0 ..^M) ⟼ (Q (i), Q (i + 1)))$
190		eqid	$⊢ (t \in ℝ ⟼ t + ⌊\frac{π - t}{T}⌋ T) = (t \in ℝ ⟼ t + ⌊\frac{π - t}{T}⌋ T)$
191	154 156 69 70 160 78 8 84 161 91 10 163 166 184 185 189 190	fourierdlem71	$⊢ φ \to \exists z \in ℝ \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z$
192	191	adantr	$⊢ (φ \land i \in (0 ..^M)) \to \exists z \in ℝ \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z$
193		nfv	$⊢ Ⅎ t (φ \land i \in (0 ..^M))$
194		nfra1	$⊢ Ⅎ t \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z$
195	193 194	nfan	$⊢ Ⅎ t ((φ \land i \in (0 ..^M)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z)$
196	128 131	eqtrdi	$⊢ (φ \land i \in (0 ..^M)) \to ℝ D ({F ↾}_{(Q (i), Q (i + 1))}) = {F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}$
197	196	fveq1d	$⊢ (φ \land i \in (0 ..^M)) \to {({F ↾}_{(Q (i), Q (i + 1))})}_{ℝ}^{'} (t) = ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) (t)$
198		fvres	$⊢ t \in (Q (i), Q (i + 1)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) (t) = F_{ℝ}^{'} (t)$
199	197 198	sylan9eq	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \to {({F ↾}_{(Q (i), Q (i + 1))})}_{ℝ}^{'} (t) = F_{ℝ}^{'} (t)$
200	199	fveq2d	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \to \|{({F ↾}_{(Q (i), Q (i + 1))})}_{ℝ}^{'} (t)\| = \|F_{ℝ}^{'} (t)\|$
201	200	adantlr	$⊢ (((φ \land i \in (0 ..^M)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z) \land t \in (Q (i), Q (i + 1))) \to \|{({F ↾}_{(Q (i), Q (i + 1))})}_{ℝ}^{'} (t)\| = \|F_{ℝ}^{'} (t)\|$
202		simplr	$⊢ (((φ \land i \in (0 ..^M)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z) \land t \in (Q (i), Q (i + 1))) \to \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z$
203		ssdmres	$⊢ (Q (i), Q (i + 1)) \subseteq dom F_{ℝ}^{'} \leftrightarrow dom ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1))$
204	136 203	sylibr	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq dom F_{ℝ}^{'}$
205	204	ad2antrr	$⊢ (((φ \land i \in (0 ..^M)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z) \land t \in (Q (i), Q (i + 1))) \to (Q (i), Q (i + 1)) \subseteq dom F_{ℝ}^{'}$
206		simpr	$⊢ (((φ \land i \in (0 ..^M)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z) \land t \in (Q (i), Q (i + 1))) \to t \in (Q (i), Q (i + 1))$
207	205 206	sseldd	$⊢ (((φ \land i \in (0 ..^M)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z) \land t \in (Q (i), Q (i + 1))) \to t \in dom F_{ℝ}^{'}$
208		rspa	$⊢ (\forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z \land t \in dom F_{ℝ}^{'}) \to \|F_{ℝ}^{'} (t)\| \leq z$
209	202 207 208	syl2anc	$⊢ (((φ \land i \in (0 ..^M)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z) \land t \in (Q (i), Q (i + 1))) \to \|F_{ℝ}^{'} (t)\| \leq z$
210	201 209	eqbrtrd	$⊢ (((φ \land i \in (0 ..^M)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z) \land t \in (Q (i), Q (i + 1))) \to \|{({F ↾}_{(Q (i), Q (i + 1))})}_{ℝ}^{'} (t)\| \leq z$
211	195 210	ralrimia	$⊢ ((φ \land i \in (0 ..^M)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z) \to \forall t \in (Q (i), Q (i + 1)) \|{({F ↾}_{(Q (i), Q (i + 1))})}_{ℝ}^{'} (t)\| \leq z$
212	211	ex	$⊢ (φ \land i \in (0 ..^M)) \to (\forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z \to \forall t \in (Q (i), Q (i + 1)) \|{({F ↾}_{(Q (i), Q (i + 1))})}_{ℝ}^{'} (t)\| \leq z)$
213	212	reximdv	$⊢ (φ \land i \in (0 ..^M)) \to (\exists z \in ℝ \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z \to \exists z \in ℝ \forall t \in (Q (i), Q (i + 1)) \|{({F ↾}_{(Q (i), Q (i + 1))})}_{ℝ}^{'} (t)\| \leq z)$
214	192 213	mpd	$⊢ (φ \land i \in (0 ..^M)) \to \exists z \in ℝ \forall t \in (Q (i), Q (i + 1)) \|{({F ↾}_{(Q (i), Q (i + 1))})}_{ℝ}^{'} (t)\| \leq z$
215	148 144 152 137 214	ioodvbdlimc1	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) \neq \emptyset$
216	120 140 151 215 125	ellimciota	$⊢ (φ \land i \in (0 ..^M)) \to (ι y \| y \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))) \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
217	148 144 152 137 214	ioodvbdlimc2	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) \neq \emptyset$
218	120 140 165 217 125	ellimciota	$⊢ (φ \land i \in (0 ..^M)) \to (ι y \| y \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))) \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
219		resindm	$⊢ {F_{ℝ}^{'} ↾}_{((−∞, X) \cap dom F_{ℝ}^{'})} = {F_{ℝ}^{'} ↾}_{(−∞, X)}$
220	219	a1i	$⊢ φ \to {F_{ℝ}^{'} ↾}_{((−∞, X) \cap dom F_{ℝ}^{'})} = {F_{ℝ}^{'} ↾}_{(−∞, X)}$
221		inss2	$⊢ (−∞, X) \cap dom F_{ℝ}^{'} \subseteq dom F_{ℝ}^{'}$
222	221	a1i	$⊢ φ \to (−∞, X) \cap dom F_{ℝ}^{'} \subseteq dom F_{ℝ}^{'}$
223	156 222	fssresd	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{((−∞, X) \cap dom F_{ℝ}^{'})}) : (−∞, X) \cap dom F_{ℝ}^{'} ⟶ ℝ$
224	220 223	feq1dd	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{(−∞, X)}) : (−∞, X) \cap dom F_{ℝ}^{'} ⟶ ℝ$
225	224 118	fssd	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{(−∞, X)}) : (−∞, X) \cap dom F_{ℝ}^{'} ⟶ ℂ$
226		ioosscn	$⊢ (−∞, X) \subseteq ℂ$
227		ssinss1	$⊢ (−∞, X) \subseteq ℂ \to (−∞, X) \cap dom F_{ℝ}^{'} \subseteq ℂ$
228	226 227	ax-mp	$⊢ (−∞, X) \cap dom F_{ℝ}^{'} \subseteq ℂ$
229	228	a1i	$⊢ φ \to (−∞, X) \cap dom F_{ℝ}^{'} \subseteq ℂ$
230		3simpb	$⊢ (φ \land x \in dom F_{ℝ}^{'} \land k \in ℤ) \to (φ \land k \in ℤ)$
231		simp2	$⊢ (φ \land x \in dom F_{ℝ}^{'} \land k \in ℤ) \to x \in dom F_{ℝ}^{'}$
232	167	adantr	$⊢ ((φ \land k \in ℤ) \land x \in ℝ) \to F : ℝ ⟶ ℂ$
233	173	adantr	$⊢ ((φ \land k \in ℤ) \land x \in ℝ) \to T \in ℝ$
234		simplr	$⊢ ((φ \land k \in ℤ) \land x \in ℝ) \to k \in ℤ$
235		simpr	$⊢ ((φ \land k \in ℤ) \land x \in ℝ) \to x \in ℝ$
236		eleq1w	$⊢ x = y \to (x \in ℝ \leftrightarrow y \in ℝ)$
237	236	anbi2d	$⊢ x = y \to ((φ \land x \in ℝ) \leftrightarrow (φ \land y \in ℝ))$
238		fvoveq1	$⊢ x = y \to F (x + T) = F (y + T)$
239		fveq2	$⊢ x = y \to F (x) = F (y)$
240	238 239	eqeq12d	$⊢ x = y \to (F (x + T) = F (x) \leftrightarrow F (y + T) = F (y))$
241	237 240	imbi12d	$⊢ x = y \to (((φ \land x \in ℝ) \to F (x + T) = F (x)) \leftrightarrow ((φ \land y \in ℝ) \to F (y + T) = F (y)))$
242	241 3	chvarvv	$⊢ (φ \land y \in ℝ) \to F (y + T) = F (y)$
243	242	ad4ant14	$⊢ (((φ \land k \in ℤ) \land x \in ℝ) \land y \in ℝ) \to F (y + T) = F (y)$
244	232 233 234 235 243	fperiodmul	$⊢ ((φ \land k \in ℤ) \land x \in ℝ) \to F (x + k T) = F (x)$
245	167 174 244 181	fperdvper	$⊢ ((φ \land k \in ℤ) \land x \in dom F_{ℝ}^{'}) \to (x + k T \in dom F_{ℝ}^{'} \land F_{ℝ}^{'} (x + k T) = F_{ℝ}^{'} (x))$
246	230 231 245	syl2anc	$⊢ (φ \land x \in dom F_{ℝ}^{'} \land k \in ℤ) \to (x + k T \in dom F_{ℝ}^{'} \land F_{ℝ}^{'} (x + k T) = F_{ℝ}^{'} (x))$
247	246	simpld	$⊢ (φ \land x \in dom F_{ℝ}^{'} \land k \in ℤ) \to x + k T \in dom F_{ℝ}^{'}$
248		oveq2	$⊢ w = x \to π - w = π - x$
249	248	fvoveq1d	$⊢ w = x \to ⌊\frac{π - w}{T}⌋ = ⌊\frac{π - x}{T}⌋$
250	249	oveq1d	$⊢ w = x \to ⌊\frac{π - w}{T}⌋ T = ⌊\frac{π - x}{T}⌋ T$
251	250	cbvmptv	$⊢ (w \in ℝ ⟼ ⌊\frac{π - w}{T}⌋ T) = (x \in ℝ ⟼ ⌊\frac{π - x}{T}⌋ T)$
252		eqid	$⊢ (x \in ℝ ⟼ x + (w \in ℝ ⟼ ⌊\frac{π - w}{T}⌋ T) (x)) = (x \in ℝ ⟼ x + (w \in ℝ ⟼ ⌊\frac{π - w}{T}⌋ T) (x))$
253	69 70 160 78 247 4 251 252 7 8 9 204	fourierdlem41	$⊢ φ \to (\exists y \in ℝ (y < X \land (y, X) \subseteq dom F_{ℝ}^{'}) \land \exists y \in ℝ (X < y \land (X, y) \subseteq dom F_{ℝ}^{'}))$
254	253	simpld	$⊢ φ \to \exists y \in ℝ (y < X \land (y, X) \subseteq dom F_{ℝ}^{'})$
255	125	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
256		mnfxr	$⊢ −∞ \in ℝ^{*}$
257		rexr	$⊢ y \in ℝ \to y \in ℝ^{*}$
258	257	mnfled	$⊢ y \in ℝ \to −∞ \leq y$
259		iooss1	$⊢ (−∞ \in ℝ^{*} \land −∞ \leq y) \to (y, X) \subseteq (−∞, X)$
260	256 258 259	sylancr	$⊢ y \in ℝ \to (y, X) \subseteq (−∞, X)$
261	260	3ad2ant2	$⊢ (φ \land y \in ℝ \land (y, X) \subseteq dom F_{ℝ}^{'}) \to (y, X) \subseteq (−∞, X)$
262		simp3	$⊢ (φ \land y \in ℝ \land (y, X) \subseteq dom F_{ℝ}^{'}) \to (y, X) \subseteq dom F_{ℝ}^{'}$
263	261 262	ssind	$⊢ (φ \land y \in ℝ \land (y, X) \subseteq dom F_{ℝ}^{'}) \to (y, X) \subseteq (−∞, X) \cap dom F_{ℝ}^{'}$
264		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
265	264	lpss3	$⊢ (TopOpen (ℂ_{fld}) \in Top \land (−∞, X) \cap dom F_{ℝ}^{'} \subseteq ℂ \land (y, X) \subseteq (−∞, X) \cap dom F_{ℝ}^{'}) \to limPt (TopOpen (ℂ_{fld})) ((y, X)) \subseteq limPt (TopOpen (ℂ_{fld})) ((−∞, X) \cap dom F_{ℝ}^{'})$
266	255 228 263 265	mp3an12i	$⊢ (φ \land y \in ℝ \land (y, X) \subseteq dom F_{ℝ}^{'}) \to limPt (TopOpen (ℂ_{fld})) ((y, X)) \subseteq limPt (TopOpen (ℂ_{fld})) ((−∞, X) \cap dom F_{ℝ}^{'})$
267	266	3adant3l	$⊢ (φ \land y \in ℝ \land (y < X \land (y, X) \subseteq dom F_{ℝ}^{'})) \to limPt (TopOpen (ℂ_{fld})) ((y, X)) \subseteq limPt (TopOpen (ℂ_{fld})) ((−∞, X) \cap dom F_{ℝ}^{'})$
268	257	3ad2ant2	$⊢ (φ \land y \in ℝ \land (y < X \land (y, X) \subseteq dom F_{ℝ}^{'})) \to y \in ℝ^{*}$
269	4	3ad2ant1	$⊢ (φ \land y \in ℝ \land (y < X \land (y, X) \subseteq dom F_{ℝ}^{'})) \to X \in ℝ$
270		simp3l	$⊢ (φ \land y \in ℝ \land (y < X \land (y, X) \subseteq dom F_{ℝ}^{'})) \to y < X$
271	125 268 269 270	lptioo2cn	$⊢ (φ \land y \in ℝ \land (y < X \land (y, X) \subseteq dom F_{ℝ}^{'})) \to X \in limPt (TopOpen (ℂ_{fld})) ((y, X))$
272	267 271	sseldd	$⊢ (φ \land y \in ℝ \land (y < X \land (y, X) \subseteq dom F_{ℝ}^{'})) \to X \in limPt (TopOpen (ℂ_{fld})) ((−∞, X) \cap dom F_{ℝ}^{'})$
273	272	rexlimdv3a	$⊢ φ \to (\exists y \in ℝ (y < X \land (y, X) \subseteq dom F_{ℝ}^{'}) \to X \in limPt (TopOpen (ℂ_{fld})) ((−∞, X) \cap dom F_{ℝ}^{'}))$
274	254 273	mpd	$⊢ φ \to X \in limPt (TopOpen (ℂ_{fld})) ((−∞, X) \cap dom F_{ℝ}^{'})$
275	246	simprd	$⊢ (φ \land x \in dom F_{ℝ}^{'} \land k \in ℤ) \to F_{ℝ}^{'} (x + k T) = F_{ℝ}^{'} (x)$
276		oveq2	$⊢ y = x \to π - y = π - x$
277	276	fvoveq1d	$⊢ y = x \to ⌊\frac{π - y}{T}⌋ = ⌊\frac{π - x}{T}⌋$
278	277	oveq1d	$⊢ y = x \to ⌊\frac{π - y}{T}⌋ T = ⌊\frac{π - x}{T}⌋ T$
279	278	cbvmptv	$⊢ (y \in ℝ ⟼ ⌊\frac{π - y}{T}⌋ T) = (x \in ℝ ⟼ ⌊\frac{π - x}{T}⌋ T)$
280		id	$⊢ z = x \to z = x$
281		fveq2	$⊢ z = x \to (y \in ℝ ⟼ ⌊\frac{π - y}{T}⌋ T) (z) = (y \in ℝ ⟼ ⌊\frac{π - y}{T}⌋ T) (x)$
282	280 281	oveq12d	$⊢ z = x \to z + (y \in ℝ ⟼ ⌊\frac{π - y}{T}⌋ T) (z) = x + (y \in ℝ ⟼ ⌊\frac{π - y}{T}⌋ T) (x)$
283	282	cbvmptv	$⊢ (z \in ℝ ⟼ z + (y \in ℝ ⟼ ⌊\frac{π - y}{T}⌋ T) (z)) = (x \in ℝ ⟼ x + (y \in ℝ ⟼ ⌊\frac{π - y}{T}⌋ T) (x))$
284	69 70 160 7 78 8 9 154 156 247 275 10 166 4 279 283	fourierdlem49	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{(−∞, X)}) {lim}_{ℂ} X \neq \emptyset$
285	225 229 274 284 125	ellimciota	$⊢ φ \to (ι x \| x \in (({F_{ℝ}^{'} ↾}_{(−∞, X)}) {lim}_{ℂ} X)) \in (({F_{ℝ}^{'} ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
286		resindm	$⊢ {F_{ℝ}^{'} ↾}_{((X, +∞) \cap dom F_{ℝ}^{'})} = {F_{ℝ}^{'} ↾}_{(X, +∞)}$
287	286	a1i	$⊢ φ \to {F_{ℝ}^{'} ↾}_{((X, +∞) \cap dom F_{ℝ}^{'})} = {F_{ℝ}^{'} ↾}_{(X, +∞)}$
288		inss2	$⊢ (X, +∞) \cap dom F_{ℝ}^{'} \subseteq dom F_{ℝ}^{'}$
289	288	a1i	$⊢ φ \to (X, +∞) \cap dom F_{ℝ}^{'} \subseteq dom F_{ℝ}^{'}$
290	156 289	fssresd	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{((X, +∞) \cap dom F_{ℝ}^{'})}) : (X, +∞) \cap dom F_{ℝ}^{'} ⟶ ℝ$
291	287 290	feq1dd	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{(X, +∞)}) : (X, +∞) \cap dom F_{ℝ}^{'} ⟶ ℝ$
292	291 118	fssd	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{(X, +∞)}) : (X, +∞) \cap dom F_{ℝ}^{'} ⟶ ℂ$
293		ioosscn	$⊢ (X, +∞) \subseteq ℂ$
294		ssinss1	$⊢ (X, +∞) \subseteq ℂ \to (X, +∞) \cap dom F_{ℝ}^{'} \subseteq ℂ$
295	293 294	ax-mp	$⊢ (X, +∞) \cap dom F_{ℝ}^{'} \subseteq ℂ$
296	295	a1i	$⊢ φ \to (X, +∞) \cap dom F_{ℝ}^{'} \subseteq ℂ$
297	253	simprd	$⊢ φ \to \exists y \in ℝ (X < y \land (X, y) \subseteq dom F_{ℝ}^{'})$
298		pnfxr	$⊢ +∞ \in ℝ^{*}$
299	257	pnfged	$⊢ y \in ℝ \to y \leq +∞$
300		iooss2	$⊢ (+∞ \in ℝ^{*} \land y \leq +∞) \to (X, y) \subseteq (X, +∞)$
301	298 299 300	sylancr	$⊢ y \in ℝ \to (X, y) \subseteq (X, +∞)$
302	301	3ad2ant2	$⊢ (φ \land y \in ℝ \land (X, y) \subseteq dom F_{ℝ}^{'}) \to (X, y) \subseteq (X, +∞)$
303		simp3	$⊢ (φ \land y \in ℝ \land (X, y) \subseteq dom F_{ℝ}^{'}) \to (X, y) \subseteq dom F_{ℝ}^{'}$
304	302 303	ssind	$⊢ (φ \land y \in ℝ \land (X, y) \subseteq dom F_{ℝ}^{'}) \to (X, y) \subseteq (X, +∞) \cap dom F_{ℝ}^{'}$
305	264	lpss3	$⊢ (TopOpen (ℂ_{fld}) \in Top \land (X, +∞) \cap dom F_{ℝ}^{'} \subseteq ℂ \land (X, y) \subseteq (X, +∞) \cap dom F_{ℝ}^{'}) \to limPt (TopOpen (ℂ_{fld})) ((X, y)) \subseteq limPt (TopOpen (ℂ_{fld})) ((X, +∞) \cap dom F_{ℝ}^{'})$
306	255 295 304 305	mp3an12i	$⊢ (φ \land y \in ℝ \land (X, y) \subseteq dom F_{ℝ}^{'}) \to limPt (TopOpen (ℂ_{fld})) ((X, y)) \subseteq limPt (TopOpen (ℂ_{fld})) ((X, +∞) \cap dom F_{ℝ}^{'})$
307	306	3adant3l	$⊢ (φ \land y \in ℝ \land (X < y \land (X, y) \subseteq dom F_{ℝ}^{'})) \to limPt (TopOpen (ℂ_{fld})) ((X, y)) \subseteq limPt (TopOpen (ℂ_{fld})) ((X, +∞) \cap dom F_{ℝ}^{'})$
308	257	3ad2ant2	$⊢ (φ \land y \in ℝ \land (X < y \land (X, y) \subseteq dom F_{ℝ}^{'})) \to y \in ℝ^{*}$
309	4	3ad2ant1	$⊢ (φ \land y \in ℝ \land (X < y \land (X, y) \subseteq dom F_{ℝ}^{'})) \to X \in ℝ$
310		simp3l	$⊢ (φ \land y \in ℝ \land (X < y \land (X, y) \subseteq dom F_{ℝ}^{'})) \to X < y$
311	125 308 309 310	lptioo1cn	$⊢ (φ \land y \in ℝ \land (X < y \land (X, y) \subseteq dom F_{ℝ}^{'})) \to X \in limPt (TopOpen (ℂ_{fld})) ((X, y))$
312	307 311	sseldd	$⊢ (φ \land y \in ℝ \land (X < y \land (X, y) \subseteq dom F_{ℝ}^{'})) \to X \in limPt (TopOpen (ℂ_{fld})) ((X, +∞) \cap dom F_{ℝ}^{'})$
313	312	rexlimdv3a	$⊢ φ \to (\exists y \in ℝ (X < y \land (X, y) \subseteq dom F_{ℝ}^{'}) \to X \in limPt (TopOpen (ℂ_{fld})) ((X, +∞) \cap dom F_{ℝ}^{'}))$
314	297 313	mpd	$⊢ φ \to X \in limPt (TopOpen (ℂ_{fld})) ((X, +∞) \cap dom F_{ℝ}^{'})$
315		biid	$⊢ ((((φ \land i \in (0 ..^M)) \land w \in [Q (i), Q (i + 1))) \land k \in ℤ) \land w = X + k T) \leftrightarrow ((((φ \land i \in (0 ..^M)) \land w \in [Q (i), Q (i + 1))) \land k \in ℤ) \land w = X + k T)$
316	69 70 160 7 78 8 9 156 247 275 10 163 4 279 283 315	fourierdlem48	$⊢ φ \to ({F_{ℝ}^{'} ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset$
317	292 296 314 316 125	ellimciota	$⊢ φ \to (ι x \| x \in (({F_{ℝ}^{'} ↾}_{(X, +∞)}) {lim}_{ℂ} X)) \in (({F_{ℝ}^{'} ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
318		fveq2	$⊢ n = k \to A (n) = A (k)$
319		fvoveq1	$⊢ n = k \to \cos n X = \cos k X$
320	318 319	oveq12d	$⊢ n = k \to A (n) \cos n X = A (k) \cos k X$
321		fveq2	$⊢ n = k \to B (n) = B (k)$
322		fvoveq1	$⊢ n = k \to \sin n X = \sin k X$
323	321 322	oveq12d	$⊢ n = k \to B (n) \sin n X = B (k) \sin k X$
324	320 323	oveq12d	$⊢ n = k \to A (n) \cos n X + B (n) \sin n X = A (k) \cos k X + B (k) \sin k X$
325	324	cbvsumv	$⊢ \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X) = \sum_{k = 1}^{m} (A (k) \cos k X + B (k) \sin k X)$
326		oveq2	$⊢ j = m \to (1 \dots j) = (1 \dots m)$
327	326	eqcomd	$⊢ j = m \to (1 \dots m) = (1 \dots j)$
328	327	sumeq1d	$⊢ j = m \to \sum_{k = 1}^{m} (A (k) \cos k X + B (k) \sin k X) = \sum_{k = 1}^{j} (A (k) \cos k X + B (k) \sin k X)$
329	325 328	eqtr2id	$⊢ j = m \to \sum_{k = 1}^{j} (A (k) \cos k X + B (k) \sin k X) = \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X)$
330	329	oveq2d	$⊢ j = m \to (\frac{A (0)}{2}) + \sum_{k = 1}^{j} (A (k) \cos k X + B (k) \sin k X) = (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X)$
331	330	cbvmptv	$⊢ (j \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{k = 1}^{j} (A (k) \cos k X + B (k) \sin k X)) = (m \in ℕ ⟼ (\frac{A (0)}{2}) + \sum_{n = 1}^{m} (A (n) \cos n X + B (n) \sin n X))$
332	1	fdmd	$⊢ φ \to dom F = ℝ$
333	332	eqimssd	$⊢ φ \to dom F \subseteq ℝ$
334	1	ffdmd	$⊢ φ \to F : dom F ⟶ ℝ$
335	333	sselda	$⊢ (φ \land t \in dom F) \to t \in ℝ$
336	335	adantr	$⊢ ((φ \land t \in dom F) \land k \in ℤ) \to t \in ℝ$
337	168	adantl	$⊢ ((φ \land t \in dom F) \land k \in ℤ) \to k \in ℝ$
338	173	adantlr	$⊢ ((φ \land t \in dom F) \land k \in ℤ) \to T \in ℝ$
339	337 338	remulcld	$⊢ ((φ \land t \in dom F) \land k \in ℤ) \to k T \in ℝ$
340	336 339	readdcld	$⊢ ((φ \land t \in dom F) \land k \in ℤ) \to t + k T \in ℝ$
341	332	eqcomd	$⊢ φ \to ℝ = dom F$
342	341	ad2antrr	$⊢ ((φ \land t \in dom F) \land k \in ℤ) \to ℝ = dom F$
343	340 342	eleqtrd	$⊢ ((φ \land t \in dom F) \land k \in ℤ) \to t + k T \in dom F$
344		id	$⊢ (φ \land k \in ℤ) \to (φ \land k \in ℤ)$
345	344	adantlr	$⊢ ((φ \land t \in dom F) \land k \in ℤ) \to (φ \land k \in ℤ)$
346	345 336 180	syl2anc	$⊢ ((φ \land t \in dom F) \land k \in ℤ) \to F (t + k T) = F (t)$
347	333 334 69 70 160 78 8 84 161 91 139 216 218 343 346 189 190	fourierdlem71	$⊢ φ \to \exists u \in ℝ \forall t \in dom F \|F (t)\| \leq u$
348	332	raleqdv	$⊢ φ \to (\forall t \in dom F \|F (t)\| \leq u \leftrightarrow \forall t \in ℝ \|F (t)\| \leq u)$
349	348	rexbidv	$⊢ φ \to (\exists u \in ℝ \forall t \in dom F \|F (t)\| \leq u \leftrightarrow \exists u \in ℝ \forall t \in ℝ \|F (t)\| \leq u)$
350	347 349	mpbid	$⊢ φ \to \exists u \in ℝ \forall t \in ℝ \|F (t)\| \leq u$
351	1 36 7 8 9 43 66 4 112 2 3 139 216 218 10 285 317 5 6 13 14 331 15 350 191 4	fourierdlem112	$⊢ φ \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 fourierdlem113

Proof