fourierdlem94

Description: For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem94.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem94.t	$⊢ T = 2 π$
	fourierdlem94.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fourierdlem94.x	$⊢ φ \to X \in ℝ$
	fourierdlem94.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))\})$
	fourierdlem94.m	$⊢ φ \to M \in ℕ$
	fourierdlem94.q	$⊢ φ \to Q \in P (M)$
	fourierdlem94.dvcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem94.dvlb	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) \neq \emptyset$
	fourierdlem94.dvub	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) \neq \emptyset$
Assertion	fourierdlem94	$⊢ φ \to (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X \neq \emptyset \land ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem94.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem94.t	$⊢ T = 2 π$
3		fourierdlem94.per	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
4		fourierdlem94.x	$⊢ φ \to X \in ℝ$
5		fourierdlem94.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))\})$
6		fourierdlem94.m	$⊢ φ \to M \in ℕ$
7		fourierdlem94.q	$⊢ φ \to Q \in P (M)$
8		fourierdlem94.dvcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
9		fourierdlem94.dvlb	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) \neq \emptyset$
10		fourierdlem94.dvub	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) \neq \emptyset$
11		pire	$⊢ π \in ℝ$
12	11	renegcli	$⊢ - π \in ℝ$
13	12	a1i	$⊢ φ \to - π \in ℝ$
14	11	a1i	$⊢ φ \to π \in ℝ$
15		negpilt0	$⊢ - π < 0$
16		pipos	$⊢ 0 < π$
17		0re	$⊢ 0 \in ℝ$
18	12 17 11	lttri	$⊢ (- π < 0 \land 0 < π) \to - π < π$
19	15 16 18	mp2an	$⊢ - π < π$
20	19	a1i	$⊢ φ \to - π < π$
21		picn	$⊢ π \in ℂ$
22	21	2timesi	$⊢ 2 π = π + π$
23	21 21	subnegi	$⊢ π - (- π) = π + π$
24	22 2 23	3eqtr4i	$⊢ T = π - (- π)$
25		ssid	$⊢ ℝ \subseteq ℝ$
26	25	a1i	$⊢ φ \to ℝ \subseteq ℝ$
27		simp2	$⊢ (φ \land x \in ℝ \land k \in ℤ) \to x \in ℝ$
28		zre	$⊢ k \in ℤ \to k \in ℝ$
29	28	3ad2ant3	$⊢ (φ \land x \in ℝ \land k \in ℤ) \to k \in ℝ$
30		2re	$⊢ 2 \in ℝ$
31	30 11	remulcli	$⊢ 2 π \in ℝ$
32	31	a1i	$⊢ φ \to 2 π \in ℝ$
33	2 32	eqeltrid	$⊢ φ \to T \in ℝ$
34	33	adantr	$⊢ (φ \land k \in ℤ) \to T \in ℝ$
35	34	3adant2	$⊢ (φ \land x \in ℝ \land k \in ℤ) \to T \in ℝ$
36	29 35	remulcld	$⊢ (φ \land x \in ℝ \land k \in ℤ) \to k T \in ℝ$
37	27 36	readdcld	$⊢ (φ \land x \in ℝ \land k \in ℤ) \to x + k T \in ℝ$
38		simp1	$⊢ (φ \land x \in ℝ \land k \in ℤ) \to φ$
39		simp3	$⊢ (φ \land x \in ℝ \land k \in ℤ) \to k \in ℤ$
40		ax-resscn	$⊢ ℝ \subseteq ℂ$
41	40	a1i	$⊢ φ \to ℝ \subseteq ℂ$
42	1 41	fssd	$⊢ φ \to F : ℝ ⟶ ℂ$
43	42	adantr	$⊢ (φ \land k \in ℤ) \to F : ℝ ⟶ ℂ$
44	43	adantr	$⊢ ((φ \land k \in ℤ) \land x \in ℝ) \to F : ℝ ⟶ ℂ$
45	34	adantr	$⊢ ((φ \land k \in ℤ) \land x \in ℝ) \to T \in ℝ$
46		simplr	$⊢ ((φ \land k \in ℤ) \land x \in ℝ) \to k \in ℤ$
47		simpr	$⊢ ((φ \land k \in ℤ) \land x \in ℝ) \to x \in ℝ$
48		eleq1w	$⊢ x = y \to (x \in ℝ \leftrightarrow y \in ℝ)$
49	48	anbi2d	$⊢ x = y \to ((φ \land x \in ℝ) \leftrightarrow (φ \land y \in ℝ))$
50		oveq1	$⊢ x = y \to x + T = y + T$
51	50	fveq2d	$⊢ x = y \to F (x + T) = F (y + T)$
52		fveq2	$⊢ x = y \to F (x) = F (y)$
53	51 52	eqeq12d	$⊢ x = y \to (F (x + T) = F (x) \leftrightarrow F (y + T) = F (y))$
54	49 53	imbi12d	$⊢ x = y \to (((φ \land x \in ℝ) \to F (x + T) = F (x)) \leftrightarrow ((φ \land y \in ℝ) \to F (y + T) = F (y)))$
55	54 3	chvarvv	$⊢ (φ \land y \in ℝ) \to F (y + T) = F (y)$
56	55	ad4ant14	$⊢ (((φ \land k \in ℤ) \land x \in ℝ) \land y \in ℝ) \to F (y + T) = F (y)$
57	44 45 46 47 56	fperiodmul	$⊢ ((φ \land k \in ℤ) \land x \in ℝ) \to F (x + k T) = F (x)$
58	38 39 27 57	syl21anc	$⊢ (φ \land x \in ℝ \land k \in ℤ) \to F (x + k T) = F (x)$
59	40	a1i	$⊢ (φ \land i \in (0 ..^M)) \to ℝ \subseteq ℂ$
60		ioossre	$⊢ (Q (i), Q (i + 1)) \subseteq ℝ$
61	60	a1i	$⊢ φ \to (Q (i), Q (i + 1)) \subseteq ℝ$
62	1 61	fssresd	$⊢ φ \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℝ$
63	62 41	fssd	$⊢ φ \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
64	63	adantr	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
65	60	a1i	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℝ$
66	42	adantr	$⊢ (φ \land i \in (0 ..^M)) \to F : ℝ ⟶ ℂ$
67	25	a1i	$⊢ (φ \land i \in (0 ..^M)) \to ℝ \subseteq ℝ$
68		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
69	68	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
70	68 69	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)))}$
71	59 66 67 65 70	syl22anc	$⊢ (φ \land i \in (0 ..^M)) \to ℝ D ({F ↾}_{(Q (i), Q (i + 1))}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((Q (i), Q (i + 1)))}$
72	71	dmeqd	$⊢ (φ \land i \in (0 ..^M)) \to dom {({F ↾}_{(Q (i), Q (i + 1))})}_{ℝ}^{'} = dom ({F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((Q (i), Q (i + 1)))})$
73		ioontr	$⊢ int (topGen (ran (.))) ((Q (i), Q (i + 1))) = (Q (i), Q (i + 1))$
74	73	reseq2i	$⊢ {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((Q (i), Q (i + 1)))} = {F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}$
75	74	dmeqi	$⊢ dom ({F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((Q (i), Q (i + 1)))}) = dom ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))})$
76	75	a1i	$⊢ (φ \land i \in (0 ..^M)) \to dom ({F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ((Q (i), Q (i + 1)))}) = dom ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))})$
77		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)) ⟶ ℂ$
78		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))$
79	8 77 78	3syl	$⊢ (φ \land i \in (0 ..^M)) \to dom ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1))$
80	72 76 79	3eqtrd	$⊢ (φ \land i \in (0 ..^M)) \to dom {({F ↾}_{(Q (i), Q (i + 1))})}_{ℝ}^{'} = (Q (i), Q (i + 1))$
81		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}{⟶} ℂ$
82	59 64 65 80 81	syl31anc	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
83	65 40	sstrdi	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq ℂ$
84	5	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))))$
85	6 84	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))))$
86	7 85	mpbid	$⊢ φ \to (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1)))$
87	86	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
88		elmapi	$⊢ Q \in (ℝ^{(0 \dots M)}) \to Q : (0 \dots M) ⟶ ℝ$
89	87 88	syl	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
90	89	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
91		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
92	91	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
93	90 92	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
94	93	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ^{*}$
95		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
96	95	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
97	90 96	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
98	86	simprrd	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
99	98	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
100	68 94 97 99	lptioo2cn	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in limPt (TopOpen (ℂ_{fld})) ((Q (i), Q (i + 1)))$
101	62	adantr	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℝ$
102	41 42 26	dvbss	$⊢ φ \to dom F_{ℝ}^{'} \subseteq ℝ$
103		dvfre	$⊢ (F : ℝ ⟶ ℝ \land ℝ \subseteq ℝ) \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
104	1 26 103	syl2anc	$⊢ φ \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
105	86	simprd	$⊢ φ \to ((Q (0) = - π \land Q (M) = π) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))$
106	105	simplld	$⊢ φ \to Q (0) = - π$
107	105	simplrd	$⊢ φ \to Q (M) = π$
108	8 77	syl	$⊢ (φ \land i \in (0 ..^M)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
109	97	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ^{*}$
110	68 109 93 99	lptioo1cn	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in limPt (TopOpen (ℂ_{fld})) ((Q (i), Q (i + 1)))$
111	108 83 110 9 68	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))$
112	108 83 100 10 68	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))$
113	28	adantl	$⊢ (φ \land k \in ℤ) \to k \in ℝ$
114	113 34	remulcld	$⊢ (φ \land k \in ℤ) \to k T \in ℝ$
115	43	adantr	$⊢ ((φ \land k \in ℤ) \land t \in ℝ) \to F : ℝ ⟶ ℂ$
116	34	adantr	$⊢ ((φ \land k \in ℤ) \land t \in ℝ) \to T \in ℝ$
117		simplr	$⊢ ((φ \land k \in ℤ) \land t \in ℝ) \to k \in ℤ$
118		simpr	$⊢ ((φ \land k \in ℤ) \land t \in ℝ) \to t \in ℝ$
119	3	ad4ant14	$⊢ (((φ \land k \in ℤ) \land t \in ℝ) \land x \in ℝ) \to F (x + T) = F (x)$
120	115 116 117 118 119	fperiodmul	$⊢ ((φ \land k \in ℤ) \land t \in ℝ) \to F (t + k T) = F (t)$
121		eqid	$⊢ ℝ D F = ℝ D F$
122	43 114 120 121	fperdvper	$⊢ ((φ \land k \in ℤ) \land t \in dom F_{ℝ}^{'}) \to (t + k T \in dom F_{ℝ}^{'} \land F_{ℝ}^{'} (t + k T) = F_{ℝ}^{'} (t))$
123	122	an32s	$⊢ ((φ \land t \in dom F_{ℝ}^{'}) \land k \in ℤ) \to (t + k T \in dom F_{ℝ}^{'} \land F_{ℝ}^{'} (t + k T) = F_{ℝ}^{'} (t))$
124	123	simpld	$⊢ ((φ \land t \in dom F_{ℝ}^{'}) \land k \in ℤ) \to t + k T \in dom F_{ℝ}^{'}$
125	123	simprd	$⊢ ((φ \land t \in dom F_{ℝ}^{'}) \land k \in ℤ) \to F_{ℝ}^{'} (t + k T) = F_{ℝ}^{'} (t)$
126		fveq2	$⊢ j = i \to Q (j) = Q (i)$
127		oveq1	$⊢ j = i \to j + 1 = i + 1$
128	127	fveq2d	$⊢ j = i \to Q (j + 1) = Q (i + 1)$
129	126 128	oveq12d	$⊢ j = i \to (Q (j), Q (j + 1)) = (Q (i), Q (i + 1))$
130	129	cbvmptv	$⊢ (j \in (0 ..^M) ⟼ (Q (j), Q (j + 1))) = (i \in (0 ..^M) ⟼ (Q (i), Q (i + 1)))$
131		eqid	$⊢ (t \in ℝ ⟼ t + ⌊\frac{π - t}{T}⌋ T) = (t \in ℝ ⟼ t + ⌊\frac{π - t}{T}⌋ T)$
132	102 104 13 14 20 24 6 89 106 107 8 111 112 124 125 130 131	fourierdlem71	$⊢ φ \to \exists z \in ℝ \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z$
133	132	adantr	$⊢ (φ \land i \in (0 ..^M)) \to \exists z \in ℝ \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z$
134		nfv	$⊢ Ⅎ t (φ \land i \in (0 ..^M))$
135		nfra1	$⊢ Ⅎ t \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z$
136	134 135	nfan	$⊢ Ⅎ t ((φ \land i \in (0 ..^M)) \land \forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z)$
137	71 74	syl6eq	$⊢ (φ \land i \in (0 ..^M)) \to ℝ D ({F ↾}_{(Q (i), Q (i + 1))}) = {F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}$
138	137	fveq1d	$⊢ (φ \land i \in (0 ..^M)) \to {({F ↾}_{(Q (i), Q (i + 1))})}_{ℝ}^{'} (t) = ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) (t)$
139		fvres	$⊢ t \in (Q (i), Q (i + 1)) \to ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) (t) = F_{ℝ}^{'} (t)$
140	138 139	sylan9eq	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \to {({F ↾}_{(Q (i), Q (i + 1))})}_{ℝ}^{'} (t) = F_{ℝ}^{'} (t)$
141	140	fveq2d	$⊢ ((φ \land i \in (0 ..^M)) \land t \in (Q (i), Q (i + 1))) \to \|{({F ↾}_{(Q (i), Q (i + 1))})}_{ℝ}^{'} (t)\| = \|F_{ℝ}^{'} (t)\|$
142	141	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)\|$
143		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$
144		ssdmres	$⊢ (Q (i), Q (i + 1)) \subseteq dom F_{ℝ}^{'} \leftrightarrow dom ({F_{ℝ}^{'} ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1))$
145	79 144	sylibr	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq dom F_{ℝ}^{'}$
146	145	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_{ℝ}^{'}$
147		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))$
148	146 147	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_{ℝ}^{'}$
149		rspa	$⊢ (\forall t \in dom F_{ℝ}^{'} \|F_{ℝ}^{'} (t)\| \leq z \land t \in dom F_{ℝ}^{'}) \to \|F_{ℝ}^{'} (t)\| \leq z$
150	143 148 149	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$
151	142 150	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$
152	151	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)$
153	136 152	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$
154	153	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)$
155	154	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)$
156	133 155	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$
157	93 97 101 80 156	ioodvbdlimc2	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) \neq \emptyset$
158	64 83 100 157 68	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))$
159		oveq2	$⊢ y = x \to π - y = π - x$
160	159	oveq1d	$⊢ y = x \to \frac{π - y}{T} = \frac{π - x}{T}$
161	160	fveq2d	$⊢ y = x \to ⌊\frac{π - y}{T}⌋ = ⌊\frac{π - x}{T}⌋$
162	161	oveq1d	$⊢ y = x \to ⌊\frac{π - y}{T}⌋ T = ⌊\frac{π - x}{T}⌋ T$
163	162	cbvmptv	$⊢ (y \in ℝ ⟼ ⌊\frac{π - y}{T}⌋ T) = (x \in ℝ ⟼ ⌊\frac{π - x}{T}⌋ T)$
164		id	$⊢ z = x \to z = x$
165		fveq2	$⊢ z = x \to (y \in ℝ ⟼ ⌊\frac{π - y}{T}⌋ T) (z) = (y \in ℝ ⟼ ⌊\frac{π - y}{T}⌋ T) (x)$
166	164 165	oveq12d	$⊢ z = x \to z + (y \in ℝ ⟼ ⌊\frac{π - y}{T}⌋ T) (z) = x + (y \in ℝ ⟼ ⌊\frac{π - y}{T}⌋ T) (x)$
167	166	cbvmptv	$⊢ (z \in ℝ ⟼ z + (y \in ℝ ⟼ ⌊\frac{π - y}{T}⌋ T) (z)) = (x \in ℝ ⟼ x + (y \in ℝ ⟼ ⌊\frac{π - y}{T}⌋ T) (x))$
168	13 14 20 5 24 6 7 26 1 37 58 82 158 4 163 167	fourierdlem49	$⊢ φ \to ({F ↾}_{(−∞, X)}) {lim}_{ℂ} X \neq \emptyset$
169	93 97 101 80 156	ioodvbdlimc1	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) \neq \emptyset$
170	64 83 110 169 68	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))$
171		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)$
172	13 14 20 5 24 6 7 1 37 58 82 170 4 163 167 171	fourierdlem48	$⊢ φ \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset$
173	168 172	jca	$⊢ φ \to (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X \neq \emptyset \land ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset)$

Metamath Proof Explorer

Theorem fourierdlem94

Proof