fourierdlem46

Description: The function F has a limit at the bounds of every interval induced by the partition Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem46.cn	$⊢ φ \to F : dom F \underset{cn}{⟶} ℂ$
	fourierdlem46.rlim	$⊢ (φ \land x \in ([- π, π) ∖ dom F)) \to ({F ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
	fourierdlem46.llim	$⊢ (φ \land x \in ((- π, π] ∖ dom F)) \to ({F ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
	fourierdlem46.qiso	$⊢ φ \to Q {Isom}_{<, <} ((0 \dots M), H)$
	fourierdlem46.qf	$⊢ φ \to Q : (0 \dots M) ⟶ H$
	fourierdlem46.i	$⊢ φ \to I \in (0 ..^M)$
	fourierdlem46.10	$⊢ φ \to Q (I) < Q (I + 1)$
	fourierdlem46.qiss	$⊢ φ \to (Q (I), Q (I + 1)) \subseteq (- π, π)$
	fourierdlem46.c	$⊢ φ \to C \in ℝ$
	fourierdlem46.h	$⊢ H = \{- π, π, C\} \cup ([- π, π] ∖ dom F)$
	fourierdlem46.ranq	$⊢ φ \to ran Q = H$
Assertion	fourierdlem46	$⊢ φ \to (({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I) \neq \emptyset \land ({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1) \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem46.cn	$⊢ φ \to F : dom F \underset{cn}{⟶} ℂ$
2		fourierdlem46.rlim	$⊢ (φ \land x \in ([- π, π) ∖ dom F)) \to ({F ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
3		fourierdlem46.llim	$⊢ (φ \land x \in ((- π, π] ∖ dom F)) \to ({F ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
4		fourierdlem46.qiso	$⊢ φ \to Q {Isom}_{<, <} ((0 \dots M), H)$
5		fourierdlem46.qf	$⊢ φ \to Q : (0 \dots M) ⟶ H$
6		fourierdlem46.i	$⊢ φ \to I \in (0 ..^M)$
7		fourierdlem46.10	$⊢ φ \to Q (I) < Q (I + 1)$
8		fourierdlem46.qiss	$⊢ φ \to (Q (I), Q (I + 1)) \subseteq (- π, π)$
9		fourierdlem46.c	$⊢ φ \to C \in ℝ$
10		fourierdlem46.h	$⊢ H = \{- π, π, C\} \cup ([- π, π] ∖ dom F)$
11		fourierdlem46.ranq	$⊢ φ \to ran Q = H$
12		pire	$⊢ π \in ℝ$
13	12	a1i	$⊢ φ \to π \in ℝ$
14	13	renegcld	$⊢ φ \to - π \in ℝ$
15		tpssi	$⊢ (- π \in ℝ \land π \in ℝ \land C \in ℝ) \to \{- π, π, C\} \subseteq ℝ$
16	14 13 9 15	syl3anc	$⊢ φ \to \{- π, π, C\} \subseteq ℝ$
17	14 13	iccssred	$⊢ φ \to [- π, π] \subseteq ℝ$
18	17	ssdifssd	$⊢ φ \to [- π, π] ∖ dom F \subseteq ℝ$
19	16 18	unssd	$⊢ φ \to \{- π, π, C\} \cup ([- π, π] ∖ dom F) \subseteq ℝ$
20	10 19	eqsstrid	$⊢ φ \to H \subseteq ℝ$
21		elfzofz	$⊢ I \in (0 ..^M) \to I \in (0 \dots M)$
22	6 21	syl	$⊢ φ \to I \in (0 \dots M)$
23	5 22	ffvelrnd	$⊢ φ \to Q (I) \in H$
24	20 23	sseldd	$⊢ φ \to Q (I) \in ℝ$
25	24	adantr	$⊢ (φ \land Q (I) \in dom F) \to Q (I) \in ℝ$
26		fzofzp1	$⊢ I \in (0 ..^M) \to I + 1 \in (0 \dots M)$
27	6 26	syl	$⊢ φ \to I + 1 \in (0 \dots M)$
28	5 27	ffvelrnd	$⊢ φ \to Q (I + 1) \in H$
29	20 28	sseldd	$⊢ φ \to Q (I + 1) \in ℝ$
30	29	rexrd	$⊢ φ \to Q (I + 1) \in ℝ^{*}$
31	30	adantr	$⊢ (φ \land Q (I) \in dom F) \to Q (I + 1) \in ℝ^{*}$
32	7	adantr	$⊢ (φ \land Q (I) \in dom F) \to Q (I) < Q (I + 1)$
33		simpr	$⊢ (Q (I) \in dom F \land x = Q (I)) \to x = Q (I)$
34		simpl	$⊢ (Q (I) \in dom F \land x = Q (I)) \to Q (I) \in dom F$
35	33 34	eqeltrd	$⊢ (Q (I) \in dom F \land x = Q (I)) \to x \in dom F$
36	35	adantll	$⊢ ((φ \land Q (I) \in dom F) \land x = Q (I)) \to x \in dom F$
37	36	adantlr	$⊢ (((φ \land Q (I) \in dom F) \land x \in [Q (I), Q (I + 1))) \land x = Q (I)) \to x \in dom F$
38		ssun2	$⊢ [- π, π] ∖ dom F \subseteq \{- π, π, C\} \cup ([- π, π] ∖ dom F)$
39	38 10	sseqtrri	$⊢ [- π, π] ∖ dom F \subseteq H$
40		ioossicc	$⊢ (- π, π) \subseteq [- π, π]$
41	8 40	sstrdi	$⊢ φ \to (Q (I), Q (I + 1)) \subseteq [- π, π]$
42	41	sselda	$⊢ (φ \land x \in (Q (I), Q (I + 1))) \to x \in [- π, π]$
43	42	adantr	$⊢ ((φ \land x \in (Q (I), Q (I + 1))) \land \neg x \in dom F) \to x \in [- π, π]$
44		simpr	$⊢ ((φ \land x \in (Q (I), Q (I + 1))) \land \neg x \in dom F) \to \neg x \in dom F$
45	43 44	eldifd	$⊢ ((φ \land x \in (Q (I), Q (I + 1))) \land \neg x \in dom F) \to x \in ([- π, π] ∖ dom F)$
46	39 45	sseldi	$⊢ ((φ \land x \in (Q (I), Q (I + 1))) \land \neg x \in dom F) \to x \in H$
47	11	eqcomd	$⊢ φ \to H = ran Q$
48	47	ad2antrr	$⊢ ((φ \land x \in (Q (I), Q (I + 1))) \land \neg x \in dom F) \to H = ran Q$
49	46 48	eleqtrd	$⊢ ((φ \land x \in (Q (I), Q (I + 1))) \land \neg x \in dom F) \to x \in ran Q$
50		simpr	$⊢ (φ \land x \in ran Q) \to x \in ran Q$
51		ffn	$⊢ Q : (0 \dots M) ⟶ H \to Q Fn (0 \dots M)$
52	5 51	syl	$⊢ φ \to Q Fn (0 \dots M)$
53	52	adantr	$⊢ (φ \land x \in ran Q) \to Q Fn (0 \dots M)$
54		fvelrnb	$⊢ Q Fn (0 \dots M) \to (x \in ran Q \leftrightarrow \exists j \in (0 \dots M) Q (j) = x)$
55	53 54	syl	$⊢ (φ \land x \in ran Q) \to (x \in ran Q \leftrightarrow \exists j \in (0 \dots M) Q (j) = x)$
56	50 55	mpbid	$⊢ (φ \land x \in ran Q) \to \exists j \in (0 \dots M) Q (j) = x$
57	56	adantlr	$⊢ ((φ \land x \in (Q (I), Q (I + 1))) \land x \in ran Q) \to \exists j \in (0 \dots M) Q (j) = x$
58		elfzelz	$⊢ j \in (0 \dots M) \to j \in ℤ$
59	58	ad2antlr	$⊢ ((((φ \land x \in (Q (I), Q (I + 1))) \land x \in ran Q) \land j \in (0 \dots M)) \land Q (j) = x) \to j \in ℤ$
60		simplll	$⊢ (((φ \land x \in (Q (I), Q (I + 1))) \land j \in (0 \dots M)) \land Q (j) = x) \to φ$
61		simplr	$⊢ (((φ \land x \in (Q (I), Q (I + 1))) \land j \in (0 \dots M)) \land Q (j) = x) \to j \in (0 \dots M)$
62		simpr	$⊢ ((φ \land x \in (Q (I), Q (I + 1))) \land Q (j) = x) \to Q (j) = x$
63		simplr	$⊢ ((φ \land x \in (Q (I), Q (I + 1))) \land Q (j) = x) \to x \in (Q (I), Q (I + 1))$
64	62 63	eqeltrd	$⊢ ((φ \land x \in (Q (I), Q (I + 1))) \land Q (j) = x) \to Q (j) \in (Q (I), Q (I + 1))$
65	64	adantlr	$⊢ (((φ \land x \in (Q (I), Q (I + 1))) \land j \in (0 \dots M)) \land Q (j) = x) \to Q (j) \in (Q (I), Q (I + 1))$
66		elfzoelz	$⊢ I \in (0 ..^M) \to I \in ℤ$
67	6 66	syl	$⊢ φ \to I \in ℤ$
68	67	ad2antrr	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) \in (Q (I), Q (I + 1))) \to I \in ℤ$
69	24	rexrd	$⊢ φ \to Q (I) \in ℝ^{*}$
70	69	ad2antrr	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) \in (Q (I), Q (I + 1))) \to Q (I) \in ℝ^{*}$
71	30	ad2antrr	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) \in (Q (I), Q (I + 1))) \to Q (I + 1) \in ℝ^{*}$
72		simpr	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) \in (Q (I), Q (I + 1))) \to Q (j) \in (Q (I), Q (I + 1))$
73		ioogtlb	$⊢ (Q (I) \in ℝ^{} \land Q (I + 1) \in ℝ^{} \land Q (j) \in (Q (I), Q (I + 1))) \to Q (I) < Q (j)$
74	70 71 72 73	syl3anc	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) \in (Q (I), Q (I + 1))) \to Q (I) < Q (j)$
75	4	ad2antrr	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) \in (Q (I), Q (I + 1))) \to Q {Isom}_{<, <} ((0 \dots M), H)$
76	22	ad2antrr	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) \in (Q (I), Q (I + 1))) \to I \in (0 \dots M)$
77		simplr	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) \in (Q (I), Q (I + 1))) \to j \in (0 \dots M)$
78		isorel	$⊢ (Q {Isom}_{<, <} ((0 \dots M), H) \land (I \in (0 \dots M) \land j \in (0 \dots M))) \to (I < j \leftrightarrow Q (I) < Q (j))$
79	75 76 77 78	syl12anc	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) \in (Q (I), Q (I + 1))) \to (I < j \leftrightarrow Q (I) < Q (j))$
80	74 79	mpbird	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) \in (Q (I), Q (I + 1))) \to I < j$
81		iooltub	$⊢ (Q (I) \in ℝ^{} \land Q (I + 1) \in ℝ^{} \land Q (j) \in (Q (I), Q (I + 1))) \to Q (j) < Q (I + 1)$
82	70 71 72 81	syl3anc	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) \in (Q (I), Q (I + 1))) \to Q (j) < Q (I + 1)$
83	27	ad2antrr	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) \in (Q (I), Q (I + 1))) \to I + 1 \in (0 \dots M)$
84		isorel	$⊢ (Q {Isom}_{<, <} ((0 \dots M), H) \land (j \in (0 \dots M) \land I + 1 \in (0 \dots M))) \to (j < I + 1 \leftrightarrow Q (j) < Q (I + 1))$
85	75 77 83 84	syl12anc	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) \in (Q (I), Q (I + 1))) \to (j < I + 1 \leftrightarrow Q (j) < Q (I + 1))$
86	82 85	mpbird	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) \in (Q (I), Q (I + 1))) \to j < I + 1$
87		btwnnz	$⊢ (I \in ℤ \land I < j \land j < I + 1) \to \neg j \in ℤ$
88	68 80 86 87	syl3anc	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) \in (Q (I), Q (I + 1))) \to \neg j \in ℤ$
89	60 61 65 88	syl21anc	$⊢ (((φ \land x \in (Q (I), Q (I + 1))) \land j \in (0 \dots M)) \land Q (j) = x) \to \neg j \in ℤ$
90	89	adantllr	$⊢ ((((φ \land x \in (Q (I), Q (I + 1))) \land x \in ran Q) \land j \in (0 \dots M)) \land Q (j) = x) \to \neg j \in ℤ$
91	59 90	pm2.65da	$⊢ (((φ \land x \in (Q (I), Q (I + 1))) \land x \in ran Q) \land j \in (0 \dots M)) \to \neg Q (j) = x$
92	91	nrexdv	$⊢ ((φ \land x \in (Q (I), Q (I + 1))) \land x \in ran Q) \to \neg \exists j \in (0 \dots M) Q (j) = x$
93	57 92	pm2.65da	$⊢ (φ \land x \in (Q (I), Q (I + 1))) \to \neg x \in ran Q$
94	93	adantr	$⊢ ((φ \land x \in (Q (I), Q (I + 1))) \land \neg x \in dom F) \to \neg x \in ran Q$
95	49 94	condan	$⊢ (φ \land x \in (Q (I), Q (I + 1))) \to x \in dom F$
96	95	ralrimiva	$⊢ φ \to \forall x \in (Q (I), Q (I + 1)) x \in dom F$
97		dfss3	$⊢ (Q (I), Q (I + 1)) \subseteq dom F \leftrightarrow \forall x \in (Q (I), Q (I + 1)) x \in dom F$
98	96 97	sylibr	$⊢ φ \to (Q (I), Q (I + 1)) \subseteq dom F$
99	98	ad2antrr	$⊢ ((φ \land x \in [Q (I), Q (I + 1))) \land \neg x = Q (I)) \to (Q (I), Q (I + 1)) \subseteq dom F$
100	69	ad2antrr	$⊢ ((φ \land x \in [Q (I), Q (I + 1))) \land \neg x = Q (I)) \to Q (I) \in ℝ^{*}$
101	30	ad2antrr	$⊢ ((φ \land x \in [Q (I), Q (I + 1))) \land \neg x = Q (I)) \to Q (I + 1) \in ℝ^{*}$
102		icossre	$⊢ (Q (I) \in ℝ \land Q (I + 1) \in ℝ^{*}) \to [Q (I), Q (I + 1)) \subseteq ℝ$
103	24 30 102	syl2anc	$⊢ φ \to [Q (I), Q (I + 1)) \subseteq ℝ$
104	103	sselda	$⊢ (φ \land x \in [Q (I), Q (I + 1))) \to x \in ℝ$
105	104	adantr	$⊢ ((φ \land x \in [Q (I), Q (I + 1))) \land \neg x = Q (I)) \to x \in ℝ$
106	24	ad2antrr	$⊢ ((φ \land x \in [Q (I), Q (I + 1))) \land \neg x = Q (I)) \to Q (I) \in ℝ$
107	69	adantr	$⊢ (φ \land x \in [Q (I), Q (I + 1))) \to Q (I) \in ℝ^{*}$
108	30	adantr	$⊢ (φ \land x \in [Q (I), Q (I + 1))) \to Q (I + 1) \in ℝ^{*}$
109		simpr	$⊢ (φ \land x \in [Q (I), Q (I + 1))) \to x \in [Q (I), Q (I + 1))$
110		icogelb	$⊢ (Q (I) \in ℝ^{} \land Q (I + 1) \in ℝ^{} \land x \in [Q (I), Q (I + 1))) \to Q (I) \leq x$
111	107 108 109 110	syl3anc	$⊢ (φ \land x \in [Q (I), Q (I + 1))) \to Q (I) \leq x$
112	111	adantr	$⊢ ((φ \land x \in [Q (I), Q (I + 1))) \land \neg x = Q (I)) \to Q (I) \leq x$
113		neqne	$⊢ \neg x = Q (I) \to x \neq Q (I)$
114	113	adantl	$⊢ ((φ \land x \in [Q (I), Q (I + 1))) \land \neg x = Q (I)) \to x \neq Q (I)$
115	106 105 112 114	leneltd	$⊢ ((φ \land x \in [Q (I), Q (I + 1))) \land \neg x = Q (I)) \to Q (I) < x$
116		icoltub	$⊢ (Q (I) \in ℝ^{} \land Q (I + 1) \in ℝ^{} \land x \in [Q (I), Q (I + 1))) \to x < Q (I + 1)$
117	107 108 109 116	syl3anc	$⊢ (φ \land x \in [Q (I), Q (I + 1))) \to x < Q (I + 1)$
118	117	adantr	$⊢ ((φ \land x \in [Q (I), Q (I + 1))) \land \neg x = Q (I)) \to x < Q (I + 1)$
119	100 101 105 115 118	eliood	$⊢ ((φ \land x \in [Q (I), Q (I + 1))) \land \neg x = Q (I)) \to x \in (Q (I), Q (I + 1))$
120	99 119	sseldd	$⊢ ((φ \land x \in [Q (I), Q (I + 1))) \land \neg x = Q (I)) \to x \in dom F$
121	120	adantllr	$⊢ (((φ \land Q (I) \in dom F) \land x \in [Q (I), Q (I + 1))) \land \neg x = Q (I)) \to x \in dom F$
122	37 121	pm2.61dan	$⊢ ((φ \land Q (I) \in dom F) \land x \in [Q (I), Q (I + 1))) \to x \in dom F$
123	122	ralrimiva	$⊢ (φ \land Q (I) \in dom F) \to \forall x \in [Q (I), Q (I + 1)) x \in dom F$
124		dfss3	$⊢ [Q (I), Q (I + 1)) \subseteq dom F \leftrightarrow \forall x \in [Q (I), Q (I + 1)) x \in dom F$
125	123 124	sylibr	$⊢ (φ \land Q (I) \in dom F) \to [Q (I), Q (I + 1)) \subseteq dom F$
126	1	adantr	$⊢ (φ \land Q (I) \in dom F) \to F : dom F \underset{cn}{⟶} ℂ$
127		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}{⟶} ℂ)$
128	125 126 127	sylc	$⊢ (φ \land Q (I) \in dom F) \to ({F ↾}_{[Q (I), Q (I + 1))}) : [Q (I), Q (I + 1)) \underset{cn}{⟶} ℂ$
129	25 31 32 128	icocncflimc	$⊢ (φ \land Q (I) \in dom F) \to ({F ↾}_{[Q (I), Q (I + 1))}) (Q (I)) \in (({({F ↾}_{[Q (I), Q (I + 1))}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I))$
130	24	leidd	$⊢ φ \to Q (I) \leq Q (I)$
131	69 30 69 130 7	elicod	$⊢ φ \to Q (I) \in [Q (I), Q (I + 1))$
132		fvres	$⊢ Q (I) \in [Q (I), Q (I + 1)) \to ({F ↾}_{[Q (I), Q (I + 1))}) (Q (I)) = F (Q (I))$
133	131 132	syl	$⊢ φ \to ({F ↾}_{[Q (I), Q (I + 1))}) (Q (I)) = F (Q (I))$
134	133	eqcomd	$⊢ φ \to F (Q (I)) = ({F ↾}_{[Q (I), Q (I + 1))}) (Q (I))$
135	134	adantr	$⊢ (φ \land Q (I) \in dom F) \to F (Q (I)) = ({F ↾}_{[Q (I), Q (I + 1))}) (Q (I))$
136		ioossico	$⊢ (Q (I), Q (I + 1)) \subseteq [Q (I), Q (I + 1))$
137	136	a1i	$⊢ (φ \land Q (I) \in dom F) \to (Q (I), Q (I + 1)) \subseteq [Q (I), Q (I + 1))$
138	137	resabs1d	$⊢ (φ \land Q (I) \in dom F) \to {({F ↾}_{[Q (I), Q (I + 1))}) ↾}_{(Q (I), Q (I + 1))} = {F ↾}_{(Q (I), Q (I + 1))}$
139	138	eqcomd	$⊢ (φ \land Q (I) \in dom F) \to {F ↾}_{(Q (I), Q (I + 1))} = {({F ↾}_{[Q (I), Q (I + 1))}) ↾}_{(Q (I), Q (I + 1))}$
140	139	oveq1d	$⊢ (φ \land Q (I) \in dom F) \to ({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I) = ({({F ↾}_{[Q (I), Q (I + 1))}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I)$
141	129 135 140	3eltr4d	$⊢ (φ \land Q (I) \in dom F) \to F (Q (I)) \in (({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I))$
142	141	ne0d	$⊢ (φ \land Q (I) \in dom F) \to ({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I) \neq \emptyset$
143		pnfxr	$⊢ +∞ \in ℝ^{*}$
144	143	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
145	29	ltpnfd	$⊢ φ \to Q (I + 1) < +∞$
146	30 144 145	xrltled	$⊢ φ \to Q (I + 1) \leq +∞$
147		iooss2	$⊢ (+∞ \in ℝ^{*} \land Q (I + 1) \leq +∞) \to (Q (I), Q (I + 1)) \subseteq (Q (I), +∞)$
148	143 146 147	sylancr	$⊢ φ \to (Q (I), Q (I + 1)) \subseteq (Q (I), +∞)$
149	148	resabs1d	$⊢ φ \to {({F ↾}_{(Q (I), +∞)}) ↾}_{(Q (I), Q (I + 1))} = {F ↾}_{(Q (I), Q (I + 1))}$
150	149	oveq1d	$⊢ φ \to ({({F ↾}_{(Q (I), +∞)}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I) = ({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I)$
151	150	eqcomd	$⊢ φ \to ({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I) = ({({F ↾}_{(Q (I), +∞)}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I)$
152	151	adantr	$⊢ (φ \land \neg Q (I) \in dom F) \to ({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I) = ({({F ↾}_{(Q (I), +∞)}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I)$
153		limcresi	$⊢ ({F ↾}_{(Q (I), +∞)}) {lim}_{ℂ} Q (I) \subseteq ({({F ↾}_{(Q (I), +∞)}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I)$
154	24	adantr	$⊢ (φ \land \neg Q (I) \in dom F) \to Q (I) \in ℝ$
155		simpl	$⊢ (φ \land \neg Q (I) \in dom F) \to φ$
156	12	renegcli	$⊢ - π \in ℝ$
157	156	rexri	$⊢ - π \in ℝ^{*}$
158	157	a1i	$⊢ φ \to - π \in ℝ^{*}$
159	12	rexri	$⊢ π \in ℝ^{*}$
160	159	a1i	$⊢ φ \to π \in ℝ^{*}$
161	14 13 24 29 7 8	fourierdlem10	$⊢ φ \to (- π \leq Q (I) \land Q (I + 1) \leq π)$
162	161	simpld	$⊢ φ \to - π \leq Q (I)$
163	161	simprd	$⊢ φ \to Q (I + 1) \leq π$
164	24 29 13 7 163	ltletrd	$⊢ φ \to Q (I) < π$
165	158 160 69 162 164	elicod	$⊢ φ \to Q (I) \in [- π, π)$
166	165	adantr	$⊢ (φ \land \neg Q (I) \in dom F) \to Q (I) \in [- π, π)$
167		simpr	$⊢ (φ \land \neg Q (I) \in dom F) \to \neg Q (I) \in dom F$
168	166 167	eldifd	$⊢ (φ \land \neg Q (I) \in dom F) \to Q (I) \in ([- π, π) ∖ dom F)$
169	155 168	jca	$⊢ (φ \land \neg Q (I) \in dom F) \to (φ \land Q (I) \in ([- π, π) ∖ dom F))$
170		eleq1	$⊢ x = Q (I) \to (x \in ([- π, π) ∖ dom F) \leftrightarrow Q (I) \in ([- π, π) ∖ dom F))$
171	170	anbi2d	$⊢ x = Q (I) \to ((φ \land x \in ([- π, π) ∖ dom F)) \leftrightarrow (φ \land Q (I) \in ([- π, π) ∖ dom F)))$
172		oveq1	$⊢ x = Q (I) \to (x, +∞) = (Q (I), +∞)$
173	172	reseq2d	$⊢ x = Q (I) \to {F ↾}_{(x, +∞)} = {F ↾}_{(Q (I), +∞)}$
174		id	$⊢ x = Q (I) \to x = Q (I)$
175	173 174	oveq12d	$⊢ x = Q (I) \to ({F ↾}_{(x, +∞)}) {lim}_{ℂ} x = ({F ↾}_{(Q (I), +∞)}) {lim}_{ℂ} Q (I)$
176	175	neeq1d	$⊢ x = Q (I) \to (({F ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset \leftrightarrow ({F ↾}_{(Q (I), +∞)}) {lim}_{ℂ} Q (I) \neq \emptyset)$
177	171 176	imbi12d	$⊢ x = Q (I) \to (((φ \land x \in ([- π, π) ∖ dom F)) \to ({F ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset) \leftrightarrow ((φ \land Q (I) \in ([- π, π) ∖ dom F)) \to ({F ↾}_{(Q (I), +∞)}) {lim}_{ℂ} Q (I) \neq \emptyset))$
178	177 2	vtoclg	$⊢ Q (I) \in ℝ \to ((φ \land Q (I) \in ([- π, π) ∖ dom F)) \to ({F ↾}_{(Q (I), +∞)}) {lim}_{ℂ} Q (I) \neq \emptyset)$
179	154 169 178	sylc	$⊢ (φ \land \neg Q (I) \in dom F) \to ({F ↾}_{(Q (I), +∞)}) {lim}_{ℂ} Q (I) \neq \emptyset$
180		ssn0	$⊢ (({F ↾}_{(Q (I), +∞)}) {lim}_{ℂ} Q (I) \subseteq ({({F ↾}_{(Q (I), +∞)}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I) \land ({F ↾}_{(Q (I), +∞)}) {lim}_{ℂ} Q (I) \neq \emptyset) \to ({({F ↾}_{(Q (I), +∞)}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I) \neq \emptyset$
181	153 179 180	sylancr	$⊢ (φ \land \neg Q (I) \in dom F) \to ({({F ↾}_{(Q (I), +∞)}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I) \neq \emptyset$
182	152 181	eqnetrd	$⊢ (φ \land \neg Q (I) \in dom F) \to ({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I) \neq \emptyset$
183	142 182	pm2.61dan	$⊢ φ \to ({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I) \neq \emptyset$
184	69	adantr	$⊢ (φ \land Q (I + 1) \in dom F) \to Q (I) \in ℝ^{*}$
185	29	adantr	$⊢ (φ \land Q (I + 1) \in dom F) \to Q (I + 1) \in ℝ$
186	7	adantr	$⊢ (φ \land Q (I + 1) \in dom F) \to Q (I) < Q (I + 1)$
187		simpr	$⊢ (Q (I + 1) \in dom F \land x = Q (I + 1)) \to x = Q (I + 1)$
188		simpl	$⊢ (Q (I + 1) \in dom F \land x = Q (I + 1)) \to Q (I + 1) \in dom F$
189	187 188	eqeltrd	$⊢ (Q (I + 1) \in dom F \land x = Q (I + 1)) \to x \in dom F$
190	189	adantll	$⊢ ((φ \land Q (I + 1) \in dom F) \land x = Q (I + 1)) \to x \in dom F$
191	190	adantlr	$⊢ (((φ \land Q (I + 1) \in dom F) \land x \in (Q (I), Q (I + 1)]) \land x = Q (I + 1)) \to x \in dom F$
192	98	ad2antrr	$⊢ ((φ \land x \in (Q (I), Q (I + 1)]) \land \neg x = Q (I + 1)) \to (Q (I), Q (I + 1)) \subseteq dom F$
193	69	ad2antrr	$⊢ ((φ \land x \in (Q (I), Q (I + 1)]) \land \neg x = Q (I + 1)) \to Q (I) \in ℝ^{*}$
194	30	ad2antrr	$⊢ ((φ \land x \in (Q (I), Q (I + 1)]) \land \neg x = Q (I + 1)) \to Q (I + 1) \in ℝ^{*}$
195	69	adantr	$⊢ (φ \land x \in (Q (I), Q (I + 1)]) \to Q (I) \in ℝ^{*}$
196	29	adantr	$⊢ (φ \land x \in (Q (I), Q (I + 1)]) \to Q (I + 1) \in ℝ$
197		iocssre	$⊢ (Q (I) \in ℝ^{*} \land Q (I + 1) \in ℝ) \to (Q (I), Q (I + 1)] \subseteq ℝ$
198	195 196 197	syl2anc	$⊢ (φ \land x \in (Q (I), Q (I + 1)]) \to (Q (I), Q (I + 1)] \subseteq ℝ$
199		simpr	$⊢ (φ \land x \in (Q (I), Q (I + 1)]) \to x \in (Q (I), Q (I + 1)]$
200	198 199	sseldd	$⊢ (φ \land x \in (Q (I), Q (I + 1)]) \to x \in ℝ$
201	200	adantr	$⊢ ((φ \land x \in (Q (I), Q (I + 1)]) \land \neg x = Q (I + 1)) \to x \in ℝ$
202	30	adantr	$⊢ (φ \land x \in (Q (I), Q (I + 1)]) \to Q (I + 1) \in ℝ^{*}$
203		iocgtlb	$⊢ (Q (I) \in ℝ^{} \land Q (I + 1) \in ℝ^{} \land x \in (Q (I), Q (I + 1)]) \to Q (I) < x$
204	195 202 199 203	syl3anc	$⊢ (φ \land x \in (Q (I), Q (I + 1)]) \to Q (I) < x$
205	204	adantr	$⊢ ((φ \land x \in (Q (I), Q (I + 1)]) \land \neg x = Q (I + 1)) \to Q (I) < x$
206	29	ad2antrr	$⊢ ((φ \land x \in (Q (I), Q (I + 1)]) \land \neg x = Q (I + 1)) \to Q (I + 1) \in ℝ$
207		iocleub	$⊢ (Q (I) \in ℝ^{} \land Q (I + 1) \in ℝ^{} \land x \in (Q (I), Q (I + 1)]) \to x \leq Q (I + 1)$
208	195 202 199 207	syl3anc	$⊢ (φ \land x \in (Q (I), Q (I + 1)]) \to x \leq Q (I + 1)$
209	208	adantr	$⊢ ((φ \land x \in (Q (I), Q (I + 1)]) \land \neg x = Q (I + 1)) \to x \leq Q (I + 1)$
210		neqne	$⊢ \neg x = Q (I + 1) \to x \neq Q (I + 1)$
211	210	necomd	$⊢ \neg x = Q (I + 1) \to Q (I + 1) \neq x$
212	211	adantl	$⊢ ((φ \land x \in (Q (I), Q (I + 1)]) \land \neg x = Q (I + 1)) \to Q (I + 1) \neq x$
213	201 206 209 212	leneltd	$⊢ ((φ \land x \in (Q (I), Q (I + 1)]) \land \neg x = Q (I + 1)) \to x < Q (I + 1)$
214	193 194 201 205 213	eliood	$⊢ ((φ \land x \in (Q (I), Q (I + 1)]) \land \neg x = Q (I + 1)) \to x \in (Q (I), Q (I + 1))$
215	192 214	sseldd	$⊢ ((φ \land x \in (Q (I), Q (I + 1)]) \land \neg x = Q (I + 1)) \to x \in dom F$
216	215	adantllr	$⊢ (((φ \land Q (I + 1) \in dom F) \land x \in (Q (I), Q (I + 1)]) \land \neg x = Q (I + 1)) \to x \in dom F$
217	191 216	pm2.61dan	$⊢ ((φ \land Q (I + 1) \in dom F) \land x \in (Q (I), Q (I + 1)]) \to x \in dom F$
218	217	ralrimiva	$⊢ (φ \land Q (I + 1) \in dom F) \to \forall x \in (Q (I), Q (I + 1)] x \in dom F$
219		dfss3	$⊢ (Q (I), Q (I + 1)] \subseteq dom F \leftrightarrow \forall x \in (Q (I), Q (I + 1)] x \in dom F$
220	218 219	sylibr	$⊢ (φ \land Q (I + 1) \in dom F) \to (Q (I), Q (I + 1)] \subseteq dom F$
221	1	adantr	$⊢ (φ \land Q (I + 1) \in dom F) \to F : dom F \underset{cn}{⟶} ℂ$
222		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}{⟶} ℂ)$
223	220 221 222	sylc	$⊢ (φ \land Q (I + 1) \in dom F) \to ({F ↾}_{(Q (I), Q (I + 1)]}) : (Q (I), Q (I + 1)] \underset{cn}{⟶} ℂ$
224	184 185 186 223	ioccncflimc	$⊢ (φ \land Q (I + 1) \in dom F) \to ({F ↾}_{(Q (I), Q (I + 1)]}) (Q (I + 1)) \in (({({F ↾}_{(Q (I), Q (I + 1)]}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1))$
225	29	leidd	$⊢ φ \to Q (I + 1) \leq Q (I + 1)$
226	69 30 30 7 225	eliocd	$⊢ φ \to Q (I + 1) \in (Q (I), Q (I + 1)]$
227		fvres	$⊢ Q (I + 1) \in (Q (I), Q (I + 1)] \to ({F ↾}_{(Q (I), Q (I + 1)]}) (Q (I + 1)) = F (Q (I + 1))$
228	226 227	syl	$⊢ φ \to ({F ↾}_{(Q (I), Q (I + 1)]}) (Q (I + 1)) = F (Q (I + 1))$
229	228	eqcomd	$⊢ φ \to F (Q (I + 1)) = ({F ↾}_{(Q (I), Q (I + 1)]}) (Q (I + 1))$
230		ioossioc	$⊢ (Q (I), Q (I + 1)) \subseteq (Q (I), Q (I + 1)]$
231		resabs1	$⊢ (Q (I), Q (I + 1)) \subseteq (Q (I), Q (I + 1)] \to {({F ↾}_{(Q (I), Q (I + 1)]}) ↾}_{(Q (I), Q (I + 1))} = {F ↾}_{(Q (I), Q (I + 1))}$
232	230 231	ax-mp	$⊢ {({F ↾}_{(Q (I), Q (I + 1)]}) ↾}_{(Q (I), Q (I + 1))} = {F ↾}_{(Q (I), Q (I + 1))}$
233	232	eqcomi	$⊢ {F ↾}_{(Q (I), Q (I + 1))} = {({F ↾}_{(Q (I), Q (I + 1)]}) ↾}_{(Q (I), Q (I + 1))}$
234	233	oveq1i	$⊢ ({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1) = ({({F ↾}_{(Q (I), Q (I + 1)]}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1)$
235	234	a1i	$⊢ φ \to ({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1) = ({({F ↾}_{(Q (I), Q (I + 1)]}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1)$
236	229 235	eleq12d	$⊢ φ \to (F (Q (I + 1)) \in (({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1)) \leftrightarrow ({F ↾}_{(Q (I), Q (I + 1)]}) (Q (I + 1)) \in (({({F ↾}_{(Q (I), Q (I + 1)]}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1)))$
237	236	adantr	$⊢ (φ \land Q (I + 1) \in dom F) \to (F (Q (I + 1)) \in (({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1)) \leftrightarrow ({F ↾}_{(Q (I), Q (I + 1)]}) (Q (I + 1)) \in (({({F ↾}_{(Q (I), Q (I + 1)]}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1)))$
238	224 237	mpbird	$⊢ (φ \land Q (I + 1) \in dom F) \to F (Q (I + 1)) \in (({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1))$
239	238	ne0d	$⊢ (φ \land Q (I + 1) \in dom F) \to ({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1) \neq \emptyset$
240		mnfxr	$⊢ −∞ \in ℝ^{*}$
241	240	a1i	$⊢ φ \to −∞ \in ℝ^{*}$
242	24	mnfltd	$⊢ φ \to −∞ < Q (I)$
243	241 69 242	xrltled	$⊢ φ \to −∞ \leq Q (I)$
244		iooss1	$⊢ (−∞ \in ℝ^{*} \land −∞ \leq Q (I)) \to (Q (I), Q (I + 1)) \subseteq (−∞, Q (I + 1))$
245	240 243 244	sylancr	$⊢ φ \to (Q (I), Q (I + 1)) \subseteq (−∞, Q (I + 1))$
246	245	resabs1d	$⊢ φ \to {({F ↾}_{(−∞, Q (I + 1))}) ↾}_{(Q (I), Q (I + 1))} = {F ↾}_{(Q (I), Q (I + 1))}$
247	246	eqcomd	$⊢ φ \to {F ↾}_{(Q (I), Q (I + 1))} = {({F ↾}_{(−∞, Q (I + 1))}) ↾}_{(Q (I), Q (I + 1))}$
248	247	adantr	$⊢ (φ \land \neg Q (I + 1) \in dom F) \to {F ↾}_{(Q (I), Q (I + 1))} = {({F ↾}_{(−∞, Q (I + 1))}) ↾}_{(Q (I), Q (I + 1))}$
249	248	oveq1d	$⊢ (φ \land \neg Q (I + 1) \in dom F) \to ({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1) = ({({F ↾}_{(−∞, Q (I + 1))}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1)$
250		limcresi	$⊢ ({F ↾}_{(−∞, Q (I + 1))}) {lim}_{ℂ} Q (I + 1) \subseteq ({({F ↾}_{(−∞, Q (I + 1))}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1)$
251	29	adantr	$⊢ (φ \land \neg Q (I + 1) \in dom F) \to Q (I + 1) \in ℝ$
252		simpl	$⊢ (φ \land \neg Q (I + 1) \in dom F) \to φ$
253	157	a1i	$⊢ (φ \land \neg Q (I + 1) \in dom F) \to - π \in ℝ^{*}$
254	159	a1i	$⊢ (φ \land \neg Q (I + 1) \in dom F) \to π \in ℝ^{*}$
255	30	adantr	$⊢ (φ \land \neg Q (I + 1) \in dom F) \to Q (I + 1) \in ℝ^{*}$
256	14 24 29 162 7	lelttrd	$⊢ φ \to - π < Q (I + 1)$
257	256	adantr	$⊢ (φ \land \neg Q (I + 1) \in dom F) \to - π < Q (I + 1)$
258	163	adantr	$⊢ (φ \land \neg Q (I + 1) \in dom F) \to Q (I + 1) \leq π$
259	253 254 255 257 258	eliocd	$⊢ (φ \land \neg Q (I + 1) \in dom F) \to Q (I + 1) \in (- π, π]$
260		simpr	$⊢ (φ \land \neg Q (I + 1) \in dom F) \to \neg Q (I + 1) \in dom F$
261	259 260	eldifd	$⊢ (φ \land \neg Q (I + 1) \in dom F) \to Q (I + 1) \in ((- π, π] ∖ dom F)$
262	252 261	jca	$⊢ (φ \land \neg Q (I + 1) \in dom F) \to (φ \land Q (I + 1) \in ((- π, π] ∖ dom F))$
263		eleq1	$⊢ x = Q (I + 1) \to (x \in ((- π, π] ∖ dom F) \leftrightarrow Q (I + 1) \in ((- π, π] ∖ dom F))$
264	263	anbi2d	$⊢ x = Q (I + 1) \to ((φ \land x \in ((- π, π] ∖ dom F)) \leftrightarrow (φ \land Q (I + 1) \in ((- π, π] ∖ dom F)))$
265		oveq2	$⊢ x = Q (I + 1) \to (−∞, x) = (−∞, Q (I + 1))$
266	265	reseq2d	$⊢ x = Q (I + 1) \to {F ↾}_{(−∞, x)} = {F ↾}_{(−∞, Q (I + 1))}$
267		id	$⊢ x = Q (I + 1) \to x = Q (I + 1)$
268	266 267	oveq12d	$⊢ x = Q (I + 1) \to ({F ↾}_{(−∞, x)}) {lim}_{ℂ} x = ({F ↾}_{(−∞, Q (I + 1))}) {lim}_{ℂ} Q (I + 1)$
269	268	neeq1d	$⊢ x = Q (I + 1) \to (({F ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset \leftrightarrow ({F ↾}_{(−∞, Q (I + 1))}) {lim}_{ℂ} Q (I + 1) \neq \emptyset)$
270	264 269	imbi12d	$⊢ x = Q (I + 1) \to (((φ \land x \in ((- π, π] ∖ dom F)) \to ({F ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset) \leftrightarrow ((φ \land Q (I + 1) \in ((- π, π] ∖ dom F)) \to ({F ↾}_{(−∞, Q (I + 1))}) {lim}_{ℂ} Q (I + 1) \neq \emptyset))$
271	270 3	vtoclg	$⊢ Q (I + 1) \in ℝ \to ((φ \land Q (I + 1) \in ((- π, π] ∖ dom F)) \to ({F ↾}_{(−∞, Q (I + 1))}) {lim}_{ℂ} Q (I + 1) \neq \emptyset)$
272	251 262 271	sylc	$⊢ (φ \land \neg Q (I + 1) \in dom F) \to ({F ↾}_{(−∞, Q (I + 1))}) {lim}_{ℂ} Q (I + 1) \neq \emptyset$
273		ssn0	$⊢ (({F ↾}_{(−∞, Q (I + 1))}) {lim}_{ℂ} Q (I + 1) \subseteq ({({F ↾}_{(−∞, Q (I + 1))}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1) \land ({F ↾}_{(−∞, Q (I + 1))}) {lim}_{ℂ} Q (I + 1) \neq \emptyset) \to ({({F ↾}_{(−∞, Q (I + 1))}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1) \neq \emptyset$
274	250 272 273	sylancr	$⊢ (φ \land \neg Q (I + 1) \in dom F) \to ({({F ↾}_{(−∞, Q (I + 1))}) ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1) \neq \emptyset$
275	249 274	eqnetrd	$⊢ (φ \land \neg Q (I + 1) \in dom F) \to ({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1) \neq \emptyset$
276	239 275	pm2.61dan	$⊢ φ \to ({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1) \neq \emptyset$
277	183 276	jca	$⊢ φ \to (({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I) \neq \emptyset \land ({F ↾}_{(Q (I), Q (I + 1))}) {lim}_{ℂ} Q (I + 1) \neq \emptyset)$

Metamath Proof Explorer

Theorem fourierdlem46

Proof