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