Proof of Theorem fourierdlem59
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fourierdlem59.f | . . . . . . . . 9
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) | 
| 2 | 1 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐹:ℝ⟶ℝ) | 
| 3 |  | fourierdlem59.x | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℝ) | 
| 4 | 3 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑋 ∈ ℝ) | 
| 5 |  | elioore 13418 | . . . . . . . . . 10
⊢ (𝑠 ∈ (𝐴(,)𝐵) → 𝑠 ∈ ℝ) | 
| 6 | 5 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℝ) | 
| 7 | 4, 6 | readdcld 11291 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ℝ) | 
| 8 | 2, 7 | ffvelcdmd 7104 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ) | 
| 9 |  | fourierdlem59.c | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 10 | 9 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℝ) | 
| 11 | 8, 10 | resubcld 11692 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℝ) | 
| 12 |  | eqcom 2743 | . . . . . . . . . . . 12
⊢ (𝑠 = 0 ↔ 0 = 𝑠) | 
| 13 | 12 | biimpi 216 | . . . . . . . . . . 11
⊢ (𝑠 = 0 → 0 = 𝑠) | 
| 14 | 13 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 0 = 𝑠) | 
| 15 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝑠 ∈ (𝐴(,)𝐵) ∧ 𝑠 = 0) → 𝑠 ∈ (𝐴(,)𝐵)) | 
| 16 | 14, 15 | eqeltrd 2840 | . . . . . . . . 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 816 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ¬ 𝑠 = 0) | 
| 21 | 20 | neqned 2946 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ≠ 0) | 
| 22 | 11, 6, 21 | redivcld 12096 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) ∈ ℝ) | 
| 23 |  | fourierdlem59.h | . . . . 5
⊢ 𝐻 = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠)) | 
| 24 | 22, 23 | fmptd 7133 | . . . 4
⊢ (𝜑 → 𝐻:(𝐴(,)𝐵)⟶ℝ) | 
| 25 |  | ioossre 13449 | . . . . 5
⊢ (𝐴(,)𝐵) ⊆ ℝ | 
| 26 | 25 | a1i 11 | . . . 4
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) | 
| 27 |  | dvfre 25990 | . . . 4
⊢ ((𝐻:(𝐴(,)𝐵)⟶ℝ ∧ (𝐴(,)𝐵) ⊆ ℝ) → (ℝ D 𝐻):dom (ℝ D 𝐻)⟶ℝ) | 
| 28 | 24, 26, 27 | syl2anc 584 | . . 3
⊢ (𝜑 → (ℝ D 𝐻):dom (ℝ D 𝐻)⟶ℝ) | 
| 29 |  | ovex 7465 | . . . . . . . . . 10
⊢ (𝐴(,)𝐵) ∈ V | 
| 30 | 29 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝐵) ∈ V) | 
| 31 |  | eqidd 2737 | . . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) | 
| 32 |  | eqidd 2737 | . . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠)) | 
| 33 | 30, 11, 6, 31, 32 | offval2 7718 | . . . . . . . 8
⊢ (𝜑 → ((𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∘f / (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠))) | 
| 34 | 23, 33 | eqtr4id 2795 | . . . . . . 7
⊢ (𝜑 → 𝐻 = ((𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∘f / (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠))) | 
| 35 | 34 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → (ℝ D 𝐻) = (ℝ D ((𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∘f / (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠)))) | 
| 36 |  | reelprrecn 11248 | . . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} | 
| 37 | 36 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) | 
| 38 | 11 | recnd 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → ((𝐹‘(𝑋 + 𝑠)) − 𝐶) ∈ ℂ) | 
| 39 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) | 
| 40 | 38, 39 | fmptd 7133 | . . . . . . 7
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)):(𝐴(,)𝐵)⟶ℂ) | 
| 41 | 6 | recnd 11290 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ ℂ) | 
| 42 |  | eldifsn 4785 | . . . . . . . . 9
⊢ (𝑠 ∈ (ℂ ∖ {0})
↔ (𝑠 ∈ ℂ
∧ 𝑠 ≠
0)) | 
| 43 | 41, 21, 42 | sylanbrc 583 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (ℂ ∖
{0})) | 
| 44 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠) | 
| 45 | 43, 44 | fmptd 7133 | . . . . . . 7
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠):(𝐴(,)𝐵)⟶(ℂ ∖
{0})) | 
| 46 |  | eqidd 2737 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) | 
| 47 |  | eqidd 2737 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) | 
| 48 | 30, 8, 10, 46, 47 | offval2 7718 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) ∘f − (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) | 
| 49 | 48 | eqcomd 2742 | . . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) = ((𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) ∘f − (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶))) | 
| 50 | 49 | oveq2d 7448 | . . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) = (ℝ D ((𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) ∘f − (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)))) | 
| 51 | 8 | recnd 11290 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ) | 
| 52 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) | 
| 53 | 51, 52 | fmptd 7133 | . . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))):(𝐴(,)𝐵)⟶ℂ) | 
| 54 | 10 | recnd 11290 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐶 ∈ ℂ) | 
| 55 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶) | 
| 56 | 54, 55 | fmptd 7133 | . . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶):(𝐴(,)𝐵)⟶ℂ) | 
| 57 |  | fourierdlem59.a | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 58 |  | fourierdlem59.b | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 59 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (ℝ
D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) = (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) | 
| 60 |  | fourierdlem59.fdv | . . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐵))–cn→ℝ)) | 
| 61 |  | cncff 24920 | . . . . . . . . . . . 12
⊢ ((ℝ
D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐵))–cn→ℝ) → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ) | 
| 62 | 60, 61 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℝ) | 
| 63 | 1, 3, 57, 58, 59, 62 | fourierdlem28 46155 | . . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) = (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠)))) | 
| 64 |  | ioosscn 13450 | . . . . . . . . . . . 12
⊢ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)) ⊆ ℂ | 
| 65 | 64 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)) ⊆ ℂ) | 
| 66 |  | ax-resscn 11213 | . . . . . . . . . . . . . 14
⊢ ℝ
⊆ ℂ | 
| 67 | 66 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → ℝ ⊆
ℂ) | 
| 68 | 62, 67 | fssd 6752 | . . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℂ) | 
| 69 |  | ssid 4005 | . . . . . . . . . . . . . 14
⊢ ℂ
⊆ ℂ | 
| 70 | 69 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → ℂ ⊆
ℂ) | 
| 71 |  | cncfcdm 24925 | . . . . . . . . . . . . 13
⊢ ((ℂ
⊆ ℂ ∧ (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐵))–cn→ℝ)) → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐵))–cn→ℂ) ↔ (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℂ)) | 
| 72 | 70, 60, 71 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐵))–cn→ℂ) ↔ (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))):((𝑋 + 𝐴)(,)(𝑋 + 𝐵))⟶ℂ)) | 
| 73 | 68, 72 | mpbird 257 | . . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵)))) ∈ (((𝑋 + 𝐴)(,)(𝑋 + 𝐵))–cn→ℂ)) | 
| 74 |  | ioosscn 13450 | . . . . . . . . . . . 12
⊢ (𝐴(,)𝐵) ⊆ ℂ | 
| 75 | 74 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ) | 
| 76 | 3 | recnd 11290 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℂ) | 
| 77 | 3, 57 | readdcld 11291 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 + 𝐴) ∈ ℝ) | 
| 78 | 77 | rexrd 11312 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 + 𝐴) ∈
ℝ*) | 
| 79 | 78 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) ∈
ℝ*) | 
| 80 | 3, 58 | readdcld 11291 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 + 𝐵) ∈ ℝ) | 
| 81 | 80 | rexrd 11312 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 + 𝐵) ∈
ℝ*) | 
| 82 | 81 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐵) ∈
ℝ*) | 
| 83 | 57 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ) | 
| 84 | 83 | rexrd 11312 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 ∈
ℝ*) | 
| 85 | 58 | rexrd 11312 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 86 | 85 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈
ℝ*) | 
| 87 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 ∈ (𝐴(,)𝐵)) | 
| 88 |  | ioogtlb 45513 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑠
∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠) | 
| 89 | 84, 86, 87, 88 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑠) | 
| 90 | 83, 6, 4, 89 | ltadd2dd 11421 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝐴) < (𝑋 + 𝑠)) | 
| 91 | 58 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝐵 ∈ ℝ) | 
| 92 |  | iooltub 45528 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑠
∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵) | 
| 93 | 84, 86, 87, 92 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → 𝑠 < 𝐵) | 
| 94 | 6, 91, 4, 93 | ltadd2dd 11421 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) < (𝑋 + 𝐵)) | 
| 95 | 79, 82, 7, 90, 94 | eliood 45516 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝐴(,)𝐵)) → (𝑋 + 𝑠) ∈ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))) | 
| 96 | 65, 73, 75, 76, 95 | fourierdlem23 46150 | . . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ ((ℝ D (𝐹 ↾ ((𝑋 + 𝐴)(,)(𝑋 + 𝐵))))‘(𝑋 + 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 97 | 63, 96 | eqeltrd 2840 | . . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠)))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 98 |  | iooretop 24787 | . . . . . . . . . . . . 13
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) | 
| 99 |  | tgioo4 24827 | . . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) | 
| 100 | 98, 99 | eleqtri 2838 | . . . . . . . . . . . 12
⊢ (𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t
ℝ) | 
| 101 | 100 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴(,)𝐵) ∈
((TopOpen‘ℂfld) ↾t
ℝ)) | 
| 102 | 9 | recnd 11290 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 103 | 37, 101, 102 | dvmptconst 45935 | . . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 0)) | 
| 104 |  | 0cnd 11255 | . . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℂ) | 
| 105 | 75, 104, 70 | constcncfg 45892 | . . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ 0) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 106 | 103, 105 | eqeltrd 2840 | . . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 107 | 37, 53, 56, 97, 106 | dvsubcncf 45944 | . . . . . . . 8
⊢ (𝜑 → (ℝ D ((𝑠 ∈ (𝐴(,)𝐵) ↦ (𝐹‘(𝑋 + 𝑠))) ∘f − (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝐶))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 108 | 50, 107 | eqeltrd 2840 | . . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 109 | 37, 101 | dvmptidg 45937 | . . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠)) = (𝑠 ∈ (𝐴(,)𝐵) ↦ 1)) | 
| 110 |  | 1cnd 11257 | . . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) | 
| 111 | 75, 110, 70 | constcncfg 45892 | . . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ (𝐴(,)𝐵) ↦ 1) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 112 | 109, 111 | eqeltrd 2840 | . . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 113 | 37, 40, 45, 108, 112 | dvdivcncf 45947 | . . . . . 6
⊢ (𝜑 → (ℝ D ((𝑠 ∈ (𝐴(,)𝐵) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝐶)) ∘f / (𝑠 ∈ (𝐴(,)𝐵) ↦ 𝑠))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 114 | 35, 113 | eqeltrd 2840 | . . . . 5
⊢ (𝜑 → (ℝ D 𝐻) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 115 |  | cncff 24920 | . . . . 5
⊢ ((ℝ
D 𝐻) ∈ ((𝐴(,)𝐵)–cn→ℂ) → (ℝ D 𝐻):(𝐴(,)𝐵)⟶ℂ) | 
| 116 |  | fdm 6744 | . . . . 5
⊢ ((ℝ
D 𝐻):(𝐴(,)𝐵)⟶ℂ → dom (ℝ D 𝐻) = (𝐴(,)𝐵)) | 
| 117 | 114, 115,
116 | 3syl 18 | . . . 4
⊢ (𝜑 → dom (ℝ D 𝐻) = (𝐴(,)𝐵)) | 
| 118 | 117 | feq2d 6721 | . . 3
⊢ (𝜑 → ((ℝ D 𝐻):dom (ℝ D 𝐻)⟶ℝ ↔ (ℝ
D 𝐻):(𝐴(,)𝐵)⟶ℝ)) | 
| 119 | 28, 118 | mpbid 232 | . 2
⊢ (𝜑 → (ℝ D 𝐻):(𝐴(,)𝐵)⟶ℝ) | 
| 120 |  | cncfcdm 24925 | . . 3
⊢ ((ℝ
⊆ ℂ ∧ (ℝ D 𝐻) ∈ ((𝐴(,)𝐵)–cn→ℂ)) → ((ℝ D 𝐻) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (ℝ D 𝐻):(𝐴(,)𝐵)⟶ℝ)) | 
| 121 | 67, 114, 120 | syl2anc 584 | . 2
⊢ (𝜑 → ((ℝ D 𝐻) ∈ ((𝐴(,)𝐵)–cn→ℝ) ↔ (ℝ D 𝐻):(𝐴(,)𝐵)⟶ℝ)) | 
| 122 | 119, 121 | mpbird 257 | 1
⊢ (𝜑 → (ℝ D 𝐻) ∈ ((𝐴(,)𝐵)–cn→ℝ)) |