Proof of Theorem fourierdlem58
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pire 26501 | . . . . . . . . . 10
⊢ π
∈ ℝ | 
| 2 | 1 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → π ∈
ℝ) | 
| 3 | 2 | renegcld 11691 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → -π ∈
ℝ) | 
| 4 | 3, 2 | iccssred 13475 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (-π[,]π) ⊆
ℝ) | 
| 5 |  | fourierdlem58.ass | . . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ (-π[,]π)) | 
| 6 | 5 | sselda 3982 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ (-π[,]π)) | 
| 7 | 4, 6 | sseldd 3983 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ℝ) | 
| 8 |  | 2re 12341 | . . . . . . . 8
⊢ 2 ∈
ℝ | 
| 9 | 8 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 2 ∈ ℝ) | 
| 10 | 7 | rehalfcld 12515 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑠 / 2) ∈ ℝ) | 
| 11 | 10 | resincld 16180 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (sin‘(𝑠 / 2)) ∈ ℝ) | 
| 12 | 9, 11 | remulcld 11292 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (2 · (sin‘(𝑠 / 2))) ∈
ℝ) | 
| 13 |  | 2cnd 12345 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 2 ∈ ℂ) | 
| 14 | 7 | recnd 11290 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ℂ) | 
| 15 | 14 | halfcld 12513 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑠 / 2) ∈ ℂ) | 
| 16 | 15 | sincld 16167 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (sin‘(𝑠 / 2)) ∈ ℂ) | 
| 17 |  | 2ne0 12371 | . . . . . . . 8
⊢ 2 ≠
0 | 
| 18 | 17 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 2 ≠ 0) | 
| 19 |  | eqcom 2743 | . . . . . . . . . . . . . 14
⊢ (𝑠 = 0 ↔ 0 = 𝑠) | 
| 20 | 19 | biimpi 216 | . . . . . . . . . . . . 13
⊢ (𝑠 = 0 → 0 = 𝑠) | 
| 21 | 20 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑠 ∈ 𝐴 ∧ 𝑠 = 0) → 0 = 𝑠) | 
| 22 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑠 ∈ 𝐴 ∧ 𝑠 = 0) → 𝑠 ∈ 𝐴) | 
| 23 | 21, 22 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ ((𝑠 ∈ 𝐴 ∧ 𝑠 = 0) → 0 ∈ 𝐴) | 
| 24 | 23 | adantll 714 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐴) ∧ 𝑠 = 0) → 0 ∈ 𝐴) | 
| 25 |  | fourierdlem58.0nA | . . . . . . . . . . 11
⊢ (𝜑 → ¬ 0 ∈ 𝐴) | 
| 26 | 25 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐴) ∧ 𝑠 = 0) → ¬ 0 ∈ 𝐴) | 
| 27 | 24, 26 | pm2.65da 816 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ¬ 𝑠 = 0) | 
| 28 | 27 | neqned 2946 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ≠ 0) | 
| 29 |  | fourierdlem44 46171 | . . . . . . . 8
⊢ ((𝑠 ∈ (-π[,]π) ∧
𝑠 ≠ 0) →
(sin‘(𝑠 / 2)) ≠
0) | 
| 30 | 6, 28, 29 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (sin‘(𝑠 / 2)) ≠ 0) | 
| 31 | 13, 16, 18, 30 | mulne0d 11916 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (2 · (sin‘(𝑠 / 2))) ≠ 0) | 
| 32 | 7, 12, 31 | redivcld 12096 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℝ) | 
| 33 |  | fourierdlem58.k | . . . . 5
⊢ 𝐾 = (𝑠 ∈ 𝐴 ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) | 
| 34 | 32, 33 | fmptd 7133 | . . . 4
⊢ (𝜑 → 𝐾:𝐴⟶ℝ) | 
| 35 | 1 | a1i 11 | . . . . . . 7
⊢ (𝜑 → π ∈
ℝ) | 
| 36 | 35 | renegcld 11691 | . . . . . 6
⊢ (𝜑 → -π ∈
ℝ) | 
| 37 | 36, 35 | iccssred 13475 | . . . . 5
⊢ (𝜑 → (-π[,]π) ⊆
ℝ) | 
| 38 | 5, 37 | sstrd 3993 | . . . 4
⊢ (𝜑 → 𝐴 ⊆ ℝ) | 
| 39 |  | dvfre 25990 | . . . 4
⊢ ((𝐾:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (ℝ D 𝐾):dom (ℝ D 𝐾)⟶ℝ) | 
| 40 | 34, 38, 39 | syl2anc 584 | . . 3
⊢ (𝜑 → (ℝ D 𝐾):dom (ℝ D 𝐾)⟶ℝ) | 
| 41 |  | fourierdlem58.4 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ (topGen‘ran
(,))) | 
| 42 |  | eqidd 2737 | . . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ 𝑠) = (𝑠 ∈ 𝐴 ↦ 𝑠)) | 
| 43 |  | eqidd 2737 | . . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))) | 
| 44 | 41, 7, 12, 42, 43 | offval2 7718 | . . . . . . . 8
⊢ (𝜑 → ((𝑠 ∈ 𝐴 ↦ 𝑠) ∘f / (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ 𝐴 ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))) | 
| 45 | 33, 44 | eqtr4id 2795 | . . . . . . 7
⊢ (𝜑 → 𝐾 = ((𝑠 ∈ 𝐴 ↦ 𝑠) ∘f / (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))))) | 
| 46 | 45 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → (ℝ D 𝐾) = (ℝ D ((𝑠 ∈ 𝐴 ↦ 𝑠) ∘f / (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))))) | 
| 47 |  | reelprrecn 11248 | . . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} | 
| 48 | 47 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) | 
| 49 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑠 ∈ 𝐴 ↦ 𝑠) = (𝑠 ∈ 𝐴 ↦ 𝑠) | 
| 50 | 14, 49 | fmptd 7133 | . . . . . . 7
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ 𝑠):𝐴⟶ℂ) | 
| 51 | 13, 16 | mulcld 11282 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (2 · (sin‘(𝑠 / 2))) ∈
ℂ) | 
| 52 | 31 | neneqd 2944 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ¬ (2 · (sin‘(𝑠 / 2))) = 0) | 
| 53 |  | elsng 4639 | . . . . . . . . . . 11
⊢ ((2
· (sin‘(𝑠 /
2))) ∈ ℝ → ((2 · (sin‘(𝑠 / 2))) ∈ {0} ↔ (2 ·
(sin‘(𝑠 / 2))) =
0)) | 
| 54 | 12, 53 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ((2 · (sin‘(𝑠 / 2))) ∈ {0} ↔ (2
· (sin‘(𝑠 /
2))) = 0)) | 
| 55 | 52, 54 | mtbird 325 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ¬ (2 · (sin‘(𝑠 / 2))) ∈
{0}) | 
| 56 | 51, 55 | eldifd 3961 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖
{0})) | 
| 57 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))) | 
| 58 | 56, 57 | fmptd 7133 | . . . . . . 7
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))):𝐴⟶(ℂ ∖
{0})) | 
| 59 |  | tgioo4 24827 | . . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) | 
| 60 | 41, 59 | eleqtrdi 2850 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈
((TopOpen‘ℂfld) ↾t
ℝ)) | 
| 61 | 48, 60 | dvmptidg 45937 | . . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ 𝐴 ↦ 𝑠)) = (𝑠 ∈ 𝐴 ↦ 1)) | 
| 62 |  | ax-resscn 11213 | . . . . . . . . . . 11
⊢ ℝ
⊆ ℂ | 
| 63 | 62 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → ℝ ⊆
ℂ) | 
| 64 | 38, 63 | sstrd 3993 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ℂ) | 
| 65 |  | 1cnd 11257 | . . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) | 
| 66 |  | ssid 4005 | . . . . . . . . . 10
⊢ ℂ
⊆ ℂ | 
| 67 | 66 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → ℂ ⊆
ℂ) | 
| 68 | 64, 65, 67 | constcncfg 45892 | . . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ 1) ∈ (𝐴–cn→ℂ)) | 
| 69 | 61, 68 | eqeltrd 2840 | . . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ 𝐴 ↦ 𝑠)) ∈ (𝐴–cn→ℂ)) | 
| 70 | 38 | resmptd 6057 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 / 2))))
↾ 𝐴) = (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))) | 
| 71 | 70 | eqcomd 2742 | . . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))) = ((𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 / 2))))
↾ 𝐴)) | 
| 72 | 71 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))) = (ℝ D ((𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2)))) ↾ 𝐴))) | 
| 73 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ (𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2)))) = (𝑠 ∈ ℝ
↦ (2 · (sin‘(𝑠 / 2)))) | 
| 74 |  | 2cnd 12345 | . . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℝ → 2 ∈
ℂ) | 
| 75 |  | recn 11246 | . . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ℝ → 𝑠 ∈
ℂ) | 
| 76 | 75 | halfcld 12513 | . . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℝ → (𝑠 / 2) ∈
ℂ) | 
| 77 | 76 | sincld 16167 | . . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℝ →
(sin‘(𝑠 / 2)) ∈
ℂ) | 
| 78 | 74, 77 | mulcld 11282 | . . . . . . . . . . . 12
⊢ (𝑠 ∈ ℝ → (2
· (sin‘(𝑠 /
2))) ∈ ℂ) | 
| 79 | 73, 78 | fmpti 7131 | . . . . . . . . . . 11
⊢ (𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2)))):ℝ⟶ℂ | 
| 80 | 79 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 /
2)))):ℝ⟶ℂ) | 
| 81 |  | ssid 4005 | . . . . . . . . . . 11
⊢ ℝ
⊆ ℝ | 
| 82 | 81 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → ℝ ⊆
ℝ) | 
| 83 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 84 | 83, 59 | dvres 25947 | . . . . . . . . . 10
⊢
(((ℝ ⊆ ℂ ∧ (𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 /
2)))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ 𝐴 ⊆ ℝ)) →
(ℝ D ((𝑠 ∈
ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ 𝐴)) = ((ℝ D (𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 / 2)))))
↾ ((int‘(topGen‘ran (,)))‘𝐴))) | 
| 85 | 63, 80, 82, 38, 84 | syl22anc 838 | . . . . . . . . 9
⊢ (𝜑 → (ℝ D ((𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2)))) ↾ 𝐴)) =
((ℝ D (𝑠 ∈
ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾
((int‘(topGen‘ran (,)))‘𝐴))) | 
| 86 |  | retop 24783 | . . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) ∈ Top | 
| 87 | 86 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → (topGen‘ran (,))
∈ Top) | 
| 88 |  | uniretop 24784 | . . . . . . . . . . . . . 14
⊢ ℝ =
∪ (topGen‘ran (,)) | 
| 89 | 88 | isopn3 23075 | . . . . . . . . . . . . 13
⊢
(((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → (𝐴 ∈ (topGen‘ran (,)) ↔
((int‘(topGen‘ran (,)))‘𝐴) = 𝐴)) | 
| 90 | 87, 38, 89 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∈ (topGen‘ran (,)) ↔
((int‘(topGen‘ran (,)))‘𝐴) = 𝐴)) | 
| 91 | 41, 90 | mpbid 232 | . . . . . . . . . . 11
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘𝐴) = 𝐴) | 
| 92 | 91 | reseq2d 5996 | . . . . . . . . . 10
⊢ (𝜑 → ((ℝ D (𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2))))) ↾ ((int‘(topGen‘ran (,)))‘𝐴)) = ((ℝ D (𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 / 2)))))
↾ 𝐴)) | 
| 93 |  | resmpt 6054 | . . . . . . . . . . . . . . . 16
⊢ (ℝ
⊆ ℂ → ((𝑠
∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ) = (𝑠 ∈ ℝ ↦ (2
· (sin‘((1 / 2) · 𝑠))))) | 
| 94 | 62, 93 | ax-mp 5 | . . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠)))) ↾ ℝ) = (𝑠 ∈ ℝ ↦ (2 ·
(sin‘((1 / 2) · 𝑠)))) | 
| 95 |  | id 22 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℂ → 𝑠 ∈
ℂ) | 
| 96 |  | 2cnd 12345 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℂ → 2 ∈
ℂ) | 
| 97 | 17 | a1i 11 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℂ → 2 ≠
0) | 
| 98 | 95, 96, 97 | divrec2d 12048 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ ℂ → (𝑠 / 2) = ((1 / 2) · 𝑠)) | 
| 99 | 98 | eqcomd 2742 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ ℂ → ((1 / 2)
· 𝑠) = (𝑠 / 2)) | 
| 100 | 75, 99 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℝ → ((1 / 2)
· 𝑠) = (𝑠 / 2)) | 
| 101 | 100 | fveq2d 6909 | . . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ℝ →
(sin‘((1 / 2) · 𝑠)) = (sin‘(𝑠 / 2))) | 
| 102 | 101 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℝ → (2
· (sin‘((1 / 2) · 𝑠))) = (2 · (sin‘(𝑠 / 2)))) | 
| 103 | 102 | mpteq2ia 5244 | . . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ℝ ↦ (2
· (sin‘((1 / 2) · 𝑠)))) = (𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 /
2)))) | 
| 104 | 94, 103 | eqtr2i 2765 | . . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2)))) = ((𝑠 ∈ ℂ
↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ) | 
| 105 | 104 | oveq2i 7443 | . . . . . . . . . . . . 13
⊢ (ℝ
D (𝑠 ∈ ℝ ↦
(2 · (sin‘(𝑠 /
2))))) = (ℝ D ((𝑠
∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾
ℝ)) | 
| 106 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠)))) = (𝑠 ∈ ℂ ↦ (2 ·
(sin‘((1 / 2) · 𝑠)))) | 
| 107 |  | halfcn 12482 | . . . . . . . . . . . . . . . . . . 19
⊢ (1 / 2)
∈ ℂ | 
| 108 | 107 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℂ → (1 / 2)
∈ ℂ) | 
| 109 | 108, 95 | mulcld 11282 | . . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ℂ → ((1 / 2)
· 𝑠) ∈
ℂ) | 
| 110 | 109 | sincld 16167 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℂ →
(sin‘((1 / 2) · 𝑠)) ∈ ℂ) | 
| 111 | 96, 110 | mulcld 11282 | . . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ℂ → (2
· (sin‘((1 / 2) · 𝑠))) ∈ ℂ) | 
| 112 | 106, 111 | fmpti 7131 | . . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠)))):ℂ⟶ℂ | 
| 113 |  | 2cn 12342 | . . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℂ | 
| 114 |  | dvasinbx 45940 | . . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D (𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠))))) = (𝑠 ∈ ℂ ↦ ((2 · (1 / 2))
· (cos‘((1 / 2) · 𝑠))))) | 
| 115 | 113, 107,
114 | mp2an 692 | . . . . . . . . . . . . . . . . . 18
⊢ (ℂ
D (𝑠 ∈ ℂ ↦
(2 · (sin‘((1 / 2) · 𝑠))))) = (𝑠 ∈ ℂ ↦ ((2 · (1 / 2))
· (cos‘((1 / 2) · 𝑠)))) | 
| 116 | 113, 17 | recidi 11999 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (2
· (1 / 2)) = 1 | 
| 117 | 116 | a1i 11 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℂ → (2
· (1 / 2)) = 1) | 
| 118 | 99 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℂ →
(cos‘((1 / 2) · 𝑠)) = (cos‘(𝑠 / 2))) | 
| 119 | 117, 118 | oveq12d 7450 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ ℂ → ((2
· (1 / 2)) · (cos‘((1 / 2) · 𝑠))) = (1 · (cos‘(𝑠 / 2)))) | 
| 120 |  | halfcl 12494 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 ∈ ℂ → (𝑠 / 2) ∈
ℂ) | 
| 121 | 120 | coscld 16168 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℂ →
(cos‘(𝑠 / 2)) ∈
ℂ) | 
| 122 | 121 | mullidd 11280 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ ℂ → (1
· (cos‘(𝑠 /
2))) = (cos‘(𝑠 /
2))) | 
| 123 | 119, 122 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ ℂ → ((2
· (1 / 2)) · (cos‘((1 / 2) · 𝑠))) = (cos‘(𝑠 / 2))) | 
| 124 | 123 | mpteq2ia 5244 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℂ ↦ ((2
· (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) = (𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) | 
| 125 | 115, 124 | eqtri 2764 | . . . . . . . . . . . . . . . . 17
⊢ (ℂ
D (𝑠 ∈ ℂ ↦
(2 · (sin‘((1 / 2) · 𝑠))))) = (𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) | 
| 126 | 125 | dmeqi 5914 | . . . . . . . . . . . . . . . 16
⊢ dom
(ℂ D (𝑠 ∈
ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = dom (𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) | 
| 127 |  | dmmptg 6261 | . . . . . . . . . . . . . . . . 17
⊢
(∀𝑠 ∈
ℂ (cos‘(𝑠 / 2))
∈ ℂ → dom (𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) =
ℂ) | 
| 128 | 127, 121 | mprg 3066 | . . . . . . . . . . . . . . . 16
⊢ dom
(𝑠 ∈ ℂ ↦
(cos‘(𝑠 / 2))) =
ℂ | 
| 129 | 126, 128 | eqtri 2764 | . . . . . . . . . . . . . . 15
⊢ dom
(ℂ D (𝑠 ∈
ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = ℂ | 
| 130 | 62, 129 | sseqtrri 4032 | . . . . . . . . . . . . . 14
⊢ ℝ
⊆ dom (ℂ D (𝑠
∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) | 
| 131 |  | dvres3 25949 | . . . . . . . . . . . . . 14
⊢
(((ℝ ∈ {ℝ, ℂ} ∧ (𝑠 ∈ ℂ ↦ (2 ·
(sin‘((1 / 2) · 𝑠)))):ℂ⟶ℂ) ∧ (ℂ
⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑠 ∈ ℂ ↦ (2 ·
(sin‘((1 / 2) · 𝑠))))))) → (ℝ D ((𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) = ((ℂ D (𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠))))) ↾ ℝ)) | 
| 132 | 47, 112, 66, 130, 131 | mp4an 693 | . . . . . . . . . . . . 13
⊢ (ℝ
D ((𝑠 ∈ ℂ
↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) = ((ℂ D (𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) | 
| 133 | 125 | reseq1i 5992 | . . . . . . . . . . . . 13
⊢ ((ℂ
D (𝑠 ∈ ℂ ↦
(2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) = ((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾
ℝ) | 
| 134 | 105, 132,
133 | 3eqtri 2768 | . . . . . . . . . . . 12
⊢ (ℝ
D (𝑠 ∈ ℝ ↦
(2 · (sin‘(𝑠 /
2))))) = ((𝑠 ∈ ℂ
↦ (cos‘(𝑠 /
2))) ↾ ℝ) | 
| 135 | 134 | reseq1i 5992 | . . . . . . . . . . 11
⊢ ((ℝ
D (𝑠 ∈ ℝ ↦
(2 · (sin‘(𝑠 /
2))))) ↾ 𝐴) =
(((𝑠 ∈ ℂ ↦
(cos‘(𝑠 / 2)))
↾ ℝ) ↾ 𝐴) | 
| 136 | 135 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → ((ℝ D (𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2))))) ↾ 𝐴) =
(((𝑠 ∈ ℂ ↦
(cos‘(𝑠 / 2)))
↾ ℝ) ↾ 𝐴)) | 
| 137 | 38 | resabs1d 6025 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾ ℝ) ↾
𝐴) = ((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾ 𝐴)) | 
| 138 | 64 | resmptd 6057 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾ 𝐴) = (𝑠 ∈ 𝐴 ↦ (cos‘(𝑠 / 2)))) | 
| 139 | 137, 138 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝜑 → (((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾ ℝ) ↾
𝐴) = (𝑠 ∈ 𝐴 ↦ (cos‘(𝑠 / 2)))) | 
| 140 | 92, 136, 139 | 3eqtrd 2780 | . . . . . . . . 9
⊢ (𝜑 → ((ℝ D (𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2))))) ↾ ((int‘(topGen‘ran (,)))‘𝐴)) = (𝑠 ∈ 𝐴 ↦ (cos‘(𝑠 / 2)))) | 
| 141 | 72, 85, 140 | 3eqtrd 2780 | . . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ 𝐴 ↦ (cos‘(𝑠 / 2)))) | 
| 142 |  | coscn 26490 | . . . . . . . . . 10
⊢ cos
∈ (ℂ–cn→ℂ) | 
| 143 | 142 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → cos ∈
(ℂ–cn→ℂ)) | 
| 144 | 64, 67 | idcncfg 45893 | . . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ 𝑠) ∈ (𝐴–cn→ℂ)) | 
| 145 |  | 2cnd 12345 | . . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℂ) | 
| 146 | 17 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 2 ≠ 0) | 
| 147 |  | eldifsn 4785 | . . . . . . . . . . . 12
⊢ (2 ∈
(ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠
0)) | 
| 148 | 145, 146,
147 | sylanbrc 583 | . . . . . . . . . . 11
⊢ (𝜑 → 2 ∈ (ℂ ∖
{0})) | 
| 149 |  | difssd 4136 | . . . . . . . . . . 11
⊢ (𝜑 → (ℂ ∖ {0})
⊆ ℂ) | 
| 150 | 64, 148, 149 | constcncfg 45892 | . . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ 2) ∈ (𝐴–cn→(ℂ ∖ {0}))) | 
| 151 | 144, 150 | divcncf 25483 | . . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (𝑠 / 2)) ∈ (𝐴–cn→ℂ)) | 
| 152 | 143, 151 | cncfmpt1f 24941 | . . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (cos‘(𝑠 / 2))) ∈ (𝐴–cn→ℂ)) | 
| 153 | 141, 152 | eqeltrd 2840 | . . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))) ∈ (𝐴–cn→ℂ)) | 
| 154 | 48, 50, 58, 69, 153 | dvdivcncf 45947 | . . . . . 6
⊢ (𝜑 → (ℝ D ((𝑠 ∈ 𝐴 ↦ 𝑠) ∘f / (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))))) ∈ (𝐴–cn→ℂ)) | 
| 155 | 46, 154 | eqeltrd 2840 | . . . . 5
⊢ (𝜑 → (ℝ D 𝐾) ∈ (𝐴–cn→ℂ)) | 
| 156 |  | cncff 24920 | . . . . 5
⊢ ((ℝ
D 𝐾) ∈ (𝐴–cn→ℂ) → (ℝ D 𝐾):𝐴⟶ℂ) | 
| 157 |  | fdm 6744 | . . . . 5
⊢ ((ℝ
D 𝐾):𝐴⟶ℂ → dom (ℝ D 𝐾) = 𝐴) | 
| 158 | 155, 156,
157 | 3syl 18 | . . . 4
⊢ (𝜑 → dom (ℝ D 𝐾) = 𝐴) | 
| 159 | 158 | feq2d 6721 | . . 3
⊢ (𝜑 → ((ℝ D 𝐾):dom (ℝ D 𝐾)⟶ℝ ↔ (ℝ
D 𝐾):𝐴⟶ℝ)) | 
| 160 | 40, 159 | mpbid 232 | . 2
⊢ (𝜑 → (ℝ D 𝐾):𝐴⟶ℝ) | 
| 161 |  | cncfcdm 24925 | . . 3
⊢ ((ℝ
⊆ ℂ ∧ (ℝ D 𝐾) ∈ (𝐴–cn→ℂ)) → ((ℝ D 𝐾) ∈ (𝐴–cn→ℝ) ↔ (ℝ D 𝐾):𝐴⟶ℝ)) | 
| 162 | 63, 155, 161 | syl2anc 584 | . 2
⊢ (𝜑 → ((ℝ D 𝐾) ∈ (𝐴–cn→ℝ) ↔ (ℝ D 𝐾):𝐴⟶ℝ)) | 
| 163 | 160, 162 | mpbird 257 | 1
⊢ (𝜑 → (ℝ D 𝐾) ∈ (𝐴–cn→ℝ)) |