Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem59 Structured version   Visualization version   GIF version

Theorem fourierdlem59 45476
Description: The derivative of 𝐻 is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem59.f (πœ‘ β†’ 𝐹:β„βŸΆβ„)
fourierdlem59.x (πœ‘ β†’ 𝑋 ∈ ℝ)
fourierdlem59.a (πœ‘ β†’ 𝐴 ∈ ℝ)
fourierdlem59.b (πœ‘ β†’ 𝐡 ∈ ℝ)
fourierdlem59.n0 (πœ‘ β†’ Β¬ 0 ∈ (𝐴(,)𝐡))
fourierdlem59.fdv (πœ‘ β†’ (ℝ D (𝐹 β†Ύ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐡))–cn→ℝ))
fourierdlem59.c (πœ‘ β†’ 𝐢 ∈ ℝ)
fourierdlem59.h 𝐻 = (𝑠 ∈ (𝐴(,)𝐡) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠))
Assertion
Ref Expression
fourierdlem59 (πœ‘ β†’ (ℝ D 𝐻) ∈ ((𝐴(,)𝐡)–cn→ℝ))
Distinct variable groups:   𝐴,𝑠   𝐡,𝑠   𝐢,𝑠   𝐹,𝑠   𝑋,𝑠   πœ‘,𝑠
Allowed substitution hint:   𝐻(𝑠)

Proof of Theorem fourierdlem59
StepHypRef Expression
1 fourierdlem59.f . . . . . . . . 9 (πœ‘ β†’ 𝐹:β„βŸΆβ„)
21adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐹:β„βŸΆβ„)
3 fourierdlem59.x . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ ℝ)
43adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑋 ∈ ℝ)
5 elioore 13378 . . . . . . . . . 10 (𝑠 ∈ (𝐴(,)𝐡) β†’ 𝑠 ∈ ℝ)
65adantl 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ ℝ)
74, 6readdcld 11265 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝑠) ∈ ℝ)
82, 7ffvelcdmd 7089 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ ℝ)
9 fourierdlem59.c . . . . . . . 8 (πœ‘ β†’ 𝐢 ∈ ℝ)
109adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐢 ∈ ℝ)
118, 10resubcld 11664 . . . . . 6 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) ∈ ℝ)
12 eqcom 2734 . . . . . . . . . . . 12 (𝑠 = 0 ↔ 0 = 𝑠)
1312biimpi 215 . . . . . . . . . . 11 (𝑠 = 0 β†’ 0 = 𝑠)
1413adantl 481 . . . . . . . . . 10 ((𝑠 ∈ (𝐴(,)𝐡) ∧ 𝑠 = 0) β†’ 0 = 𝑠)
15 simpl 482 . . . . . . . . . 10 ((𝑠 ∈ (𝐴(,)𝐡) ∧ 𝑠 = 0) β†’ 𝑠 ∈ (𝐴(,)𝐡))
1614, 15eqeltrd 2828 . . . . . . . . 9 ((𝑠 ∈ (𝐴(,)𝐡) ∧ 𝑠 = 0) β†’ 0 ∈ (𝐴(,)𝐡))
1716adantll 713 . . . . . . . 8 (((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) ∧ 𝑠 = 0) β†’ 0 ∈ (𝐴(,)𝐡))
18 fourierdlem59.n0 . . . . . . . . 9 (πœ‘ β†’ Β¬ 0 ∈ (𝐴(,)𝐡))
1918ad2antrr 725 . . . . . . . 8 (((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) ∧ 𝑠 = 0) β†’ Β¬ 0 ∈ (𝐴(,)𝐡))
2017, 19pm2.65da 816 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ Β¬ 𝑠 = 0)
2120neqned 2942 . . . . . 6 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 β‰  0)
2211, 6, 21redivcld 12064 . . . . 5 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠) ∈ ℝ)
23 fourierdlem59.h . . . . 5 𝐻 = (𝑠 ∈ (𝐴(,)𝐡) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠))
2422, 23fmptd 7118 . . . 4 (πœ‘ β†’ 𝐻:(𝐴(,)𝐡)βŸΆβ„)
25 ioossre 13409 . . . . 5 (𝐴(,)𝐡) βŠ† ℝ
2625a1i 11 . . . 4 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† ℝ)
27 dvfre 25870 . . . 4 ((𝐻:(𝐴(,)𝐡)βŸΆβ„ ∧ (𝐴(,)𝐡) βŠ† ℝ) β†’ (ℝ D 𝐻):dom (ℝ D 𝐻)βŸΆβ„)
2824, 26, 27syl2anc 583 . . 3 (πœ‘ β†’ (ℝ D 𝐻):dom (ℝ D 𝐻)βŸΆβ„)
29 ovex 7447 . . . . . . . . . 10 (𝐴(,)𝐡) ∈ V
3029a1i 11 . . . . . . . . 9 (πœ‘ β†’ (𝐴(,)𝐡) ∈ V)
31 eqidd 2728 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢)))
32 eqidd 2728 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝑠) = (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝑠))
3330, 11, 6, 31, 32offval2 7699 . . . . . . . 8 (πœ‘ β†’ ((𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢)) ∘f / (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝑠)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) / 𝑠)))
3423, 33eqtr4id 2786 . . . . . . 7 (πœ‘ β†’ 𝐻 = ((𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢)) ∘f / (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝑠)))
3534oveq2d 7430 . . . . . 6 (πœ‘ β†’ (ℝ D 𝐻) = (ℝ D ((𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢)) ∘f / (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝑠))))
36 reelprrecn 11222 . . . . . . . 8 ℝ ∈ {ℝ, β„‚}
3736a1i 11 . . . . . . 7 (πœ‘ β†’ ℝ ∈ {ℝ, β„‚})
3811recnd 11264 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢) ∈ β„‚)
39 eqid 2727 . . . . . . . 8 (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢))
4038, 39fmptd 7118 . . . . . . 7 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢)):(𝐴(,)𝐡)βŸΆβ„‚)
416recnd 11264 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ β„‚)
42 eldifsn 4786 . . . . . . . . 9 (𝑠 ∈ (β„‚ βˆ– {0}) ↔ (𝑠 ∈ β„‚ ∧ 𝑠 β‰  0))
4341, 21, 42sylanbrc 582 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ (β„‚ βˆ– {0}))
44 eqid 2727 . . . . . . . 8 (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝑠) = (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝑠)
4543, 44fmptd 7118 . . . . . . 7 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝑠):(𝐴(,)𝐡)⟢(β„‚ βˆ– {0}))
46 eqidd 2728 . . . . . . . . . . 11 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜(𝑋 + 𝑠))) = (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜(𝑋 + 𝑠))))
47 eqidd 2728 . . . . . . . . . . 11 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝐢) = (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝐢))
4830, 8, 10, 46, 47offval2 7699 . . . . . . . . . 10 (πœ‘ β†’ ((𝑠 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜(𝑋 + 𝑠))) ∘f βˆ’ (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝐢)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢)))
4948eqcomd 2733 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢)) = ((𝑠 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜(𝑋 + 𝑠))) ∘f βˆ’ (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝐢)))
5049oveq2d 7430 . . . . . . . 8 (πœ‘ β†’ (ℝ D (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢))) = (ℝ D ((𝑠 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜(𝑋 + 𝑠))) ∘f βˆ’ (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝐢))))
518recnd 11264 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ β„‚)
52 eqid 2727 . . . . . . . . . 10 (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜(𝑋 + 𝑠))) = (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜(𝑋 + 𝑠)))
5351, 52fmptd 7118 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜(𝑋 + 𝑠))):(𝐴(,)𝐡)βŸΆβ„‚)
5410recnd 11264 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐢 ∈ β„‚)
55 eqid 2727 . . . . . . . . . 10 (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝐢) = (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝐢)
5654, 55fmptd 7118 . . . . . . . . 9 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝐢):(𝐴(,)𝐡)βŸΆβ„‚)
57 fourierdlem59.a . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 ∈ ℝ)
58 fourierdlem59.b . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 ∈ ℝ)
59 eqid 2727 . . . . . . . . . . 11 (ℝ D (𝐹 β†Ύ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡)))) = (ℝ D (𝐹 β†Ύ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡))))
60 fourierdlem59.fdv . . . . . . . . . . . 12 (πœ‘ β†’ (ℝ D (𝐹 β†Ύ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐡))–cn→ℝ))
61 cncff 24800 . . . . . . . . . . . 12 ((ℝ D (𝐹 β†Ύ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐡))–cn→ℝ) β†’ (ℝ D (𝐹 β†Ύ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐡))βŸΆβ„)
6260, 61syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (ℝ D (𝐹 β†Ύ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐡))βŸΆβ„)
631, 3, 57, 58, 59, 62fourierdlem28 45446 . . . . . . . . . 10 (πœ‘ β†’ (ℝ D (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜(𝑋 + 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐡) ↦ ((ℝ D (𝐹 β†Ύ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡))))β€˜(𝑋 + 𝑠))))
64 ioosscn 13410 . . . . . . . . . . . 12 ((𝑋 + 𝐴)(,)(𝑋 + 𝐡)) βŠ† β„‚
6564a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡)) βŠ† β„‚)
66 ax-resscn 11187 . . . . . . . . . . . . . 14 ℝ βŠ† β„‚
6766a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ ℝ βŠ† β„‚)
6862, 67fssd 6734 . . . . . . . . . . . 12 (πœ‘ β†’ (ℝ D (𝐹 β†Ύ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐡))βŸΆβ„‚)
69 ssid 4000 . . . . . . . . . . . . . 14 β„‚ βŠ† β„‚
7069a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ β„‚ βŠ† β„‚)
71 cncfcdm 24805 . . . . . . . . . . . . 13 ((β„‚ βŠ† β„‚ ∧ (ℝ D (𝐹 β†Ύ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐡))–cn→ℝ)) β†’ ((ℝ D (𝐹 β†Ύ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐡))–cnβ†’β„‚) ↔ (ℝ D (𝐹 β†Ύ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐡))βŸΆβ„‚))
7270, 60, 71syl2anc 583 . . . . . . . . . . . 12 (πœ‘ β†’ ((ℝ D (𝐹 β†Ύ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐡))–cnβ†’β„‚) ↔ (ℝ D (𝐹 β†Ύ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐡))βŸΆβ„‚))
7368, 72mpbird 257 . . . . . . . . . . 11 (πœ‘ β†’ (ℝ D (𝐹 β†Ύ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐡))–cnβ†’β„‚))
74 ioosscn 13410 . . . . . . . . . . . 12 (𝐴(,)𝐡) βŠ† β„‚
7574a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† β„‚)
763recnd 11264 . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 ∈ β„‚)
773, 57readdcld 11265 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑋 + 𝐴) ∈ ℝ)
7877rexrd 11286 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑋 + 𝐴) ∈ ℝ*)
7978adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝐴) ∈ ℝ*)
803, 58readdcld 11265 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑋 + 𝐡) ∈ ℝ)
8180rexrd 11286 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑋 + 𝐡) ∈ ℝ*)
8281adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝐡) ∈ ℝ*)
8357adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 ∈ ℝ)
8483rexrd 11286 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 ∈ ℝ*)
8558rexrd 11286 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐡 ∈ ℝ*)
8685adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐡 ∈ ℝ*)
87 simpr 484 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 ∈ (𝐴(,)𝐡))
88 ioogtlb 44803 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 < 𝑠)
8984, 86, 87, 88syl3anc 1369 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐴 < 𝑠)
9083, 6, 4, 89ltadd2dd 11395 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝐴) < (𝑋 + 𝑠))
9158adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝐡 ∈ ℝ)
92 iooltub 44818 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 < 𝐡)
9384, 86, 87, 92syl3anc 1369 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ 𝑠 < 𝐡)
946, 91, 4, 93ltadd2dd 11395 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝑠) < (𝑋 + 𝐡))
9579, 82, 7, 90, 94eliood 44806 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ (𝐴(,)𝐡)) β†’ (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡)))
9665, 73, 75, 76, 95fourierdlem23 45441 . . . . . . . . . 10 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ ((ℝ D (𝐹 β†Ύ ((𝑋 + 𝐴)(,)(𝑋 + 𝐡))))β€˜(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
9763, 96eqeltrd 2828 . . . . . . . . 9 (πœ‘ β†’ (ℝ D (𝑠 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜(𝑋 + 𝑠)))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
98 iooretop 24669 . . . . . . . . . . . . 13 (𝐴(,)𝐡) ∈ (topGenβ€˜ran (,))
99 eqid 2727 . . . . . . . . . . . . . 14 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
10099tgioo2 24706 . . . . . . . . . . . . 13 (topGenβ€˜ran (,)) = ((TopOpenβ€˜β„‚fld) β†Ύt ℝ)
10198, 100eleqtri 2826 . . . . . . . . . . . 12 (𝐴(,)𝐡) ∈ ((TopOpenβ€˜β„‚fld) β†Ύt ℝ)
102101a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴(,)𝐡) ∈ ((TopOpenβ€˜β„‚fld) β†Ύt ℝ))
1039recnd 11264 . . . . . . . . . . 11 (πœ‘ β†’ 𝐢 ∈ β„‚)
10437, 102, 103dvmptconst 45226 . . . . . . . . . 10 (πœ‘ β†’ (ℝ D (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝐢)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ 0))
105 0cnd 11229 . . . . . . . . . . 11 (πœ‘ β†’ 0 ∈ β„‚)
10675, 105, 70constcncfg 45183 . . . . . . . . . 10 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ 0) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
107104, 106eqeltrd 2828 . . . . . . . . 9 (πœ‘ β†’ (ℝ D (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝐢)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
10837, 53, 56, 97, 107dvsubcncf 45235 . . . . . . . 8 (πœ‘ β†’ (ℝ D ((𝑠 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜(𝑋 + 𝑠))) ∘f βˆ’ (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝐢))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
10950, 108eqeltrd 2828 . . . . . . 7 (πœ‘ β†’ (ℝ D (𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
11037, 102dvmptidg 45228 . . . . . . . 8 (πœ‘ β†’ (ℝ D (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝑠)) = (𝑠 ∈ (𝐴(,)𝐡) ↦ 1))
111 1cnd 11231 . . . . . . . . 9 (πœ‘ β†’ 1 ∈ β„‚)
11275, 111, 70constcncfg 45183 . . . . . . . 8 (πœ‘ β†’ (𝑠 ∈ (𝐴(,)𝐡) ↦ 1) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
113110, 112eqeltrd 2828 . . . . . . 7 (πœ‘ β†’ (ℝ D (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝑠)) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
11437, 40, 45, 109, 113dvdivcncf 45238 . . . . . 6 (πœ‘ β†’ (ℝ D ((𝑠 ∈ (𝐴(,)𝐡) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ 𝐢)) ∘f / (𝑠 ∈ (𝐴(,)𝐡) ↦ 𝑠))) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
11535, 114eqeltrd 2828 . . . . 5 (πœ‘ β†’ (ℝ D 𝐻) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚))
116 cncff 24800 . . . . 5 ((ℝ D 𝐻) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚) β†’ (ℝ D 𝐻):(𝐴(,)𝐡)βŸΆβ„‚)
117 fdm 6725 . . . . 5 ((ℝ D 𝐻):(𝐴(,)𝐡)βŸΆβ„‚ β†’ dom (ℝ D 𝐻) = (𝐴(,)𝐡))
118115, 116, 1173syl 18 . . . 4 (πœ‘ β†’ dom (ℝ D 𝐻) = (𝐴(,)𝐡))
119118feq2d 6702 . . 3 (πœ‘ β†’ ((ℝ D 𝐻):dom (ℝ D 𝐻)βŸΆβ„ ↔ (ℝ D 𝐻):(𝐴(,)𝐡)βŸΆβ„))
12028, 119mpbid 231 . 2 (πœ‘ β†’ (ℝ D 𝐻):(𝐴(,)𝐡)βŸΆβ„)
121 cncfcdm 24805 . . 3 ((ℝ βŠ† β„‚ ∧ (ℝ D 𝐻) ∈ ((𝐴(,)𝐡)–cnβ†’β„‚)) β†’ ((ℝ D 𝐻) ∈ ((𝐴(,)𝐡)–cn→ℝ) ↔ (ℝ D 𝐻):(𝐴(,)𝐡)βŸΆβ„))
12267, 115, 121syl2anc 583 . 2 (πœ‘ β†’ ((ℝ D 𝐻) ∈ ((𝐴(,)𝐡)–cn→ℝ) ↔ (ℝ D 𝐻):(𝐴(,)𝐡)βŸΆβ„))
123120, 122mpbird 257 1 (πœ‘ β†’ (ℝ D 𝐻) ∈ ((𝐴(,)𝐡)–cn→ℝ))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534   ∈ wcel 2099   β‰  wne 2935  Vcvv 3469   βˆ– cdif 3941   βŠ† wss 3944  {csn 4624  {cpr 4626   class class class wbr 5142   ↦ cmpt 5225  dom cdm 5672  ran crn 5673   β†Ύ cres 5674  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7414   ∘f cof 7677  β„‚cc 11128  β„cr 11129  0cc0 11130  1c1 11131   + caddc 11133  β„*cxr 11269   < clt 11270   βˆ’ cmin 11466   / cdiv 11893  (,)cioo 13348   β†Ύt crest 17393  TopOpenctopn 17394  topGenctg 17410  β„‚fldccnfld 21266  β€“cnβ†’ccncf 24783   D cdv 25779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208  ax-addf 11209
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7865  df-1st 7987  df-2nd 7988  df-supp 8160  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-er 8718  df-map 8838  df-pm 8839  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9378  df-fi 9426  df-sup 9457  df-inf 9458  df-oi 9525  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-5 12300  df-6 12301  df-7 12302  df-8 12303  df-9 12304  df-n0 12495  df-z 12581  df-dec 12700  df-uz 12845  df-q 12955  df-rp 12999  df-xneg 13116  df-xadd 13117  df-xmul 13118  df-ioo 13352  df-icc 13355  df-fz 13509  df-fzo 13652  df-seq 13991  df-exp 14051  df-hash 14314  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-struct 17107  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-plusg 17237  df-mulr 17238  df-starv 17239  df-sca 17240  df-vsca 17241  df-ip 17242  df-tset 17243  df-ple 17244  df-ds 17246  df-unif 17247  df-hom 17248  df-cco 17249  df-rest 17395  df-topn 17396  df-0g 17414  df-gsum 17415  df-topgen 17416  df-pt 17417  df-prds 17420  df-xrs 17475  df-qtop 17480  df-imas 17481  df-xps 17483  df-mre 17557  df-mrc 17558  df-acs 17560  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-submnd 18732  df-mulg 19015  df-cntz 19259  df-cmn 19728  df-psmet 21258  df-xmet 21259  df-met 21260  df-bl 21261  df-mopn 21262  df-fbas 21263  df-fg 21264  df-cnfld 21267  df-top 22783  df-topon 22800  df-topsp 22822  df-bases 22836  df-cld 22910  df-ntr 22911  df-cls 22912  df-nei 22989  df-lp 23027  df-perf 23028  df-cn 23118  df-cnp 23119  df-t1 23205  df-haus 23206  df-tx 23453  df-hmeo 23646  df-fil 23737  df-fm 23829  df-flim 23830  df-flf 23831  df-xms 24213  df-ms 24214  df-tms 24215  df-cncf 24785  df-limc 25782  df-dv 25783
This theorem is referenced by:  fourierdlem72  45489
  Copyright terms: Public domain W3C validator