fourierdlem59

Description: The derivative of H is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem59.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem59.x	$⊢ φ \to X \in ℝ$
	fourierdlem59.a	$⊢ φ \to A \in ℝ$
	fourierdlem59.b	$⊢ φ \to B \in ℝ$
	fourierdlem59.n0	$⊢ φ \to \neg 0 \in (A, B)$
	fourierdlem59.fdv	$⊢ φ \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) \underset{cn}{⟶} ℝ$
	fourierdlem59.c	$⊢ φ \to C \in ℝ$
	fourierdlem59.h	$⊢ H = (s \in (A, B) ⟼ \frac{F (X + s) - C}{s})$
Assertion	fourierdlem59	$⊢ φ \to H_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℝ$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem59.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem59.x	$⊢ φ \to X \in ℝ$
3		fourierdlem59.a	$⊢ φ \to A \in ℝ$
4		fourierdlem59.b	$⊢ φ \to B \in ℝ$
5		fourierdlem59.n0	$⊢ φ \to \neg 0 \in (A, B)$
6		fourierdlem59.fdv	$⊢ φ \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) \underset{cn}{⟶} ℝ$
7		fourierdlem59.c	$⊢ φ \to C \in ℝ$
8		fourierdlem59.h	$⊢ H = (s \in (A, B) ⟼ \frac{F (X + s) - C}{s})$
9	1	adantr	$⊢ (φ \land s \in (A, B)) \to F : ℝ ⟶ ℝ$
10	2	adantr	$⊢ (φ \land s \in (A, B)) \to X \in ℝ$
11		elioore	$⊢ s \in (A, B) \to s \in ℝ$
12	11	adantl	$⊢ (φ \land s \in (A, B)) \to s \in ℝ$
13	10 12	readdcld	$⊢ (φ \land s \in (A, B)) \to X + s \in ℝ$
14	9 13	ffvelcdmd	$⊢ (φ \land s \in (A, B)) \to F (X + s) \in ℝ$
15	7	adantr	$⊢ (φ \land s \in (A, B)) \to C \in ℝ$
16	14 15	resubcld	$⊢ (φ \land s \in (A, B)) \to F (X + s) - C \in ℝ$
17		eqcom	$⊢ s = 0 \leftrightarrow 0 = s$
18	17	biimpi	$⊢ s = 0 \to 0 = s$
19	18	adantl	$⊢ (s \in (A, B) \land s = 0) \to 0 = s$
20		simpl	$⊢ (s \in (A, B) \land s = 0) \to s \in (A, B)$
21	19 20	eqeltrd	$⊢ (s \in (A, B) \land s = 0) \to 0 \in (A, B)$
22	21	adantll	$⊢ ((φ \land s \in (A, B)) \land s = 0) \to 0 \in (A, B)$
23	5	ad2antrr	$⊢ ((φ \land s \in (A, B)) \land s = 0) \to \neg 0 \in (A, B)$
24	22 23	pm2.65da	$⊢ (φ \land s \in (A, B)) \to \neg s = 0$
25	24	neqned	$⊢ (φ \land s \in (A, B)) \to s \neq 0$
26	16 12 25	redivcld	$⊢ (φ \land s \in (A, B)) \to \frac{F (X + s) - C}{s} \in ℝ$
27	26 8	fmptd	$⊢ φ \to H : (A, B) ⟶ ℝ$
28		ioossre	$⊢ (A, B) \subseteq ℝ$
29	28	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
30		dvfre	$⊢ (H : (A, B) ⟶ ℝ \land (A, B) \subseteq ℝ) \to H_{ℝ}^{'} : dom H_{ℝ}^{'} ⟶ ℝ$
31	27 29 30	syl2anc	$⊢ φ \to H_{ℝ}^{'} : dom H_{ℝ}^{'} ⟶ ℝ$
32		ovex	$⊢ (A, B) \in V$
33	32	a1i	$⊢ φ \to (A, B) \in V$
34		eqidd	$⊢ φ \to (s \in (A, B) ⟼ F (X + s) - C) = (s \in (A, B) ⟼ F (X + s) - C)$
35		eqidd	$⊢ φ \to (s \in (A, B) ⟼ s) = (s \in (A, B) ⟼ s)$
36	33 16 12 34 35	offval2	$⊢ φ \to (s \in (A, B) ⟼ F (X + s) - C) \div_{f} (s \in (A, B) ⟼ s) = (s \in (A, B) ⟼ \frac{F (X + s) - C}{s})$
37	8 36	eqtr4id	$⊢ φ \to H = (s \in (A, B) ⟼ F (X + s) - C) \div_{f} (s \in (A, B) ⟼ s)$
38	37	oveq2d	$⊢ φ \to ℝ D H = ℝ D ((s \in (A, B) ⟼ F (X + s) - C) \div_{f} (s \in (A, B) ⟼ s))$
39		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
40	39	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
41	16	recnd	$⊢ (φ \land s \in (A, B)) \to F (X + s) - C \in ℂ$
42		eqid	$⊢ (s \in (A, B) ⟼ F (X + s) - C) = (s \in (A, B) ⟼ F (X + s) - C)$
43	41 42	fmptd	$⊢ φ \to (s \in (A, B) ⟼ F (X + s) - C) : (A, B) ⟶ ℂ$
44	12	recnd	$⊢ (φ \land s \in (A, B)) \to s \in ℂ$
45		eldifsn	$⊢ s \in (ℂ ∖ \{0\}) \leftrightarrow (s \in ℂ \land s \neq 0)$
46	44 25 45	sylanbrc	$⊢ (φ \land s \in (A, B)) \to s \in (ℂ ∖ \{0\})$
47		eqid	$⊢ (s \in (A, B) ⟼ s) = (s \in (A, B) ⟼ s)$
48	46 47	fmptd	$⊢ φ \to (s \in (A, B) ⟼ s) : (A, B) ⟶ ℂ ∖ \{0\}$
49		eqidd	$⊢ φ \to (s \in (A, B) ⟼ F (X + s)) = (s \in (A, B) ⟼ F (X + s))$
50		eqidd	$⊢ φ \to (s \in (A, B) ⟼ C) = (s \in (A, B) ⟼ C)$
51	33 14 15 49 50	offval2	$⊢ φ \to (s \in (A, B) ⟼ F (X + s)) -_{f} (s \in (A, B) ⟼ C) = (s \in (A, B) ⟼ F (X + s) - C)$
52	51	eqcomd	$⊢ φ \to (s \in (A, B) ⟼ F (X + s) - C) = (s \in (A, B) ⟼ F (X + s)) -_{f} (s \in (A, B) ⟼ C)$
53	52	oveq2d	$⊢ φ \to \frac{d (s \in (A, B)⟼ F (X + s) - C)}{d_{ℝ} s} = ℝ D ((s \in (A, B) ⟼ F (X + s)) -_{f} (s \in (A, B) ⟼ C))$
54	14	recnd	$⊢ (φ \land s \in (A, B)) \to F (X + s) \in ℂ$
55		eqid	$⊢ (s \in (A, B) ⟼ F (X + s)) = (s \in (A, B) ⟼ F (X + s))$
56	54 55	fmptd	$⊢ φ \to (s \in (A, B) ⟼ F (X + s)) : (A, B) ⟶ ℂ$
57	15	recnd	$⊢ (φ \land s \in (A, B)) \to C \in ℂ$
58		eqid	$⊢ (s \in (A, B) ⟼ C) = (s \in (A, B) ⟼ C)$
59	57 58	fmptd	$⊢ φ \to (s \in (A, B) ⟼ C) : (A, B) ⟶ ℂ$
60		eqid	$⊢ ℝ D ({F ↾}_{(X + A, X + B)}) = ℝ D ({F ↾}_{(X + A, X + B)})$
61		cncff	$⊢ {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) \underset{cn}{⟶} ℝ \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) ⟶ ℝ$
62	6 61	syl	$⊢ φ \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) ⟶ ℝ$
63	1 2 3 4 60 62	fourierdlem28	$⊢ φ \to \frac{d (s \in (A, B)⟼ F (X + s))}{d_{ℝ} s} = (s \in (A, B) ⟼ {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s))$
64		ioosscn	$⊢ (X + A, X + B) \subseteq ℂ$
65	64	a1i	$⊢ φ \to (X + A, X + B) \subseteq ℂ$
66		ax-resscn	$⊢ ℝ \subseteq ℂ$
67	66	a1i	$⊢ φ \to ℝ \subseteq ℂ$
68	62 67	fssd	$⊢ φ \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) ⟶ ℂ$
69		ssid	$⊢ ℂ \subseteq ℂ$
70	69	a1i	$⊢ φ \to ℂ \subseteq ℂ$
71		cncfcdm	$⊢ (ℂ \subseteq ℂ \land {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) \underset{cn}{⟶} ℝ) \to ({({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) \underset{cn}{⟶} ℂ \leftrightarrow {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) ⟶ ℂ)$
72	70 6 71	syl2anc	$⊢ φ \to ({({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) \underset{cn}{⟶} ℂ \leftrightarrow {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) ⟶ ℂ)$
73	68 72	mpbird	$⊢ φ \to {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} : (X + A, X + B) \underset{cn}{⟶} ℂ$
74		ioosscn	$⊢ (A, B) \subseteq ℂ$
75	74	a1i	$⊢ φ \to (A, B) \subseteq ℂ$
76	2	recnd	$⊢ φ \to X \in ℂ$
77	2 3	readdcld	$⊢ φ \to X + A \in ℝ$
78	77	rexrd	$⊢ φ \to X + A \in ℝ^{*}$
79	78	adantr	$⊢ (φ \land s \in (A, B)) \to X + A \in ℝ^{*}$
80	2 4	readdcld	$⊢ φ \to X + B \in ℝ$
81	80	rexrd	$⊢ φ \to X + B \in ℝ^{*}$
82	81	adantr	$⊢ (φ \land s \in (A, B)) \to X + B \in ℝ^{*}$
83	3	adantr	$⊢ (φ \land s \in (A, B)) \to A \in ℝ$
84	83	rexrd	$⊢ (φ \land s \in (A, B)) \to A \in ℝ^{*}$
85	4	rexrd	$⊢ φ \to B \in ℝ^{*}$
86	85	adantr	$⊢ (φ \land s \in (A, B)) \to B \in ℝ^{*}$
87		simpr	$⊢ (φ \land s \in (A, B)) \to s \in (A, B)$
88		ioogtlb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land s \in (A, B)) \to A < s$
89	84 86 87 88	syl3anc	$⊢ (φ \land s \in (A, B)) \to A < s$
90	83 12 10 89	ltadd2dd	$⊢ (φ \land s \in (A, B)) \to X + A < X + s$
91	4	adantr	$⊢ (φ \land s \in (A, B)) \to B \in ℝ$
92		iooltub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land s \in (A, B)) \to s < B$
93	84 86 87 92	syl3anc	$⊢ (φ \land s \in (A, B)) \to s < B$
94	12 91 10 93	ltadd2dd	$⊢ (φ \land s \in (A, B)) \to X + s < X + B$
95	79 82 13 90 94	eliood	$⊢ (φ \land s \in (A, B)) \to X + s \in (X + A, X + B)$
96	65 73 75 76 95	fourierdlem23	$⊢ φ \to (s \in (A, B) ⟼ {({F ↾}_{(X + A, X + B)})}_{ℝ}^{'} (X + s)) : (A, B) \underset{cn}{⟶} ℂ$
97	63 96	eqeltrd	$⊢ φ \to \frac{d (s \in (A, B)⟼ F (X + s))}{d_{ℝ} s} : (A, B) \underset{cn}{⟶} ℂ$
98		iooretop	$⊢ (A, B) \in topGen (ran (.))$
99		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
100	98 99	eleqtri	$⊢ (A, B) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
101	100	a1i	$⊢ φ \to (A, B) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
102	7	recnd	$⊢ φ \to C \in ℂ$
103	40 101 102	dvmptconst	$⊢ φ \to \frac{d (s \in (A, B)⟼ C)}{d_{ℝ} s} = (s \in (A, B) ⟼ 0)$
104		0cnd	$⊢ φ \to 0 \in ℂ$
105	75 104 70	constcncfg	$⊢ φ \to (s \in (A, B) ⟼ 0) : (A, B) \underset{cn}{⟶} ℂ$
106	103 105	eqeltrd	$⊢ φ \to \frac{d (s \in (A, B)⟼ C)}{d_{ℝ} s} : (A, B) \underset{cn}{⟶} ℂ$
107	40 56 59 97 106	dvsubcncf	$⊢ φ \to {((s \in (A, B) ⟼ F (X + s)) -_{f} (s \in (A, B) ⟼ C))}_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$
108	53 107	eqeltrd	$⊢ φ \to \frac{d (s \in (A, B)⟼ F (X + s) - C)}{d_{ℝ} s} : (A, B) \underset{cn}{⟶} ℂ$
109	40 101	dvmptidg	$⊢ φ \to \frac{d (s \in (A, B)⟼ s)}{d_{ℝ} s} = (s \in (A, B) ⟼ 1)$
110		1cnd	$⊢ φ \to 1 \in ℂ$
111	75 110 70	constcncfg	$⊢ φ \to (s \in (A, B) ⟼ 1) : (A, B) \underset{cn}{⟶} ℂ$
112	109 111	eqeltrd	$⊢ φ \to \frac{d (s \in (A, B)⟼ s)}{d_{ℝ} s} : (A, B) \underset{cn}{⟶} ℂ$
113	40 43 48 108 112	dvdivcncf	$⊢ φ \to {((s \in (A, B) ⟼ F (X + s) - C) \div_{f} (s \in (A, B) ⟼ s))}_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$
114	38 113	eqeltrd	$⊢ φ \to H_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ$
115		cncff	$⊢ H_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ \to H_{ℝ}^{'} : (A, B) ⟶ ℂ$
116		fdm	$⊢ H_{ℝ}^{'} : (A, B) ⟶ ℂ \to dom H_{ℝ}^{'} = (A, B)$
117	114 115 116	3syl	$⊢ φ \to dom H_{ℝ}^{'} = (A, B)$
118	117	feq2d	$⊢ φ \to (H_{ℝ}^{'} : dom H_{ℝ}^{'} ⟶ ℝ \leftrightarrow H_{ℝ}^{'} : (A, B) ⟶ ℝ)$
119	31 118	mpbid	$⊢ φ \to H_{ℝ}^{'} : (A, B) ⟶ ℝ$
120		cncfcdm	$⊢ (ℝ \subseteq ℂ \land H_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℂ) \to (H_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℝ \leftrightarrow H_{ℝ}^{'} : (A, B) ⟶ ℝ)$
121	67 114 120	syl2anc	$⊢ φ \to (H_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℝ \leftrightarrow H_{ℝ}^{'} : (A, B) ⟶ ℝ)$
122	119 121	mpbird	$⊢ φ \to H_{ℝ}^{'} : (A, B) \underset{cn}{⟶} ℝ$

Metamath Proof Explorer

Theorem fourierdlem59

Proof