fourierdlem40

Description: H is a continuous function on any partition interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem40.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem40.a	$⊢ φ \to A \in [- π, π]$
	fourierdlem40.b	$⊢ φ \to B \in [- π, π]$
	fourierdlem40.x	$⊢ φ \to X \in ℝ$
	fourierdlem40.nxelab	$⊢ φ \to \neg 0 \in (A, B)$
	fourierdlem40.fcn	$⊢ φ \to ({F ↾}_{(A + X, B + X)}) : (A + X, B + X) \underset{cn}{⟶} ℂ$
	fourierdlem40.y	$⊢ φ \to Y \in ℝ$
	fourierdlem40.w	$⊢ φ \to W \in ℝ$
	fourierdlem40.h	$⊢ H = (s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
Assertion	fourierdlem40	$⊢ φ \to ({H ↾}_{(A, B)}) : (A, B) \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem40.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem40.a	$⊢ φ \to A \in [- π, π]$
3		fourierdlem40.b	$⊢ φ \to B \in [- π, π]$
4		fourierdlem40.x	$⊢ φ \to X \in ℝ$
5		fourierdlem40.nxelab	$⊢ φ \to \neg 0 \in (A, B)$
6		fourierdlem40.fcn	$⊢ φ \to ({F ↾}_{(A + X, B + X)}) : (A + X, B + X) \underset{cn}{⟶} ℂ$
7		fourierdlem40.y	$⊢ φ \to Y \in ℝ$
8		fourierdlem40.w	$⊢ φ \to W \in ℝ$
9		fourierdlem40.h	$⊢ H = (s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
10	9	reseq1i	$⊢ {H ↾}_{(A, B)} = {(s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s})) ↾}_{(A, B)}$
11	10	a1i	$⊢ φ \to {H ↾}_{(A, B)} = {(s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s})) ↾}_{(A, B)}$
12		pire	$⊢ π \in ℝ$
13	12	renegcli	$⊢ - π \in ℝ$
14	13	a1i	$⊢ (φ \land s \in (A, B)) \to - π \in ℝ$
15	12	a1i	$⊢ (φ \land s \in (A, B)) \to π \in ℝ$
16		elioore	$⊢ s \in (A, B) \to s \in ℝ$
17	16	adantl	$⊢ (φ \land s \in (A, B)) \to s \in ℝ$
18	13	a1i	$⊢ φ \to - π \in ℝ$
19	12	a1i	$⊢ φ \to π \in ℝ$
20	18 19	iccssred	$⊢ φ \to [- π, π] \subseteq ℝ$
21	20 2	sseldd	$⊢ φ \to A \in ℝ$
22	21	adantr	$⊢ (φ \land s \in (A, B)) \to A \in ℝ$
23	13 12	elicc2i	$⊢ A \in [- π, π] \leftrightarrow (A \in ℝ \land - π \leq A \land A \leq π)$
24	23	simp2bi	$⊢ A \in [- π, π] \to - π \leq A$
25	2 24	syl	$⊢ φ \to - π \leq A$
26	25	adantr	$⊢ (φ \land s \in (A, B)) \to - π \leq A$
27	22	rexrd	$⊢ (φ \land s \in (A, B)) \to A \in ℝ^{*}$
28	20 3	sseldd	$⊢ φ \to B \in ℝ$
29	28	rexrd	$⊢ φ \to B \in ℝ^{*}$
30	29	adantr	$⊢ (φ \land s \in (A, B)) \to B \in ℝ^{*}$
31		simpr	$⊢ (φ \land s \in (A, B)) \to s \in (A, B)$
32		ioogtlb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land s \in (A, B)) \to A < s$
33	27 30 31 32	syl3anc	$⊢ (φ \land s \in (A, B)) \to A < s$
34	14 22 17 26 33	lelttrd	$⊢ (φ \land s \in (A, B)) \to - π < s$
35	14 17 34	ltled	$⊢ (φ \land s \in (A, B)) \to - π \leq s$
36	28	adantr	$⊢ (φ \land s \in (A, B)) \to B \in ℝ$
37		iooltub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land s \in (A, B)) \to s < B$
38	27 30 31 37	syl3anc	$⊢ (φ \land s \in (A, B)) \to s < B$
39	13 12	elicc2i	$⊢ B \in [- π, π] \leftrightarrow (B \in ℝ \land - π \leq B \land B \leq π)$
40	39	simp3bi	$⊢ B \in [- π, π] \to B \leq π$
41	3 40	syl	$⊢ φ \to B \leq π$
42	41	adantr	$⊢ (φ \land s \in (A, B)) \to B \leq π$
43	17 36 15 38 42	ltletrd	$⊢ (φ \land s \in (A, B)) \to s < π$
44	17 15 43	ltled	$⊢ (φ \land s \in (A, B)) \to s \leq π$
45	14 15 17 35 44	eliccd	$⊢ (φ \land s \in (A, B)) \to s \in [- π, π]$
46	45	ex	$⊢ φ \to (s \in (A, B) \to s \in [- π, π])$
47	46	ssrdv	$⊢ φ \to (A, B) \subseteq [- π, π]$
48	47	resmptd	$⊢ φ \to {(s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s})) ↾}_{(A, B)} = (s \in (A, B) ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
49		eleq1	$⊢ s = 0 \to (s \in (A, B) \leftrightarrow 0 \in (A, B))$
50	49	biimpac	$⊢ (s \in (A, B) \land s = 0) \to 0 \in (A, B)$
51	50	adantll	$⊢ ((φ \land s \in (A, B)) \land s = 0) \to 0 \in (A, B)$
52	5	ad2antrr	$⊢ ((φ \land s \in (A, B)) \land s = 0) \to \neg 0 \in (A, B)$
53	51 52	pm2.65da	$⊢ (φ \land s \in (A, B)) \to \neg s = 0$
54	53	iffalsed	$⊢ (φ \land s \in (A, B)) \to if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}) = \frac{F (X + s) - if (0 < s, Y, W)}{s}$
55	1	adantr	$⊢ (φ \land s \in (A, B)) \to F : ℝ ⟶ ℝ$
56	4	adantr	$⊢ (φ \land s \in (A, B)) \to X \in ℝ$
57	56 17	readdcld	$⊢ (φ \land s \in (A, B)) \to X + s \in ℝ$
58	55 57	ffvelcdmd	$⊢ (φ \land s \in (A, B)) \to F (X + s) \in ℝ$
59	7 8	ifcld	$⊢ φ \to if (0 < s, Y, W) \in ℝ$
60	59	adantr	$⊢ (φ \land s \in (A, B)) \to if (0 < s, Y, W) \in ℝ$
61	58 60	resubcld	$⊢ (φ \land s \in (A, B)) \to F (X + s) - if (0 < s, Y, W) \in ℝ$
62	61	recnd	$⊢ (φ \land s \in (A, B)) \to F (X + s) - if (0 < s, Y, W) \in ℂ$
63	17	recnd	$⊢ (φ \land s \in (A, B)) \to s \in ℂ$
64	53	neqned	$⊢ (φ \land s \in (A, B)) \to s \neq 0$
65	62 63 64	divrecd	$⊢ (φ \land s \in (A, B)) \to \frac{F (X + s) - if (0 < s, Y, W)}{s} = (F (X + s) - if (0 < s, Y, W)) (\frac{1}{s})$
66	54 65	eqtrd	$⊢ (φ \land s \in (A, B)) \to if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}) = (F (X + s) - if (0 < s, Y, W)) (\frac{1}{s})$
67	66	mpteq2dva	$⊢ φ \to (s \in (A, B) ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s})) = (s \in (A, B) ⟼ (F (X + s) - if (0 < s, Y, W)) (\frac{1}{s}))$
68	11 48 67	3eqtrd	$⊢ φ \to {H ↾}_{(A, B)} = (s \in (A, B) ⟼ (F (X + s) - if (0 < s, Y, W)) (\frac{1}{s}))$
69	58	recnd	$⊢ (φ \land s \in (A, B)) \to F (X + s) \in ℂ$
70	60	recnd	$⊢ (φ \land s \in (A, B)) \to if (0 < s, Y, W) \in ℂ$
71	69 70	negsubd	$⊢ (φ \land s \in (A, B)) \to F (X + s) + (- if (0 < s, Y, W)) = F (X + s) - if (0 < s, Y, W)$
72	71	eqcomd	$⊢ (φ \land s \in (A, B)) \to F (X + s) - if (0 < s, Y, W) = F (X + s) + (- if (0 < s, Y, W))$
73	72	mpteq2dva	$⊢ φ \to (s \in (A, B) ⟼ F (X + s) - if (0 < s, Y, W)) = (s \in (A, B) ⟼ F (X + s) + (- if (0 < s, Y, W)))$
74	21 4	readdcld	$⊢ φ \to A + X \in ℝ$
75	74	rexrd	$⊢ φ \to A + X \in ℝ^{*}$
76	75	adantr	$⊢ (φ \land s \in (A, B)) \to A + X \in ℝ^{*}$
77	28 4	readdcld	$⊢ φ \to B + X \in ℝ$
78	77	rexrd	$⊢ φ \to B + X \in ℝ^{*}$
79	78	adantr	$⊢ (φ \land s \in (A, B)) \to B + X \in ℝ^{*}$
80	21	recnd	$⊢ φ \to A \in ℂ$
81	4	recnd	$⊢ φ \to X \in ℂ$
82	80 81	addcomd	$⊢ φ \to A + X = X + A$
83	82	adantr	$⊢ (φ \land s \in (A, B)) \to A + X = X + A$
84	22 17 56 33	ltadd2dd	$⊢ (φ \land s \in (A, B)) \to X + A < X + s$
85	83 84	eqbrtrd	$⊢ (φ \land s \in (A, B)) \to A + X < X + s$
86	17 36 56 38	ltadd2dd	$⊢ (φ \land s \in (A, B)) \to X + s < X + B$
87	28	recnd	$⊢ φ \to B \in ℂ$
88	81 87	addcomd	$⊢ φ \to X + B = B + X$
89	88	adantr	$⊢ (φ \land s \in (A, B)) \to X + B = B + X$
90	86 89	breqtrd	$⊢ (φ \land s \in (A, B)) \to X + s < B + X$
91	76 79 57 85 90	eliood	$⊢ (φ \land s \in (A, B)) \to X + s \in (A + X, B + X)$
92		fvres	$⊢ X + s \in (A + X, B + X) \to ({F ↾}_{(A + X, B + X)}) (X + s) = F (X + s)$
93	91 92	syl	$⊢ (φ \land s \in (A, B)) \to ({F ↾}_{(A + X, B + X)}) (X + s) = F (X + s)$
94	93	eqcomd	$⊢ (φ \land s \in (A, B)) \to F (X + s) = ({F ↾}_{(A + X, B + X)}) (X + s)$
95	94	mpteq2dva	$⊢ φ \to (s \in (A, B) ⟼ F (X + s)) = (s \in (A, B) ⟼ ({F ↾}_{(A + X, B + X)}) (X + s))$
96		ioosscn	$⊢ (A + X, B + X) \subseteq ℂ$
97	96	a1i	$⊢ φ \to (A + X, B + X) \subseteq ℂ$
98		ioosscn	$⊢ (A, B) \subseteq ℂ$
99	98	a1i	$⊢ φ \to (A, B) \subseteq ℂ$
100	97 6 99 81 91	fourierdlem23	$⊢ φ \to (s \in (A, B) ⟼ ({F ↾}_{(A + X, B + X)}) (X + s)) : (A, B) \underset{cn}{⟶} ℂ$
101	95 100	eqeltrd	$⊢ φ \to (s \in (A, B) ⟼ F (X + s)) : (A, B) \underset{cn}{⟶} ℂ$
102		0red	$⊢ ((φ \land 0 \leq A) \land s \in (A, B)) \to 0 \in ℝ$
103	21	ad2antrr	$⊢ ((φ \land 0 \leq A) \land s \in (A, B)) \to A \in ℝ$
104	16	adantl	$⊢ ((φ \land 0 \leq A) \land s \in (A, B)) \to s \in ℝ$
105		simplr	$⊢ ((φ \land 0 \leq A) \land s \in (A, B)) \to 0 \leq A$
106	33	adantlr	$⊢ ((φ \land 0 \leq A) \land s \in (A, B)) \to A < s$
107	102 103 104 105 106	lelttrd	$⊢ ((φ \land 0 \leq A) \land s \in (A, B)) \to 0 < s$
108	107	iftrued	$⊢ ((φ \land 0 \leq A) \land s \in (A, B)) \to if (0 < s, Y, W) = Y$
109	108	negeqd	$⊢ ((φ \land 0 \leq A) \land s \in (A, B)) \to - if (0 < s, Y, W) = - Y$
110	109	mpteq2dva	$⊢ (φ \land 0 \leq A) \to (s \in (A, B) ⟼ - if (0 < s, Y, W)) = (s \in (A, B) ⟼ - Y)$
111	7	renegcld	$⊢ φ \to - Y \in ℝ$
112	111	recnd	$⊢ φ \to - Y \in ℂ$
113		ssid	$⊢ ℂ \subseteq ℂ$
114	113	a1i	$⊢ φ \to ℂ \subseteq ℂ$
115	99 112 114	constcncfg	$⊢ φ \to (s \in (A, B) ⟼ - Y) : (A, B) \underset{cn}{⟶} ℂ$
116	115	adantr	$⊢ (φ \land 0 \leq A) \to (s \in (A, B) ⟼ - Y) : (A, B) \underset{cn}{⟶} ℂ$
117	110 116	eqeltrd	$⊢ (φ \land 0 \leq A) \to (s \in (A, B) ⟼ - if (0 < s, Y, W)) : (A, B) \underset{cn}{⟶} ℂ$
118	21	rexrd	$⊢ φ \to A \in ℝ^{*}$
119	118	ad2antrr	$⊢ ((φ \land \neg 0 \leq A) \land \neg B \leq 0) \to A \in ℝ^{*}$
120	29	ad2antrr	$⊢ ((φ \land \neg 0 \leq A) \land \neg B \leq 0) \to B \in ℝ^{*}$
121		0red	$⊢ ((φ \land \neg 0 \leq A) \land \neg B \leq 0) \to 0 \in ℝ$
122		simpr	$⊢ (φ \land \neg 0 \leq A) \to \neg 0 \leq A$
123	21	adantr	$⊢ (φ \land \neg 0 \leq A) \to A \in ℝ$
124		0red	$⊢ (φ \land \neg 0 \leq A) \to 0 \in ℝ$
125	123 124	ltnled	$⊢ (φ \land \neg 0 \leq A) \to (A < 0 \leftrightarrow \neg 0 \leq A)$
126	122 125	mpbird	$⊢ (φ \land \neg 0 \leq A) \to A < 0$
127	126	adantr	$⊢ ((φ \land \neg 0 \leq A) \land \neg B \leq 0) \to A < 0$
128		simpr	$⊢ (φ \land \neg B \leq 0) \to \neg B \leq 0$
129		0red	$⊢ (φ \land \neg B \leq 0) \to 0 \in ℝ$
130	28	adantr	$⊢ (φ \land \neg B \leq 0) \to B \in ℝ$
131	129 130	ltnled	$⊢ (φ \land \neg B \leq 0) \to (0 < B \leftrightarrow \neg B \leq 0)$
132	128 131	mpbird	$⊢ (φ \land \neg B \leq 0) \to 0 < B$
133	132	adantlr	$⊢ ((φ \land \neg 0 \leq A) \land \neg B \leq 0) \to 0 < B$
134	119 120 121 127 133	eliood	$⊢ ((φ \land \neg 0 \leq A) \land \neg B \leq 0) \to 0 \in (A, B)$
135	5	ad2antrr	$⊢ ((φ \land \neg 0 \leq A) \land \neg B \leq 0) \to \neg 0 \in (A, B)$
136	134 135	condan	$⊢ (φ \land \neg 0 \leq A) \to B \leq 0$
137	16	adantl	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to s \in ℝ$
138		0red	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to 0 \in ℝ$
139	28	ad2antrr	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to B \in ℝ$
140	38	adantlr	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to s < B$
141		simplr	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to B \leq 0$
142	137 139 138 140 141	ltletrd	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to s < 0$
143	137 138 142	ltnsymd	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to \neg 0 < s$
144	143	iffalsed	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to if (0 < s, Y, W) = W$
145	144	negeqd	$⊢ ((φ \land B \leq 0) \land s \in (A, B)) \to - if (0 < s, Y, W) = - W$
146	145	mpteq2dva	$⊢ (φ \land B \leq 0) \to (s \in (A, B) ⟼ - if (0 < s, Y, W)) = (s \in (A, B) ⟼ - W)$
147	8	recnd	$⊢ φ \to W \in ℂ$
148	147	negcld	$⊢ φ \to - W \in ℂ$
149	99 148 114	constcncfg	$⊢ φ \to (s \in (A, B) ⟼ - W) : (A, B) \underset{cn}{⟶} ℂ$
150	149	adantr	$⊢ (φ \land B \leq 0) \to (s \in (A, B) ⟼ - W) : (A, B) \underset{cn}{⟶} ℂ$
151	146 150	eqeltrd	$⊢ (φ \land B \leq 0) \to (s \in (A, B) ⟼ - if (0 < s, Y, W)) : (A, B) \underset{cn}{⟶} ℂ$
152	136 151	syldan	$⊢ (φ \land \neg 0 \leq A) \to (s \in (A, B) ⟼ - if (0 < s, Y, W)) : (A, B) \underset{cn}{⟶} ℂ$
153	117 152	pm2.61dan	$⊢ φ \to (s \in (A, B) ⟼ - if (0 < s, Y, W)) : (A, B) \underset{cn}{⟶} ℂ$
154	101 153	addcncf	$⊢ φ \to (s \in (A, B) ⟼ F (X + s) + (- if (0 < s, Y, W))) : (A, B) \underset{cn}{⟶} ℂ$
155	73 154	eqeltrd	$⊢ φ \to (s \in (A, B) ⟼ F (X + s) - if (0 < s, Y, W)) : (A, B) \underset{cn}{⟶} ℂ$
156		eqid	$⊢ (s \in (ℂ ∖ \{0\}) ⟼ \frac{1}{s}) = (s \in (ℂ ∖ \{0\}) ⟼ \frac{1}{s})$
157		1cnd	$⊢ φ \to 1 \in ℂ$
158	156	cdivcncf	$⊢ 1 \in ℂ \to (s \in (ℂ ∖ \{0\}) ⟼ \frac{1}{s}) : (ℂ ∖ \{0\}) \underset{cn}{⟶} ℂ$
159	157 158	syl	$⊢ φ \to (s \in (ℂ ∖ \{0\}) ⟼ \frac{1}{s}) : (ℂ ∖ \{0\}) \underset{cn}{⟶} ℂ$
160		velsn	$⊢ s \in \{0\} \leftrightarrow s = 0$
161	53 160	sylnibr	$⊢ (φ \land s \in (A, B)) \to \neg s \in \{0\}$
162	63 161	eldifd	$⊢ (φ \land s \in (A, B)) \to s \in (ℂ ∖ \{0\})$
163	162	ralrimiva	$⊢ φ \to \forall s \in (A, B) s \in (ℂ ∖ \{0\})$
164		dfss3	$⊢ (A, B) \subseteq ℂ ∖ \{0\} \leftrightarrow \forall s \in (A, B) s \in (ℂ ∖ \{0\})$
165	163 164	sylibr	$⊢ φ \to (A, B) \subseteq ℂ ∖ \{0\}$
166	17 64	rereccld	$⊢ (φ \land s \in (A, B)) \to \frac{1}{s} \in ℝ$
167	166	recnd	$⊢ (φ \land s \in (A, B)) \to \frac{1}{s} \in ℂ$
168	156 159 165 114 167	cncfmptssg	$⊢ φ \to (s \in (A, B) ⟼ \frac{1}{s}) : (A, B) \underset{cn}{⟶} ℂ$
169	155 168	mulcncf	$⊢ φ \to (s \in (A, B) ⟼ (F (X + s) - if (0 < s, Y, W)) (\frac{1}{s})) : (A, B) \underset{cn}{⟶} ℂ$
170	68 169	eqeltrd	$⊢ φ \to ({H ↾}_{(A, B)}) : (A, B) \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem fourierdlem40

Proof