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

Metamath Proof Explorer

Theorem fourierdlem59

Proof