Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem62 Structured version   Visualization version   GIF version

Theorem fourierdlem62 40703
 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 2655 . . . . . 6 (𝑦 = 𝑠 → (𝑦 = 0 ↔ 𝑠 = 0))
3 id 22 . . . . . . 7 (𝑦 = 𝑠𝑦 = 𝑠)
4 oveq1 6697 . . . . . . . . 9 (𝑦 = 𝑠 → (𝑦 / 2) = (𝑠 / 2))
54fveq2d 6233 . . . . . . . 8 (𝑦 = 𝑠 → (sin‘(𝑦 / 2)) = (sin‘(𝑠 / 2)))
65oveq2d 6706 . . . . . . 7 (𝑦 = 𝑠 → (2 · (sin‘(𝑦 / 2))) = (2 · (sin‘(𝑠 / 2))))
73, 6oveq12d 6708 . . . . . 6 (𝑦 = 𝑠 → (𝑦 / (2 · (sin‘(𝑦 / 2)))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
82, 7ifbieq2d 4144 . . . . 5 (𝑦 = 𝑠 → if(𝑦 = 0, 1, (𝑦 / (2 · (sin‘(𝑦 / 2))))) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
98cbvmptv 4783 . . . 4 (𝑦 ∈ (-π[,]π) ↦ if(𝑦 = 0, 1, (𝑦 / (2 · (sin‘(𝑦 / 2)))))) = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
101, 9eqtri 2673 . . 3 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
1110fourierdlem43 40685 . 2 𝐾:(-π[,]π)⟶ℝ
12 ax-resscn 10031 . . 3 ℝ ⊆ ℂ
13 fss 6094 . . . . . 6 ((𝐾:(-π[,]π)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐾:(-π[,]π)⟶ℂ)
1411, 12, 13mp2an 708 . . . . 5 𝐾:(-π[,]π)⟶ℂ
1514a1i 11 . . . . . . . . 9 (𝑠 = 0 → 𝐾:(-π[,]π)⟶ℂ)
16 difss 3770 . . . . . . . . . . . . . . . . 17 ((-π(,)π) ∖ {0}) ⊆ (-π(,)π)
17 elioore 12243 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (-π(,)π) → 𝑠 ∈ ℝ)
1817ssriv 3640 . . . . . . . . . . . . . . . . 17 (-π(,)π) ⊆ ℝ
1916, 18sstri 3645 . . . . . . . . . . . . . . . 16 ((-π(,)π) ∖ {0}) ⊆ ℝ
2019a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ((-π(,)π) ∖ {0}) ⊆ ℝ)
21 eqid 2651 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)
2219sseli 3632 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-π(,)π) ∖ {0}) → 𝑥 ∈ ℝ)
2321, 22fmpti 6423 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥):((-π(,)π) ∖ {0})⟶ℝ
2423a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥):((-π(,)π) ∖ {0})⟶ℝ)
25 eqid 2651 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))
26 2re 11128 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℝ
2726a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ)
2822rehalfcld 11317 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) → (𝑥 / 2) ∈ ℝ)
2928resincld 14917 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑥 / 2)) ∈ ℝ)
3027, 29remulcld 10108 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-π(,)π) ∖ {0}) → (2 · (sin‘(𝑥 / 2))) ∈ ℝ)
3125, 30fmpti 6423 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))):((-π(,)π) ∖ {0})⟶ℝ
3231a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))):((-π(,)π) ∖ {0})⟶ℝ)
33 iooretop 22616 . . . . . . . . . . . . . . . 16 (-π(,)π) ∈ (topGen‘ran (,))
3433a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (-π(,)π) ∈ (topGen‘ran (,)))
35 0re 10078 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
36 negpilt0 39806 . . . . . . . . . . . . . . . . 17 -π < 0
37 pipos 24257 . . . . . . . . . . . . . . . . 17 0 < π
38 pire 24255 . . . . . . . . . . . . . . . . . . . 20 π ∈ ℝ
3938renegcli 10380 . . . . . . . . . . . . . . . . . . 19 -π ∈ ℝ
4039rexri 10135 . . . . . . . . . . . . . . . . . 18 -π ∈ ℝ*
4138rexri 10135 . . . . . . . . . . . . . . . . . 18 π ∈ ℝ*
42 elioo2 12254 . . . . . . . . . . . . . . . . . 18 ((-π ∈ ℝ* ∧ π ∈ ℝ*) → (0 ∈ (-π(,)π) ↔ (0 ∈ ℝ ∧ -π < 0 ∧ 0 < π)))
4340, 41, 42mp2an 708 . . . . . . . . . . . . . . . . 17 (0 ∈ (-π(,)π) ↔ (0 ∈ ℝ ∧ -π < 0 ∧ 0 < π))
4435, 36, 37, 43mpbir3an 1263 . . . . . . . . . . . . . . . 16 0 ∈ (-π(,)π)
4544a1i 11 . . . . . . . . . . . . . . 15 (⊤ → 0 ∈ (-π(,)π))
46 eqid 2651 . . . . . . . . . . . . . . 15 ((-π(,)π) ∖ {0}) = ((-π(,)π) ∖ {0})
47 1ex 10073 . . . . . . . . . . . . . . . . . . 19 1 ∈ V
48 eqid 2651 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1)
4947, 48dmmpti 6061 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = ((-π(,)π) ∖ {0})
50 reelprrecn 10066 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ ∈ {ℝ, ℂ}
5150a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ℝ ∈ {ℝ, ℂ})
5212sseli 3632 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
5352adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
54 1red 10093 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
5551dvmptid 23765 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
56 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . 23 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
5756tgioo2 22653 . . . . . . . . . . . . . . . . . . . . . 22 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
58 sncldre 39522 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 ∈ ℝ → {0} ∈ (Clsd‘(topGen‘ran (,))))
5935, 58ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 {0} ∈ (Clsd‘(topGen‘ran (,)))
60 retopon 22614 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
6160toponunii 20769 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℝ = (topGen‘ran (,))
6261difopn 20886 . . . . . . . . . . . . . . . . . . . . . . . 24 (((-π(,)π) ∈ (topGen‘ran (,)) ∧ {0} ∈ (Clsd‘(topGen‘ran (,)))) → ((-π(,)π) ∖ {0}) ∈ (topGen‘ran (,)))
6333, 59, 62mp2an 708 . . . . . . . . . . . . . . . . . . . . . . 23 ((-π(,)π) ∖ {0}) ∈ (topGen‘ran (,))
6463a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ((-π(,)π) ∖ {0}) ∈ (topGen‘ran (,)))
6551, 53, 54, 55, 20, 57, 56, 64dvmptres 23771 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1))
6665trud 1533 . . . . . . . . . . . . . . . . . . . 20 (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1)
6766eqcomi 2660 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
6867dmeqi 5357 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
6949, 68eqtr3i 2675 . . . . . . . . . . . . . . . . 17 ((-π(,)π) ∖ {0}) = dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
7069eqimssi 3692 . . . . . . . . . . . . . . . 16 ((-π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
7170a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ((-π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)))
72 fvex 6239 . . . . . . . . . . . . . . . . . . 19 (cos‘(𝑥 / 2)) ∈ V
73 eqid 2651 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))
7472, 73dmmpti 6061 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = ((-π(,)π) ∖ {0})
75 2cnd 11131 . . . . . . . . . . . . . . . . . . . . . . 23 ((⊤ ∧ 𝑥 ∈ ℝ) → 2 ∈ ℂ)
7653halfcld 11315 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⊤ ∧ 𝑥 ∈ ℝ) → (𝑥 / 2) ∈ ℂ)
7776sincld 14904 . . . . . . . . . . . . . . . . . . . . . . 23 ((⊤ ∧ 𝑥 ∈ ℝ) → (sin‘(𝑥 / 2)) ∈ ℂ)
7875, 77mulcld 10098 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → (2 · (sin‘(𝑥 / 2))) ∈ ℂ)
7976coscld 14905 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → (cos‘(𝑥 / 2)) ∈ ℂ)
80 2cnd 11131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → 2 ∈ ℂ)
81 2ne0 11151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 2 ≠ 0
8281a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → 2 ≠ 0)
8352, 80, 82divrec2d 10843 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → (𝑥 / 2) = ((1 / 2) · 𝑥))
8483fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℝ → (sin‘(𝑥 / 2)) = (sin‘((1 / 2) · 𝑥)))
8584oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ → (2 · (sin‘(𝑥 / 2))) = (2 · (sin‘((1 / 2) · 𝑥))))
8685mpteq2ia 4773 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))
8786oveq2i 6701 . . . . . . . . . . . . . . . . . . . . . . . 24 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2))))) = (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))
88 resmpt 5484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℝ ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))
8912, 88ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))
9089eqcomi 2660 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) = ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ)
9190oveq2i 6701 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (ℝ D ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ))
92 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) = (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))
93 2cnd 11131 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℂ → 2 ∈ ℂ)
94 halfcn 11285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (1 / 2) ∈ ℂ
9594a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℂ → (1 / 2) ∈ ℂ)
96 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℂ → 𝑥 ∈ ℂ)
9795, 96mulcld 10098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℂ → ((1 / 2) · 𝑥) ∈ ℂ)
9897sincld 14904 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℂ → (sin‘((1 / 2) · 𝑥)) ∈ ℂ)
9993, 98mulcld 10098 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℂ → (2 · (sin‘((1 / 2) · 𝑥))) ∈ ℂ)
10092, 99fmpti 6423 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))):ℂ⟶ℂ
101 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
102 2cn 11129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2 ∈ ℂ
103102, 94mulcli 10083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (2 · (1 / 2)) ∈ ℂ
104103a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ ℂ → (2 · (1 / 2)) ∈ ℂ)
10597coscld 14905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ ℂ → (cos‘((1 / 2) · 𝑥)) ∈ ℂ)
106104, 105mulcld 10098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ ℂ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) ∈ ℂ)
107106adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((⊤ ∧ 𝑥 ∈ ℂ) → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) ∈ ℂ)
108101, 107dmmptd 6062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⊤ → dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = ℂ)
109108trud 1533 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = ℂ
11012, 109sseqtr4i 3671 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℝ ⊆ dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
111 dvasinbx 40453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))))
112102, 94, 111mp2an 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
113112dmeqi 5357 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 dom (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
114110, 113sseqtr4i 3671 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℝ ⊆ dom (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))
115 dvcnre 40448 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))):ℂ⟶ℂ ∧ ℝ ⊆ dom (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))) → (ℝ D ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ)) = ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ))
116100, 114, 115mp2an 708 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℝ D ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ)) = ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ)
117112reseq1i 5424 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ) = ((𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) ↾ ℝ)
118 resmpt 5484 . . . . . . . . . . . . . . . . . . . . . . . . . . 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) · 𝑥))))
120102, 81recidi 10794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (2 · (1 / 2)) = 1
121120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → (2 · (1 / 2)) = 1)
12283eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℝ → ((1 / 2) · 𝑥) = (𝑥 / 2))
123122fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → (cos‘((1 / 2) · 𝑥)) = (cos‘(𝑥 / 2)))
124121, 123oveq12d 6708 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) = (1 · (cos‘(𝑥 / 2))))
12552halfcld 11315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℝ → (𝑥 / 2) ∈ ℂ)
126125coscld 14905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → (cos‘(𝑥 / 2)) ∈ ℂ)
127126mulid2d 10096 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → (1 · (cos‘(𝑥 / 2))) = (cos‘(𝑥 / 2)))
128124, 127eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℝ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) = (cos‘(𝑥 / 2)))
129128mpteq2ia 4773 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
130117, 119, 1293eqtri 2677 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
13191, 116, 1303eqtri 2677 . . . . . . . . . . . . . . . . . . . . . . . 24 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
13287, 131eqtri 2673 . . . . . . . . . . . . . . . . . . . . . . 23 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
133132a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2))))
13451, 78, 79, 133, 20, 57, 56, 64dvmptres 23771 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))))
135134trud 1533 . . . . . . . . . . . . . . . . . . . 20 (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))
136135eqcomi 2660 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
137136dmeqi 5357 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
13874, 137eqtr3i 2675 . . . . . . . . . . . . . . . . 17 ((-π(,)π) ∖ {0}) = dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
139138eqimssi 3692 . . . . . . . . . . . . . . . 16 ((-π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
140139a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ((-π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))))
14117recnd 10106 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (-π(,)π) → 𝑠 ∈ ℂ)
142141ssriv 3640 . . . . . . . . . . . . . . . . . . . . . . 23 (-π(,)π) ⊆ ℂ
143142a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (-π(,)π) ⊆ ℂ)
144 ssid 3657 . . . . . . . . . . . . . . . . . . . . . . 23 ℂ ⊆ ℂ
145144a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ℂ ⊆ ℂ)
146143, 145idcncfg 40403 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑥 ∈ (-π(,)π) ↦ 𝑥) ∈ ((-π(,)π)–cn→ℂ))
147146trud 1533 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (-π(,)π) ↦ 𝑥) ∈ ((-π(,)π)–cn→ℂ)
148 cnlimc 23697 . . . . . . . . . . . . . . . . . . . . 21 ((-π(,)π) ⊆ ℂ → ((𝑥 ∈ (-π(,)π) ↦ 𝑥) ∈ ((-π(,)π)–cn→ℂ) ↔ ((𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦))))
149142, 148ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (-π(,)π) ↦ 𝑥) ∈ ((-π(,)π)–cn→ℂ) ↔ ((𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦)))
150147, 149mpbi 220 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦))
151150simpri 477 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦)
152 fveq2 6229 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) = ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0))
153 oveq2 6698 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦) = ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0))
154152, 153eleq12d 2724 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 0 → (((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦) ↔ ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0)))
155154rspccva 3339 . . . . . . . . . . . . . . . . . 18 ((∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦) ∧ 0 ∈ (-π(,)π)) → ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0))
156151, 44, 155mp2an 708 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0)
157 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → 𝑥 = 0)
158 eqid 2651 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (-π(,)π) ↦ 𝑥) = (𝑥 ∈ (-π(,)π) ↦ 𝑥)
159 c0ex 10072 . . . . . . . . . . . . . . . . . . 19 0 ∈ V
160157, 158, 159fvmpt 6321 . . . . . . . . . . . . . . . . . 18 (0 ∈ (-π(,)π) → ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) = 0)
16144, 160ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) = 0
162 elioore 12243 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (-π(,)π) → 𝑥 ∈ ℝ)
163162recnd 10106 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (-π(,)π) → 𝑥 ∈ ℂ)
164158, 163fmpti 6423 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ
165164a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ)
166165limcdif 23685 . . . . . . . . . . . . . . . . . . 19 (⊤ → ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0) = (((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) lim 0))
167166trud 1533 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0) = (((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) lim 0)
168 resmpt 5484 . . . . . . . . . . . . . . . . . . . 20 (((-π(,)π) ∖ {0}) ⊆ (-π(,)π) → ((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
16916, 168ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)
170169oveq1i 6700 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) lim 0) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) lim 0)
171167, 170eqtri 2673 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) lim 0)
172156, 161, 1713eltr3i 2742 . . . . . . . . . . . . . . . 16 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) lim 0)
173172a1i 11 . . . . . . . . . . . . . . 15 (⊤ → 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) lim 0))
174 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℂ ↦ 2) = (𝑥 ∈ ℂ ↦ 2)
175144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 ∈ ℂ → ℂ ⊆ ℂ)
176 2cnd 11131 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 ∈ ℂ → 2 ∈ ℂ)
177175, 176, 175constcncfg 40402 . . . . . . . . . . . . . . . . . . . . . . . 24 (2 ∈ ℂ → (𝑥 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
178102, 177mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → (𝑥 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
179 2cnd 11131 . . . . . . . . . . . . . . . . . . . . . . 23 ((⊤ ∧ 𝑥 ∈ (-π(,)π)) → 2 ∈ ℂ)
180174, 178, 143, 145, 179cncfmptssg 40401 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑥 ∈ (-π(,)π) ↦ 2) ∈ ((-π(,)π)–cn→ℂ))
181 sincn 24243 . . . . . . . . . . . . . . . . . . . . . . . 24 sin ∈ (ℂ–cn→ℂ)
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → sin ∈ (ℂ–cn→ℂ))
183 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℂ ↦ (𝑥 / 2)) = (𝑥 ∈ ℂ ↦ (𝑥 / 2))
184183divccncf 22756 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ (ℂ–cn→ℂ))
185102, 81, 184mp2an 708 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ (ℂ–cn→ℂ)
186185a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (⊤ → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ (ℂ–cn→ℂ))
187163adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⊤ ∧ 𝑥 ∈ (-π(,)π)) → 𝑥 ∈ ℂ)
188187halfcld 11315 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⊤ ∧ 𝑥 ∈ (-π(,)π)) → (𝑥 / 2) ∈ ℂ)
189183, 186, 143, 145, 188cncfmptssg 40401 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → (𝑥 ∈ (-π(,)π) ↦ (𝑥 / 2)) ∈ ((-π(,)π)–cn→ℂ))
190182, 189cncfmpt1f 22763 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑥 ∈ (-π(,)π) ↦ (sin‘(𝑥 / 2))) ∈ ((-π(,)π)–cn→ℂ))
191180, 190mulcncf 23261 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ∈ ((-π(,)π)–cn→ℂ))
192191trud 1533 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ∈ ((-π(,)π)–cn→ℂ)
193 cnlimc 23697 . . . . . . . . . . . . . . . . . . . . 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 220 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦))
196195simpri 477 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦)
197 fveq2 6229 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0))
198 oveq2 6698 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦) = ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0))
199197, 198eleq12d 2724 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 0 → (((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦) ↔ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)))
200199rspccva 3339 . . . . . . . . . . . . . . . . . 18 ((∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦) ∧ 0 ∈ (-π(,)π)) → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0))
201196, 44, 200mp2an 708 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)
202 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 0 → (𝑥 / 2) = (0 / 2))
203102, 81div0i 10797 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 / 2) = 0
204202, 203syl6eq 2701 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 0 → (𝑥 / 2) = 0)
205204fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 0 → (sin‘(𝑥 / 2)) = (sin‘0))
206 sin0 14923 . . . . . . . . . . . . . . . . . . . . . 22 (sin‘0) = 0
207205, 206syl6eq 2701 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 0 → (sin‘(𝑥 / 2)) = 0)
208207oveq2d 6706 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 0 → (2 · (sin‘(𝑥 / 2))) = (2 · 0))
209 2t0e0 11221 . . . . . . . . . . . . . . . . . . . 20 (2 · 0) = 0
210208, 209syl6eq 2701 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → (2 · (sin‘(𝑥 / 2))) = 0)
211 eqid 2651 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))
212210, 211, 159fvmpt 6321 . . . . . . . . . . . . . . . . . 18 (0 ∈ (-π(,)π) → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) = 0)
21344, 212ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) = 0
214 2cnd 11131 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (-π(,)π) → 2 ∈ ℂ)
215163halfcld 11315 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ (-π(,)π) → (𝑥 / 2) ∈ ℂ)
216215sincld 14904 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (-π(,)π) → (sin‘(𝑥 / 2)) ∈ ℂ)
217214, 216mulcld 10098 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (-π(,)π) → (2 · (sin‘(𝑥 / 2))) ∈ ℂ)
218211, 217fmpti 6423 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):(-π(,)π)⟶ℂ
219218a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):(-π(,)π)⟶ℂ)
220219limcdif 23685 . . . . . . . . . . . . . . . . . . 19 (⊤ → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0) = (((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) lim 0))
221220trud 1533 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0) = (((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) lim 0)
222 resmpt 5484 . . . . . . . . . . . . . . . . . . . 20 (((-π(,)π) ∖ {0}) ⊆ (-π(,)π) → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
22316, 222ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))
224223oveq1i 6700 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) lim 0) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)
225221, 224eqtri 2673 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)
226201, 213, 2253eltr3i 2742 . . . . . . . . . . . . . . . 16 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)
227226a1i 11 . . . . . . . . . . . . . . 15 (⊤ → 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0))
228 eqidd 2652 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
229 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑥 / 2) = (𝑦 / 2))
230229fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (sin‘(𝑥 / 2)) = (sin‘(𝑦 / 2)))
231230oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → (2 · (sin‘(𝑥 / 2))) = (2 · (sin‘(𝑦 / 2))))
232231adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑦) → (2 · (sin‘(𝑥 / 2))) = (2 · (sin‘(𝑦 / 2))))
233 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ ((-π(,)π) ∖ {0}))
23426a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ)
23519sseli 3632 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ ℝ)
236235rehalfcld 11317 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑦 / 2) ∈ ℝ)
237236resincld 14917 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑦 / 2)) ∈ ℝ)
238234, 237remulcld 10108 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (2 · (sin‘(𝑦 / 2))) ∈ ℝ)
239228, 232, 233, 238fvmptd 6327 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = (2 · (sin‘(𝑦 / 2))))
240 2cnd 11131 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℂ)
241237recnd 10106 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑦 / 2)) ∈ ℂ)
24281a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 2 ≠ 0)
243 ioossicc 12297 . . . . . . . . . . . . . . . . . . . . . . 23 (-π(,)π) ⊆ (-π[,]π)
244 eldifi 3765 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ (-π(,)π))
245243, 244sseldi 3634 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ (-π[,]π))
246 eldifsni 4353 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ≠ 0)
247 fourierdlem44 40686 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ (-π[,]π) ∧ 𝑦 ≠ 0) → (sin‘(𝑦 / 2)) ≠ 0)
248245, 246, 247syl2anc 694 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑦 / 2)) ≠ 0)
249240, 241, 242, 248mulne0d 10717 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (2 · (sin‘(𝑦 / 2))) ≠ 0)
250239, 249eqnetrd 2890 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ≠ 0)
251250neneqd 2828 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ¬ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0)
252251nrex 3029 . . . . . . . . . . . . . . . . 17 ¬ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0
25325fnmpt 6058 . . . . . . . . . . . . . . . . . . 19 (∀𝑥 ∈ ((-π(,)π) ∖ {0})(2 · (sin‘(𝑥 / 2))) ∈ ℝ → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) Fn ((-π(,)π) ∖ {0}))
254253, 30mprg 2955 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) Fn ((-π(,)π) ∖ {0})
255 ssid 3657 . . . . . . . . . . . . . . . . . 18 ((-π(,)π) ∖ {0}) ⊆ ((-π(,)π) ∖ {0})
256 fvelimab 6292 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) Fn ((-π(,)π) ∖ {0}) ∧ ((-π(,)π) ∖ {0}) ⊆ ((-π(,)π) ∖ {0})) → (0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) “ ((-π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0))
257254, 255, 256mp2an 708 . . . . . . . . . . . . . . . . 17 (0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) “ ((-π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0)
258252, 257mtbir 312 . . . . . . . . . . . . . . . 16 ¬ 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) “ ((-π(,)π) ∖ {0}))
259258a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ¬ 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) “ ((-π(,)π) ∖ {0})))
260 eqidd 2652 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))))
261229fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (cos‘(𝑥 / 2)) = (cos‘(𝑦 / 2)))
262261adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑦) → (cos‘(𝑥 / 2)) = (cos‘(𝑦 / 2)))
263235recnd 10106 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ ℂ)
264263halfcld 11315 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑦 / 2) ∈ ℂ)
265264coscld 14905 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑦 / 2)) ∈ ℂ)
266260, 262, 233, 265fvmptd 6327 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = (cos‘(𝑦 / 2)))
267236rered 14008 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (ℜ‘(𝑦 / 2)) = (𝑦 / 2))
268 halfpire 24261 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π / 2) ∈ ℝ
269268renegcli 10380 . . . . . . . . . . . . . . . . . . . . . . . . . 26 -(π / 2) ∈ ℝ
270269a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ)
271270rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ*)
272268a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (π / 2) ∈ ℝ)
273272rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (π / 2) ∈ ℝ*)
274 picn 24256 . . . . . . . . . . . . . . . . . . . . . . . . . 26 π ∈ ℂ
275 divneg 10757 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(π / 2) = (-π / 2))
276274, 102, 81, 275mp3an 1464 . . . . . . . . . . . . . . . . . . . . . . . . 25 -(π / 2) = (-π / 2)
27739a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -π ∈ ℝ)
278 2rp 11875 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ∈ ℝ+
279278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ+)
28040a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -π ∈ ℝ*)
28141a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ((-π(,)π) ∖ {0}) → π ∈ ℝ*)
282 ioogtlb 40035 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝑦 ∈ (-π(,)π)) → -π < 𝑦)
283280, 281, 244, 282syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -π < 𝑦)
284277, 235, 279, 283ltdiv1dd 11967 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (-π / 2) < (𝑦 / 2))
285276, 284syl5eqbr 4720 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) < (𝑦 / 2))
28638a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → π ∈ ℝ)
287 iooltub 40053 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝑦 ∈ (-π(,)π)) → 𝑦 < π)
288280, 281, 244, 287syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 < π)
289235, 286, 279, 288ltdiv1dd 11967 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑦 / 2) < (π / 2))
290271, 273, 236, 285, 289eliood 40038 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑦 / 2) ∈ (-(π / 2)(,)(π / 2)))
291267, 290eqeltrd 2730 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (ℜ‘(𝑦 / 2)) ∈ (-(π / 2)(,)(π / 2)))
292 cosne0 24321 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 / 2) ∈ ℂ ∧ (ℜ‘(𝑦 / 2)) ∈ (-(π / 2)(,)(π / 2))) → (cos‘(𝑦 / 2)) ≠ 0)
293264, 291, 292syl2anc 694 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑦 / 2)) ≠ 0)
294266, 293eqnetrd 2890 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) ≠ 0)
295294neneqd 2828 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ¬ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0)
296295nrex 3029 . . . . . . . . . . . . . . . . . 18 ¬ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0
29772, 73fnmpti 6060 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) Fn ((-π(,)π) ∖ {0})
298 fvelimab 6292 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) Fn ((-π(,)π) ∖ {0}) ∧ ((-π(,)π) ∖ {0}) ⊆ ((-π(,)π) ∖ {0})) → (0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0))
299297, 255, 298mp2an 708 . . . . . . . . . . . . . . . . . 18 (0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0)
300296, 299mtbir 312 . . . . . . . . . . . . . . . . 17 ¬ 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0}))
301135imaeq1i 5498 . . . . . . . . . . . . . . . . . 18 ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) “ ((-π(,)π) ∖ {0})) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0}))
302301eleq2i 2722 . . . . . . . . . . . . . . . . 17 (0 ∈ ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) “ ((-π(,)π) ∖ {0})) ↔ 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0})))
303300, 302mtbir 312 . . . . . . . . . . . . . . . 16 ¬ 0 ∈ ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) “ ((-π(,)π) ∖ {0}))
304303a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ¬ 0 ∈ ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) “ ((-π(,)π) ∖ {0})))
305 eqid 2651 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑠 / 2))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑠 / 2)))
306 eqid 2651 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2))))
30719sseli 3632 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 ∈ ℝ)
308307recnd 10106 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 ∈ ℂ)
309308halfcld 11315 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑠 / 2) ∈ ℂ)
310309coscld 14905 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ∈ ℂ)
311307rehalfcld 11317 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑠 / 2) ∈ ℝ)
312311rered 14008 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (ℜ‘(𝑠 / 2)) = (𝑠 / 2))
313269a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ)
314313rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ*)
315268a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (π / 2) ∈ ℝ)
316315rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (π / 2) ∈ ℝ*)
31738a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ((-π(,)π) ∖ {0}) → π ∈ ℝ)
318317renegcld 10495 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -π ∈ ℝ)
319278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ+)
32040a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -π ∈ ℝ*)
32141a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ((-π(,)π) ∖ {0}) → π ∈ ℝ*)
322 eldifi 3765 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 ∈ (-π(,)π))
323 ioogtlb 40035 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝑠 ∈ (-π(,)π)) → -π < 𝑠)
324320, 321, 322, 323syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -π < 𝑠)
325318, 307, 319, 324ltdiv1dd 11967 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (-π / 2) < (𝑠 / 2))
326276, 325syl5eqbr 4720 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) < (𝑠 / 2))
327 iooltub 40053 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝑠 ∈ (-π(,)π)) → 𝑠 < π)
328320, 321, 322, 327syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 < π)
329307, 317, 319, 328ltdiv1dd 11967 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑠 / 2) < (π / 2))
330314, 316, 311, 326, 329eliood 40038 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑠 / 2) ∈ (-(π / 2)(,)(π / 2)))
331312, 330eqeltrd 2730 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (ℜ‘(𝑠 / 2)) ∈ (-(π / 2)(,)(π / 2)))
332 cosne0 24321 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 / 2) ∈ ℂ ∧ (ℜ‘(𝑠 / 2)) ∈ (-(π / 2)(,)(π / 2))) → (cos‘(𝑠 / 2)) ≠ 0)
333309, 331, 332syl2anc 694 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ≠ 0)
334333neneqd 2828 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ¬ (cos‘(𝑠 / 2)) = 0)
335311recoscld 14918 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ∈ ℝ)
336 elsng 4224 . . . . . . . . . . . . . . . . . . . . 21 ((cos‘(𝑠 / 2)) ∈ ℝ → ((cos‘(𝑠 / 2)) ∈ {0} ↔ (cos‘(𝑠 / 2)) = 0))
337335, 336syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((cos‘(𝑠 / 2)) ∈ {0} ↔ (cos‘(𝑠 / 2)) = 0))
338334, 337mtbird 314 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ¬ (cos‘(𝑠 / 2)) ∈ {0})
339310, 338eldifd 3618 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ∈ (ℂ ∖ {0}))
340339adantl 481 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑠 ∈ ((-π(,)π) ∖ {0})) → (cos‘(𝑠 / 2)) ∈ (ℂ ∖ {0}))
341309ad2antrl 764 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ (𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ (𝑠 / 2) ≠ 0)) → (𝑠 / 2) ∈ ℂ)
342 cosf 14899 . . . . . . . . . . . . . . . . . . . 20 cos:ℂ⟶ℂ
343342a1i 11 . . . . . . . . . . . . . . . . . . 19 (⊤ → cos:ℂ⟶ℂ)
344343ffvelrnda 6399 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ ℂ) → (cos‘𝑥) ∈ ℂ)
345 eqid 2651 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ℂ ↦ (𝑠 / 2)) = (𝑠 ∈ ℂ ↦ (𝑠 / 2))
346345divccncf 22756 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑠 ∈ ℂ ↦ (𝑠 / 2)) ∈ (ℂ–cn→ℂ))
347102, 81, 346mp2an 708 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ℂ ↦ (𝑠 / 2)) ∈ (ℂ–cn→ℂ)
348347a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑠 ∈ ℂ ↦ (𝑠 / 2)) ∈ (ℂ–cn→ℂ))
349141adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑠 ∈ (-π(,)π)) → 𝑠 ∈ ℂ)
350349halfcld 11315 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑠 ∈ (-π(,)π)) → (𝑠 / 2) ∈ ℂ)
351345, 348, 143, 145, 350cncfmptssg 40401 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ∈ ((-π(,)π)–cn→ℂ))
352 oveq1 6697 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 0 → (𝑠 / 2) = (0 / 2))
353352, 203syl6eq 2701 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → (𝑠 / 2) = 0)
354351, 45, 353cnmptlimc 23699 . . . . . . . . . . . . . . . . . . 19 (⊤ → 0 ∈ ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) lim 0))
355 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) = (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2))
356141halfcld 11315 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (-π(,)π) → (𝑠 / 2) ∈ ℂ)
357355, 356fmpti 6423 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)):(-π(,)π)⟶ℂ
358357a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)):(-π(,)π)⟶ℂ)
359358limcdif 23685 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) lim 0) = (((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) lim 0))
360359trud 1533 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) lim 0) = (((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) lim 0)
361 resmpt 5484 . . . . . . . . . . . . . . . . . . . . . 22 (((-π(,)π) ∖ {0}) ⊆ (-π(,)π) → ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2)))
36216, 361ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2))
363362oveq1i 6700 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2)) lim 0)
364360, 363eqtri 2673 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2)) lim 0)
365354, 364syl6eleq 2740 . . . . . . . . . . . . . . . . . 18 (⊤ → 0 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2)) lim 0))
366 ffn 6083 . . . . . . . . . . . . . . . . . . . . . . 23 (cos:ℂ⟶ℂ → cos Fn ℂ)
367342, 366ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 cos Fn ℂ
368 dffn5 6280 . . . . . . . . . . . . . . . . . . . . . 22 (cos Fn ℂ ↔ cos = (𝑥 ∈ ℂ ↦ (cos‘𝑥)))
369367, 368mpbi 220 . . . . . . . . . . . . . . . . . . . . 21 cos = (𝑥 ∈ ℂ ↦ (cos‘𝑥))
370 coscn 24244 . . . . . . . . . . . . . . . . . . . . 21 cos ∈ (ℂ–cn→ℂ)
371369, 370eqeltrri 2727 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℂ ↦ (cos‘𝑥)) ∈ (ℂ–cn→ℂ)
372371a1i 11 . . . . . . . . . . . . . . . . . . 19 (⊤ → (𝑥 ∈ ℂ ↦ (cos‘𝑥)) ∈ (ℂ–cn→ℂ))
373 0cnd 10071 . . . . . . . . . . . . . . . . . . 19 (⊤ → 0 ∈ ℂ)
374 fveq2 6229 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 0 → (cos‘𝑥) = (cos‘0))
375 cos0 14924 . . . . . . . . . . . . . . . . . . . 20 (cos‘0) = 1
376374, 375syl6eq 2701 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → (cos‘𝑥) = 1)
377372, 373, 376cnmptlimc 23699 . . . . . . . . . . . . . . . . . 18 (⊤ → 1 ∈ ((𝑥 ∈ ℂ ↦ (cos‘𝑥)) lim 0))
378 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑠 / 2) → (cos‘𝑥) = (cos‘(𝑠 / 2)))
379 fveq2 6229 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 / 2) = 0 → (cos‘(𝑠 / 2)) = (cos‘0))
380379, 375syl6eq 2701 . . . . . . . . . . . . . . . . . . 19 ((𝑠 / 2) = 0 → (cos‘(𝑠 / 2)) = 1)
381380ad2antll 765 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ (𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ (𝑠 / 2) = 0)) → (cos‘(𝑠 / 2)) = 1)
382341, 344, 365, 377, 378, 381limcco 23702 . . . . . . . . . . . . . . . . 17 (⊤ → 1 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑠 / 2))) lim 0))
383 ax-1ne0 10043 . . . . . . . . . . . . . . . . . 18 1 ≠ 0
384383a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → 1 ≠ 0)
385305, 306, 340, 382, 384reclimc 40203 . . . . . . . . . . . . . . . 16 (⊤ → (1 / 1) ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) lim 0))
386 1div1e1 10755 . . . . . . . . . . . . . . . 16 (1 / 1) = 1
38766fveq1i 6230 . . . . . . . . . . . . . . . . . . . 20 ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1)‘𝑠)
388 eqidd 2652 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1))
389 eqidd 2652 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → 1 = 1)
390 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 ∈ ((-π(,)π) ∖ {0}))
391 1red 10093 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 1 ∈ ℝ)
392388, 389, 390, 391fvmptd 6327 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1)‘𝑠) = 1)
393387, 392syl5req 2698 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 1 = ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠))
394135a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))))
395 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑠 → (𝑥 / 2) = (𝑠 / 2))
396395fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑠 → (cos‘(𝑥 / 2)) = (cos‘(𝑠 / 2)))
397396adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (cos‘(𝑥 / 2)) = (cos‘(𝑠 / 2)))
398394, 397, 390, 335fvmptd 6327 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠) = (cos‘(𝑠 / 2)))
399398eqcomd 2657 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) = ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠))
400393, 399oveq12d 6708 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (1 / (cos‘(𝑠 / 2))) = (((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) / ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠)))
401400mpteq2ia 4773 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) / ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠)))
402401oveq1i 6700 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) / ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠))) lim 0)
403385, 386, 4023eltr3g 2746 . . . . . . . . . . . . . . 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 23824 . . . . . . . . . . . . . 14 (⊤ → 1 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) lim 0))
405404trud 1533 . . . . . . . . . . . . 13 1 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) lim 0)
406 eqidd 2652 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
407 simpr 476 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → 𝑥 = 𝑠)
408406, 407, 390, 307fvmptd 6327 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) = 𝑠)
409 eqidd 2652 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
410407oveq1d 6705 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (𝑥 / 2) = (𝑠 / 2))
411410fveq2d 6233 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (sin‘(𝑥 / 2)) = (sin‘(𝑠 / 2)))
412411oveq2d 6706 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (2 · (sin‘(𝑥 / 2))) = (2 · (sin‘(𝑠 / 2))))
41326a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ)
414311resincld 14917 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑠 / 2)) ∈ ℝ)
415413, 414remulcld 10108 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
416409, 412, 390, 415fvmptd 6327 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠) = (2 · (sin‘(𝑠 / 2))))
417408, 416oveq12d 6708 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠)) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
418417mpteq2ia 4773 . . . . . . . . . . . . . 14 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
419418oveq1i 6700 . . . . . . . . . . . . 13 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim 0)
420405, 419eleqtri 2728 . . . . . . . . . . . 12 1 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim 0)
42110oveq1i 6700 . . . . . . . . . . . . . 14 (𝐾 lim 0) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0)
42210feq1i 6074 . . . . . . . . . . . . . . . . . . 19 (𝐾:(-π[,]π)⟶ℂ ↔ (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π[,]π)⟶ℂ)
42314, 422mpbi 220 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π[,]π)⟶ℂ
424423a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π[,]π)⟶ℂ)
425243a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → (-π(,)π) ⊆ (-π[,]π))
426 iccssre 12293 . . . . . . . . . . . . . . . . . . . 20 ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
42739, 38, 426mp2an 708 . . . . . . . . . . . . . . . . . . 19 (-π[,]π) ⊆ ℝ
428427a1i 11 . . . . . . . . . . . . . . . . . 18 (⊤ → (-π[,]π) ⊆ ℝ)
429428, 12syl6ss 3648 . . . . . . . . . . . . . . . . 17 (⊤ → (-π[,]π) ⊆ ℂ)
430 eqid 2651 . . . . . . . . . . . . . . . . 17 ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})) = ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0}))
43139, 35, 36ltleii 10198 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -π ≤ 0
43235, 38, 37ltleii 10198 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ≤ π
43339, 38elicc2i 12277 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (0 ∈ (-π[,]π) ↔ (0 ∈ ℝ ∧ -π ≤ 0 ∧ 0 ≤ π))
43435, 431, 432, 433mpbir3an 1263 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ∈ (-π[,]π)
435159snss 4348 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 ∈ (-π[,]π) ↔ {0} ⊆ (-π[,]π))
436434, 435mpbi 220 . . . . . . . . . . . . . . . . . . . . . . . . 25 {0} ⊆ (-π[,]π)
437 ssequn2 3819 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({0} ⊆ (-π[,]π) ↔ ((-π[,]π) ∪ {0}) = (-π[,]π))
438436, 437mpbi 220 . . . . . . . . . . . . . . . . . . . . . . . 24 ((-π[,]π) ∪ {0}) = (-π[,]π)
439438oveq2i 6701 . . . . . . . . . . . . . . . . . . . . . . 23 ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})) = ((TopOpen‘ℂfld) ↾t (-π[,]π))
440 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . . 25 (topGen‘ran (,)) = (topGen‘ran (,))
44156, 440tgiooss 40051 . . . . . . . . . . . . . . . . . . . . . . . 24 ((-π[,]π) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (-π[,]π)) = ((topGen‘ran (,)) ↾t (-π[,]π)))
442427, 441ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((TopOpen‘ℂfld) ↾t (-π[,]π)) = ((topGen‘ran (,)) ↾t (-π[,]π))
443439, 442eqtri 2673 . . . . . . . . . . . . . . . . . . . . . 22 ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})) = ((topGen‘ran (,)) ↾t (-π[,]π))
444443fveq2i 6232 . . . . . . . . . . . . . . . . . . . . 21 (int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0}))) = (int‘((topGen‘ran (,)) ↾t (-π[,]π)))
445159snss 4348 . . . . . . . . . . . . . . . . . . . . . . 23 (0 ∈ (-π(,)π) ↔ {0} ⊆ (-π(,)π))
44644, 445mpbi 220 . . . . . . . . . . . . . . . . . . . . . 22 {0} ⊆ (-π(,)π)
447 ssequn2 3819 . . . . . . . . . . . . . . . . . . . . . 22 ({0} ⊆ (-π(,)π) ↔ ((-π(,)π) ∪ {0}) = (-π(,)π))
448446, 447mpbi 220 . . . . . . . . . . . . . . . . . . . . 21 ((-π(,)π) ∪ {0}) = (-π(,)π)
449444, 448fveq12i 6234 . . . . . . . . . . . . . . . . . . . 20 ((int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})))‘((-π(,)π) ∪ {0})) = ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘(-π(,)π))
450 resttopon 21013 . . . . . . . . . . . . . . . . . . . . . . 23 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (-π[,]π) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (-π[,]π)) ∈ (TopOn‘(-π[,]π)))
45160, 427, 450mp2an 708 . . . . . . . . . . . . . . . . . . . . . 22 ((topGen‘ran (,)) ↾t (-π[,]π)) ∈ (TopOn‘(-π[,]π))
452451topontopi 20768 . . . . . . . . . . . . . . . . . . . . 21 ((topGen‘ran (,)) ↾t (-π[,]π)) ∈ Top
453 retop 22612 . . . . . . . . . . . . . . . . . . . . . . . 24 (topGen‘ran (,)) ∈ Top
454 ovex 6718 . . . . . . . . . . . . . . . . . . . . . . . 24 (-π[,]π) ∈ V
455453, 454pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . . 23 ((topGen‘ran (,)) ∈ Top ∧ (-π[,]π) ∈ V)
456 ssid 3657 . . . . . . . . . . . . . . . . . . . . . . . 24 (-π(,)π) ⊆ (-π(,)π)
45733, 243, 4563pm3.2i 1259 . . . . . . . . . . . . . . . . . . . . . . 23 ((-π(,)π) ∈ (topGen‘ran (,)) ∧ (-π(,)π) ⊆ (-π[,]π) ∧ (-π(,)π) ⊆ (-π(,)π))
458 restopnb 21027 . . . . . . . . . . . . . . . . . . . . . . 23 ((((topGen‘ran (,)) ∈ Top ∧ (-π[,]π) ∈ V) ∧ ((-π(,)π) ∈ (topGen‘ran (,)) ∧ (-π(,)π) ⊆ (-π[,]π) ∧ (-π(,)π) ⊆ (-π(,)π))) → ((-π(,)π) ∈ (topGen‘ran (,)) ↔ (-π(,)π) ∈ ((topGen‘ran (,)) ↾t (-π[,]π))))
459455, 457, 458mp2an 708 . . . . . . . . . . . . . . . . . . . . . 22 ((-π(,)π) ∈ (topGen‘ran (,)) ↔ (-π(,)π) ∈ ((topGen‘ran (,)) ↾t (-π[,]π)))
46033, 459mpbi 220 . . . . . . . . . . . . . . . . . . . . 21 (-π(,)π) ∈ ((topGen‘ran (,)) ↾t (-π[,]π))
461 isopn3i 20934 . . . . . . . . . . . . . . . . . . . . 21 ((((topGen‘ran (,)) ↾t (-π[,]π)) ∈ Top ∧ (-π(,)π) ∈ ((topGen‘ran (,)) ↾t (-π[,]π))) → ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘(-π(,)π)) = (-π(,)π))
462452, 460, 461mp2an 708 . . . . . . . . . . . . . . . . . . . 20 ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘(-π(,)π)) = (-π(,)π)
463 eqid 2651 . . . . . . . . . . . . . . . . . . . 20 (-π(,)π) = (-π(,)π)
464449, 462, 4633eqtrri 2678 . . . . . . . . . . . . . . . . . . 19 (-π(,)π) = ((int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})))‘((-π(,)π) ∪ {0}))
46544, 464eleqtri 2728 . . . . . . . . . . . . . . . . . 18 0 ∈ ((int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})))‘((-π(,)π) ∪ {0}))
466465a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → 0 ∈ ((int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})))‘((-π(,)π) ∪ {0})))
467424, 425, 429, 56, 430, 466limcres 23695 . . . . . . . . . . . . . . . 16 (⊤ → (((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (-π(,)π)) lim 0) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0))
468467trud 1533 . . . . . . . . . . . . . . 15 (((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (-π(,)π)) lim 0) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0)
469468eqcomi 2660 . . . . . . . . . . . . . 14 ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0) = (((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (-π(,)π)) lim 0)
470 resmpt 5484 . . . . . . . . . . . . . . . 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 6700 . . . . . . . . . . . . . 14 (((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (-π(,)π)) lim 0) = ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0)
473421, 469, 4723eqtri 2677 . . . . . . . . . . . . 13 (𝐾 lim 0) = ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0)
474 eqid 2651 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
475 iftrue 4125 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = 1)
476 1cnd 10094 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → 1 ∈ ℂ)
477475, 476eqeltrd 2730 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 0 → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
478477adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (-π(,)π) ∧ 𝑠 = 0) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
479 iffalse 4128 . . . . . . . . . . . . . . . . . . . 20 𝑠 = 0 → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
480479adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
481141adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ℂ)
482 2cnd 11131 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → 2 ∈ ℂ)
483481halfcld 11315 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (𝑠 / 2) ∈ ℂ)
484483sincld 14904 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (sin‘(𝑠 / 2)) ∈ ℂ)
485482, 484mulcld 10098 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
48681a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → 2 ≠ 0)
487243sseli 3632 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ (-π(,)π) → 𝑠 ∈ (-π[,]π))
488 neqne 2831 . . . . . . . . . . . . . . . . . . . . . 22 𝑠 = 0 → 𝑠 ≠ 0)
489 fourierdlem44 40686 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
490487, 488, 489syl2an 493 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (sin‘(𝑠 / 2)) ≠ 0)
491482, 484, 486, 490mulne0d 10717 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
492481, 485, 491divcld 10839 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
493480, 492eqeltrd 2730 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
494478, 493pm2.61dan 849 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (-π(,)π) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
495474, 494fmpti 6423 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π(,)π)⟶ℂ
496495a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π(,)π)⟶ℂ)
497496limcdif 23685 . . . . . . . . . . . . . 14 (⊤ → ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0) = (((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π(,)π) ∖ {0})) lim 0))
498497trud 1533 . . . . . . . . . . . . 13 ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0) = (((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π(,)π) ∖ {0})) lim 0)
499 resmpt 5484 . . . . . . . . . . . . . . . 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 3766 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ¬ 𝑠 ∈ {0})
502 velsn 4226 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ {0} ↔ 𝑠 = 0)
503501, 502sylnib 317 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ¬ 𝑠 = 0)
504503, 479syl 17 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((-π(,)π) ∖ {0}) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
505504mpteq2ia 4773 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
506500, 505eqtri 2673 . . . . . . . . . . . . . 14 ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π(,)π) ∖ {0})) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
507506oveq1i 6700 . . . . . . . . . . . . 13 (((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π(,)π) ∖ {0})) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim 0)
508473, 498, 5073eqtrri 2678 . . . . . . . . . . . 12 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim 0) = (𝐾 lim 0)
509420, 508eleqtri 2728 . . . . . . . . . . 11 1 ∈ (𝐾 lim 0)
510509a1i 11 . . . . . . . . . 10 (𝑠 = 0 → 1 ∈ (𝐾 lim 0))
511 fveq2 6229 . . . . . . . . . . 11 (𝑠 = 0 → (𝐾𝑠) = (𝐾‘0))
512475, 10, 47fvmpt 6321 . . . . . . . . . . . 12 (0 ∈ (-π[,]π) → (𝐾‘0) = 1)
513434, 512ax-mp 5 . . . . . . . . . . 11 (𝐾‘0) = 1
514511, 513syl6eq 2701 . . . . . . . . . 10 (𝑠 = 0 → (𝐾𝑠) = 1)
515 oveq2 6698 . . . . . . . . . 10 (𝑠 = 0 → (𝐾 lim 𝑠) = (𝐾 lim 0))
516510, 514, 5153eltr4d 2745 . . . . . . . . 9 (𝑠 = 0 → (𝐾𝑠) ∈ (𝐾 lim 𝑠))
517427, 12sstri 3645 . . . . . . . . . . 11 (-π[,]π) ⊆ ℂ
518517a1i 11 . . . . . . . . . 10 (𝑠 = 0 → (-π[,]π) ⊆ ℂ)
51938a1i 11 . . . . . . . . . . . 12 (𝑠 = 0 → π ∈ ℝ)
520519renegcld 10495 . . . . . . . . . . 11 (𝑠 = 0 → -π ∈ ℝ)
521 id 22 . . . . . . . . . . . 12 (𝑠 = 0 → 𝑠 = 0)
52235a1i 11 . . . . . . . . . . . 12 (𝑠 = 0 → 0 ∈ ℝ)
523521, 522eqeltrd 2730 . . . . . . . . . . 11 (𝑠 = 0 → 𝑠 ∈ ℝ)
524431, 521syl5breqr 4723 . . . . . . . . . . 11 (𝑠 = 0 → -π ≤ 𝑠)
525521, 432syl6eqbr 4724 . . . . . . . . . . 11 (𝑠 = 0 → 𝑠 ≤ π)
526520, 519, 523, 524, 525eliccd 40044 . . . . . . . . . 10 (𝑠 = 0 → 𝑠 ∈ (-π[,]π))
52757oveq1i 6700 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t (-π[,]π)) = (((TopOpen‘ℂfld) ↾t ℝ) ↾t (-π[,]π))
52856cnfldtop 22634 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) ∈ Top
529 reex 10065 . . . . . . . . . . . . 13 ℝ ∈ V
530 restabs 21017 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ∈ Top ∧ (-π[,]π) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂfld) ↾t ℝ) ↾t (-π[,]π)) = ((TopOpen‘ℂfld) ↾t (-π[,]π)))
531528, 427, 529, 530mp3an 1464 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ↾t ℝ) ↾t (-π[,]π)) = ((TopOpen‘ℂfld) ↾t (-π[,]π))
532527, 531eqtri 2673 . . . . . . . . . . 11 ((topGen‘ran (,)) ↾t (-π[,]π)) = ((TopOpen‘ℂfld) ↾t (-π[,]π))
53356, 532cnplimc 23696 . . . . . . . . . 10 (((-π[,]π) ⊆ ℂ ∧ 𝑠 ∈ (-π[,]π)) → (𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠) ↔ (𝐾:(-π[,]π)⟶ℂ ∧ (𝐾𝑠) ∈ (𝐾 lim 𝑠))))
534518, 526, 533syl2anc 694 . . . . . . . . 9 (𝑠 = 0 → (𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠) ↔ (𝐾:(-π[,]π)⟶ℂ ∧ (𝐾𝑠) ∈ (𝐾 lim 𝑠))))
53515, 516, 534mpbir2and 977 . . . . . . . 8 (𝑠 = 0 → 𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))
536535adantl 481 . . . . . . 7 ((𝑠 ∈ (-π[,]π) ∧ 𝑠 = 0) → 𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))
537 simpl 472 . . . . . . . . . . 11 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ (-π[,]π))
538502notbii 309 . . . . . . . . . . . . 13 𝑠 ∈ {0} ↔ ¬ 𝑠 = 0)
539538biimpri 218 . . . . . . . . . . . 12 𝑠 = 0 → ¬ 𝑠 ∈ {0})
540539adantl 481 . . . . . . . . . . 11 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → ¬ 𝑠 ∈ {0})
541537, 540eldifd 3618 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ((-π[,]π) ∖ {0}))
542 fveq2 6229 . . . . . . . . . . . 12 (𝑥 = 𝑠 → ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥) = ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠))
543542eleq2d 2716 . . . . . . . . . . 11 (𝑥 = 𝑠 → ((𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥) ↔ (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠)))
544429ssdifssd 3781 . . . . . . . . . . . . . . . . 17 (⊤ → ((-π[,]π) ∖ {0}) ⊆ ℂ)
545544, 145idcncfg 40403 . . . . . . . . . . . . . . . 16 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ 𝑠) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
546 eqid 2651 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2))))
547 2cnd 11131 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 2 ∈ ℂ)
548 eldifi 3765 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 𝑠 ∈ (-π[,]π))
549517, 548sseldi 3634 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 𝑠 ∈ ℂ)
550549halfcld 11315 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (𝑠 / 2) ∈ ℂ)
551550sincld 14904 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (sin‘(𝑠 / 2)) ∈ ℂ)
552547, 551mulcld 10098 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
55381a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 2 ≠ 0)
554 eldifsni 4353 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 𝑠 ≠ 0)
555548, 554, 489syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (sin‘(𝑠 / 2)) ≠ 0)
556547, 551, 553, 555mulne0d 10717 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
557556neneqd 2828 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π[,]π) ∖ {0}) → ¬ (2 · (sin‘(𝑠 / 2))) = 0)
558 elsng 4224 . . . . . . . . . . . . . . . . . . . . . 22 ((2 · (sin‘(𝑠 / 2))) ∈ ℂ → ((2 · (sin‘(𝑠 / 2))) ∈ {0} ↔ (2 · (sin‘(𝑠 / 2))) = 0))
559552, 558syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π[,]π) ∖ {0}) → ((2 · (sin‘(𝑠 / 2))) ∈ {0} ↔ (2 · (sin‘(𝑠 / 2))) = 0))
560557, 559mtbird 314 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π[,]π) ∖ {0}) → ¬ (2 · (sin‘(𝑠 / 2))) ∈ {0})
561552, 560eldifd 3618 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
562546, 561fmpti 6423 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))):((-π[,]π) ∖ {0})⟶(ℂ ∖ {0})
563 difss 3770 . . . . . . . . . . . . . . . . . . 19 (ℂ ∖ {0}) ⊆ ℂ
564 eqid 2651 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ℂ ↦ 2) = (𝑠 ∈ ℂ ↦ 2)
565175, 176, 175constcncfg 40402 . . . . . . . . . . . . . . . . . . . . . . 23 (2 ∈ ℂ → (𝑠 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
566102, 565mp1i 13 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑠 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
567 2cnd 11131 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑠 ∈ ((-π[,]π) ∖ {0})) → 2 ∈ ℂ)
568564, 566, 544, 145, 567cncfmptssg 40401 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ 2) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
569549, 547, 553divrecd 10842 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (𝑠 / 2) = (𝑠 · (1 / 2)))
570569mpteq2ia 4773 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / 2)) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 · (1 / 2)))
571 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ℂ ↦ (1 / 2)) = (𝑠 ∈ ℂ ↦ (1 / 2))
572144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 / 2) ∈ ℂ → ℂ ⊆ ℂ)
573 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 / 2) ∈ ℂ → (1 / 2) ∈ ℂ)
574572, 573, 572constcncfg 40402 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 / 2) ∈ ℂ → (𝑠 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
57594, 574mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⊤ → (𝑠 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
57694a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⊤ ∧ 𝑠 ∈ ((-π[,]π) ∖ {0})) → (1 / 2) ∈ ℂ)
577571, 575, 544, 145, 576cncfmptssg 40401 . . . . . . . . . . . . . . . . . . . . . . . 24 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (1 / 2)) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
578545, 577mulcncf 23261 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 · (1 / 2))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
579570, 578syl5eqel 2734 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / 2)) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
580182, 579cncfmpt1f 22763 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (sin‘(𝑠 / 2))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
581568, 580mulcncf 23261 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
582581trud 1533 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ)
583 cncffvrn 22748 . . . . . . . . . . . . . . . . . . 19 (((ℂ ∖ {0}) ⊆ ℂ ∧ (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ)) → ((𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))):((-π[,]π) ∖ {0})⟶(ℂ ∖ {0})))
584563, 582, 583mp2an 708 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))):((-π[,]π) ∖ {0})⟶(ℂ ∖ {0}))
585562, 584mpbir 221 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→(ℂ ∖ {0}))
586585a1i 11 . . . . . . . . . . . . . . . 16 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→(ℂ ∖ {0})))
587545, 586divcncf 23262 . . . . . . . . . . . . . . 15 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
588587trud 1533 . . . . . . . . . . . . . 14 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ)
589428ssdifssd 3781 . . . . . . . . . . . . . . . . 17 (⊤ → ((-π[,]π) ∖ {0}) ⊆ ℝ)
590589trud 1533 . . . . . . . . . . . . . . . 16 ((-π[,]π) ∖ {0}) ⊆ ℝ
591590, 12sstri 3645 . . . . . . . . . . . . . . 15 ((-π[,]π) ∖ {0}) ⊆ ℂ
59257oveq1i 6700 . . . . . . . . . . . . . . . . 17 ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) = (((TopOpen‘ℂfld) ↾t ℝ) ↾t ((-π[,]π) ∖ {0}))
593 restabs 21017 . . . . . . . . . . . . . . . . . 18 (((TopOpen‘ℂfld) ∈ Top ∧ ((-π[,]π) ∖ {0}) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂfld) ↾t ℝ) ↾t ((-π[,]π) ∖ {0})) = ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∖ {0})))
594528, 590, 529, 593mp3an 1464 . . . . . . . . . . . . . . . . 17 (((TopOpen‘ℂfld) ↾t ℝ) ↾t ((-π[,]π) ∖ {0})) = ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∖ {0}))
595592, 594eqtri 2673 . . . . . . . . . . . . . . . 16 ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) = ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∖ {0}))
596 unicntop 22636 . . . . . . . . . . . . . . . . . . 19 ℂ = (TopOpen‘ℂfld)
597596restid 16141 . . . . . . . . . . . . . . . . . 18 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
598528, 597ax-mp 5 . . . . . . . . . . . . . . . . 17 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
599598eqcomi 2660 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
60056, 595, 599cncfcn 22759 . . . . . . . . . . . . . . 15 ((((-π[,]π) ∖ {0}) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (((-π[,]π) ∖ {0})–cn→ℂ) = (((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) Cn (TopOpen‘ℂfld)))
601591, 144, 600mp2an 708 . . . . . . . . . . . . . 14 (((-π[,]π) ∖ {0})–cn→ℂ) = (((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) Cn (TopOpen‘ℂfld))
602588, 601eleqtri 2728 . . . . . . . . . . . . 13 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) Cn (TopOpen‘ℂfld))
603 resttopon 21013 . . . . . . . . . . . . . . 15 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((-π[,]π) ∖ {0}) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) ∈ (TopOn‘((-π[,]π) ∖ {0})))
60460, 590, 603mp2an 708 . . . . . . . . . . . . . 14 ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) ∈ (TopOn‘((-π[,]π) ∖ {0}))
60556cnfldtopon 22633 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
606 cncnp 21132 . . . . . . . . . . . . . 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))‘𝑥))))
607604, 605, 606mp2an 708 . . . . . . . . . . . . 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))‘𝑥)))
608602, 607mpbi 220 . . . . . . . . . . . 12 ((𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))):((-π[,]π) ∖ {0})⟶ℂ ∧ ∀𝑥 ∈ ((-π[,]π) ∖ {0})(𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥))
609608simpri 477 . . . . . . . . . . 11 𝑥 ∈ ((-π[,]π) ∖ {0})(𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥)
610543, 609vtoclri 3314 . . . . . . . . . 10 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠))
611541, 610syl 17 . . . . . . . . 9 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠))
61210reseq1i 5424 . . . . . . . . . 10 (𝐾 ↾ ((-π[,]π) ∖ {0})) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π[,]π) ∖ {0}))
613 difss 3770 . . . . . . . . . . 11 ((-π[,]π) ∖ {0}) ⊆ (-π[,]π)
614 resmpt 5484 . . . . . . . . . . 11 (((-π[,]π) ∖ {0}) ⊆ (-π[,]π) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π[,]π) ∖ {0})) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))))
615613, 614ax-mp 5 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π[,]π) ∖ {0})) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
616 eldifn 3766 . . . . . . . . . . . . 13 (𝑠 ∈ ((-π[,]π) ∖ {0}) → ¬ 𝑠 ∈ {0})
617616, 502sylnib 317 . . . . . . . . . . . 12 (𝑠 ∈ ((-π[,]π) ∖ {0}) → ¬ 𝑠 = 0)
618617, 479syl 17 . . . . . . . . . . 11 (𝑠 ∈ ((-π[,]π) ∖ {0}) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
619618mpteq2ia 4773 . . . . . . . . . 10 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
620612, 615, 6193eqtri 2677 . . . . . . . . 9 (𝐾 ↾ ((-π[,]π) ∖ {0})) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
621 restabs 21017 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ Top ∧ ((-π[,]π) ∖ {0}) ⊆ (-π[,]π) ∧ (-π[,]π) ∈ V) → (((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) = ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})))
622453, 613, 454, 621mp3an 1464 . . . . . . . . . . 11 (((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) = ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0}))
623622oveq1i 6700 . . . . . . . . . 10 ((((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld)) = (((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))
624623fveq1i 6230 . . . . . . . . 9 (((((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠) = ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠)
625611, 620, 6243eltr4g 2747 . . . . . . . 8 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → (𝐾 ↾ ((-π[,]π) ∖ {0})) ∈ (((((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠))
626452, 613pm3.2i 470 . . . . . . . . . 10 (((topGen‘ran (,)) ↾t (-π[,]π)) ∈ Top ∧ ((-π[,]π) ∖ {0}) ⊆ (-π[,]π))
627626a1i 11 . . . . . . . . 9 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → (((topGen‘ran (,)) ↾t (-π[,]π)) ∈ Top ∧ ((-π[,]π) ∖ {0}) ⊆ (-π[,]π)))
628 ssdif 3778 . . . . . . . . . . . . . 14 ((-π[,]π) ⊆ ℝ → ((-π[,]π) ∖ {0}) ⊆ (ℝ ∖ {0}))
629427, 628ax-mp 5 . . . . . . . . . . . . 13 ((-π[,]π) ∖ {0}) ⊆ (ℝ ∖ {0})
630629, 541sseldi 3634 . . . . . . . . . . . 12 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ (ℝ ∖ {0}))
631 sscon 3777 . . . . . . . . . . . . . . . . 17 ({0} ⊆ (-π[,]π) → (ℝ ∖ (-π[,]π)) ⊆ (ℝ ∖ {0}))
632436, 631ax-mp 5 . . . . . . . . . . . . . . . 16 (ℝ ∖ (-π[,]π)) ⊆ (ℝ ∖ {0})
633629, 632unssi 3821 . . . . . . . . . . . . . . 15 (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))) ⊆ (ℝ ∖ {0})
634 simpr 476 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (-π[,]π))
635 eldifn 3766 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (ℝ ∖ {0}) → ¬ 𝑠 ∈ {0})
636635adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ (-π[,]π)) → ¬ 𝑠 ∈ {0})
637634, 636eldifd 3618 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ ((-π[,]π) ∖ {0}))
638 elun1 3813 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
639637, 638syl 17 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
640 eldifi 3765 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (ℝ ∖ {0}) → 𝑠 ∈ ℝ)
641640adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ ℝ)
642 simpr 476 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ (-π[,]π)) → ¬ 𝑠 ∈ (-π[,]π))
643641, 642eldifd 3618 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (ℝ ∖ (-π[,]π)))
644 elun2 3814 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (ℝ ∖ (-π[,]π)) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
645643, 644syl 17 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
646639, 645pm2.61dan 849 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (ℝ ∖ {0}) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
647646ssriv 3640 . . . . . . . . . . . . . . 15 (ℝ ∖ {0}) ⊆ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))
648633, 647eqssi 3652 . . . . . . . . . . . . . 14 (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))) = (ℝ ∖ {0})
649648fveq2i 6232 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) = ((int‘(topGen‘ran (,)))‘(ℝ ∖ {0}))
65061cldopn 20883 . . . . . . . . . . . . . . 15 ({0} ∈ (Clsd‘(topGen‘ran (,))) → (ℝ ∖ {0}) ∈ (topGen‘ran (,)))
65159, 650ax-mp 5 . . . . . . . . . . . . . 14 (ℝ ∖ {0}) ∈ (topGen‘ran (,))
652 isopn3i 20934 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ Top ∧ (ℝ ∖ {0}) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘(ℝ ∖ {0})) = (ℝ ∖ {0}))
653453, 651, 652mp2an 708 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘(ℝ ∖ {0})) = (ℝ ∖ {0})
654649, 653eqtri 2673 . . . . . . . . . . . 12 ((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) = (ℝ ∖ {0})
655630, 654syl6eleqr 2741 . . . . . . . . . . 11 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))))
656655, 537elind 3831 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ (((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) ∩ (-π[,]π)))
657 eqid 2651 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t (-π[,]π)) = ((topGen‘ran (,)) ↾t (-π[,]π))
65861, 657restntr 21034 . . . . . . . . . . 11 (((topGen‘ran (,)) ∈ Top ∧ (-π[,]π) ⊆ ℝ ∧ ((-π[,]π) ∖ {0}) ⊆ (-π[,]π)) → ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘((-π[,]π) ∖ {0})) = (((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) ∩ (-π[,]π)))
659453, 427, 613, 658mp3an 1464 . . . . . . . . . 10 ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘((-π[,]π) ∖ {0})) = (((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) ∩ (-π[,]π))
660656, 659syl6eleqr 2741 . . . . . . . . 9 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘((-π[,]π) ∖ {0})))
66114a1i 11 . . . . . . . . 9 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝐾:(-π[,]π)⟶ℂ)
662451toponunii 20769 . . . . . . . . . 10 (-π[,]π) = ((topGen‘ran (,)) ↾t (-π[,]π))
663662, 596cnprest 21141 . . . . . . . . 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))‘𝑠)))
664627, 660, 661, 663syl12anc 1364 . . . . . . . 8 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → (𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠) ↔ (𝐾 ↾ ((-π[,]π) ∖ {0})) ∈ (((((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠)))
665625, 664mpbird 247 . . . . . . 7 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))
666536, 665pm2.61dan 849 . . . . . 6 (𝑠 ∈ (-π[,]π) → 𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))
667666rgen 2951 . . . . 5 𝑠 ∈ (-π[,]π)𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠)
668 cncnp 21132 . . . . . 6 ((((topGen‘ran (,)) ↾t (-π[,]π)) ∈ (TopOn‘(-π[,]π)) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → (𝐾 ∈ (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld)) ↔ (𝐾:(-π[,]π)⟶ℂ ∧ ∀𝑠 ∈ (-π[,]π)𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))))
669451, 605, 668mp2an 708 . . . . 5 (𝐾 ∈ (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld)) ↔ (𝐾:(-π[,]π)⟶ℂ ∧ ∀𝑠 ∈ (-π[,]π)𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠)))
67014, 667, 669mpbir2an 975 . . . 4 𝐾 ∈ (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld))
67156, 532, 599cncfcn 22759 . . . . . 6 (((-π[,]π) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((-π[,]π)–cn→ℂ) = (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld)))
672517, 144, 671mp2an 708 . . . . 5 ((-π[,]π)–cn→ℂ) = (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld))
673672eqcomi 2660 . . . 4 (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld)) = ((-π[,]π)–cn→ℂ)
674670, 673eleqtri 2728 . . 3 𝐾 ∈ ((-π[,]π)–cn→ℂ)
675 cncffvrn 22748 . . 3 ((ℝ ⊆ ℂ ∧ 𝐾 ∈ ((-π[,]π)–cn→ℂ)) → (𝐾 ∈ ((-π[,]π)–cn→ℝ) ↔ 𝐾:(-π[,]π)⟶ℝ))
67612, 674, 675mp2an 708 . 2 (𝐾 ∈ ((-π[,]π)–cn→ℝ) ↔ 𝐾:(-π[,]π)⟶ℝ)
67711, 676mpbir 221 1 𝐾 ∈ ((-π[,]π)–cn→ℝ)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523  ⊤wtru 1524   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  Vcvv 3231   ∖ cdif 3604   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ifcif 4119  {csn 4210  {cpr 4212   class class class wbr 4685   ↦ cmpt 4762  dom cdm 5143  ran crn 5144   ↾ cres 5145   “ cima 5146   Fn wfn 5921  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   · cmul 9979  ℝ*cxr 10111   < clt 10112   ≤ cle 10113  -cneg 10305   / cdiv 10722  2c2 11108  ℝ+crp 11870  (,)cioo 12213  [,]cicc 12216  ℜcre 13881  sincsin 14838  cosccos 14839  πcpi 14841   ↾t crest 16128  TopOpenctopn 16129  topGenctg 16145  ℂfldccnfld 19794  Topctop 20746  TopOnctopon 20763  Clsdccld 20868  intcnt 20869   Cn ccn 21076   CnP ccnp 21077  –cn→ccncf 22726   limℂ climc 23671   D cdv 23672 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-ef 14842  df-sin 14844  df-cos 14845  df-pi 14847  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-t1 21166  df-haus 21167  df-cmp 21238  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-limc 23675  df-dv 23676 This theorem is referenced by:  fourierdlem77  40718  fourierdlem78  40719  fourierdlem85  40726  fourierdlem88  40729
 Copyright terms: Public domain W3C validator