Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem62 Structured version   Visualization version   GIF version
Theorem fourierdlem62 47451
Description: The function 𝐾 is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
fourierdlem62.k 𝐾 = (𝑦 ∈ ( -π[,]π) ↦ if(𝑦 = 0, 1, (𝑦 / (2 · (sin‘(𝑦 / 2))))))
Assertion
Ref Expression
fourierdlem62 𝐾 ∈ (( -π[,]π)–cn→ℝ)
Proof of Theorem fourierdlem62
Dummy variables 𝑠 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem62.k . . . 4 𝐾 = (𝑦 ∈ ( -π[,]π) ↦ if(𝑦 = 0, 1, (𝑦 / (2 · (sin‘(𝑦 / 2))))))
2 eqeq1 2767 . . . . . 6 (𝑦 = 𝑠 → (𝑦 = 0 ↔ 𝑠 = 0))
3 id 23 . . . . . . 7 (𝑦 = 𝑠 → 𝑦 = 𝑠)
4 oveq1 7458 . . . . . . . . 9 (𝑦 = 𝑠 → (𝑦 / 2) = (𝑠 / 2))
54fveq2d 6920 . . . . . . . 8 (𝑦 = 𝑠 → (sin‘(𝑦 / 2)) = (sin‘(𝑠 / 2)))
65oveq2d 7467 . . . . . . 7 (𝑦 = 𝑠 → (2 · (sin‘(𝑦 / 2))) = (2 · (sin‘(𝑠 / 2))))
73, 6oveq12d 7469 . . . . . 6 (𝑦 = 𝑠 → (𝑦 / (2 · (sin‘(𝑦 / 2)))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
82, 7ifbieq2d 4512 . . . . 5 (𝑦 = 𝑠 → if(𝑦 = 0, 1, (𝑦 / (2 · (sin‘(𝑦 / 2))))) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
98cbvmptv 5215 . . . 4 (𝑦 ∈ ( -π[,]π) ↦ if(𝑦 = 0, 1, (𝑦 / (2 · (sin‘(𝑦 / 2)))))) = (𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
101, 9eqtri 2786 . . 3 𝐾 = (𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
1110fourierdlem43 47433 . 2 𝐾:( -π[,]π)⟶ℝ
12 ax-resscn 11296 . . 3 ℝ ⊆ ℂ
13 fss 6756 . . . . . 6 ((𝐾:( -π[,]π)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐾:( -π[,]π)⟶ℂ)
1411, 12, 13mp2an 705 . . . . 5 𝐾:( -π[,]π)⟶ℂ
1514a1i 11 . . . . . . . . 9 (𝑠 = 0 → 𝐾:( -π[,]π)⟶ℂ)
16 difss 4075 . . . . . . . . . . . . . . . . 17 (( -π(,)π) ∖ {0}) ⊆ ( -π(,)π)
17 elioore 13546 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ( -π(,)π) → 𝑠 ∈ ℝ)
1817ssriv 3917 . . . . . . . . . . . . . . . . 17 ( -π(,)π) ⊆ ℝ
1916, 18sstri 3922 . . . . . . . . . . . . . . . 16 (( -π(,)π) ∖ {0}) ⊆ ℝ
2019a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (( -π(,)π) ∖ {0}) ⊆ ℝ)
21 eqid 2763 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥)
2219sseli 3909 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (( -π(,)π) ∖ {0}) → 𝑥 ∈ ℝ)
2321, 22fmpti 7144 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥):(( -π(,)π) ∖ {0})⟶ℝ
2423a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥):(( -π(,)π) ∖ {0})⟶ℝ)
25 eqid 2763 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))
26 2re 12457 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℝ
2726a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (( -π(,)π) ∖ {0}) → 2 ∈ ℝ)
2822rehalfcld 12633 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (( -π(,)π) ∖ {0}) → (𝑥 / 2) ∈ ℝ)
2928resincld 16355 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (( -π(,)π) ∖ {0}) → (sin‘(𝑥 / 2)) ∈ ℝ)
3027, 29remulcld 11378 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (( -π(,)π) ∖ {0}) → (2 · (sin‘(𝑥 / 2))) ∈ ℝ)
3125, 30fmpti 7144 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))):(( -π(,)π) ∖ {0})⟶ℝ
3231a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))):(( -π(,)π) ∖ {0})⟶ℝ)
33 iooretop 25139 . . . . . . . . . . . . . . . 16 ( -π(,)π) ∈ (topGen‘ran (,))
3433a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ( -π(,)π) ∈ (topGen‘ran (,)))
35 0re 11349 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
36 negpilt0 46570 . . . . . . . . . . . . . . . . 17 -π < 0
37 pipos 26844 . . . . . . . . . . . . . . . . 17 0 < π
38 pire 26840 . . . . . . . . . . . . . . . . . . . 20 π ∈ ℝ
3938renegcli 11658 . . . . . . . . . . . . . . . . . . 19 -π ∈ ℝ
4039rexri 11406 . . . . . . . . . . . . . . . . . 18 -π ∈ ℝ*
4138rexri 11406 . . . . . . . . . . . . . . . . . 18 π ∈ ℝ*
42 elioo2 13557 . . . . . . . . . . . . . . . . . 18 (( -π ∈ ℝ* ∧ π ∈ ℝ*) → (0 ∈ ( -π(,)π) ↔ (0 ∈ ℝ ∧ -π < 0 ∧ 0 < π)))
4340, 41, 42mp2an 705 . . . . . . . . . . . . . . . . 17 (0 ∈ ( -π(,)π) ↔ (0 ∈ ℝ ∧ -π < 0 ∧ 0 < π))
4435, 36, 37, 43mpbir3an 1360 . . . . . . . . . . . . . . . 16 0 ∈ ( -π(,)π)
4544a1i 11 . . . . . . . . . . . . . . 15 (⊤ → 0 ∈ ( -π(,)π))
46 eqid 2763 . . . . . . . . . . . . . . 15 (( -π(,)π) ∖ {0}) = (( -π(,)π) ∖ {0})
47 1ex 11342 . . . . . . . . . . . . . . . . . . 19 1 ∈ V
48 eqid 2763 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 1) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 1)
4947, 48dmmpti 6713 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 1) = (( -π(,)π) ∖ {0})
50 reelprrecn 11331 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ ∈ {ℝ, ℂ}
5150a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ℝ ∈ {ℝ, ℂ})
5212sseli 3909 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
5352adantl 487 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
54 1red 11348 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
5551dvmptid 26332 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
56 tgioo4 25179 . . . . . . . . . . . . . . . . . . . . . 22 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
57 eqid 2763 . . . . . . . . . . . . . . . . . . . . . 22 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
58 sncldre 46335 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 ∈ ℝ → {0} ∈ (Clsd‘(topGen‘ran (,))))
5935, 58ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 {0} ∈ (Clsd‘(topGen‘ran (,)))
60 retopon 25137 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
6160toponunii 23289 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℝ = ∪ (topGen‘ran (,))
6261difopn 23407 . . . . . . . . . . . . . . . . . . . . . . . 24 ((( -π(,)π) ∈ (topGen‘ran (,)) ∧ {0} ∈ (Clsd‘(topGen‘ran (,)))) → (( -π(,)π) ∖ {0}) ∈ (topGen‘ran (,)))
6333, 59, 62mp2an 705 . . . . . . . . . . . . . . . . . . . . . . 23 (( -π(,)π) ∖ {0}) ∈ (topGen‘ran (,))
6463a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (( -π(,)π) ∖ {0}) ∈ (topGen‘ran (,)))
6551, 53, 54, 55, 20, 56, 57, 64dvmptres 26338 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥)) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 1))
6665mptru 1577 . . . . . . . . . . . . . . . . . . . 20 (ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥)) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 1)
6766eqcomi 2772 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 1) = (ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥))
6867dmeqi 5898 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 1) = dom (ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥))
6949, 68eqtr3i 2788 . . . . . . . . . . . . . . . . 17 (( -π(,)π) ∖ {0}) = dom (ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥))
7069eqimssi 3973 . . . . . . . . . . . . . . . 16 (( -π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥))
7170a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (( -π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥)))
72 fvex 6929 . . . . . . . . . . . . . . . . . . 19 (cos‘(𝑥 / 2)) ∈ V
73 eqid 2763 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))
7472, 73dmmpti 6713 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = (( -π(,)π) ∖ {0})
75 2cnd 12461 . . . . . . . . . . . . . . . . . . . . . . 23 ((⊤ ∧ 𝑥 ∈ ℝ) → 2 ∈ ℂ)
7653halfcld 12631 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⊤ ∧ 𝑥 ∈ ℝ) → (𝑥 / 2) ∈ ℂ)
7776sincld 16342 . . . . . . . . . . . . . . . . . . . . . . 23 ((⊤ ∧ 𝑥 ∈ ℝ) → (sin‘(𝑥 / 2)) ∈ ℂ)
7875, 77mulcld 11368 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → (2 · (sin‘(𝑥 / 2))) ∈ ℂ)
7976coscld 16343 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → (cos‘(𝑥 / 2)) ∈ ℂ)
80 2cnd 12461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → 2 ∈ ℂ)
81 2ne0 12489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 2 ≠ 0
8281a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → 2 ≠ 0)
8352, 80, 82divrec2d 12137 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → (𝑥 / 2) = ((1 / 2) · 𝑥))
8483fveq2d 6920 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℝ → (sin‘(𝑥 / 2)) = (sin‘((1 / 2) · 𝑥)))
8584oveq2d 7467 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ → (2 · (sin‘(𝑥 / 2))) = (2 · (sin‘((1 / 2) · 𝑥))))
8685mpteq2ia 5206 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))
8786oveq2i 7462 . . . . . . . . . . . . . . . . . . . . . . . 24 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2))))) = (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))
88 resmpt 6047 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℝ ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))
8912, 88ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))
9089eqcomi 2772 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) = ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ)
9190oveq2i 7462 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (ℝ D ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ))
92 eqid 2763 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) = (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))
93 2cnd 12461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℂ → 2 ∈ ℂ)
94 halfcn 12600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (1 / 2) ∈ ℂ
9594a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℂ → (1 / 2) ∈ ℂ)
96 id 23 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℂ → 𝑥 ∈ ℂ)
9795, 96mulcld 11368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℂ → ((1 / 2) · 𝑥) ∈ ℂ)
9897sincld 16342 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℂ → (sin‘((1 / 2) · 𝑥)) ∈ ℂ)
9993, 98mulcld 11368 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℂ → (2 · (sin‘((1 / 2) · 𝑥))) ∈ ℂ)
10092, 99fmpti 7144 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))):ℂ⟶ℂ
101 eqid 2763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
102 2cn 12458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2 ∈ ℂ
103102, 94mulcli 11355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (2 · (1 / 2)) ∈ ℂ
104103a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ ℂ → (2 · (1 / 2)) ∈ ℂ)
10597coscld 16343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ ℂ → (cos‘((1 / 2) · 𝑥)) ∈ ℂ)
106104, 105mulcld 11368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ ℂ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) ∈ ℂ)
107106adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((⊤ ∧ 𝑥 ∈ ℂ) → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) ∈ ℂ)
108101, 107dmmptd 6714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⊤ → dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = ℂ)
109108mptru 1577 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = ℂ
11012, 109sseqtrri 3962 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℝ ⊆ dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
111 dvasinbx 47203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))))
112102, 94, 111mp2an 705 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
113112dmeqi 5898 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 dom (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
114110, 113sseqtrri 3962 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℝ ⊆ dom (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))
115 dvcnre 47199 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))):ℂ⟶ℂ ∧ ℝ ⊆ dom (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))) → (ℝ D ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ)) = ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ))
116100, 114, 115mp2an 705 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℝ D ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ)) = ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ)
117112reseq1i 5982 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ) = ((𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) ↾ ℝ)
118 resmpt 6047 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ℝ ⊆ ℂ → ((𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))))
11912, 118ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
120 2thalfe1 12490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (2 · (1 / 2)) = 1
121120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → (2 · (1 / 2)) = 1)
12283eqcomd 2769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℝ → ((1 / 2) · 𝑥) = (𝑥 / 2))
123122fveq2d 6920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → (cos‘((1 / 2) · 𝑥)) = (cos‘(𝑥 / 2)))
124121, 123oveq12d 7469 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) = (1 · (cos‘(𝑥 / 2))))
12552halfcld 12631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℝ → (𝑥 / 2) ∈ ℂ)
126125coscld 16343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → (cos‘(𝑥 / 2)) ∈ ℂ)
127126mullidd 11366 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → (1 · (cos‘(𝑥 / 2))) = (cos‘(𝑥 / 2)))
128124, 127eqtrd 2798 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℝ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) = (cos‘(𝑥 / 2)))
129128mpteq2ia 5206 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
130117, 119, 1293eqtri 2790 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
13191, 116, 1303eqtri 2790 . . . . . . . . . . . . . . . . . . . . . . . 24 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
13287, 131eqtri 2786 . . . . . . . . . . . . . . . . . . . . . . 23 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
133132a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2))))
13451, 78, 79, 133, 20, 56, 57, 64dvmptres 26338 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))))
135134mptru 1577 . . . . . . . . . . . . . . . . . . . 20 (ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))
136135eqcomi 2772 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = (ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
137136dmeqi 5898 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = dom (ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
13874, 137eqtr3i 2788 . . . . . . . . . . . . . . . . 17 (( -π(,)π) ∖ {0}) = dom (ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
139138eqimssi 3973 . . . . . . . . . . . . . . . 16 (( -π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
140139a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (( -π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))))
14117recnd 11376 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ( -π(,)π) → 𝑠 ∈ ℂ)
142141ssriv 3917 . . . . . . . . . . . . . . . . . . . . . . 23 ( -π(,)π) ⊆ ℂ
143142a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ( -π(,)π) ⊆ ℂ)
144 ssid 3935 . . . . . . . . . . . . . . . . . . . . . . 23 ℂ ⊆ ℂ
145144a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ℂ ⊆ ℂ)
146143, 145idcncfg 47156 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑥 ∈ ( -π(,)π) ↦ 𝑥) ∈ (( -π(,)π)–cn→ℂ))
147146mptru 1577 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ( -π(,)π) ↦ 𝑥) ∈ (( -π(,)π)–cn→ℂ)
148 cnlimc 26263 . . . . . . . . . . . . . . . . . . . . 21 (( -π(,)π) ⊆ ℂ → ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) ∈ (( -π(,)π)–cn→ℂ) ↔ ((𝑥 ∈ ( -π(,)π) ↦ 𝑥):( -π(,)π)⟶ℂ ∧ ∀𝑦 ∈ ( -π(,)π)((𝑥 ∈ ( -π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) limℂ 𝑦))))
149142, 148ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) ∈ (( -π(,)π)–cn→ℂ) ↔ ((𝑥 ∈ ( -π(,)π) ↦ 𝑥):( -π(,)π)⟶ℂ ∧ ∀𝑦 ∈ ( -π(,)π)((𝑥 ∈ ( -π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) limℂ 𝑦)))
150147, 149mpbi 233 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ( -π(,)π) ↦ 𝑥):( -π(,)π)⟶ℂ ∧ ∀𝑦 ∈ ( -π(,)π)((𝑥 ∈ ( -π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) limℂ 𝑦))
151150simpri 491 . . . . . . . . . . . . . . . . . 18 ∀𝑦 ∈ ( -π(,)π)((𝑥 ∈ ( -π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) limℂ 𝑦)
152 fveq2 6916 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ ( -π(,)π) ↦ 𝑥)‘𝑦) = ((𝑥 ∈ ( -π(,)π) ↦ 𝑥)‘0))
153 oveq2 7459 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) limℂ 𝑦) = ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) limℂ 0))
154152, 153eleq12d 2858 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 0 → (((𝑥 ∈ ( -π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) limℂ 𝑦) ↔ ((𝑥 ∈ ( -π(,)π) ↦ 𝑥)‘0) ∈ ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) limℂ 0)))
155154rspccva 3579 . . . . . . . . . . . . . . . . . 18 ((∀𝑦 ∈ ( -π(,)π)((𝑥 ∈ ( -π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) limℂ 𝑦) ∧ 0 ∈ ( -π(,)π)) → ((𝑥 ∈ ( -π(,)π) ↦ 𝑥)‘0) ∈ ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) limℂ 0))
156151, 44, 155mp2an 705 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ( -π(,)π) ↦ 𝑥)‘0) ∈ ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) limℂ 0)
157 id 23 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → 𝑥 = 0)
158 eqid 2763 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ( -π(,)π) ↦ 𝑥) = (𝑥 ∈ ( -π(,)π) ↦ 𝑥)
159 c0ex 11339 . . . . . . . . . . . . . . . . . . 19 0 ∈ V
160157, 158, 159fvmpt 7024 . . . . . . . . . . . . . . . . . 18 (0 ∈ ( -π(,)π) → ((𝑥 ∈ ( -π(,)π) ↦ 𝑥)‘0) = 0)
16144, 160ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ( -π(,)π) ↦ 𝑥)‘0) = 0
162 elioore 13546 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ( -π(,)π) → 𝑥 ∈ ℝ)
163162recnd 11376 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ( -π(,)π) → 𝑥 ∈ ℂ)
164158, 163fmpti 7144 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ( -π(,)π) ↦ 𝑥):( -π(,)π)⟶ℂ
165164a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ ( -π(,)π) ↦ 𝑥):( -π(,)π)⟶ℂ)
166165limcdif 26251 . . . . . . . . . . . . . . . . . . 19 (⊤ → ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) limℂ 0) = (((𝑥 ∈ ( -π(,)π) ↦ 𝑥) ↾ (( -π(,)π) ∖ {0})) limℂ 0))
167166mptru 1577 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) limℂ 0) = (((𝑥 ∈ ( -π(,)π) ↦ 𝑥) ↾ (( -π(,)π) ∖ {0})) limℂ 0)
168 resmpt 6047 . . . . . . . . . . . . . . . . . . . 20 ((( -π(,)π) ∖ {0}) ⊆ ( -π(,)π) → ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) ↾ (( -π(,)π) ∖ {0})) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥))
16916, 168ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) ↾ (( -π(,)π) ∖ {0})) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥)
170169oveq1i 7461 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ( -π(,)π) ↦ 𝑥) ↾ (( -π(,)π) ∖ {0})) limℂ 0) = ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥) limℂ 0)
171167, 170eqtri 2786 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ( -π(,)π) ↦ 𝑥) limℂ 0) = ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥) limℂ 0)
172156, 161, 1713eltr3i 2876 . . . . . . . . . . . . . . . 16 0 ∈ ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥) limℂ 0)
173172a1i 11 . . . . . . . . . . . . . . 15 (⊤ → 0 ∈ ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥) limℂ 0))
174 eqid 2763 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℂ ↦ 2) = (𝑥 ∈ ℂ ↦ 2)
175144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 ∈ ℂ → ℂ ⊆ ℂ)
176 2cnd 12461 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 ∈ ℂ → 2 ∈ ℂ)
177175, 176, 175constcncfg 47155 . . . . . . . . . . . . . . . . . . . . . . . 24 (2 ∈ ℂ → (𝑥 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
178102, 177mp1i 14 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → (𝑥 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
179 2cnd 12461 . . . . . . . . . . . . . . . . . . . . . . 23 ((⊤ ∧ 𝑥 ∈ ( -π(,)π)) → 2 ∈ ℂ)
180174, 178, 143, 145, 179cncfmptssg 47154 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑥 ∈ ( -π(,)π) ↦ 2) ∈ (( -π(,)π)–cn→ℂ))
181 sincn 26828 . . . . . . . . . . . . . . . . . . . . . . . 24 sin ∈ (ℂ–cn→ℂ)
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → sin ∈ (ℂ–cn→ℂ))
183 eqid 2763 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℂ ↦ (𝑥 / 2)) = (𝑥 ∈ ℂ ↦ (𝑥 / 2))
184183divccncf 25282 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ (ℂ–cn→ℂ))
185102, 81, 184mp2an 705 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ (ℂ–cn→ℂ)
186185a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (⊤ → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ (ℂ–cn→ℂ))
187163adantl 487 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⊤ ∧ 𝑥 ∈ ( -π(,)π)) → 𝑥 ∈ ℂ)
188187halfcld 12631 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⊤ ∧ 𝑥 ∈ ( -π(,)π)) → (𝑥 / 2) ∈ ℂ)
189183, 186, 143, 145, 188cncfmptssg 47154 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → (𝑥 ∈ ( -π(,)π) ↦ (𝑥 / 2)) ∈ (( -π(,)π)–cn→ℂ))
190182, 189cncfmpt1f 25290 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑥 ∈ ( -π(,)π) ↦ (sin‘(𝑥 / 2))) ∈ (( -π(,)π)–cn→ℂ))
191180, 190mulcncf 25822 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ∈ (( -π(,)π)–cn→ℂ))
192191mptru 1577 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ∈ (( -π(,)π)–cn→ℂ)
193 cnlimc 26263 . . . . . . . . . . . . . . . . . . . . 21 (( -π(,)π) ⊆ ℂ → ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ∈ (( -π(,)π)–cn→ℂ) ↔ ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):( -π(,)π)⟶ℂ ∧ ∀𝑦 ∈ ( -π(,)π)((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 𝑦))))
194142, 193ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ∈ (( -π(,)π)–cn→ℂ) ↔ ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):( -π(,)π)⟶ℂ ∧ ∀𝑦 ∈ ( -π(,)π)((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 𝑦)))
195192, 194mpbi 233 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):( -π(,)π)⟶ℂ ∧ ∀𝑦 ∈ ( -π(,)π)((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 𝑦))
196195simpri 491 . . . . . . . . . . . . . . . . . 18 ∀𝑦 ∈ ( -π(,)π)((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 𝑦)
197 fveq2 6916 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0))
198 oveq2 7459 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 𝑦) = ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 0))
199197, 198eleq12d 2858 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 0 → (((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 𝑦) ↔ ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) ∈ ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 0)))
200199rspccva 3579 . . . . . . . . . . . . . . . . . 18 ((∀𝑦 ∈ ( -π(,)π)((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 𝑦) ∧ 0 ∈ ( -π(,)π)) → ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) ∈ ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 0))
201196, 44, 200mp2an 705 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) ∈ ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 0)
202 oveq1 7458 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 0 → (𝑥 / 2) = (0 / 2))
203102, 81div0i 12091 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 / 2) = 0
204202, 203eqtrdi 2814 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 0 → (𝑥 / 2) = 0)
205204fveq2d 6920 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 0 → (sin‘(𝑥 / 2)) = (sin‘0))
206 sin0 16361 . . . . . . . . . . . . . . . . . . . . . 22 (sin‘0) = 0
207205, 206eqtrdi 2814 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 0 → (sin‘(𝑥 / 2)) = 0)
208207oveq2d 7467 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 0 → (2 · (sin‘(𝑥 / 2))) = (2 · 0))
209 2t0e0 12553 . . . . . . . . . . . . . . . . . . . 20 (2 · 0) = 0
210208, 209eqtrdi 2814 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → (2 · (sin‘(𝑥 / 2))) = 0)
211 eqid 2763 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))
212210, 211, 159fvmpt 7024 . . . . . . . . . . . . . . . . . 18 (0 ∈ ( -π(,)π) → ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) = 0)
21344, 212ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) = 0
214 2cnd 12461 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ( -π(,)π) → 2 ∈ ℂ)
215163halfcld 12631 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ( -π(,)π) → (𝑥 / 2) ∈ ℂ)
216215sincld 16342 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ( -π(,)π) → (sin‘(𝑥 / 2)) ∈ ℂ)
217214, 216mulcld 11368 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ( -π(,)π) → (2 · (sin‘(𝑥 / 2))) ∈ ℂ)
218211, 217fmpti 7144 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):( -π(,)π)⟶ℂ
219218a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):( -π(,)π)⟶ℂ)
220219limcdif 26251 . . . . . . . . . . . . . . . . . . 19 (⊤ → ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 0) = (((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ (( -π(,)π) ∖ {0})) limℂ 0))
221220mptru 1577 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 0) = (((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ (( -π(,)π) ∖ {0})) limℂ 0)
222 resmpt 6047 . . . . . . . . . . . . . . . . . . . 20 ((( -π(,)π) ∖ {0}) ⊆ ( -π(,)π) → ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ (( -π(,)π) ∖ {0})) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
22316, 222ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ (( -π(,)π) ∖ {0})) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))
224223oveq1i 7461 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ (( -π(,)π) ∖ {0})) limℂ 0) = ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 0)
225221, 224eqtri 2786 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ( -π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 0) = ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 0)
226201, 213, 2253eltr3i 2876 . . . . . . . . . . . . . . . 16 0 ∈ ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 0)
227226a1i 11 . . . . . . . . . . . . . . 15 (⊤ → 0 ∈ ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) limℂ 0))
228 eqidd 2764 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (( -π(,)π) ∖ {0}) → (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
229 oveq1 7458 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑥 / 2) = (𝑦 / 2))
230229fveq2d 6920 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (sin‘(𝑥 / 2)) = (sin‘(𝑦 / 2)))
231230oveq2d 7467 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → (2 · (sin‘(𝑥 / 2))) = (2 · (sin‘(𝑦 / 2))))
232231adantl 487 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ (( -π(,)π) ∖ {0}) ∧ 𝑥 = 𝑦) → (2 · (sin‘(𝑥 / 2))) = (2 · (sin‘(𝑦 / 2))))
233 id 23 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (( -π(,)π) ∖ {0}) → 𝑦 ∈ (( -π(,)π) ∖ {0}))
23426a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (( -π(,)π) ∖ {0}) → 2 ∈ ℝ)
23519sseli 3909 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (( -π(,)π) ∖ {0}) → 𝑦 ∈ ℝ)
236235rehalfcld 12633 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (( -π(,)π) ∖ {0}) → (𝑦 / 2) ∈ ℝ)
237236resincld 16355 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (( -π(,)π) ∖ {0}) → (sin‘(𝑦 / 2)) ∈ ℝ)
238234, 237remulcld 11378 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (( -π(,)π) ∖ {0}) → (2 · (sin‘(𝑦 / 2))) ∈ ℝ)
239228, 232, 233, 238fvmptd 7032 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (( -π(,)π) ∖ {0}) → ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = (2 · (sin‘(𝑦 / 2))))
240 2cnd 12461 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (( -π(,)π) ∖ {0}) → 2 ∈ ℂ)
241237recnd 11376 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (( -π(,)π) ∖ {0}) → (sin‘(𝑦 / 2)) ∈ ℂ)
24281a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (( -π(,)π) ∖ {0}) → 2 ≠ 0)
243 ioossicc 13604 . . . . . . . . . . . . . . . . . . . . . . 23 ( -π(,)π) ⊆ ( -π[,]π)
244 eldifi 4070 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (( -π(,)π) ∖ {0}) → 𝑦 ∈ ( -π(,)π))
245243, 244sselid 3911 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (( -π(,)π) ∖ {0}) → 𝑦 ∈ ( -π[,]π))
246 eldifsni 4755 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (( -π(,)π) ∖ {0}) → 𝑦 ≠ 0)
247 fourierdlem44 47434 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ( -π[,]π) ∧ 𝑦 ≠ 0) → (sin‘(𝑦 / 2)) ≠ 0)
248245, 246, 247syl2anc 596 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (( -π(,)π) ∖ {0}) → (sin‘(𝑦 / 2)) ≠ 0)
249240, 241, 242, 248mulne0d 12008 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (( -π(,)π) ∖ {0}) → (2 · (sin‘(𝑦 / 2))) ≠ 0)
250239, 249eqnetrd 3026 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (( -π(,)π) ∖ {0}) → ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ≠ 0)
251250neneqd 2964 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (( -π(,)π) ∖ {0}) → ¬ ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0)
252251nrex 3094 . . . . . . . . . . . . . . . . 17 ¬ ∃𝑦 ∈ (( -π(,)π) ∖ {0})((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0
25325fnmpt 6709 . . . . . . . . . . . . . . . . . . 19 (∀𝑥 ∈ (( -π(,)π) ∖ {0})(2 · (sin‘(𝑥 / 2))) ∈ ℝ → (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) Fn (( -π(,)π) ∖ {0}))
254253, 30mprg 3086 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) Fn (( -π(,)π) ∖ {0})
255 ssid 3935 . . . . . . . . . . . . . . . . . 18 (( -π(,)π) ∖ {0}) ⊆ (( -π(,)π) ∖ {0})
256 fvelimab 6988 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) Fn (( -π(,)π) ∖ {0}) ∧ (( -π(,)π) ∖ {0}) ⊆ (( -π(,)π) ∖ {0})) → (0 ∈ ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) “ (( -π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ (( -π(,)π) ∖ {0})((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0))
257254, 255, 256mp2an 705 . . . . . . . . . . . . . . . . 17 (0 ∈ ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) “ (( -π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ (( -π(,)π) ∖ {0})((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0)
258252, 257mtbir 326 . . . . . . . . . . . . . . . 16 ¬ 0 ∈ ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) “ (( -π(,)π) ∖ {0}))
259258a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ¬ 0 ∈ ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) “ (( -π(,)π) ∖ {0})))
260 eqidd 2764 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (( -π(,)π) ∖ {0}) → (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))))
261229fveq2d 6920 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (cos‘(𝑥 / 2)) = (cos‘(𝑦 / 2)))
262261adantl 487 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ (( -π(,)π) ∖ {0}) ∧ 𝑥 = 𝑦) → (cos‘(𝑥 / 2)) = (cos‘(𝑦 / 2)))
263235recnd 11376 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (( -π(,)π) ∖ {0}) → 𝑦 ∈ ℂ)
264263halfcld 12631 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (( -π(,)π) ∖ {0}) → (𝑦 / 2) ∈ ℂ)
265264coscld 16343 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (( -π(,)π) ∖ {0}) → (cos‘(𝑦 / 2)) ∈ ℂ)
266260, 262, 233, 265fvmptd 7032 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (( -π(,)π) ∖ {0}) → ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = (cos‘(𝑦 / 2)))
267236rered 15434 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (( -π(,)π) ∖ {0}) → (ℜ‘(𝑦 / 2)) = (𝑦 / 2))
268 halfpire 26850 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π / 2) ∈ ℝ
269268renegcli 11658 . . . . . . . . . . . . . . . . . . . . . . . . . 26 -(π / 2) ∈ ℝ
270269a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (( -π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ)
271270rexrd 11398 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (( -π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ*)
272268a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (( -π(,)π) ∖ {0}) → (π / 2) ∈ ℝ)
273272rexrd 11398 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (( -π(,)π) ∖ {0}) → (π / 2) ∈ ℝ*)
274 picn 26842 . . . . . . . . . . . . . . . . . . . . . . . . . 26 π ∈ ℂ
275 divneg 12048 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(π / 2) = ( -π / 2))
276274, 102, 81, 275mp3an 1491 . . . . . . . . . . . . . . . . . . . . . . . . 25 -(π / 2) = ( -π / 2)
27739a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (( -π(,)π) ∖ {0}) → -π ∈ ℝ)
278 2rp 13165 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ∈ ℝ+
279278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (( -π(,)π) ∖ {0}) → 2 ∈ ℝ+)
28040a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ (( -π(,)π) ∖ {0}) → -π ∈ ℝ*)
28141a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ (( -π(,)π) ∖ {0}) → π ∈ ℝ*)
282 ioogtlb 46780 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (( -π ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑦 ∈ ( -π(,)π)) → -π < 𝑦)
283280, 281, 244, 282syl3anc 1399 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (( -π(,)π) ∖ {0}) → -π < 𝑦)
284277, 235, 279, 283ltdiv1dd 13261 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (( -π(,)π) ∖ {0}) → ( -π / 2) < (𝑦 / 2))
285276, 284eqbrtrid 5146 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (( -π(,)π) ∖ {0}) → -(π / 2) < (𝑦 / 2))
28638a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (( -π(,)π) ∖ {0}) → π ∈ ℝ)
287 iooltub 46795 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( -π ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑦 ∈ ( -π(,)π)) → 𝑦 < π)
288280, 281, 244, 287syl3anc 1399 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (( -π(,)π) ∖ {0}) → 𝑦 < π)
289235, 286, 279, 288ltdiv1dd 13261 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (( -π(,)π) ∖ {0}) → (𝑦 / 2) < (π / 2))
290271, 273, 236, 285, 289eliood 46783 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (( -π(,)π) ∖ {0}) → (𝑦 / 2) ∈ ( -(π / 2)(,)(π / 2)))
291267, 290eqeltrd 2864 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (( -π(,)π) ∖ {0}) → (ℜ‘(𝑦 / 2)) ∈ ( -(π / 2)(,)(π / 2)))
292 cosne0 26914 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 / 2) ∈ ℂ ∧ (ℜ‘(𝑦 / 2)) ∈ ( -(π / 2)(,)(π / 2))) → (cos‘(𝑦 / 2)) ≠ 0)
293264, 291, 292syl2anc 596 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (( -π(,)π) ∖ {0}) → (cos‘(𝑦 / 2)) ≠ 0)
294266, 293eqnetrd 3026 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (( -π(,)π) ∖ {0}) → ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) ≠ 0)
295294neneqd 2964 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (( -π(,)π) ∖ {0}) → ¬ ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0)
296295nrex 3094 . . . . . . . . . . . . . . . . . 18 ¬ ∃𝑦 ∈ (( -π(,)π) ∖ {0})((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0
29772, 73fnmpti 6712 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) Fn (( -π(,)π) ∖ {0})
298 fvelimab 6988 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) Fn (( -π(,)π) ∖ {0}) ∧ (( -π(,)π) ∖ {0}) ⊆ (( -π(,)π) ∖ {0})) → (0 ∈ ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ (( -π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ (( -π(,)π) ∖ {0})((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0))
299297, 255, 298mp2an 705 . . . . . . . . . . . . . . . . . 18 (0 ∈ ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ (( -π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ (( -π(,)π) ∖ {0})((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0)
300296, 299mtbir 326 . . . . . . . . . . . . . . . . 17 ¬ 0 ∈ ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ (( -π(,)π) ∖ {0}))
301135imaeq1i 6067 . . . . . . . . . . . . . . . . . 18 ((ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) “ (( -π(,)π) ∖ {0})) = ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ (( -π(,)π) ∖ {0}))
302301eleq2i 2856 . . . . . . . . . . . . . . . . 17 (0 ∈ ((ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) “ (( -π(,)π) ∖ {0})) ↔ 0 ∈ ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ (( -π(,)π) ∖ {0})))
303300, 302mtbir 326 . . . . . . . . . . . . . . . 16 ¬ 0 ∈ ((ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) “ (( -π(,)π) ∖ {0}))
304303a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ¬ 0 ∈ ((ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) “ (( -π(,)π) ∖ {0})))
305 eqid 2763 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑠 / 2))) = (𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑠 / 2)))
306 eqid 2763 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) = (𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2))))
30719sseli 3909 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ (( -π(,)π) ∖ {0}) → 𝑠 ∈ ℝ)
308307recnd 11376 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (( -π(,)π) ∖ {0}) → 𝑠 ∈ ℂ)
309308halfcld 12631 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (𝑠 / 2) ∈ ℂ)
310309coscld 16343 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ∈ ℂ)
311307rehalfcld 12633 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (𝑠 / 2) ∈ ℝ)
312311rered 15434 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (ℜ‘(𝑠 / 2)) = (𝑠 / 2))
313269a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ (( -π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ)
314313rexrd 11398 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (( -π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ*)
315268a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (π / 2) ∈ ℝ)
316315rexrd 11398 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (π / 2) ∈ ℝ*)
31738a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ (( -π(,)π) ∖ {0}) → π ∈ ℝ)
318317renegcld 11782 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∈ (( -π(,)π) ∖ {0}) → -π ∈ ℝ)
319278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∈ (( -π(,)π) ∖ {0}) → 2 ∈ ℝ+)
32040a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ (( -π(,)π) ∖ {0}) → -π ∈ ℝ*)
32141a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ (( -π(,)π) ∖ {0}) → π ∈ ℝ*)
322 eldifi 4070 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ (( -π(,)π) ∖ {0}) → 𝑠 ∈ ( -π(,)π))
323 ioogtlb 46780 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (( -π ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑠 ∈ ( -π(,)π)) → -π < 𝑠)
324320, 321, 322, 323syl3anc 1399 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∈ (( -π(,)π) ∖ {0}) → -π < 𝑠)
325318, 307, 319, 324ltdiv1dd 13261 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ (( -π(,)π) ∖ {0}) → ( -π / 2) < (𝑠 / 2))
326276, 325eqbrtrid 5146 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (( -π(,)π) ∖ {0}) → -(π / 2) < (𝑠 / 2))
327 iooltub 46795 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (( -π ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑠 ∈ ( -π(,)π)) → 𝑠 < π)
328320, 321, 322, 327syl3anc 1399 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ (( -π(,)π) ∖ {0}) → 𝑠 < π)
329307, 317, 319, 328ltdiv1dd 13261 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (𝑠 / 2) < (π / 2))
330314, 316, 311, 326, 329eliood 46783 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (𝑠 / 2) ∈ ( -(π / 2)(,)(π / 2)))
331312, 330eqeltrd 2864 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (ℜ‘(𝑠 / 2)) ∈ ( -(π / 2)(,)(π / 2)))
332 cosne0 26914 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 / 2) ∈ ℂ ∧ (ℜ‘(𝑠 / 2)) ∈ ( -(π / 2)(,)(π / 2))) → (cos‘(𝑠 / 2)) ≠ 0)
333309, 331, 332syl2anc 596 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ≠ 0)
334333neneqd 2964 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (( -π(,)π) ∖ {0}) → ¬ (cos‘(𝑠 / 2)) = 0)
335311recoscld 16356 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ∈ ℝ)
336 elsng 4598 . . . . . . . . . . . . . . . . . . . . 21 ((cos‘(𝑠 / 2)) ∈ ℝ → ((cos‘(𝑠 / 2)) ∈ {0} ↔ (cos‘(𝑠 / 2)) = 0))
337335, 336syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (( -π(,)π) ∖ {0}) → ((cos‘(𝑠 / 2)) ∈ {0} ↔ (cos‘(𝑠 / 2)) = 0))
338334, 337mtbird 328 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (( -π(,)π) ∖ {0}) → ¬ (cos‘(𝑠 / 2)) ∈ {0})
339310, 338eldifd 4053 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ∈ (ℂ ∖ {0}))
340339adantl 487 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑠 ∈ (( -π(,)π) ∖ {0})) → (cos‘(𝑠 / 2)) ∈ (ℂ ∖ {0}))
341309ad2antrl 741 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ (𝑠 ∈ (( -π(,)π) ∖ {0}) ∧ (𝑠 / 2) ≠ 0)) → (𝑠 / 2) ∈ ℂ)
342 cosf 16337 . . . . . . . . . . . . . . . . . . . 20 cos:ℂ⟶ℂ
343342a1i 11 . . . . . . . . . . . . . . . . . . 19 (⊤ → cos:ℂ⟶ℂ)
344343ffvelcdmda 7116 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ ℂ) → (cos‘𝑥) ∈ ℂ)
345 eqid 2763 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ℂ ↦ (𝑠 / 2)) = (𝑠 ∈ ℂ ↦ (𝑠 / 2))
346345divccncf 25282 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑠 ∈ ℂ ↦ (𝑠 / 2)) ∈ (ℂ–cn→ℂ))
347102, 81, 346mp2an 705 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ℂ ↦ (𝑠 / 2)) ∈ (ℂ–cn→ℂ)
348347a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑠 ∈ ℂ ↦ (𝑠 / 2)) ∈ (ℂ–cn→ℂ))
349141adantl 487 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑠 ∈ ( -π(,)π)) → 𝑠 ∈ ℂ)
350349halfcld 12631 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑠 ∈ ( -π(,)π)) → (𝑠 / 2) ∈ ℂ)
351345, 348, 143, 145, 350cncfmptssg 47154 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑠 ∈ ( -π(,)π) ↦ (𝑠 / 2)) ∈ (( -π(,)π)–cn→ℂ))
352 oveq1 7458 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 0 → (𝑠 / 2) = (0 / 2))
353352, 203eqtrdi 2814 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → (𝑠 / 2) = 0)
354351, 45, 353cnmptlimc 26265 . . . . . . . . . . . . . . . . . . 19 (⊤ → 0 ∈ ((𝑠 ∈ ( -π(,)π) ↦ (𝑠 / 2)) limℂ 0))
355 eqid 2763 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ( -π(,)π) ↦ (𝑠 / 2)) = (𝑠 ∈ ( -π(,)π) ↦ (𝑠 / 2))
356141halfcld 12631 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ( -π(,)π) → (𝑠 / 2) ∈ ℂ)
357355, 356fmpti 7144 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ( -π(,)π) ↦ (𝑠 / 2)):( -π(,)π)⟶ℂ
358357a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑠 ∈ ( -π(,)π) ↦ (𝑠 / 2)):( -π(,)π)⟶ℂ)
359358limcdif 26251 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → ((𝑠 ∈ ( -π(,)π) ↦ (𝑠 / 2)) limℂ 0) = (((𝑠 ∈ ( -π(,)π) ↦ (𝑠 / 2)) ↾ (( -π(,)π) ∖ {0})) limℂ 0))
360359mptru 1577 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ ( -π(,)π) ↦ (𝑠 / 2)) limℂ 0) = (((𝑠 ∈ ( -π(,)π) ↦ (𝑠 / 2)) ↾ (( -π(,)π) ∖ {0})) limℂ 0)
361 resmpt 6047 . . . . . . . . . . . . . . . . . . . . . 22 ((( -π(,)π) ∖ {0}) ⊆ ( -π(,)π) → ((𝑠 ∈ ( -π(,)π) ↦ (𝑠 / 2)) ↾ (( -π(,)π) ∖ {0})) = (𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (𝑠 / 2)))
36216, 361ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ ( -π(,)π) ↦ (𝑠 / 2)) ↾ (( -π(,)π) ∖ {0})) = (𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (𝑠 / 2))
363362oveq1i 7461 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ ( -π(,)π) ↦ (𝑠 / 2)) ↾ (( -π(,)π) ∖ {0})) limℂ 0) = ((𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (𝑠 / 2)) limℂ 0)
364360, 363eqtri 2786 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ ( -π(,)π) ↦ (𝑠 / 2)) limℂ 0) = ((𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (𝑠 / 2)) limℂ 0)
365354, 364eleqtrdi 2874 . . . . . . . . . . . . . . . . . 18 (⊤ → 0 ∈ ((𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (𝑠 / 2)) limℂ 0))
366 ffn 6739 . . . . . . . . . . . . . . . . . . . . . . 23 (cos:ℂ⟶ℂ → cos Fn ℂ)
367342, 366ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 cos Fn ℂ
368 dffn5 6974 . . . . . . . . . . . . . . . . . . . . . 22 (cos Fn ℂ ↔ cos = (𝑥 ∈ ℂ ↦ (cos‘𝑥)))
369367, 368mpbi 233 . . . . . . . . . . . . . . . . . . . . 21 cos = (𝑥 ∈ ℂ ↦ (cos‘𝑥))
370 coscn 26829 . . . . . . . . . . . . . . . . . . . . 21 cos ∈ (ℂ–cn→ℂ)
371369, 370eqeltrri 2861 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℂ ↦ (cos‘𝑥)) ∈ (ℂ–cn→ℂ)
372371a1i 11 . . . . . . . . . . . . . . . . . . 19 (⊤ → (𝑥 ∈ ℂ ↦ (cos‘𝑥)) ∈ (ℂ–cn→ℂ))
373 0cnd 11338 . . . . . . . . . . . . . . . . . . 19 (⊤ → 0 ∈ ℂ)
374 fveq2 6916 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 0 → (cos‘𝑥) = (cos‘0))
375 cos0 16362 . . . . . . . . . . . . . . . . . . . 20 (cos‘0) = 1
376374, 375eqtrdi 2814 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → (cos‘𝑥) = 1)
377372, 373, 376cnmptlimc 26265 . . . . . . . . . . . . . . . . . 18 (⊤ → 1 ∈ ((𝑥 ∈ ℂ ↦ (cos‘𝑥)) limℂ 0))
378 fveq2 6916 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑠 / 2) → (cos‘𝑥) = (cos‘(𝑠 / 2)))
379 fveq2 6916 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 / 2) = 0 → (cos‘(𝑠 / 2)) = (cos‘0))
380379, 375eqtrdi 2814 . . . . . . . . . . . . . . . . . . 19 ((𝑠 / 2) = 0 → (cos‘(𝑠 / 2)) = 1)
381380ad2antll 742 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ (𝑠 ∈ (( -π(,)π) ∖ {0}) ∧ (𝑠 / 2) = 0)) → (cos‘(𝑠 / 2)) = 1)
382341, 344, 365, 377, 378, 381limcco 26268 . . . . . . . . . . . . . . . . 17 (⊤ → 1 ∈ ((𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑠 / 2))) limℂ 0))
383 ax-1ne0 11308 . . . . . . . . . . . . . . . . . 18 1 ≠ 0
384383a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → 1 ≠ 0)
385305, 306, 340, 382, 384reclimc 46936 . . . . . . . . . . . . . . . 16 (⊤ → (1 / 1) ∈ ((𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) limℂ 0))
386 1div1e1 12047 . . . . . . . . . . . . . . . 16 (1 / 1) = 1
38766fveq1i 6917 . . . . . . . . . . . . . . . . . . . 20 ((ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) = ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 1)‘𝑠)
388 eqidd 2764 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 1) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 1))
389 eqidd 2764 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (( -π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → 1 = 1)
390 id 23 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (( -π(,)π) ∖ {0}) → 𝑠 ∈ (( -π(,)π) ∖ {0}))
391 1red 11348 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (( -π(,)π) ∖ {0}) → 1 ∈ ℝ)
392388, 389, 390, 391fvmptd 7032 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (( -π(,)π) ∖ {0}) → ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 1)‘𝑠) = 1)
393387, 392eqtr2id 2811 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (( -π(,)π) ∖ {0}) → 1 = ((ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠))
394135a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))))
395 oveq1 7458 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑠 → (𝑥 / 2) = (𝑠 / 2))
396395fveq2d 6920 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑠 → (cos‘(𝑥 / 2)) = (cos‘(𝑠 / 2)))
397396adantl 487 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (( -π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (cos‘(𝑥 / 2)) = (cos‘(𝑠 / 2)))
398394, 397, 390, 335fvmptd 7032 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (( -π(,)π) ∖ {0}) → ((ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠) = (cos‘(𝑠 / 2)))
399398eqcomd 2769 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) = ((ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠))
400393, 399oveq12d 7469 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (1 / (cos‘(𝑠 / 2))) = (((ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) / ((ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠)))
401400mpteq2ia 5206 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) = (𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (((ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) / ((ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠)))
402401oveq1i 7461 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) limℂ 0) = ((𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (((ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) / ((ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠))) limℂ 0)
403385, 386, 4023eltr3g 2880 . . . . . . . . . . . . . . 15 (⊤ → 1 ∈ ((𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (((ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) / ((ℝ D (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠))) limℂ 0))
40420, 24, 32, 34, 45, 46, 71, 140, 173, 227, 259, 304, 403lhop 26391 . . . . . . . . . . . . . 14 (⊤ → 1 ∈ ((𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) limℂ 0))
405404mptru 1577 . . . . . . . . . . . . 13 1 ∈ ((𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) limℂ 0)
406 eqidd 2764 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥))
407 simpr 490 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (( -π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → 𝑥 = 𝑠)
408406, 407, 390, 307fvmptd 7032 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (( -π(,)π) ∖ {0}) → ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) = 𝑠)
409 eqidd 2764 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
410407oveq1d 7466 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (( -π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (𝑥 / 2) = (𝑠 / 2))
411410fveq2d 6920 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (( -π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (sin‘(𝑥 / 2)) = (sin‘(𝑠 / 2)))
412411oveq2d 7467 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (( -π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (2 · (sin‘(𝑥 / 2))) = (2 · (sin‘(𝑠 / 2))))
41326a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (( -π(,)π) ∖ {0}) → 2 ∈ ℝ)
414311resincld 16355 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (sin‘(𝑠 / 2)) ∈ ℝ)
415413, 414remulcld 11378 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
416409, 412, 390, 415fvmptd 7032 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (( -π(,)π) ∖ {0}) → ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠) = (2 · (sin‘(𝑠 / 2))))
417408, 416oveq12d 7469 . . . . . . . . . . . . . . 15 (𝑠 ∈ (( -π(,)π) ∖ {0}) → (((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠)) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
418417mpteq2ia 5206 . . . . . . . . . . . . . 14 (𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) = (𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
419418oveq1i 7461 . . . . . . . . . . . . 13 ((𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ (( -π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) limℂ 0) = ((𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) limℂ 0)
420405, 419eleqtri 2862 . . . . . . . . . . . 12 1 ∈ ((𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) limℂ 0)
42110oveq1i 7461 . . . . . . . . . . . . . 14 (𝐾 limℂ 0) = ((𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) limℂ 0)
42210feq1i 6730 . . . . . . . . . . . . . . . . . . 19 (𝐾:( -π[,]π)⟶ℂ ↔ (𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):( -π[,]π)⟶ℂ)
42314, 422mpbi 233 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):( -π[,]π)⟶ℂ
424423a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → (𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):( -π[,]π)⟶ℂ)
425243a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → ( -π(,)π) ⊆ ( -π[,]π))
426 iccssre 13600 . . . . . . . . . . . . . . . . . . . 20 (( -π ∈ ℝ ∧ π ∈ ℝ) → ( -π[,]π) ⊆ ℝ)
42739, 38, 426mp2an 705 . . . . . . . . . . . . . . . . . . 19 ( -π[,]π) ⊆ ℝ
428427a1i 11 . . . . . . . . . . . . . . . . . 18 (⊤ → ( -π[,]π) ⊆ ℝ)
429428, 12sstrdi 3925 . . . . . . . . . . . . . . . . 17 (⊤ → ( -π[,]π) ⊆ ℂ)
430 eqid 2763 . . . . . . . . . . . . . . . . 17 ((TopOpen‘ℂfld) ↾t (( -π[,]π) ∪ {0})) = ((TopOpen‘ℂfld) ↾t (( -π[,]π) ∪ {0}))
43139, 35, 36ltleii 11472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -π ≤ 0
43235, 38, 37ltleii 11472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ≤ π
43339, 38elicc2i 13583 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (0 ∈ ( -π[,]π) ↔ (0 ∈ ℝ ∧ -π ≤ 0 ∧ 0 ≤ π))
43435, 431, 432, 433mpbir3an 1360 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ∈ ( -π[,]π)
435159snss 4747 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 ∈ ( -π[,]π) ↔ {0} ⊆ ( -π[,]π))
436434, 435mpbi 233 . . . . . . . . . . . . . . . . . . . . . . . . 25 {0} ⊆ ( -π[,]π)
437 ssequn2 4190 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({0} ⊆ ( -π[,]π) ↔ (( -π[,]π) ∪ {0}) = ( -π[,]π))
438436, 437mpbi 233 . . . . . . . . . . . . . . . . . . . . . . . 24 (( -π[,]π) ∪ {0}) = ( -π[,]π)
439438oveq2i 7462 . . . . . . . . . . . . . . . . . . . . . . 23 ((TopOpen‘ℂfld) ↾t (( -π[,]π) ∪ {0})) = ((TopOpen‘ℂfld) ↾t ( -π[,]π))
440 eqid 2763 . . . . . . . . . . . . . . . . . . . . . . . . 25 (topGen‘ran (,)) = (topGen‘ran (,))
44157, 440rerest 25178 . . . . . . . . . . . . . . . . . . . . . . . 24 (( -π[,]π) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t ( -π[,]π)) = ((topGen‘ran (,)) ↾t ( -π[,]π)))
442427, 441ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((TopOpen‘ℂfld) ↾t ( -π[,]π)) = ((topGen‘ran (,)) ↾t ( -π[,]π))
443439, 442eqtri 2786 . . . . . . . . . . . . . . . . . . . . . 22 ((TopOpen‘ℂfld) ↾t (( -π[,]π) ∪ {0})) = ((topGen‘ran (,)) ↾t ( -π[,]π))
444443fveq2i 6919 . . . . . . . . . . . . . . . . . . . . 21 (int‘((TopOpen‘ℂfld) ↾t (( -π[,]π) ∪ {0}))) = (int‘((topGen‘ran (,)) ↾t ( -π[,]π)))
445159snss 4747 . . . . . . . . . . . . . . . . . . . . . . 23 (0 ∈ ( -π(,)π) ↔ {0} ⊆ ( -π(,)π))
44644, 445mpbi 233 . . . . . . . . . . . . . . . . . . . . . 22 {0} ⊆ ( -π(,)π)
447 ssequn2 4190 . . . . . . . . . . . . . . . . . . . . . 22 ({0} ⊆ ( -π(,)π) ↔ (( -π(,)π) ∪ {0}) = ( -π(,)π))
448446, 447mpbi 233 . . . . . . . . . . . . . . . . . . . . 21 (( -π(,)π) ∪ {0}) = ( -π(,)π)
449444, 448fveq12i 6922 . . . . . . . . . . . . . . . . . . . 20 ((int‘((TopOpen‘ℂfld) ↾t (( -π[,]π) ∪ {0})))‘(( -π(,)π) ∪ {0})) = ((int‘((topGen‘ran (,)) ↾t ( -π[,]π)))‘( -π(,)π))
450 resttopon 23534 . . . . . . . . . . . . . . . . . . . . . . 23 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ( -π[,]π) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ( -π[,]π)) ∈ (TopOn‘( -π[,]π)))
45160, 427, 450mp2an 705 . . . . . . . . . . . . . . . . . . . . . 22 ((topGen‘ran (,)) ↾t ( -π[,]π)) ∈ (TopOn‘( -π[,]π))
452451topontopi 23288 . . . . . . . . . . . . . . . . . . . . 21 ((topGen‘ran (,)) ↾t ( -π[,]π)) ∈ Top
453 retop 25135 . . . . . . . . . . . . . . . . . . . . . . . 24 (topGen‘ran (,)) ∈ Top
454 ovex 7484 . . . . . . . . . . . . . . . . . . . . . . . 24 ( -π[,]π) ∈ V
455453, 454pm3.2i 476 . . . . . . . . . . . . . . . . . . . . . . 23 ((topGen‘ran (,)) ∈ Top ∧ ( -π[,]π) ∈ V)
456 ssid 3935 . . . . . . . . . . . . . . . . . . . . . . . 24 ( -π(,)π) ⊆ ( -π(,)π)
45733, 243, 4563pm3.2i 1358 . . . . . . . . . . . . . . . . . . . . . . 23 (( -π(,)π) ∈ (topGen‘ran (,)) ∧ ( -π(,)π) ⊆ ( -π[,]π) ∧ ( -π(,)π) ⊆ ( -π(,)π))
458 restopnb 23548 . . . . . . . . . . . . . . . . . . . . . . 23 ((((topGen‘ran (,)) ∈ Top ∧ ( -π[,]π) ∈ V) ∧ (( -π(,)π) ∈ (topGen‘ran (,)) ∧ ( -π(,)π) ⊆ ( -π[,]π) ∧ ( -π(,)π) ⊆ ( -π(,)π))) → (( -π(,)π) ∈ (topGen‘ran (,)) ↔ ( -π(,)π) ∈ ((topGen‘ran (,)) ↾t ( -π[,]π))))
459455, 457, 458mp2an 705 . . . . . . . . . . . . . . . . . . . . . 22 (( -π(,)π) ∈ (topGen‘ran (,)) ↔ ( -π(,)π) ∈ ((topGen‘ran (,)) ↾t ( -π[,]π)))
46033, 459mpbi 233 . . . . . . . . . . . . . . . . . . . . 21 ( -π(,)π) ∈ ((topGen‘ran (,)) ↾t ( -π[,]π))
461 isopn3i 23455 . . . . . . . . . . . . . . . . . . . . 21 ((((topGen‘ran (,)) ↾t ( -π[,]π)) ∈ Top ∧ ( -π(,)π) ∈ ((topGen‘ran (,)) ↾t ( -π[,]π))) → ((int‘((topGen‘ran (,)) ↾t ( -π[,]π)))‘( -π(,)π)) = ( -π(,)π))
462452, 460, 461mp2an 705 . . . . . . . . . . . . . . . . . . . 20 ((int‘((topGen‘ran (,)) ↾t ( -π[,]π)))‘( -π(,)π)) = ( -π(,)π)
463 eqid 2763 . . . . . . . . . . . . . . . . . . . 20 ( -π(,)π) = ( -π(,)π)
464449, 462, 4633eqtrri 2791 . . . . . . . . . . . . . . . . . . 19 ( -π(,)π) = ((int‘((TopOpen‘ℂfld) ↾t (( -π[,]π) ∪ {0})))‘(( -π(,)π) ∪ {0}))
46544, 464eleqtri 2862 . . . . . . . . . . . . . . . . . 18 0 ∈ ((int‘((TopOpen‘ℂfld) ↾t (( -π[,]π) ∪ {0})))‘(( -π(,)π) ∪ {0}))
466465a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → 0 ∈ ((int‘((TopOpen‘ℂfld) ↾t (( -π[,]π) ∪ {0})))‘(( -π(,)π) ∪ {0})))
467424, 425, 429, 57, 430, 466limcres 26261 . . . . . . . . . . . . . . . 16 (⊤ → (((𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ( -π(,)π)) limℂ 0) = ((𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) limℂ 0))
468467mptru 1577 . . . . . . . . . . . . . . 15 (((𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ( -π(,)π)) limℂ 0) = ((𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) limℂ 0)
469468eqcomi 2772 . . . . . . . . . . . . . 14 ((𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) limℂ 0) = (((𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ( -π(,)π)) limℂ 0)
470 resmpt 6047 . . . . . . . . . . . . . . . 16 (( -π(,)π) ⊆ ( -π[,]π) → ((𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ( -π(,)π)) = (𝑠 ∈ ( -π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
471243, 470ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ( -π(,)π)) = (𝑠 ∈ ( -π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
472471oveq1i 7461 . . . . . . . . . . . . . 14 (((𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ( -π(,)π)) limℂ 0) = ((𝑠 ∈ ( -π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) limℂ 0)
473421, 469, 4723eqtri 2790 . . . . . . . . . . . . 13 (𝐾 limℂ 0) = ((𝑠 ∈ ( -π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) limℂ 0)
474 eqid 2763 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ( -π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ( -π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
475 iftrue 4491 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = 1)
476 1cnd 11341 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → 1 ∈ ℂ)
477475, 476eqeltrd 2864 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 0 → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
478477adantl 487 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ( -π(,)π) ∧ 𝑠 = 0) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
479 iffalse 4494 . . . . . . . . . . . . . . . . . . . 20 (¬ 𝑠 = 0 → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
480479adantl 487 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ ( -π(,)π) ∧ ¬ 𝑠 = 0) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
481141adantr 486 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ ( -π(,)π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ℂ)
482 2cnd 12461 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ ( -π(,)π) ∧ ¬ 𝑠 = 0) → 2 ∈ ℂ)
483481halfcld 12631 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ ( -π(,)π) ∧ ¬ 𝑠 = 0) → (𝑠 / 2) ∈ ℂ)
484483sincld 16342 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ ( -π(,)π) ∧ ¬ 𝑠 = 0) → (sin‘(𝑠 / 2)) ∈ ℂ)
485482, 484mulcld 11368 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ ( -π(,)π) ∧ ¬ 𝑠 = 0) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
48681a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ ( -π(,)π) ∧ ¬ 𝑠 = 0) → 2 ≠ 0)
487243sseli 3909 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ( -π(,)π) → 𝑠 ∈ ( -π[,]π))
488 neqne 2967 . . . . . . . . . . . . . . . . . . . . . 22 (¬ 𝑠 = 0 → 𝑠 ≠ 0)
489 fourierdlem44 47434 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ ( -π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
490487, 488, 489syl2an 608 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ ( -π(,)π) ∧ ¬ 𝑠 = 0) → (sin‘(𝑠 / 2)) ≠ 0)
491482, 484, 486, 490mulne0d 12008 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ ( -π(,)π) ∧ ¬ 𝑠 = 0) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
492481, 485, 491divcld 12133 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ ( -π(,)π) ∧ ¬ 𝑠 = 0) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
493480, 492eqeltrd 2864 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ( -π(,)π) ∧ ¬ 𝑠 = 0) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
494478, 493pm2.61dan 825 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ( -π(,)π) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
495474, 494fmpti 7144 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ( -π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):( -π(,)π)⟶ℂ
496495a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑠 ∈ ( -π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):( -π(,)π)⟶ℂ)
497496limcdif 26251 . . . . . . . . . . . . . 14 (⊤ → ((𝑠 ∈ ( -π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) limℂ 0) = (((𝑠 ∈ ( -π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (( -π(,)π) ∖ {0})) limℂ 0))
498497mptru 1577 . . . . . . . . . . . . 13 ((𝑠 ∈ ( -π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) limℂ 0) = (((𝑠 ∈ ( -π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (( -π(,)π) ∖ {0})) limℂ 0)
499 resmpt 6047 . . . . . . . . . . . . . . . 16 ((( -π(,)π) ∖ {0}) ⊆ ( -π(,)π) → ((𝑠 ∈ ( -π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (( -π(,)π) ∖ {0})) = (𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
50016, 499ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑠 ∈ ( -π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (( -π(,)π) ∖ {0})) = (𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
501 eldifn 4071 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (( -π(,)π) ∖ {0}) → ¬ 𝑠 ∈ {0})
502 velsn 4600 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ {0} ↔ 𝑠 = 0)
503501, 502sylnib 331 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (( -π(,)π) ∖ {0}) → ¬ 𝑠 = 0)
504503, 479syl 18 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (( -π(,)π) ∖ {0}) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
505504mpteq2ia 5206 . . . . . . . . . . . . . . 15 (𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
506500, 505eqtri 2786 . . . . . . . . . . . . . 14 ((𝑠 ∈ ( -π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (( -π(,)π) ∖ {0})) = (𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
507506oveq1i 7461 . . . . . . . . . . . . 13 (((𝑠 ∈ ( -π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (( -π(,)π) ∖ {0})) limℂ 0) = ((𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) limℂ 0)
508473, 498, 5073eqtrri 2791 . . . . . . . . . . . 12 ((𝑠 ∈ (( -π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) limℂ 0) = (𝐾 limℂ 0)
509420, 508eleqtri 2862 . . . . . . . . . . 11 1 ∈ (𝐾 limℂ 0)
510509a1i 11 . . . . . . . . . 10 (𝑠 = 0 → 1 ∈ (𝐾 limℂ 0))
511 fveq2 6916 . . . . . . . . . . 11 (𝑠 = 0 → (𝐾‘𝑠) = (𝐾‘0))
512475, 10, 47fvmpt 7024 . . . . . . . . . . . 12 (0 ∈ ( -π[,]π) → (𝐾‘0) = 1)
513434, 512ax-mp 5 . . . . . . . . . . 11 (𝐾‘0) = 1
514511, 513eqtrdi 2814 . . . . . . . . . 10 (𝑠 = 0 → (𝐾‘𝑠) = 1)
515 oveq2 7459 . . . . . . . . . 10 (𝑠 = 0 → (𝐾 limℂ 𝑠) = (𝐾 limℂ 0))
516510, 514, 5153eltr4d 2879 . . . . . . . . 9 (𝑠 = 0 → (𝐾‘𝑠) ∈ (𝐾 limℂ 𝑠))
517427, 12sstri 3922 . . . . . . . . . . 11 ( -π[,]π) ⊆ ℂ
518517a1i 11 . . . . . . . . . 10 (𝑠 = 0 → ( -π[,]π) ⊆ ℂ)
51938a1i 11 . . . . . . . . . . . 12 (𝑠 = 0 → π ∈ ℝ)
520519renegcld 11782 . . . . . . . . . . 11 (𝑠 = 0 → -π ∈ ℝ)
521 id 23 . . . . . . . . . . . 12 (𝑠 = 0 → 𝑠 = 0)
52235a1i 11 . . . . . . . . . . . 12 (𝑠 = 0 → 0 ∈ ℝ)
523521, 522eqeltrd 2864 . . . . . . . . . . 11 (𝑠 = 0 → 𝑠 ∈ ℝ)
524431, 521breqtrrid 5149 . . . . . . . . . . 11 (𝑠 = 0 → -π ≤ 𝑠)
525521, 432eqbrtrdi 5150 . . . . . . . . . . 11 (𝑠 = 0 → 𝑠 ≤ π)
526520, 519, 523, 524, 525eliccd 46789 . . . . . . . . . 10 (𝑠 = 0 → 𝑠 ∈ ( -π[,]π))
52756oveq1i 7461 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t ( -π[,]π)) = (((TopOpen‘ℂfld) ↾t ℝ) ↾t ( -π[,]π))
52857cnfldtop 25157 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) ∈ Top
529 reex 11330 . . . . . . . . . . . . 13 ℝ ∈ V
530 restabs 23538 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ∈ Top ∧ ( -π[,]π) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂfld) ↾t ℝ) ↾t ( -π[,]π)) = ((TopOpen‘ℂfld) ↾t ( -π[,]π)))
531528, 427, 529, 530mp3an 1491 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ↾t ℝ) ↾t ( -π[,]π)) = ((TopOpen‘ℂfld) ↾t ( -π[,]π))
532527, 531eqtri 2786 . . . . . . . . . . 11 ((topGen‘ran (,)) ↾t ( -π[,]π)) = ((TopOpen‘ℂfld) ↾t ( -π[,]π))
53357, 532cnplimc 26262 . . . . . . . . . 10 ((( -π[,]π) ⊆ ℂ ∧ 𝑠 ∈ ( -π[,]π)) → (𝐾 ∈ ((((topGen‘ran (,)) ↾t ( -π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠) ↔ (𝐾:( -π[,]π)⟶ℂ ∧ (𝐾‘𝑠) ∈ (𝐾 limℂ 𝑠))))
534518, 526, 533syl2anc 596 . . . . . . . . 9 (𝑠 = 0 → (𝐾 ∈ ((((topGen‘ran (,)) ↾t ( -π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠) ↔ (𝐾:( -π[,]π)⟶ℂ ∧ (𝐾‘𝑠) ∈ (𝐾 limℂ 𝑠))))
53515, 516, 534mpbir2and 726 . . . . . . . 8 (𝑠 = 0 → 𝐾 ∈ ((((topGen‘ran (,)) ↾t ( -π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))
536535adantl 487 . . . . . . 7 ((𝑠 ∈ ( -π[,]π) ∧ 𝑠 = 0) → 𝐾 ∈ ((((topGen‘ran (,)) ↾t ( -π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))
537 simpl 488 . . . . . . . . . . 11 ((𝑠 ∈ ( -π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ( -π[,]π))
538502notbii 323 . . . . . . . . . . . 12 (¬ 𝑠 ∈ {0} ↔ ¬ 𝑠 = 0)
539538bilanri 512 . . . . . . . . . . 11 ((𝑠 ∈ ( -π[,]π) ∧ ¬ 𝑠 = 0) → ¬ 𝑠 ∈ {0})
540537, 539eldifd 4053 . . . . . . . . . 10 ((𝑠 ∈ ( -π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ (( -π[,]π) ∖ {0}))
541 fveq2 6916 . . . . . . . . . . . 12 (𝑥 = 𝑠 → ((((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥) = ((((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠))
542541eleq2d 2850 . . . . . . . . . . 11 (𝑥 = 𝑠 → ((𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥) ↔ (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠)))
543429ssdifssd 4086 . . . . . . . . . . . . . . . . 17 (⊤ → (( -π[,]π) ∖ {0}) ⊆ ℂ)
544543, 145idcncfg 47156 . . . . . . . . . . . . . . . 16 (⊤ → (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ 𝑠) ∈ ((( -π[,]π) ∖ {0})–cn→ℂ))
545 eqid 2763 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2))))
546 2cnd 12461 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (( -π[,]π) ∖ {0}) → 2 ∈ ℂ)
547 eldifi 4070 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (( -π[,]π) ∖ {0}) → 𝑠 ∈ ( -π[,]π))
548517, 547sselid 3911 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ (( -π[,]π) ∖ {0}) → 𝑠 ∈ ℂ)
549548halfcld 12631 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ (( -π[,]π) ∖ {0}) → (𝑠 / 2) ∈ ℂ)
550549sincld 16342 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (( -π[,]π) ∖ {0}) → (sin‘(𝑠 / 2)) ∈ ℂ)
551546, 550mulcld 11368 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (( -π[,]π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
55281a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ (( -π[,]π) ∖ {0}) → 2 ≠ 0)
553 eldifsni 4755 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (( -π[,]π) ∖ {0}) → 𝑠 ≠ 0)
554547, 553, 489syl2anc 596 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ (( -π[,]π) ∖ {0}) → (sin‘(𝑠 / 2)) ≠ 0)
555546, 550, 552, 554mulne0d 12008 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ (( -π[,]π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
556555neneqd 2964 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (( -π[,]π) ∖ {0}) → ¬ (2 · (sin‘(𝑠 / 2))) = 0)
557 elsng 4598 . . . . . . . . . . . . . . . . . . . . . 22 ((2 · (sin‘(𝑠 / 2))) ∈ ℂ → ((2 · (sin‘(𝑠 / 2))) ∈ {0} ↔ (2 · (sin‘(𝑠 / 2))) = 0))
558551, 557syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (( -π[,]π) ∖ {0}) → ((2 · (sin‘(𝑠 / 2))) ∈ {0} ↔ (2 · (sin‘(𝑠 / 2))) = 0))
559556, 558mtbird 328 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (( -π[,]π) ∖ {0}) → ¬ (2 · (sin‘(𝑠 / 2))) ∈ {0})
560551, 559eldifd 4053 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (( -π[,]π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
561545, 560fmpti 7144 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))):(( -π[,]π) ∖ {0})⟶(ℂ ∖ {0})
562 difss 4075 . . . . . . . . . . . . . . . . . . 19 (ℂ ∖ {0}) ⊆ ℂ
563 eqid 2763 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ℂ ↦ 2) = (𝑠 ∈ ℂ ↦ 2)
564175, 176, 175constcncfg 47155 . . . . . . . . . . . . . . . . . . . . . . 23 (2 ∈ ℂ → (𝑠 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
565102, 564mp1i 14 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑠 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
566 2cnd 12461 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑠 ∈ (( -π[,]π) ∖ {0})) → 2 ∈ ℂ)
567563, 565, 543, 145, 566cncfmptssg 47154 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ 2) ∈ ((( -π[,]π) ∖ {0})–cn→ℂ))
568548, 546, 552divrecd 12136 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (( -π[,]π) ∖ {0}) → (𝑠 / 2) = (𝑠 · (1 / 2)))
569568mpteq2ia 5206 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / 2)) = (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 · (1 / 2)))
570 eqid 2763 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ℂ ↦ (1 / 2)) = (𝑠 ∈ ℂ ↦ (1 / 2))
571144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 / 2) ∈ ℂ → ℂ ⊆ ℂ)
572 id 23 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 / 2) ∈ ℂ → (1 / 2) ∈ ℂ)
573571, 572, 571constcncfg 47155 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 / 2) ∈ ℂ → (𝑠 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
57494, 573mp1i 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⊤ → (𝑠 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
57594a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⊤ ∧ 𝑠 ∈ (( -π[,]π) ∖ {0})) → (1 / 2) ∈ ℂ)
576570, 574, 543, 145, 575cncfmptssg 47154 . . . . . . . . . . . . . . . . . . . . . . . 24 (⊤ → (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (1 / 2)) ∈ ((( -π[,]π) ∖ {0})–cn→ℂ))
577544, 576mulcncf 25822 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 · (1 / 2))) ∈ ((( -π[,]π) ∖ {0})–cn→ℂ))
578569, 577eqeltrid 2868 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / 2)) ∈ ((( -π[,]π) ∖ {0})–cn→ℂ))
579182, 578cncfmpt1f 25290 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (sin‘(𝑠 / 2))) ∈ ((( -π[,]π) ∖ {0})–cn→ℂ))
580567, 579mulcncf 25822 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ ((( -π[,]π) ∖ {0})–cn→ℂ))
581580mptru 1577 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ ((( -π[,]π) ∖ {0})–cn→ℂ)
582 cncfcdm 25274 . . . . . . . . . . . . . . . . . . 19 (((ℂ ∖ {0}) ⊆ ℂ ∧ (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ ((( -π[,]π) ∖ {0})–cn→ℂ)) → ((𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ ((( -π[,]π) ∖ {0})–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))):(( -π[,]π) ∖ {0})⟶(ℂ ∖ {0})))
583562, 581, 582mp2an 705 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ ((( -π[,]π) ∖ {0})–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))):(( -π[,]π) ∖ {0})⟶(ℂ ∖ {0}))
584561, 583mpbir 234 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ ((( -π[,]π) ∖ {0})–cn→(ℂ ∖ {0}))
585584a1i 11 . . . . . . . . . . . . . . . 16 (⊤ → (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ ((( -π[,]π) ∖ {0})–cn→(ℂ ∖ {0})))
586544, 585divcncf 25823 . . . . . . . . . . . . . . 15 (⊤ → (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((( -π[,]π) ∖ {0})–cn→ℂ))
587586mptru 1577 . . . . . . . . . . . . . 14 (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((( -π[,]π) ∖ {0})–cn→ℂ)
588428ssdifssd 4086 . . . . . . . . . . . . . . . . 17 (⊤ → (( -π[,]π) ∖ {0}) ⊆ ℝ)
589588mptru 1577 . . . . . . . . . . . . . . . 16 (( -π[,]π) ∖ {0}) ⊆ ℝ
590589, 12sstri 3922 . . . . . . . . . . . . . . 15 (( -π[,]π) ∖ {0}) ⊆ ℂ
59156oveq1i 7461 . . . . . . . . . . . . . . . . 17 ((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) = (((TopOpen‘ℂfld) ↾t ℝ) ↾t (( -π[,]π) ∖ {0}))
592 restabs 23538 . . . . . . . . . . . . . . . . . 18 (((TopOpen‘ℂfld) ∈ Top ∧ (( -π[,]π) ∖ {0}) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂfld) ↾t ℝ) ↾t (( -π[,]π) ∖ {0})) = ((TopOpen‘ℂfld) ↾t (( -π[,]π) ∖ {0})))
593528, 589, 529, 592mp3an 1491 . . . . . . . . . . . . . . . . 17 (((TopOpen‘ℂfld) ↾t ℝ) ↾t (( -π[,]π) ∖ {0})) = ((TopOpen‘ℂfld) ↾t (( -π[,]π) ∖ {0}))
594591, 593eqtri 2786 . . . . . . . . . . . . . . . 16 ((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) = ((TopOpen‘ℂfld) ↾t (( -π[,]π) ∖ {0}))
595 unicntop 25159 . . . . . . . . . . . . . . . . . . 19 ℂ = ∪ (TopOpen‘ℂfld)
596595restid 17654 . . . . . . . . . . . . . . . . . 18 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
597528, 596ax-mp 5 . . . . . . . . . . . . . . . . 17 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
598597eqcomi 2772 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
59957, 594, 598cncfcn 25286 . . . . . . . . . . . . . . 15 (((( -π[,]π) ∖ {0}) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((( -π[,]π) ∖ {0})–cn→ℂ) = (((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) Cn (TopOpen‘ℂfld)))
600590, 144, 599mp2an 705 . . . . . . . . . . . . . 14 ((( -π[,]π) ∖ {0})–cn→ℂ) = (((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) Cn (TopOpen‘ℂfld))
601587, 600eleqtri 2862 . . . . . . . . . . . . 13 (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) Cn (TopOpen‘ℂfld))
602 resttopon 23534 . . . . . . . . . . . . . . 15 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (( -π[,]π) ∖ {0}) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) ∈ (TopOn‘(( -π[,]π) ∖ {0})))
60360, 589, 602mp2an 705 . . . . . . . . . . . . . 14 ((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) ∈ (TopOn‘(( -π[,]π) ∖ {0}))
60457cnfldtopon 25156 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
605 cncnp 23653 . . . . . . . . . . . . . 14 ((((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) ∈ (TopOn‘(( -π[,]π) ∖ {0})) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → ((𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) Cn (TopOpen‘ℂfld)) ↔ ((𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))):(( -π[,]π) ∖ {0})⟶ℂ ∧ ∀𝑥 ∈ (( -π[,]π) ∖ {0})(𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥))))
606603, 604, 605mp2an 705 . . . . . . . . . . . . 13 ((𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) Cn (TopOpen‘ℂfld)) ↔ ((𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))):(( -π[,]π) ∖ {0})⟶ℂ ∧ ∀𝑥 ∈ (( -π[,]π) ∖ {0})(𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥)))
607601, 606mpbi 233 . . . . . . . . . . . 12 ((𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))):(( -π[,]π) ∖ {0})⟶ℂ ∧ ∀𝑥 ∈ (( -π[,]π) ∖ {0})(𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥))
608607simpri 491 . . . . . . . . . . 11 ∀𝑥 ∈ (( -π[,]π) ∖ {0})(𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥)
609542, 608vtoclri 3548 . . . . . . . . . 10 (𝑠 ∈ (( -π[,]π) ∖ {0}) → (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠))
610540, 609syl 18 . . . . . . . . 9 ((𝑠 ∈ ( -π[,]π) ∧ ¬ 𝑠 = 0) → (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠))
61110reseq1i 5982 . . . . . . . . . 10 (𝐾 ↾ (( -π[,]π) ∖ {0})) = ((𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (( -π[,]π) ∖ {0}))
612 difss 4075 . . . . . . . . . . 11 (( -π[,]π) ∖ {0}) ⊆ ( -π[,]π)
613 resmpt 6047 . . . . . . . . . . 11 ((( -π[,]π) ∖ {0}) ⊆ ( -π[,]π) → ((𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (( -π[,]π) ∖ {0})) = (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
614612, 613ax-mp 5 . . . . . . . . . 10 ((𝑠 ∈ ( -π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (( -π[,]π) ∖ {0})) = (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
615 eldifn 4071 . . . . . . . . . . . . 13 (𝑠 ∈ (( -π[,]π) ∖ {0}) → ¬ 𝑠 ∈ {0})
616615, 502sylnib 331 . . . . . . . . . . . 12 (𝑠 ∈ (( -π[,]π) ∖ {0}) → ¬ 𝑠 = 0)
617616, 479syl 18 . . . . . . . . . . 11 (𝑠 ∈ (( -π[,]π) ∖ {0}) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
618617mpteq2ia 5206 . . . . . . . . . 10 (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
619611, 614, 6183eqtri 2790 . . . . . . . . 9 (𝐾 ↾ (( -π[,]π) ∖ {0})) = (𝑠 ∈ (( -π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
620 restabs 23538 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ Top ∧ (( -π[,]π) ∖ {0}) ⊆ ( -π[,]π) ∧ ( -π[,]π) ∈ V) → (((topGen‘ran (,)) ↾t ( -π[,]π)) ↾t (( -π[,]π) ∖ {0})) = ((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})))
621453, 612, 454, 620mp3an 1491 . . . . . . . . . . 11 (((topGen‘ran (,)) ↾t ( -π[,]π)) ↾t (( -π[,]π) ∖ {0})) = ((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0}))
622621oveq1i 7461 . . . . . . . . . 10 ((((topGen‘ran (,)) ↾t ( -π[,]π)) ↾t (( -π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld)) = (((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))
623622fveq1i 6917 . . . . . . . . 9 (((((topGen‘ran (,)) ↾t ( -π[,]π)) ↾t (( -π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠) = ((((topGen‘ran (,)) ↾t (( -π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠)
624610, 619, 6233eltr4g 2881 . . . . . . . 8 ((𝑠 ∈ ( -π[,]π) ∧ ¬ 𝑠 = 0) → (𝐾 ↾ (( -π[,]π) ∖ {0})) ∈ (((((topGen‘ran (,)) ↾t ( -π[,]π)) ↾t (( -π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠))
625452, 612pm3.2i 476 . . . . . . . . . 10 (((topGen‘ran (,)) ↾t ( -π[,]π)) ∈ Top ∧ (( -π[,]π) ∖ {0}) ⊆ ( -π[,]π))
626625a1i 11 . . . . . . . . 9 ((𝑠 ∈ ( -π[,]π) ∧ ¬ 𝑠 = 0) → (((topGen‘ran (,)) ↾t ( -π[,]π)) ∈ Top ∧ (( -π[,]π) ∖ {0}) ⊆ ( -π[,]π)))
627 ssdif 4083 . . . . . . . . . . . . . 14 (( -π[,]π) ⊆ ℝ → (( -π[,]π) ∖ {0}) ⊆ (ℝ ∖ {0}))
628427, 627ax-mp 5 . . . . . . . . . . . . 13 (( -π[,]π) ∖ {0}) ⊆ (ℝ ∖ {0})
629628, 540sselid 3911 . . . . . . . . . . . 12 ((𝑠 ∈ ( -π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ (ℝ ∖ {0}))
630 sscon 4082 . . . . . . . . . . . . . . . . 17 ({0} ⊆ ( -π[,]π) → (ℝ ∖ ( -π[,]π)) ⊆ (ℝ ∖ {0}))
631436, 630ax-mp 5 . . . . . . . . . . . . . . . 16 (ℝ ∖ ( -π[,]π)) ⊆ (ℝ ∖ {0})
632628, 631unssi 4192 . . . . . . . . . . . . . . 15 ((( -π[,]π) ∖ {0}) ∪ (ℝ ∖ ( -π[,]π))) ⊆ (ℝ ∖ {0})
633 simpr 490 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ ( -π[,]π)) → 𝑠 ∈ ( -π[,]π))
634 eldifn 4071 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (ℝ ∖ {0}) → ¬ 𝑠 ∈ {0})
635634adantr 486 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ ( -π[,]π)) → ¬ 𝑠 ∈ {0})
636633, 635eldifd 4053 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ ( -π[,]π)) → 𝑠 ∈ (( -π[,]π) ∖ {0}))
637 elun1 4183 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (( -π[,]π) ∖ {0}) → 𝑠 ∈ ((( -π[,]π) ∖ {0}) ∪ (ℝ ∖ ( -π[,]π))))
638636, 637syl 18 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ ( -π[,]π)) → 𝑠 ∈ ((( -π[,]π) ∖ {0}) ∪ (ℝ ∖ ( -π[,]π))))
639 eldifi 4070 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (ℝ ∖ {0}) → 𝑠 ∈ ℝ)
640639adantr 486 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ ( -π[,]π)) → 𝑠 ∈ ℝ)
641 simpr 490 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ ( -π[,]π)) → ¬ 𝑠 ∈ ( -π[,]π))
642640, 641eldifd 4053 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ ( -π[,]π)) → 𝑠 ∈ (ℝ ∖ ( -π[,]π)))
643 elun2 4184 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (ℝ ∖ ( -π[,]π)) → 𝑠 ∈ ((( -π[,]π) ∖ {0}) ∪ (ℝ ∖ ( -π[,]π))))
644642, 643syl 18 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ ( -π[,]π)) → 𝑠 ∈ ((( -π[,]π) ∖ {0}) ∪ (ℝ ∖ ( -π[,]π))))
645638, 644pm2.61dan 825 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (ℝ ∖ {0}) → 𝑠 ∈ ((( -π[,]π) ∖ {0}) ∪ (ℝ ∖ ( -π[,]π))))
646645ssriv 3917 . . . . . . . . . . . . . . 15 (ℝ ∖ {0}) ⊆ ((( -π[,]π) ∖ {0}) ∪ (ℝ ∖ ( -π[,]π)))
647632, 646eqssi 3929 . . . . . . . . . . . . . 14 ((( -π[,]π) ∖ {0}) ∪ (ℝ ∖ ( -π[,]π))) = (ℝ ∖ {0})
648647fveq2i 6919 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘((( -π[,]π) ∖ {0}) ∪ (ℝ ∖ ( -π[,]π)))) = ((int‘(topGen‘ran (,)))‘(ℝ ∖ {0}))
64961cldopn 23404 . . . . . . . . . . . . . . 15 ({0} ∈ (Clsd‘(topGen‘ran (,))) → (ℝ ∖ {0}) ∈ (topGen‘ran (,)))
65059, 649ax-mp 5 . . . . . . . . . . . . . 14 (ℝ ∖ {0}) ∈ (topGen‘ran (,))
651 isopn3i 23455 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ Top ∧ (ℝ ∖ {0}) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘(ℝ ∖ {0})) = (ℝ ∖ {0}))
652453, 650, 651mp2an 705 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘(ℝ ∖ {0})) = (ℝ ∖ {0})
653648, 652eqtri 2786 . . . . . . . . . . . 12 ((int‘(topGen‘ran (,)))‘((( -π[,]π) ∖ {0}) ∪ (ℝ ∖ ( -π[,]π)))) = (ℝ ∖ {0})
654629, 653eleqtrrdi 2875 . . . . . . . . . . 11 ((𝑠 ∈ ( -π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ((int‘(topGen‘ran (,)))‘((( -π[,]π) ∖ {0}) ∪ (ℝ ∖ ( -π[,]π)))))
655654, 537elind 4100 . . . . . . . . . 10 ((𝑠 ∈ ( -π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ (((int‘(topGen‘ran (,)))‘((( -π[,]π) ∖ {0}) ∪ (ℝ ∖ ( -π[,]π)))) ∩ ( -π[,]π)))
656 eqid 2763 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t ( -π[,]π)) = ((topGen‘ran (,)) ↾t ( -π[,]π))
65761, 656restntr 23555 . . . . . . . . . . 11 (((topGen‘ran (,)) ∈ Top ∧ ( -π[,]π) ⊆ ℝ ∧ (( -π[,]π) ∖ {0}) ⊆ ( -π[,]π)) → ((int‘((topGen‘ran (,)) ↾t ( -π[,]π)))‘(( -π[,]π) ∖ {0})) = (((int‘(topGen‘ran (,)))‘((( -π[,]π) ∖ {0}) ∪ (ℝ ∖ ( -π[,]π)))) ∩ ( -π[,]π)))
658453, 427, 612, 657mp3an 1491 . . . . . . . . . 10 ((int‘((topGen‘ran (,)) ↾t ( -π[,]π)))‘(( -π[,]π) ∖ {0})) = (((int‘(topGen‘ran (,)))‘((( -π[,]π) ∖ {0}) ∪ (ℝ ∖ ( -π[,]π)))) ∩ ( -π[,]π))
659655, 658eleqtrrdi 2875 . . . . . . . . 9 ((𝑠 ∈ ( -π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ((int‘((topGen‘ran (,)) ↾t ( -π[,]π)))‘(( -π[,]π) ∖ {0})))
66014a1i 11 . . . . . . . . 9 ((𝑠 ∈ ( -π[,]π) ∧ ¬ 𝑠 = 0) → 𝐾:( -π[,]π)⟶ℂ)
661451toponunii 23289 . . . . . . . . . 10 ( -π[,]π) = ∪ ((topGen‘ran (,)) ↾t ( -π[,]π))
662661, 595cnprest 23662 . . . . . . . . 9 (((((topGen‘ran (,)) ↾t ( -π[,]π)) ∈ Top ∧ (( -π[,]π) ∖ {0}) ⊆ ( -π[,]π)) ∧ (𝑠 ∈ ((int‘((topGen‘ran (,)) ↾t ( -π[,]π)))‘(( -π[,]π) ∖ {0})) ∧ 𝐾:( -π[,]π)⟶ℂ)) → (𝐾 ∈ ((((topGen‘ran (,)) ↾t ( -π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠) ↔ (𝐾 ↾ (( -π[,]π) ∖ {0})) ∈ (((((topGen‘ran (,)) ↾t ( -π[,]π)) ↾t (( -π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠)))
663626, 659, 660, 662syl12anc 850 . . . . . . . 8 ((𝑠 ∈ ( -π[,]π) ∧ ¬ 𝑠 = 0) → (𝐾 ∈ ((((topGen‘ran (,)) ↾t ( -π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠) ↔ (𝐾 ↾ (( -π[,]π) ∖ {0})) ∈ (((((topGen‘ran (,)) ↾t ( -π[,]π)) ↾t (( -π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠)))
664624, 663mpbird 260 . . . . . . 7 ((𝑠 ∈ ( -π[,]π) ∧ ¬ 𝑠 = 0) → 𝐾 ∈ ((((topGen‘ran (,)) ↾t ( -π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))
665536, 664pm2.61dan 825 . . . . . 6 (𝑠 ∈ ( -π[,]π) → 𝐾 ∈ ((((topGen‘ran (,)) ↾t ( -π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))
666665rgen 3082 . . . . 5 ∀𝑠 ∈ ( -π[,]π)𝐾 ∈ ((((topGen‘ran (,)) ↾t ( -π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠)
667 cncnp 23653 . . . . . 6 ((((topGen‘ran (,)) ↾t ( -π[,]π)) ∈ (TopOn‘( -π[,]π)) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → (𝐾 ∈ (((topGen‘ran (,)) ↾t ( -π[,]π)) Cn (TopOpen‘ℂfld)) ↔ (𝐾:( -π[,]π)⟶ℂ ∧ ∀𝑠 ∈ ( -π[,]π)𝐾 ∈ ((((topGen‘ran (,)) ↾t ( -π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))))
668451, 604, 667mp2an 705 . . . . 5 (𝐾 ∈ (((topGen‘ran (,)) ↾t ( -π[,]π)) Cn (TopOpen‘ℂfld)) ↔ (𝐾:( -π[,]π)⟶ℂ ∧ ∀𝑠 ∈ ( -π[,]π)𝐾 ∈ ((((topGen‘ran (,)) ↾t ( -π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠)))
66914, 666, 668mpbir2an 724 . . . 4 𝐾 ∈ (((topGen‘ran (,)) ↾t ( -π[,]π)) Cn (TopOpen‘ℂfld))
67057, 532, 598cncfcn 25286 . . . . . 6 ((( -π[,]π) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (( -π[,]π)–cn→ℂ) = (((topGen‘ran (,)) ↾t ( -π[,]π)) Cn (TopOpen‘ℂfld)))
671517, 144, 670mp2an 705 . . . . 5 (( -π[,]π)–cn→ℂ) = (((topGen‘ran (,)) ↾t ( -π[,]π)) Cn (TopOpen‘ℂfld))
672671eqcomi 2772 . . . 4 (((topGen‘ran (,)) ↾t ( -π[,]π)) Cn (TopOpen‘ℂfld)) = (( -π[,]π)–cn→ℂ)
673669, 672eleqtri 2862 . . 3 𝐾 ∈ (( -π[,]π)–cn→ℂ)
674 cncfcdm 25274 . . 3 ((ℝ ⊆ ℂ ∧ 𝐾 ∈ (( -π[,]π)–cn→ℂ)) → (𝐾 ∈ (( -π[,]π)–cn→ℝ) ↔ 𝐾:( -π[,]π)⟶ℝ))
67512, 673, 674mp2an 705 . 2 (𝐾 ∈ (( -π[,]π)–cn→ℝ) ↔ 𝐾:( -π[,]π)⟶ℝ)
67611, 675mpbir 234 1 𝐾 ∈ (( -π[,]π)–cn→ℝ)
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ⊤wtru 1571   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048   ∩ cin 4092   ∪ cun 4152  ifcif 4485  {csn 4588  {cpr 4590   class class class wbr 5108   ↦ cmpt 5192  dom cdm 5658  ran crn 5659   ↾ cres 5660   “ cima 5661   Fn wfn 6561  ⟶wf 6562  ‘cfv 6566  (class class class)co 7451  ℂcc 11237  ℝcr 11238  0cc0 11239  1c1 11240   · cmul 11244  ℝ*cxr 11381   < clt 11382   ≤ cle 11383   -cneg 11581   / cdiv 12013  2c2 12437  ℝ+crp 13160  (,)cioo 13516  [,]cicc 13519  ℜcre 15307  sincsin 16273  cosccos 16274  πcpi 16276   ↾t crest 17641  TopOpenctopn 17642  topGenctg 17658  ℂfldccnfld 21729  Topctop 23266  TopOnctopon 23283  Clsdccld 23389  intcnt 23390   Cn ccn 23597   CnP ccnp 23598  –cn→ccncf 25252   limℂ climc 26237   D cdv 26238
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-inf2 9679  ax-cnex 11295  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316  ax-pre-sup 11317  ax-addf 11318
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4841  df-uni 4873  df-int 4913  df-iun 4958  df-iin 4959  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-isom 6575  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-of 7725  df-om 7912  df-1st 8035  df-2nd 8036  df-supp 8215  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-1o 8514  df-2o 8515  df-er 8755  df-map 8887  df-pm 8888  df-ixp 8964  df-en 9012  df-dom 9013  df-sdom 9014  df-fin 9015  df-fsupp 9392  df-fi 9440  df-sup 9471  df-inf 9472  df-oi 9541  df-card 10057  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583  df-div 12014  df-nn 12376  df-2 12445  df-3 12446  df-4 12447  df-5 12448  df-6 12449  df-7 12450  df-8 12451  df-9 12452  df-n0 12647  df-z 12734  df-dec 12855  df-uz 13006  df-q 13116  df-rp 13161  df-xneg 13281  df-xadd 13282  df-xmul 13283  df-ioo 13520  df-ioc 13521  df-ico 13522  df-icc 13523  df-fz 13680  df-fzo 13829  df-fl 13972  df-mod 14050  df-seq 14185  df-exp 14245  df-fac 14459  df-bc 14488  df-hash 14516  df-shft 15263  df-cj 15309  df-re 15310  df-im 15311  df-sqrt 15445  df-abs 15446  df-limsup 15682  df-clim 15699  df-rlim 15700  df-sum 15898  df-ef 16277  df-sin 16279  df-cos 16280  df-pi 16282  df-struct 17369  df-sets 17386  df-slot 17404  df-ndx 17416  df-base 17432  df-ress 17453  df-plusg 17486  df-mulr 17487  df-starv 17488  df-sca 17489  df-vsca 17490  df-ip 17491  df-tset 17492  df-ple 17493  df-ds 17495  df-unif 17496  df-hom 17497  df-cco 17498  df-euf 17499  df-rest 17643  df-topn 17644  df-0g 17662  df-gsum 17663  df-topgen 17664  df-pt 17665  df-prds 17668  df-xrs 17724  df-qtop 17729  df-imas 17730  df-xps 17732  df-mre 17806  df-mrc 17807  df-acs 17809  df-mgm 18866  df-sgrp 18958  df-mnd 18974  df-submnd 19029  df-mulg 19328  df-cntz 19582  df-cmn 20047  df-psmet 21721  df-xmet 21722  df-met 21723  df-bl 21724  df-mopn 21725  df-fbas 21726  df-fg 21727  df-cnfld 21730  df-top 23267  df-topon 23284  df-topsp 23306  df-bases 23319  df-cld 23392  df-ntr 23393  df-cls 23394  df-nei 23471  df-lp 23509  df-perf 23510  df-cn 23600  df-cnp 23601  df-t1 23687  df-haus 23688  df-cmp 23760  df-tx 23936  df-hmeo 24129  df-fil 24220  df-fm 24312  df-flim 24313  df-flf 24314  df-xms 24694  df-ms 24695  df-tms 24696  df-cncf 25254  df-limc 26241  df-dv 26242
This theorem is used by:  fourierdlem77  47466  fourierdlem78  47467  fourierdlem85  47474  fourierdlem88  47477
  Copyright terms: Public domain W3C validator