fourierdlem69

Description: A piecewise continuous function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem69.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))\})$
	fourierdlem69.m	$⊢ φ \to M \in ℕ$
	fourierdlem69.q	$⊢ φ \to Q \in P (M)$
	fourierdlem69.f	$⊢ φ \to F : [A, B] ⟶ ℂ$
	fourierdlem69.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem69.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
	fourierdlem69.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
Assertion	fourierdlem69	$⊢ φ \to F \in 𝐿^{1}$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem69.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		fourierdlem69.m	$⊢ φ \to M \in ℕ$
3		fourierdlem69.q	$⊢ φ \to Q \in P (M)$
4		fourierdlem69.f	$⊢ φ \to F : [A, B] ⟶ ℂ$
5		fourierdlem69.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
6		fourierdlem69.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
7		fourierdlem69.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
8	1	fourierdlem2	$⊢ M \in ℕ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
9	2 8	syl	$⊢ φ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
10	3 9	mpbid	$⊢ φ \to (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1)))$
11	10	simprd	$⊢ φ \to ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))$
12	11	simpld	$⊢ φ \to (Q (0) = A \land Q (M) = B)$
13	12	simpld	$⊢ φ \to Q (0) = A$
14	12	simprd	$⊢ φ \to Q (M) = B$
15	13 14	oveq12d	$⊢ φ \to [Q (0), Q (M)] = [A, B]$
16	15	feq2d	$⊢ φ \to (F : [Q (0), Q (M)] ⟶ ℂ \leftrightarrow F : [A, B] ⟶ ℂ)$
17	4 16	mpbird	$⊢ φ \to F : [Q (0), Q (M)] ⟶ ℂ$
18	17	feqmptd	$⊢ φ \to F = (x \in [Q (0), Q (M)] ⟼ F (x))$
19		nfv	$⊢ Ⅎ x φ$
20		0zd	$⊢ φ \to 0 \in ℤ$
21		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
22		1e0p1	$⊢ 1 = 0 + 1$
23	22	fveq2i	$⊢ ℤ_{\geq 1} = ℤ_{\geq (0 + 1)}$
24	21 23	eqtri	$⊢ ℕ = ℤ_{\geq (0 + 1)}$
25	2 24	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq (0 + 1)}$
26	10	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
27		elmapi	$⊢ Q \in (ℝ^{(0 \dots M)}) \to Q : (0 \dots M) ⟶ ℝ$
28	26 27	syl	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
29	28	ffvelcdmda	$⊢ (φ \land i \in (0 \dots M)) \to Q (i) \in ℝ$
30	11	simprd	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
31	30	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
32	4	adantr	$⊢ (φ \land x \in [Q (0), Q (M)]) \to F : [A, B] ⟶ ℂ$
33		simpr	$⊢ (φ \land x \in [Q (0), Q (M)]) \to x \in [Q (0), Q (M)]$
34	13	adantr	$⊢ (φ \land x \in [Q (0), Q (M)]) \to Q (0) = A$
35	14	adantr	$⊢ (φ \land x \in [Q (0), Q (M)]) \to Q (M) = B$
36	34 35	oveq12d	$⊢ (φ \land x \in [Q (0), Q (M)]) \to [Q (0), Q (M)] = [A, B]$
37	33 36	eleqtrd	$⊢ (φ \land x \in [Q (0), Q (M)]) \to x \in [A, B]$
38	32 37	ffvelcdmd	$⊢ (φ \land x \in [Q (0), Q (M)]) \to F (x) \in ℂ$
39	28	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
40		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
41	40	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
42	39 41	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
43		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
44	43	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
45	39 44	ffvelcdmd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
46	4	adantr	$⊢ (φ \land i \in (0 ..^M)) \to F : [A, B] ⟶ ℂ$
47		ioossicc	$⊢ (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]$
48	1 2 3	fourierdlem11	$⊢ φ \to (A \in ℝ \land B \in ℝ \land A < B)$
49	48	simp1d	$⊢ φ \to A \in ℝ$
50	49	rexrd	$⊢ φ \to A \in ℝ^{*}$
51	50	adantr	$⊢ (φ \land i \in (0 ..^M)) \to A \in ℝ^{*}$
52	48	simp2d	$⊢ φ \to B \in ℝ$
53	52	rexrd	$⊢ φ \to B \in ℝ^{*}$
54	53	adantr	$⊢ (φ \land i \in (0 ..^M)) \to B \in ℝ^{*}$
55	1 2 3	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [A, B]$
56	55	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ [A, B]$
57		simpr	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 ..^M)$
58	51 54 56 57	fourierdlem8	$⊢ (φ \land i \in (0 ..^M)) \to [Q (i), Q (i + 1)] \subseteq [A, B]$
59	47 58	sstrid	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq [A, B]$
60	46 59	feqresmpt	$⊢ (φ \land i \in (0 ..^M)) \to {F ↾}_{(Q (i), Q (i + 1))} = (x \in (Q (i), Q (i + 1)) ⟼ F (x))$
61	60 5	eqeltrrd	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (Q (i), Q (i + 1)) ⟼ F (x)) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
62	60	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) = (x \in (Q (i), Q (i + 1)) ⟼ F (x)) {lim}_{ℂ} Q (i + 1)$
63	7 62	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to L \in ((x \in (Q (i), Q (i + 1)) ⟼ F (x)) {lim}_{ℂ} Q (i + 1))$
64	60	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = (x \in (Q (i), Q (i + 1)) ⟼ F (x)) {lim}_{ℂ} Q (i)$
65	6 64	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to R \in ((x \in (Q (i), Q (i + 1)) ⟼ F (x)) {lim}_{ℂ} Q (i))$
66	42 45 61 63 65	iblcncfioo	$⊢ (φ \land i \in (0 ..^M)) \to (x \in (Q (i), Q (i + 1)) ⟼ F (x)) \in 𝐿^{1}$
67	46	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to F : [A, B] ⟶ ℂ$
68	58	sselda	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to x \in [A, B]$
69	67 68	ffvelcdmd	$⊢ ((φ \land i \in (0 ..^M)) \land x \in [Q (i), Q (i + 1)]) \to F (x) \in ℂ$
70	42 45 66 69	ibliooicc	$⊢ (φ \land i \in (0 ..^M)) \to (x \in [Q (i), Q (i + 1)] ⟼ F (x)) \in 𝐿^{1}$
71	19 20 25 29 31 38 70	iblspltprt	$⊢ φ \to (x \in [Q (0), Q (M)] ⟼ F (x)) \in 𝐿^{1}$
72	18 71	eqeltrd	$⊢ φ \to F \in 𝐿^{1}$

Metamath Proof Explorer

Theorem fourierdlem69

Proof