Proof of Theorem fourierdlem59
Step | Hyp | Ref
| Expression |
1 | | fourierdlem59.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
2 | 1 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐹:ℝ⟶ℝ) |
3 | | fourierdlem59.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℝ) |
4 | 3 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℝ) |
5 | | elioore 12965 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ) |
6 | 5 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ) |
7 | 4, 6 | readdcld 10862 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ℝ) |
8 | 2, 7 | ffvelrnd 6905 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ) |
9 | | fourierdlem59.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℝ) |
10 | 9 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℝ) |
11 | 8, 10 | resubcld 11260 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℝ) |
12 | | eqcom 2744 |
. . . . . . . . . . . 12
⊢ (𝑠 = 0 ↔ 0 = 𝑠) |
13 | 12 | biimpi 219 |
. . . . . . . . . . 11
⊢ (𝑠 = 0 → 0 = 𝑠) |
14 | 13 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 0 = 𝑠) |
15 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 𝑠 ∈ (𝐴(,)𝐵)) |
16 | 14, 15 | eqeltrd 2838 |
. . . . . . . . 9
⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵)) |
17 | 16 | adantll 714 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → 0 ∈ (𝐴(,)𝐵)) |
18 | | fourierdlem59.n0 |
. . . . . . . . 9
⊢ (𝜑 → ¬ 0 ∈ (𝐴(,)𝐵)) |
19 | 18 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) ∧ 𝑠 = 0) → ¬ 0 ∈ (𝐴(,)𝐵)) |
20 | 17, 19 | pm2.65da 817 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ¬ 𝑠 = 0) |
21 | 20 | neqned 2947 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≠ 0) |
22 | 11, 6, 21 | redivcld 11660 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) ∈ ℝ) |
23 | | fourierdlem59.h |
. . . . 5
⊢ 𝐻 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) |
24 | 22, 23 | fmptd 6931 |
. . . 4
⊢ (𝜑 → 𝐻:(𝐴(,)𝐵)⟶ℝ) |
25 | | ioossre 12996 |
. . . . 5
⊢ (𝐴(,)𝐵) ⊆ ℝ |
26 | 25 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
27 | | dvfre 24848 |
. . . 4
⊢ ((𝐻:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐻):dom (ℝ D 𝐻)⟶ℝ) |
28 | 24, 26, 27 | syl2anc 587 |
. . 3
⊢ (𝜑 → (ℝ D 𝐻):dom (ℝ D 𝐻)⟶ℝ) |
29 | | ovex 7246 |
. . . . . . . . . 10
⊢ (𝐴(,)𝐵) ∈ V |
30 | 29 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝐵) ∈ V) |
31 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) |
32 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠)) |
33 | 30, 11, 6, 31, 32 | offval2 7488 |
. . . . . . . 8
⊢ (𝜑 → ((𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∘f / (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠))) |
34 | 23, 33 | eqtr4id 2797 |
. . . . . . 7
⊢ (𝜑 → 𝐻 = ((𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∘f / (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠))) |
35 | 34 | oveq2d 7229 |
. . . . . 6
⊢ (𝜑 → (ℝ D 𝐻) = (ℝ D ((𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∘f / (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠)))) |
36 | | reelprrecn 10821 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
37 | 36 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
38 | 11 | recnd 10861 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ) |
39 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) |
40 | 38, 39 | fmptd 6931 |
. . . . . . 7
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)):(𝐴(,)𝐵)⟶ℂ) |
41 | 6 | recnd 10861 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℂ) |
42 | | eldifsn 4700 |
. . . . . . . . 9
⊢ (𝑠 ∈ (ℂ ∖ {0})
↔ (𝑠 ∈ ℂ
∧ 𝑠 ≠
0)) |
43 | 41, 21, 42 | sylanbrc 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (ℂ ∖
{0})) |
44 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠) |
45 | 43, 44 | fmptd 6931 |
. . . . . . 7
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠):(𝐴(,)𝐵)⟶(ℂ ∖
{0})) |
46 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) |
47 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) |
48 | 30, 8, 10, 46, 47 | offval2 7488 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) ∘f − (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) |
49 | 48 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) = ((𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) ∘f − (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶))) |
50 | 49 | oveq2d 7229 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (ℝ D ((𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) ∘f − (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)))) |
51 | 8 | recnd 10861 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ) |
52 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) |
53 | 51, 52 | fmptd 6931 |
. . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))):(𝐴(,)𝐵)⟶ℂ) |
54 | 10 | recnd 10861 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℂ) |
55 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶) |
56 | 54, 55 | fmptd 6931 |
. . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶):(𝐴(,)𝐵)⟶ℂ) |
57 | | fourierdlem59.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
58 | | fourierdlem59.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
59 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (ℝ
D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) = (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) |
60 | | fourierdlem59.fdv |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐵))–cn→ℝ)) |
61 | | cncff 23790 |
. . . . . . . . . . . 12
⊢ ((ℝ
D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐵))–cn→ℝ) → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ) |
63 | 1, 3, 57, 58, 59, 62 | fourierdlem28 43351 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))) |
64 | | ioosscn 12997 |
. . . . . . . . . . . 12
⊢ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)) ⊆ ℂ |
65 | 64 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)) ⊆ ℂ) |
66 | | ax-resscn 10786 |
. . . . . . . . . . . . . 14
⊢ ℝ
⊆ ℂ |
67 | 66 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℝ ⊆
ℂ) |
68 | 62, 67 | fssd 6563 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℂ) |
69 | | ssid 3923 |
. . . . . . . . . . . . . 14
⊢ ℂ
⊆ ℂ |
70 | 69 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℂ ⊆
ℂ) |
71 | | cncffvrn 23795 |
. . . . . . . . . . . . 13
⊢ ((ℂ
⊆ ℂ ∧ (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐵))–cn→ℝ)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐵))–cn→ℂ) ↔ (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℂ)) |
72 | 70, 60, 71 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐵))–cn→ℂ) ↔ (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℂ)) |
73 | 68, 72 | mpbird 260 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐵))–cn→ℂ)) |
74 | | ioosscn 12997 |
. . . . . . . . . . . 12
⊢ (𝐴(,)𝐵) ⊆ ℂ |
75 | 74 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) |
76 | 3 | recnd 10861 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℂ) |
77 | 3, 57 | readdcld 10862 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 + 𝐴) ∈ ℝ) |
78 | 77 | rexrd 10883 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 + 𝐴) ∈
ℝ*) |
79 | 78 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) ∈
ℝ*) |
80 | 3, 58 | readdcld 10862 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 + 𝐵) ∈ ℝ) |
81 | 80 | rexrd 10883 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 + 𝐵) ∈
ℝ*) |
82 | 81 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐵) ∈
ℝ*) |
83 | 57 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ) |
84 | 83 | rexrd 10883 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈
ℝ*) |
85 | 58 | rexrd 10883 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
86 | 85 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈
ℝ*) |
87 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴(,)𝐵)) |
88 | | ioogtlb 42708 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑠
∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠) |
89 | 84, 86, 87, 88 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠) |
90 | 83, 6, 4, 89 | ltadd2dd 10991 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) < (𝑋 + 𝑠)) |
91 | 58 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ) |
92 | | iooltub 42723 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑠
∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵) |
93 | 84, 86, 87, 92 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵) |
94 | 6, 91, 4, 93 | ltadd2dd 10991 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝑋 + 𝐵)) |
95 | 79, 82, 7, 90, 94 | eliood 42711 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) |
96 | 65, 73, 75, 76, 95 | fourierdlem23 43346 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
97 | 63, 96 | eqeltrd 2838 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
98 | | iooretop 23663 |
. . . . . . . . . . . . 13
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) |
99 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
100 | 99 | tgioo2 23700 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
101 | 98, 100 | eleqtri 2836 |
. . . . . . . . . . . 12
⊢ (𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t
ℝ) |
102 | 101 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t
ℝ)) |
103 | 9 | recnd 10861 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℂ) |
104 | 37, 102, 103 | dvmptconst 43131 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 0)) |
105 | | 0cnd 10826 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℂ) |
106 | 75, 105, 70 | constcncfg 43088 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ 0) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
107 | 104, 106 | eqeltrd 2838 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
108 | 37, 53, 56, 97, 107 | dvsubcncf 43140 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D ((𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) ∘f − (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
109 | 50, 108 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
110 | 37, 102 | dvmptidg 43133 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 1)) |
111 | | 1cnd 10828 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) |
112 | 75, 111, 70 | constcncfg 43088 |
. . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ 1) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
113 | 110, 112 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
114 | 37, 40, 45, 109, 113 | dvdivcncf 43143 |
. . . . . 6
⊢ (𝜑 → (ℝ D ((𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∘f / (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
115 | 35, 114 | eqeltrd 2838 |
. . . . 5
⊢ (𝜑 → (ℝ D 𝐻) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
116 | | cncff 23790 |
. . . . 5
⊢ ((ℝ
D 𝐻) ∈ ((𝐴(,)𝐵)–cn→ℂ) → (ℝ D 𝐻):(𝐴(,)𝐵)⟶ℂ) |
117 | | fdm 6554 |
. . . . 5
⊢ ((ℝ
D 𝐻):(𝐴(,)𝐵)⟶ℂ → dom (ℝ D 𝐻) = (𝐴(,)𝐵)) |
118 | 115, 116,
117 | 3syl 18 |
. . . 4
⊢ (𝜑 → dom (ℝ D 𝐻) = (𝐴(,)𝐵)) |
119 | 118 | feq2d 6531 |
. . 3
⊢ (𝜑 → ((ℝ D 𝐻):dom (ℝ D 𝐻)⟶ℝ ↔ (ℝ
D 𝐻):(𝐴(,)𝐵)⟶ℝ)) |
120 | 28, 119 | mpbid 235 |
. 2
⊢ (𝜑 → (ℝ D 𝐻):(𝐴(,)𝐵)⟶ℝ) |
121 | | cncffvrn 23795 |
. . 3
⊢ ((ℝ
⊆ ℂ ∧ (ℝ D 𝐻) ∈ ((𝐴(,)𝐵)–cn→ℂ)) → ((ℝ D 𝐻) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (ℝ D 𝐻):(𝐴(,)𝐵)⟶ℝ)) |
122 | 67, 115, 121 | syl2anc 587 |
. 2
⊢ (𝜑 → ((ℝ D 𝐻) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (ℝ D 𝐻):(𝐴(,)𝐵)⟶ℝ)) |
123 | 120, 122 | mpbird 260 |
1
⊢ (𝜑 → (ℝ D 𝐻) ∈ ((𝐴(,)𝐵)–cn→ℝ)) |