fourierdlem38

Description: The function F is continuous on every interval induced by the partition Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem38.cn	$⊢ φ \to F : dom F \underset{cn}{⟶} ℂ$
	fourierdlem38.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))\})$
	fourierdlem38.m	$⊢ φ \to M \in ℕ$
	fourierdlem38.q	$⊢ φ \to Q \in P (M)$
	fourierdlem38.h	$⊢ H = A \cup ([- π, π] ∖ dom F)$
	fourierdlem38.ranq	$⊢ φ \to ran Q = H$
Assertion	fourierdlem38	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem38.cn	$⊢ φ \to F : dom F \underset{cn}{⟶} ℂ$
2		fourierdlem38.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))\})$
3		fourierdlem38.m	$⊢ φ \to M \in ℕ$
4		fourierdlem38.q	$⊢ φ \to Q \in P (M)$
5		fourierdlem38.h	$⊢ H = A \cup ([- π, π] ∖ dom F)$
6		fourierdlem38.ranq	$⊢ φ \to ran Q = H$
7		simplr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \land \neg x \in dom F) \to x \in (Q (i), Q (i + 1))$
8		simplll	$⊢ (((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \land \neg x \in dom F) \to φ$
9		ioossicc	$⊢ (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]$
10		pire	$⊢ π \in ℝ$
11	10	renegcli	$⊢ - π \in ℝ$
12	11	rexri	$⊢ - π \in ℝ^{*}$
13	12	a1i	$⊢ (φ \land i \in (0 ..^M)) \to - π \in ℝ^{*}$
14	10	rexri	$⊢ π \in ℝ^{*}$
15	14	a1i	$⊢ (φ \land i \in (0 ..^M)) \to π \in ℝ^{*}$
16	2 3 4	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [- π, π]$
17	16	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ [- π, π]$
18		simpr	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 ..^M)$
19	13 15 17 18	fourierdlem8	$⊢ (φ \land i \in (0 ..^M)) \to [Q (i), Q (i + 1)] \subseteq [- π, π]$
20	9 19	sstrid	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq [- π, π]$
21	20	sselda	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to x \in [- π, π]$
22	21	adantr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \land \neg x \in dom F) \to x \in [- π, π]$
23		simpr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \land \neg x \in dom F) \to \neg x \in dom F$
24		simpllr	$⊢ (((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \land \neg x \in dom F) \to i \in (0 ..^M)$
25	3	3ad2ant1	$⊢ (φ \land x \in [- π, π] \land \neg x \in dom F) \to M \in ℕ$
26	4	3ad2ant1	$⊢ (φ \land x \in [- π, π] \land \neg x \in dom F) \to Q \in P (M)$
27		simp2	$⊢ (φ \land x \in [- π, π] \land \neg x \in dom F) \to x \in [- π, π]$
28		simp3	$⊢ (φ \land x \in [- π, π] \land \neg x \in dom F) \to \neg x \in dom F$
29	27 28	eldifd	$⊢ (φ \land x \in [- π, π] \land \neg x \in dom F) \to x \in ([- π, π] ∖ dom F)$
30		elun2	$⊢ x \in ([- π, π] ∖ dom F) \to x \in (A \cup ([- π, π] ∖ dom F))$
31	29 30	syl	$⊢ (φ \land x \in [- π, π] \land \neg x \in dom F) \to x \in (A \cup ([- π, π] ∖ dom F))$
32	6 5	eqtr2di	$⊢ φ \to A \cup ([- π, π] ∖ dom F) = ran Q$
33	32	3ad2ant1	$⊢ (φ \land x \in [- π, π] \land \neg x \in dom F) \to A \cup ([- π, π] ∖ dom F) = ran Q$
34	31 33	eleqtrd	$⊢ (φ \land x \in [- π, π] \land \neg x \in dom F) \to x \in ran Q$
35	2 25 26 34	fourierdlem12	$⊢ ((φ \land x \in [- π, π] \land \neg x \in dom F) \land i \in (0 ..^M)) \to \neg x \in (Q (i), Q (i + 1))$
36	8 22 23 24 35	syl31anc	$⊢ (((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \land \neg x \in dom F) \to \neg x \in (Q (i), Q (i + 1))$
37	7 36	condan	$⊢ ((φ \land i \in (0 ..^M)) \land x \in (Q (i), Q (i + 1))) \to x \in dom F$
38	37	ralrimiva	$⊢ (φ \land i \in (0 ..^M)) \to \forall x \in (Q (i), Q (i + 1)) x \in dom F$
39		dfss3	$⊢ (Q (i), Q (i + 1)) \subseteq dom F \leftrightarrow \forall x \in (Q (i), Q (i + 1)) x \in dom F$
40	38 39	sylibr	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq dom F$
41	1	adantr	$⊢ (φ \land i \in (0 ..^M)) \to F : dom F \underset{cn}{⟶} ℂ$
42		rescncf	$⊢ (Q (i), Q (i + 1)) \subseteq dom F \to (F : dom F \underset{cn}{⟶} ℂ \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ)$
43	40 41 42	sylc	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem fourierdlem38

Proof