Proof of Theorem fourierdlem58
Step | Hyp | Ref
| Expression |
1 | | pire 25348 |
. . . . . . . . . 10
⊢ π
∈ ℝ |
2 | 1 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → π ∈
ℝ) |
3 | 2 | renegcld 11259 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → -π ∈
ℝ) |
4 | 3, 2 | iccssred 13022 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (-π[,]π) ⊆
ℝ) |
5 | | fourierdlem58.ass |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ (-π[,]π)) |
6 | 5 | sselda 3901 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ (-π[,]π)) |
7 | 4, 6 | sseldd 3902 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ℝ) |
8 | | 2re 11904 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 2 ∈ ℝ) |
10 | 7 | rehalfcld 12077 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑠 / 2) ∈ ℝ) |
11 | 10 | resincld 15704 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (sin‘(𝑠 / 2)) ∈ ℝ) |
12 | 9, 11 | remulcld 10863 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (2 · (sin‘(𝑠 / 2))) ∈
ℝ) |
13 | | 2cnd 11908 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 2 ∈ ℂ) |
14 | 7 | recnd 10861 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ℂ) |
15 | 14 | halfcld 12075 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑠 / 2) ∈ ℂ) |
16 | 15 | sincld 15691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (sin‘(𝑠 / 2)) ∈ ℂ) |
17 | | 2ne0 11934 |
. . . . . . . 8
⊢ 2 ≠
0 |
18 | 17 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 2 ≠ 0) |
19 | | eqcom 2744 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 0 ↔ 0 = 𝑠) |
20 | 19 | biimpi 219 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 0 → 0 = 𝑠) |
21 | 20 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∈ 𝐴 ∧ 𝑠 = 0) → 0 = 𝑠) |
22 | | simpl 486 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∈ 𝐴 ∧ 𝑠 = 0) → 𝑠 ∈ 𝐴) |
23 | 21, 22 | eqeltrd 2838 |
. . . . . . . . . . 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 817 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ¬ 𝑠 = 0) |
28 | 27 | neqned 2947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ≠ 0) |
29 | | fourierdlem44 43367 |
. . . . . . . 8
⊢ ((𝑠 ∈ (-π[,]π) ∧
𝑠 ≠ 0) →
(sin‘(𝑠 / 2)) ≠
0) |
30 | 6, 28, 29 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (sin‘(𝑠 / 2)) ≠ 0) |
31 | 13, 16, 18, 30 | mulne0d 11484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (2 · (sin‘(𝑠 / 2))) ≠ 0) |
32 | 7, 12, 31 | redivcld 11660 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℝ) |
33 | | fourierdlem58.k |
. . . . 5
⊢ 𝐾 = (𝑠 ∈ 𝐴 ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) |
34 | 32, 33 | fmptd 6931 |
. . . 4
⊢ (𝜑 → 𝐾:𝐴⟶ℝ) |
35 | 1 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → π ∈
ℝ) |
36 | 35 | renegcld 11259 |
. . . . . 6
⊢ (𝜑 → -π ∈
ℝ) |
37 | 36, 35 | iccssred 13022 |
. . . . 5
⊢ (𝜑 → (-π[,]π) ⊆
ℝ) |
38 | 5, 37 | sstrd 3911 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
39 | | dvfre 24848 |
. . . 4
⊢ ((𝐾:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) → (ℝ D 𝐾):dom (ℝ D 𝐾)⟶ℝ) |
40 | 34, 38, 39 | syl2anc 587 |
. . 3
⊢ (𝜑 → (ℝ D 𝐾):dom (ℝ D 𝐾)⟶ℝ) |
41 | | fourierdlem58.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ (topGen‘ran
(,))) |
42 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ 𝑠) = (𝑠 ∈ 𝐴 ↦ 𝑠)) |
43 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))) |
44 | 41, 7, 12, 42, 43 | offval2 7488 |
. . . . . . . 8
⊢ (𝜑 → ((𝑠 ∈ 𝐴 ↦ 𝑠) ∘f / (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ 𝐴 ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))) |
45 | 33, 44 | eqtr4id 2797 |
. . . . . . 7
⊢ (𝜑 → 𝐾 = ((𝑠 ∈ 𝐴 ↦ 𝑠) ∘f / (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))))) |
46 | 45 | oveq2d 7229 |
. . . . . 6
⊢ (𝜑 → (ℝ D 𝐾) = (ℝ D ((𝑠 ∈ 𝐴 ↦ 𝑠) ∘f / (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))))) |
47 | | reelprrecn 10821 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
48 | 47 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
49 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑠 ∈ 𝐴 ↦ 𝑠) = (𝑠 ∈ 𝐴 ↦ 𝑠) |
50 | 14, 49 | fmptd 6931 |
. . . . . . 7
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ 𝑠):𝐴⟶ℂ) |
51 | 13, 16 | mulcld 10853 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (2 · (sin‘(𝑠 / 2))) ∈
ℂ) |
52 | 31 | neneqd 2945 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ¬ (2 · (sin‘(𝑠 / 2))) = 0) |
53 | | elsng 4555 |
. . . . . . . . . . 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 328 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ¬ (2 · (sin‘(𝑠 / 2))) ∈
{0}) |
56 | 51, 55 | eldifd 3877 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖
{0})) |
57 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))) |
58 | 56, 57 | fmptd 6931 |
. . . . . . 7
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))):𝐴⟶(ℂ ∖
{0})) |
59 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
60 | 59 | tgioo2 23700 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
61 | 41, 60 | eleqtrdi 2848 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈
((TopOpen‘ℂfld) ↾t
ℝ)) |
62 | 48, 61 | dvmptidg 43133 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ 𝐴 ↦ 𝑠)) = (𝑠 ∈ 𝐴 ↦ 1)) |
63 | | ax-resscn 10786 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
64 | 63 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ⊆
ℂ) |
65 | 38, 64 | sstrd 3911 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
66 | | 1cnd 10828 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) |
67 | | ssid 3923 |
. . . . . . . . . 10
⊢ ℂ
⊆ ℂ |
68 | 67 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℂ ⊆
ℂ) |
69 | 65, 66, 68 | constcncfg 43088 |
. . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ 1) ∈ (𝐴–cn→ℂ)) |
70 | 62, 69 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ 𝐴 ↦ 𝑠)) ∈ (𝐴–cn→ℂ)) |
71 | 38 | resmptd 5908 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 / 2))))
↾ 𝐴) = (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))) |
72 | 71 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))) = ((𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 / 2))))
↾ 𝐴)) |
73 | 72 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))) = (ℝ D ((𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2)))) ↾ 𝐴))) |
74 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2)))) = (𝑠 ∈ ℝ
↦ (2 · (sin‘(𝑠 / 2)))) |
75 | | 2cnd 11908 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℝ → 2 ∈
ℂ) |
76 | | recn 10819 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ℝ → 𝑠 ∈
ℂ) |
77 | 76 | halfcld 12075 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℝ → (𝑠 / 2) ∈
ℂ) |
78 | 77 | sincld 15691 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ℝ →
(sin‘(𝑠 / 2)) ∈
ℂ) |
79 | 75, 78 | mulcld 10853 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ℝ → (2
· (sin‘(𝑠 /
2))) ∈ ℂ) |
80 | 74, 79 | fmpti 6929 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2)))):ℝ⟶ℂ |
81 | 80 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 /
2)))):ℝ⟶ℂ) |
82 | | ssid 3923 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℝ |
83 | 82 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ⊆
ℝ) |
84 | 59, 60 | dvres 24808 |
. . . . . . . . . 10
⊢
(((ℝ ⊆ ℂ ∧ (𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 /
2)))):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ 𝐴 ⊆ ℝ)) →
(ℝ D ((𝑠 ∈
ℝ ↦ (2 · (sin‘(𝑠 / 2)))) ↾ 𝐴)) = ((ℝ D (𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 / 2)))))
↾ ((int‘(topGen‘ran (,)))‘𝐴))) |
85 | 64, 81, 83, 38, 84 | syl22anc 839 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D ((𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2)))) ↾ 𝐴)) =
((ℝ D (𝑠 ∈
ℝ ↦ (2 · (sin‘(𝑠 / 2))))) ↾
((int‘(topGen‘ran (,)))‘𝐴))) |
86 | | retop 23659 |
. . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) ∈ Top |
87 | 86 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (topGen‘ran (,))
∈ Top) |
88 | | uniretop 23660 |
. . . . . . . . . . . . . 14
⊢ ℝ =
∪ (topGen‘ran (,)) |
89 | 88 | isopn3 21963 |
. . . . . . . . . . . . 13
⊢
(((topGen‘ran (,)) ∈ Top ∧ 𝐴 ⊆ ℝ) → (𝐴 ∈ (topGen‘ran (,)) ↔
((int‘(topGen‘ran (,)))‘𝐴) = 𝐴)) |
90 | 87, 38, 89 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∈ (topGen‘ran (,)) ↔
((int‘(topGen‘ran (,)))‘𝐴) = 𝐴)) |
91 | 41, 90 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘𝐴) = 𝐴) |
92 | 91 | reseq2d 5851 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℝ D (𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2))))) ↾ ((int‘(topGen‘ran (,)))‘𝐴)) = ((ℝ D (𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 / 2)))))
↾ 𝐴)) |
93 | | resmpt 5905 |
. . . . . . . . . . . . . . . 16
⊢ (ℝ
⊆ ℂ → ((𝑠
∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ) = (𝑠 ∈ ℝ ↦ (2
· (sin‘((1 / 2) · 𝑠))))) |
94 | 63, 93 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠)))) ↾ ℝ) = (𝑠 ∈ ℝ ↦ (2 ·
(sin‘((1 / 2) · 𝑠)))) |
95 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℂ → 𝑠 ∈
ℂ) |
96 | | 2cnd 11908 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℂ → 2 ∈
ℂ) |
97 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℂ → 2 ≠
0) |
98 | 95, 96, 97 | divrec2d 11612 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ ℂ → (𝑠 / 2) = ((1 / 2) · 𝑠)) |
99 | 98 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ ℂ → ((1 / 2)
· 𝑠) = (𝑠 / 2)) |
100 | 76, 99 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℝ → ((1 / 2)
· 𝑠) = (𝑠 / 2)) |
101 | 100 | fveq2d 6721 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ℝ →
(sin‘((1 / 2) · 𝑠)) = (sin‘(𝑠 / 2))) |
102 | 101 | oveq2d 7229 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℝ → (2
· (sin‘((1 / 2) · 𝑠))) = (2 · (sin‘(𝑠 / 2)))) |
103 | 102 | mpteq2ia 5146 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ℝ ↦ (2
· (sin‘((1 / 2) · 𝑠)))) = (𝑠 ∈ ℝ ↦ (2 ·
(sin‘(𝑠 /
2)))) |
104 | 94, 103 | eqtr2i 2766 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2)))) = ((𝑠 ∈ ℂ
↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ) |
105 | 104 | oveq2i 7224 |
. . . . . . . . . . . . 13
⊢ (ℝ
D (𝑠 ∈ ℝ ↦
(2 · (sin‘(𝑠 /
2))))) = (ℝ D ((𝑠
∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾
ℝ)) |
106 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠)))) = (𝑠 ∈ ℂ ↦ (2 ·
(sin‘((1 / 2) · 𝑠)))) |
107 | | halfcn 12045 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 / 2)
∈ ℂ |
108 | 107 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℂ → (1 / 2)
∈ ℂ) |
109 | 108, 95 | mulcld 10853 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ℂ → ((1 / 2)
· 𝑠) ∈
ℂ) |
110 | 109 | sincld 15691 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ ℂ →
(sin‘((1 / 2) · 𝑠)) ∈ ℂ) |
111 | 96, 110 | mulcld 10853 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ ℂ → (2
· (sin‘((1 / 2) · 𝑠))) ∈ ℂ) |
112 | 106, 111 | fmpti 6929 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠)))):ℂ⟶ℂ |
113 | | 2cn 11905 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℂ |
114 | | dvasinbx 43136 |
. . . . . . . . . . . . . . . . . . 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 11563 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2
· (1 / 2)) = 1 |
117 | 116 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℂ → (2
· (1 / 2)) = 1) |
118 | 99 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℂ →
(cos‘((1 / 2) · 𝑠)) = (cos‘(𝑠 / 2))) |
119 | 117, 118 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ ℂ → ((2
· (1 / 2)) · (cos‘((1 / 2) · 𝑠))) = (1 · (cos‘(𝑠 / 2)))) |
120 | | halfcl 12055 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 ∈ ℂ → (𝑠 / 2) ∈
ℂ) |
121 | 120 | coscld 15692 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℂ →
(cos‘(𝑠 / 2)) ∈
ℂ) |
122 | 121 | mulid2d 10851 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ ℂ → (1
· (cos‘(𝑠 /
2))) = (cos‘(𝑠 /
2))) |
123 | 119, 122 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ ℂ → ((2
· (1 / 2)) · (cos‘((1 / 2) · 𝑠))) = (cos‘(𝑠 / 2))) |
124 | 123 | mpteq2ia 5146 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℂ ↦ ((2
· (1 / 2)) · (cos‘((1 / 2) · 𝑠)))) = (𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) |
125 | 115, 124 | eqtri 2765 |
. . . . . . . . . . . . . . . . 17
⊢ (ℂ
D (𝑠 ∈ ℂ ↦
(2 · (sin‘((1 / 2) · 𝑠))))) = (𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) |
126 | 125 | dmeqi 5773 |
. . . . . . . . . . . . . . . 16
⊢ dom
(ℂ D (𝑠 ∈
ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = dom (𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) |
127 | | dmmptg 6105 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑠 ∈
ℂ (cos‘(𝑠 / 2))
∈ ℂ → dom (𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) =
ℂ) |
128 | 127, 121 | mprg 3075 |
. . . . . . . . . . . . . . . 16
⊢ dom
(𝑠 ∈ ℂ ↦
(cos‘(𝑠 / 2))) =
ℂ |
129 | 126, 128 | eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢ dom
(ℂ D (𝑠 ∈
ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) = ℂ |
130 | 63, 129 | sseqtrri 3938 |
. . . . . . . . . . . . . 14
⊢ ℝ
⊆ dom (ℂ D (𝑠
∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑠))))) |
131 | | dvres3 24810 |
. . . . . . . . . . . . . 14
⊢
(((ℝ ∈ {ℝ, ℂ} ∧ (𝑠 ∈ ℂ ↦ (2 ·
(sin‘((1 / 2) · 𝑠)))):ℂ⟶ℂ) ∧ (ℂ
⊆ ℂ ∧ ℝ ⊆ dom (ℂ D (𝑠 ∈ ℂ ↦ (2 ·
(sin‘((1 / 2) · 𝑠))))))) → (ℝ D ((𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) = ((ℂ D (𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠))))) ↾ ℝ)) |
132 | 47, 112, 67, 130, 131 | mp4an 693 |
. . . . . . . . . . . . 13
⊢ (ℝ
D ((𝑠 ∈ ℂ
↦ (2 · (sin‘((1 / 2) · 𝑠)))) ↾ ℝ)) = ((ℂ D (𝑠 ∈ ℂ ↦ (2
· (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) |
133 | 125 | reseq1i 5847 |
. . . . . . . . . . . . 13
⊢ ((ℂ
D (𝑠 ∈ ℂ ↦
(2 · (sin‘((1 / 2) · 𝑠))))) ↾ ℝ) = ((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾
ℝ) |
134 | 105, 132,
133 | 3eqtri 2769 |
. . . . . . . . . . . 12
⊢ (ℝ
D (𝑠 ∈ ℝ ↦
(2 · (sin‘(𝑠 /
2))))) = ((𝑠 ∈ ℂ
↦ (cos‘(𝑠 /
2))) ↾ ℝ) |
135 | 134 | reseq1i 5847 |
. . . . . . . . . . 11
⊢ ((ℝ
D (𝑠 ∈ ℝ ↦
(2 · (sin‘(𝑠 /
2))))) ↾ 𝐴) =
(((𝑠 ∈ ℂ ↦
(cos‘(𝑠 / 2)))
↾ ℝ) ↾ 𝐴) |
136 | 135 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ((ℝ D (𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2))))) ↾ 𝐴) =
(((𝑠 ∈ ℂ ↦
(cos‘(𝑠 / 2)))
↾ ℝ) ↾ 𝐴)) |
137 | 38 | resabs1d 5882 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾ ℝ) ↾
𝐴) = ((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾ 𝐴)) |
138 | 65 | resmptd 5908 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾ 𝐴) = (𝑠 ∈ 𝐴 ↦ (cos‘(𝑠 / 2)))) |
139 | 137, 138 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑠 ∈ ℂ ↦ (cos‘(𝑠 / 2))) ↾ ℝ) ↾
𝐴) = (𝑠 ∈ 𝐴 ↦ (cos‘(𝑠 / 2)))) |
140 | 92, 136, 139 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ (𝜑 → ((ℝ D (𝑠 ∈ ℝ ↦ (2
· (sin‘(𝑠 /
2))))) ↾ ((int‘(topGen‘ran (,)))‘𝐴)) = (𝑠 ∈ 𝐴 ↦ (cos‘(𝑠 / 2)))) |
141 | 73, 85, 140 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))) = (𝑠 ∈ 𝐴 ↦ (cos‘(𝑠 / 2)))) |
142 | | coscn 25337 |
. . . . . . . . . 10
⊢ cos
∈ (ℂ–cn→ℂ) |
143 | 142 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → cos ∈
(ℂ–cn→ℂ)) |
144 | 65, 68 | idcncfg 43089 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ 𝑠) ∈ (𝐴–cn→ℂ)) |
145 | | 2cnd 11908 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℂ) |
146 | 17 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ≠ 0) |
147 | | eldifsn 4700 |
. . . . . . . . . . . 12
⊢ (2 ∈
(ℂ ∖ {0}) ↔ (2 ∈ ℂ ∧ 2 ≠
0)) |
148 | 145, 146,
147 | sylanbrc 586 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈ (ℂ ∖
{0})) |
149 | | difssd 4047 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℂ ∖ {0})
⊆ ℂ) |
150 | 65, 148, 149 | constcncfg 43088 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ 2) ∈ (𝐴–cn→(ℂ ∖ {0}))) |
151 | 144, 150 | divcncf 24344 |
. . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (𝑠 / 2)) ∈ (𝐴–cn→ℂ)) |
152 | 143, 151 | cncfmpt1f 23811 |
. . . . . . . 8
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ (cos‘(𝑠 / 2))) ∈ (𝐴–cn→ℂ)) |
153 | 141, 152 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2))))) ∈ (𝐴–cn→ℂ)) |
154 | 48, 50, 58, 70, 153 | dvdivcncf 43143 |
. . . . . 6
⊢ (𝜑 → (ℝ D ((𝑠 ∈ 𝐴 ↦ 𝑠) ∘f / (𝑠 ∈ 𝐴 ↦ (2 · (sin‘(𝑠 / 2)))))) ∈ (𝐴–cn→ℂ)) |
155 | 46, 154 | eqeltrd 2838 |
. . . . 5
⊢ (𝜑 → (ℝ D 𝐾) ∈ (𝐴–cn→ℂ)) |
156 | | cncff 23790 |
. . . . 5
⊢ ((ℝ
D 𝐾) ∈ (𝐴–cn→ℂ) → (ℝ D 𝐾):𝐴⟶ℂ) |
157 | | fdm 6554 |
. . . . 5
⊢ ((ℝ
D 𝐾):𝐴⟶ℂ → dom (ℝ D 𝐾) = 𝐴) |
158 | 155, 156,
157 | 3syl 18 |
. . . 4
⊢ (𝜑 → dom (ℝ D 𝐾) = 𝐴) |
159 | 158 | feq2d 6531 |
. . 3
⊢ (𝜑 → ((ℝ D 𝐾):dom (ℝ D 𝐾)⟶ℝ ↔ (ℝ
D 𝐾):𝐴⟶ℝ)) |
160 | 40, 159 | mpbid 235 |
. 2
⊢ (𝜑 → (ℝ D 𝐾):𝐴⟶ℝ) |
161 | | cncffvrn 23795 |
. . 3
⊢ ((ℝ
⊆ ℂ ∧ (ℝ D 𝐾) ∈ (𝐴–cn→ℂ)) → ((ℝ D 𝐾) ∈ (𝐴–cn→ℝ) ↔ (ℝ D 𝐾):𝐴⟶ℝ)) |
162 | 64, 155, 161 | syl2anc 587 |
. 2
⊢ (𝜑 → ((ℝ D 𝐾) ∈ (𝐴–cn→ℝ) ↔ (ℝ D 𝐾):𝐴⟶ℝ)) |
163 | 160, 162 | mpbird 260 |
1
⊢ (𝜑 → (ℝ D 𝐾) ∈ (𝐴–cn→ℝ)) |