fourierdlem100

Description: A piecewise continuous function is integrable on any closed interval. This lemma uses local definitions, so that the proof is more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierlemiblglemlem.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem100.t	$⊢ T = B - A$
	fourierdlem100.m	$⊢ φ \to M \in ℕ$
	fourierdlem100.q	$⊢ φ \to Q \in P (M)$
	fourierdlem100.f	$⊢ φ \to F : ℝ ⟶ ℂ$
	fourierdlem100.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fourierdlem100.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem100.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
	fourierdlem100.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
	fourierdlem100.c	$⊢ φ \to C \in ℝ$
	fourierdlem100.d	$⊢ φ \to D \in (C, +∞)$
	fourierdlem100.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = C \land p (m) = D) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem100.n	$⊢ N = \|H\| - 1$
	fourierdlem100.h	$⊢ H = \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}$
	fourierdlem100.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), H))$
	fourierdlem100.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
	fourierdlem100.j	$⊢ J = (y \in (A, B] ⟼ if (y = B, A, y))$
	fourierdlem100.i	$⊢ I = (x \in ℝ ⟼ sup (\{i \in (0 ..^M) \| Q (i) \leq J (E (x))\} ℝ <))$
Assertion	fourierdlem100	$⊢ φ \to (x \in [C, D] ⟼ F (x)) \in 𝐿^{1}$

Proof

Step	Hyp	Ref	Expression
1		fourierlemiblglemlem.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
2		fourierdlem100.t	$⊢ T = B - A$
3		fourierdlem100.m	$⊢ φ \to M \in ℕ$
4		fourierdlem100.q	$⊢ φ \to Q \in P (M)$
5		fourierdlem100.f	$⊢ φ \to F : ℝ ⟶ ℂ$
6		fourierdlem100.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
7		fourierdlem100.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
8		fourierdlem100.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
9		fourierdlem100.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
10		fourierdlem100.c	$⊢ φ \to C \in ℝ$
11		fourierdlem100.d	$⊢ φ \to D \in (C, +∞)$
12		fourierdlem100.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = C \land p (m) = D) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
13		fourierdlem100.n	$⊢ N = \|H\| - 1$
14		fourierdlem100.h	$⊢ H = \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}$
15		fourierdlem100.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), H))$
16		fourierdlem100.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
17		fourierdlem100.j	$⊢ J = (y \in (A, B] ⟼ if (y = B, A, y))$
18		fourierdlem100.i	$⊢ I = (x \in ℝ ⟼ sup (\{i \in (0 ..^M) \| Q (i) \leq J (E (x))\} ℝ <))$
19		elioore	$⊢ D \in (C, +∞) \to D \in ℝ$
20	11 19	syl	$⊢ φ \to D \in ℝ$
21	10 20	iccssred	$⊢ φ \to [C, D] \subseteq ℝ$
22	5 21	feqresmpt	$⊢ φ \to {F ↾}_{[C, D]} = (x \in [C, D] ⟼ F (x))$
23		fveq2	$⊢ i = j \to p (i) = p (j)$
24		oveq1	$⊢ i = j \to i + 1 = j + 1$
25	24	fveq2d	$⊢ i = j \to p (i + 1) = p (j + 1)$
26	23 25	breq12d	$⊢ i = j \to (p (i) < p (i + 1) \leftrightarrow p (j) < p (j + 1))$
27	26	cbvralvw	$⊢ \forall i \in (0 ..^m) p (i) < p (i + 1) \leftrightarrow \forall j \in (0 ..^m) p (j) < p (j + 1)$
28	27	anbi2i	$⊢ ((p (0) = C \land p (m) = D) \land \forall i \in (0 ..^m) p (i) < p (i + 1)) \leftrightarrow ((p (0) = C \land p (m) = D) \land \forall j \in (0 ..^m) p (j) < p (j + 1))$
29	28	a1i	$⊢ p \in (ℝ^{(0 \dots m)}) \to (((p (0) = C \land p (m) = D) \land \forall i \in (0 ..^m) p (i) < p (i + 1)) \leftrightarrow ((p (0) = C \land p (m) = D) \land \forall j \in (0 ..^m) p (j) < p (j + 1)))$
30	29	rabbiia	$⊢ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = C \land p (m) = D) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\} = \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = C \land p (m) = D) \land \forall j \in (0 ..^m) p (j) < p (j + 1))\}$
31	30	mpteq2i	$⊢ (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = C \land p (m) = D) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\}) = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = C \land p (m) = D) \land \forall j \in (0 ..^m) p (j) < p (j + 1))\})$
32	12 31	eqtri	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = C \land p (m) = D) \land \forall j \in (0 ..^m) p (j) < p (j + 1))\})$
33		elioo4g	$⊢ D \in (C, +∞) \leftrightarrow ((C \in ℝ^{} \land +∞ \in ℝ^{} \land D \in ℝ) \land (C < D \land D < +∞))$
34	11 33	sylib	$⊢ φ \to ((C \in ℝ^{} \land +∞ \in ℝ^{} \land D \in ℝ) \land (C < D \land D < +∞))$
35	34	simprd	$⊢ φ \to (C < D \land D < +∞)$
36	35	simpld	$⊢ φ \to C < D$
37		id	$⊢ y = x \to y = x$
38	2	eqcomi	$⊢ B - A = T$
39	38	oveq2i	$⊢ k (B - A) = k T$
40	39	a1i	$⊢ y = x \to k (B - A) = k T$
41	37 40	oveq12d	$⊢ y = x \to y + k (B - A) = x + k T$
42	41	eleq1d	$⊢ y = x \to (y + k (B - A) \in ran Q \leftrightarrow x + k T \in ran Q)$
43	42	rexbidv	$⊢ y = x \to (\exists k \in ℤ y + k (B - A) \in ran Q \leftrightarrow \exists k \in ℤ x + k T \in ran Q)$
44	43	cbvrabv	$⊢ \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\} = \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
45	44	uneq2i	$⊢ \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\} = \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
46	39	eqcomi	$⊢ k T = k (B - A)$
47	46	oveq2i	$⊢ y + k T = y + k (B - A)$
48	47	eleq1i	$⊢ y + k T \in ran Q \leftrightarrow y + k (B - A) \in ran Q$
49	48	rexbii	$⊢ \exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists k \in ℤ y + k (B - A) \in ran Q$
50	49	rgenw	$⊢ \forall y \in [C, D] (\exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists k \in ℤ y + k (B - A) \in ran Q)$
51		rabbi	$⊢ \forall y \in [C, D] (\exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists k \in ℤ y + k (B - A) \in ran Q) \leftrightarrow \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} = \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}$
52	50 51	mpbi	$⊢ \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} = \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}$
53	52	uneq2i	$⊢ \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} = \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}$
54	14 53	eqtri	$⊢ H = \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}$
55	54	fveq2i	$⊢ \|H\| = \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}\|$
56	55	oveq1i	$⊢ \|H\| - 1 = \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}\| - 1$
57	13 56	eqtri	$⊢ N = \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}\| - 1$
58		isoeq5	$⊢ H = \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\} \to (f {Isom}_{<, <} ((0 \dots N), H) \leftrightarrow f {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}))$
59	54 58	ax-mp	$⊢ f {Isom}_{<, <} ((0 \dots N), H) \leftrightarrow f {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\})$
60	59	iotabii	$⊢ (ι f \| f {Isom}_{<, <} ((0 \dots N), H)) = (ι f \| f {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}))$
61	15 60	eqtri	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}))$
62	2 1 3 4 10 20 36 12 45 57 61	fourierdlem54	$⊢ φ \to ((N \in ℕ \land S \in O (N)) \land S {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}))$
63	62	simpld	$⊢ φ \to (N \in ℕ \land S \in O (N))$
64	63	simpld	$⊢ φ \to N \in ℕ$
65	63	simprd	$⊢ φ \to S \in O (N)$
66	5 21	fssresd	$⊢ φ \to ({F ↾}_{[C, D]}) : [C, D] ⟶ ℂ$
67		ioossicc	$⊢ (S (j), S (j + 1)) \subseteq [S (j), S (j + 1)]$
68	10	adantr	$⊢ (φ \land j \in (0 ..^N)) \to C \in ℝ$
69	68	rexrd	$⊢ (φ \land j \in (0 ..^N)) \to C \in ℝ^{*}$
70	11	adantr	$⊢ (φ \land j \in (0 ..^N)) \to D \in (C, +∞)$
71	70 19	syl	$⊢ (φ \land j \in (0 ..^N)) \to D \in ℝ$
72	71	rexrd	$⊢ (φ \land j \in (0 ..^N)) \to D \in ℝ^{*}$
73	12 64 65	fourierdlem15	$⊢ φ \to S : (0 \dots N) ⟶ [C, D]$
74	73	adantr	$⊢ (φ \land j \in (0 ..^N)) \to S : (0 \dots N) ⟶ [C, D]$
75		simpr	$⊢ (φ \land j \in (0 ..^N)) \to j \in (0 ..^N)$
76	69 72 74 75	fourierdlem8	$⊢ (φ \land j \in (0 ..^N)) \to [S (j), S (j + 1)] \subseteq [C, D]$
77	67 76	sstrid	$⊢ (φ \land j \in (0 ..^N)) \to (S (j), S (j + 1)) \subseteq [C, D]$
78	77	resabs1d	$⊢ (φ \land j \in (0 ..^N)) \to {({F ↾}_{[C, D]}) ↾}_{(S (j), S (j + 1))} = {F ↾}_{(S (j), S (j + 1))}$
79	3	adantr	$⊢ (φ \land j \in (0 ..^N)) \to M \in ℕ$
80	4	adantr	$⊢ (φ \land j \in (0 ..^N)) \to Q \in P (M)$
81	5	adantr	$⊢ (φ \land j \in (0 ..^N)) \to F : ℝ ⟶ ℂ$
82	6	adantlr	$⊢ ((φ \land j \in (0 ..^N)) \land x \in ℝ) \to F (x + T) = F (x)$
83	7	adantlr	$⊢ ((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
84		eqid	$⊢ S (j + 1) - E (S (j + 1)) = S (j + 1) - E (S (j + 1))$
85		eqid	$⊢ {F ↾}_{(J (E (S (j))), E (S (j + 1)))} = {F ↾}_{(J (E (S (j))), E (S (j + 1)))}$
86		eqid	$⊢ (y \in (J (E (S (j))) + S (j + 1) - E (S (j + 1)), E (S (j + 1)) + S (j + 1) - E (S (j + 1))) ⟼ ({F ↾}_{(J (E (S (j))), E (S (j + 1)))}) (y - (S (j + 1) - E (S (j + 1))))) = (y \in (J (E (S (j))) + S (j + 1) - E (S (j + 1)), E (S (j + 1)) + S (j + 1) - E (S (j + 1))) ⟼ ({F ↾}_{(J (E (S (j))), E (S (j + 1)))}) (y - (S (j + 1) - E (S (j + 1)))))$
87	1 2 79 80 81 82 83 68 70 12 14 13 15 16 17 75 84 85 86 18	fourierdlem90	$⊢ (φ \land j \in (0 ..^N)) \to ({F ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ$
88	78 87	eqeltrd	$⊢ (φ \land j \in (0 ..^N)) \to ({({F ↾}_{[C, D]}) ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ$
89	8	adantlr	$⊢ ((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
90		eqid	$⊢ (i \in (0 ..^M) ⟼ R) = (i \in (0 ..^M) ⟼ R)$
91	1 2 79 80 81 82 83 89 68 70 12 14 13 15 16 17 75 84 18 90	fourierdlem89	$⊢ (φ \land j \in (0 ..^N)) \to if (J (E (S (j))) = Q (I (S (j))), (i \in (0 ..^M) ⟼ R) (I (S (j))), F (J (E (S (j))))) \in (({F ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))$
92	78	eqcomd	$⊢ (φ \land j \in (0 ..^N)) \to {F ↾}_{(S (j), S (j + 1))} = {({F ↾}_{[C, D]}) ↾}_{(S (j), S (j + 1))}$
93	92	oveq1d	$⊢ (φ \land j \in (0 ..^N)) \to ({F ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j) = ({({F ↾}_{[C, D]}) ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j)$
94	91 93	eleqtrd	$⊢ (φ \land j \in (0 ..^N)) \to if (J (E (S (j))) = Q (I (S (j))), (i \in (0 ..^M) ⟼ R) (I (S (j))), F (J (E (S (j))))) \in (({({F ↾}_{[C, D]}) ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))$
95	9	adantlr	$⊢ ((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
96		eqid	$⊢ (i \in (0 ..^M) ⟼ L) = (i \in (0 ..^M) ⟼ L)$
97	1 2 79 80 81 82 83 95 68 70 12 14 13 15 16 17 75 84 18 96	fourierdlem91	$⊢ (φ \land j \in (0 ..^N)) \to if (E (S (j + 1)) = Q (I (S (j)) + 1), (i \in (0 ..^M) ⟼ L) (I (S (j))), F (E (S (j + 1)))) \in (({F ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1))$
98	92	oveq1d	$⊢ (φ \land j \in (0 ..^N)) \to ({F ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1) = ({({F ↾}_{[C, D]}) ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)$
99	97 98	eleqtrd	$⊢ (φ \land j \in (0 ..^N)) \to if (E (S (j + 1)) = Q (I (S (j)) + 1), (i \in (0 ..^M) ⟼ L) (I (S (j))), F (E (S (j + 1)))) \in (({({F ↾}_{[C, D]}) ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1))$
100	32 64 65 66 88 94 99	fourierdlem69	$⊢ φ \to {F ↾}_{[C, D]} \in 𝐿^{1}$
101	22 100	eqeltrrd	$⊢ φ \to (x \in [C, D] ⟼ F (x)) \in 𝐿^{1}$

Metamath Proof Explorer

Theorem fourierdlem100

Proof