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 45369
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 2728 . . . . . 6 (𝑦 = 𝑠 → (𝑦 = 0 ↔ 𝑠 = 0))
3 id 22 . . . . . . 7 (𝑦 = 𝑠𝑦 = 𝑠)
4 oveq1 7408 . . . . . . . . 9 (𝑦 = 𝑠 → (𝑦 / 2) = (𝑠 / 2))
54fveq2d 6885 . . . . . . . 8 (𝑦 = 𝑠 → (sin‘(𝑦 / 2)) = (sin‘(𝑠 / 2)))
65oveq2d 7417 . . . . . . 7 (𝑦 = 𝑠 → (2 · (sin‘(𝑦 / 2))) = (2 · (sin‘(𝑠 / 2))))
73, 6oveq12d 7419 . . . . . 6 (𝑦 = 𝑠 → (𝑦 / (2 · (sin‘(𝑦 / 2)))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
82, 7ifbieq2d 4546 . . . . 5 (𝑦 = 𝑠 → if(𝑦 = 0, 1, (𝑦 / (2 · (sin‘(𝑦 / 2))))) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
98cbvmptv 5251 . . . 4 (𝑦 ∈ (-π[,]π) ↦ if(𝑦 = 0, 1, (𝑦 / (2 · (sin‘(𝑦 / 2)))))) = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
101, 9eqtri 2752 . . 3 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
1110fourierdlem43 45351 . 2 𝐾:(-π[,]π)⟶ℝ
12 ax-resscn 11163 . . 3 ℝ ⊆ ℂ
13 fss 6724 . . . . . 6 ((𝐾:(-π[,]π)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐾:(-π[,]π)⟶ℂ)
1411, 12, 13mp2an 689 . . . . 5 𝐾:(-π[,]π)⟶ℂ
1514a1i 11 . . . . . . . . 9 (𝑠 = 0 → 𝐾:(-π[,]π)⟶ℂ)
16 difss 4123 . . . . . . . . . . . . . . . . 17 ((-π(,)π) ∖ {0}) ⊆ (-π(,)π)
17 elioore 13351 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (-π(,)π) → 𝑠 ∈ ℝ)
1817ssriv 3978 . . . . . . . . . . . . . . . . 17 (-π(,)π) ⊆ ℝ
1916, 18sstri 3983 . . . . . . . . . . . . . . . 16 ((-π(,)π) ∖ {0}) ⊆ ℝ
2019a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ((-π(,)π) ∖ {0}) ⊆ ℝ)
21 eqid 2724 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)
2219sseli 3970 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-π(,)π) ∖ {0}) → 𝑥 ∈ ℝ)
2321, 22fmpti 7103 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥):((-π(,)π) ∖ {0})⟶ℝ
2423a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥):((-π(,)π) ∖ {0})⟶ℝ)
25 eqid 2724 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))
26 2re 12283 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℝ
2726a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ)
2822rehalfcld 12456 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) → (𝑥 / 2) ∈ ℝ)
2928resincld 16083 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑥 / 2)) ∈ ℝ)
3027, 29remulcld 11241 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-π(,)π) ∖ {0}) → (2 · (sin‘(𝑥 / 2))) ∈ ℝ)
3125, 30fmpti 7103 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))):((-π(,)π) ∖ {0})⟶ℝ
3231a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))):((-π(,)π) ∖ {0})⟶ℝ)
33 iooretop 24604 . . . . . . . . . . . . . . . 16 (-π(,)π) ∈ (topGen‘ran (,))
3433a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (-π(,)π) ∈ (topGen‘ran (,)))
35 0re 11213 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
36 negpilt0 44475 . . . . . . . . . . . . . . . . 17 -π < 0
37 pipos 26312 . . . . . . . . . . . . . . . . 17 0 < π
38 pire 26310 . . . . . . . . . . . . . . . . . . . 20 π ∈ ℝ
3938renegcli 11518 . . . . . . . . . . . . . . . . . . 19 -π ∈ ℝ
4039rexri 11269 . . . . . . . . . . . . . . . . . 18 -π ∈ ℝ*
4138rexri 11269 . . . . . . . . . . . . . . . . . 18 π ∈ ℝ*
42 elioo2 13362 . . . . . . . . . . . . . . . . . 18 ((-π ∈ ℝ* ∧ π ∈ ℝ*) → (0 ∈ (-π(,)π) ↔ (0 ∈ ℝ ∧ -π < 0 ∧ 0 < π)))
4340, 41, 42mp2an 689 . . . . . . . . . . . . . . . . 17 (0 ∈ (-π(,)π) ↔ (0 ∈ ℝ ∧ -π < 0 ∧ 0 < π))
4435, 36, 37, 43mpbir3an 1338 . . . . . . . . . . . . . . . 16 0 ∈ (-π(,)π)
4544a1i 11 . . . . . . . . . . . . . . 15 (⊤ → 0 ∈ (-π(,)π))
46 eqid 2724 . . . . . . . . . . . . . . 15 ((-π(,)π) ∖ {0}) = ((-π(,)π) ∖ {0})
47 1ex 11207 . . . . . . . . . . . . . . . . . . 19 1 ∈ V
48 eqid 2724 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1)
4947, 48dmmpti 6684 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = ((-π(,)π) ∖ {0})
50 reelprrecn 11198 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ ∈ {ℝ, ℂ}
5150a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ℝ ∈ {ℝ, ℂ})
5212sseli 3970 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
5352adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
54 1red 11212 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
5551dvmptid 25811 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
56 eqid 2724 . . . . . . . . . . . . . . . . . . . . . . 23 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
5756tgioo2 24641 . . . . . . . . . . . . . . . . . . . . . 22 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
58 sncldre 44217 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 ∈ ℝ → {0} ∈ (Clsd‘(topGen‘ran (,))))
5935, 58ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 {0} ∈ (Clsd‘(topGen‘ran (,)))
60 retopon 24602 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
6160toponunii 22740 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℝ = (topGen‘ran (,))
6261difopn 22860 . . . . . . . . . . . . . . . . . . . . . . . 24 (((-π(,)π) ∈ (topGen‘ran (,)) ∧ {0} ∈ (Clsd‘(topGen‘ran (,)))) → ((-π(,)π) ∖ {0}) ∈ (topGen‘ran (,)))
6333, 59, 62mp2an 689 . . . . . . . . . . . . . . . . . . . . . . 23 ((-π(,)π) ∖ {0}) ∈ (topGen‘ran (,))
6463a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ((-π(,)π) ∖ {0}) ∈ (topGen‘ran (,)))
6551, 53, 54, 55, 20, 57, 56, 64dvmptres 25817 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1))
6665mptru 1540 . . . . . . . . . . . . . . . . . . . 20 (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1)
6766eqcomi 2733 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
6867dmeqi 5894 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
6949, 68eqtr3i 2754 . . . . . . . . . . . . . . . . 17 ((-π(,)π) ∖ {0}) = dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
7069eqimssi 4034 . . . . . . . . . . . . . . . 16 ((-π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
7170a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ((-π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)))
72 fvex 6894 . . . . . . . . . . . . . . . . . . 19 (cos‘(𝑥 / 2)) ∈ V
73 eqid 2724 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))
7472, 73dmmpti 6684 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = ((-π(,)π) ∖ {0})
75 2cnd 12287 . . . . . . . . . . . . . . . . . . . . . . 23 ((⊤ ∧ 𝑥 ∈ ℝ) → 2 ∈ ℂ)
7653halfcld 12454 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⊤ ∧ 𝑥 ∈ ℝ) → (𝑥 / 2) ∈ ℂ)
7776sincld 16070 . . . . . . . . . . . . . . . . . . . . . . 23 ((⊤ ∧ 𝑥 ∈ ℝ) → (sin‘(𝑥 / 2)) ∈ ℂ)
7875, 77mulcld 11231 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → (2 · (sin‘(𝑥 / 2))) ∈ ℂ)
7976coscld 16071 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → (cos‘(𝑥 / 2)) ∈ ℂ)
80 2cnd 12287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → 2 ∈ ℂ)
81 2ne0 12313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 2 ≠ 0
8281a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → 2 ≠ 0)
8352, 80, 82divrec2d 11991 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → (𝑥 / 2) = ((1 / 2) · 𝑥))
8483fveq2d 6885 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℝ → (sin‘(𝑥 / 2)) = (sin‘((1 / 2) · 𝑥)))
8584oveq2d 7417 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ → (2 · (sin‘(𝑥 / 2))) = (2 · (sin‘((1 / 2) · 𝑥))))
8685mpteq2ia 5241 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))
8786oveq2i 7412 . . . . . . . . . . . . . . . . . . . . . . . 24 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2))))) = (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))
88 resmpt 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℝ ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))
8912, 88ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))
9089eqcomi 2733 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) = ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ)
9190oveq2i 7412 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (ℝ D ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ))
92 eqid 2724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) = (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))
93 2cnd 12287 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℂ → 2 ∈ ℂ)
94 halfcn 12424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (1 / 2) ∈ ℂ
9594a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℂ → (1 / 2) ∈ ℂ)
96 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℂ → 𝑥 ∈ ℂ)
9795, 96mulcld 11231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℂ → ((1 / 2) · 𝑥) ∈ ℂ)
9897sincld 16070 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℂ → (sin‘((1 / 2) · 𝑥)) ∈ ℂ)
9993, 98mulcld 11231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℂ → (2 · (sin‘((1 / 2) · 𝑥))) ∈ ℂ)
10092, 99fmpti 7103 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))):ℂ⟶ℂ
101 eqid 2724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
102 2cn 12284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2 ∈ ℂ
103102, 94mulcli 11218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (2 · (1 / 2)) ∈ ℂ
104103a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ ℂ → (2 · (1 / 2)) ∈ ℂ)
10597coscld 16071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ ℂ → (cos‘((1 / 2) · 𝑥)) ∈ ℂ)
106104, 105mulcld 11231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ ℂ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) ∈ ℂ)
107106adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((⊤ ∧ 𝑥 ∈ ℂ) → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) ∈ ℂ)
108101, 107dmmptd 6685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⊤ → dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = ℂ)
109108mptru 1540 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = ℂ
11012, 109sseqtrri 4011 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℝ ⊆ dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
111 dvasinbx 45121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))))
112102, 94, 111mp2an 689 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
113112dmeqi 5894 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 dom (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
114110, 113sseqtrri 4011 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℝ ⊆ dom (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))
115 dvcnre 45117 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))):ℂ⟶ℂ ∧ ℝ ⊆ dom (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))) → (ℝ D ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ)) = ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ))
116100, 114, 115mp2an 689 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℝ D ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ)) = ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ)
117112reseq1i 5967 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ) = ((𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) ↾ ℝ)
118 resmpt 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (2 · (1 / 2)) = 1
121120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → (2 · (1 / 2)) = 1)
12283eqcomd 2730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℝ → ((1 / 2) · 𝑥) = (𝑥 / 2))
123122fveq2d 6885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → (cos‘((1 / 2) · 𝑥)) = (cos‘(𝑥 / 2)))
124121, 123oveq12d 7419 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) = (1 · (cos‘(𝑥 / 2))))
12552halfcld 12454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℝ → (𝑥 / 2) ∈ ℂ)
126125coscld 16071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → (cos‘(𝑥 / 2)) ∈ ℂ)
127126mullidd 11229 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → (1 · (cos‘(𝑥 / 2))) = (cos‘(𝑥 / 2)))
128124, 127eqtrd 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℝ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) = (cos‘(𝑥 / 2)))
129128mpteq2ia 5241 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
130117, 119, 1293eqtri 2756 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
13191, 116, 1303eqtri 2756 . . . . . . . . . . . . . . . . . . . . . . . 24 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
13287, 131eqtri 2752 . . . . . . . . . . . . . . . . . . . . . . 23 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
133132a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2))))
13451, 78, 79, 133, 20, 57, 56, 64dvmptres 25817 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))))
135134mptru 1540 . . . . . . . . . . . . . . . . . . . 20 (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))
136135eqcomi 2733 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
137136dmeqi 5894 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
13874, 137eqtr3i 2754 . . . . . . . . . . . . . . . . 17 ((-π(,)π) ∖ {0}) = dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
139138eqimssi 4034 . . . . . . . . . . . . . . . 16 ((-π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
140139a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ((-π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))))
14117recnd 11239 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (-π(,)π) → 𝑠 ∈ ℂ)
142141ssriv 3978 . . . . . . . . . . . . . . . . . . . . . . 23 (-π(,)π) ⊆ ℂ
143142a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (-π(,)π) ⊆ ℂ)
144 ssid 3996 . . . . . . . . . . . . . . . . . . . . . . 23 ℂ ⊆ ℂ
145144a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ℂ ⊆ ℂ)
146143, 145idcncfg 45074 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑥 ∈ (-π(,)π) ↦ 𝑥) ∈ ((-π(,)π)–cn→ℂ))
147146mptru 1540 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (-π(,)π) ↦ 𝑥) ∈ ((-π(,)π)–cn→ℂ)
148 cnlimc 25739 . . . . . . . . . . . . . . . . . . . . 21 ((-π(,)π) ⊆ ℂ → ((𝑥 ∈ (-π(,)π) ↦ 𝑥) ∈ ((-π(,)π)–cn→ℂ) ↔ ((𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦))))
149142, 148ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (-π(,)π) ↦ 𝑥) ∈ ((-π(,)π)–cn→ℂ) ↔ ((𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦)))
150147, 149mpbi 229 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦))
151150simpri 485 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦)
152 fveq2 6881 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) = ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0))
153 oveq2 7409 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦) = ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0))
154152, 153eleq12d 2819 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 0 → (((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦) ↔ ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0)))
155154rspccva 3603 . . . . . . . . . . . . . . . . . 18 ((∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦) ∧ 0 ∈ (-π(,)π)) → ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0))
156151, 44, 155mp2an 689 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0)
157 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → 𝑥 = 0)
158 eqid 2724 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (-π(,)π) ↦ 𝑥) = (𝑥 ∈ (-π(,)π) ↦ 𝑥)
159 c0ex 11205 . . . . . . . . . . . . . . . . . . 19 0 ∈ V
160157, 158, 159fvmpt 6988 . . . . . . . . . . . . . . . . . 18 (0 ∈ (-π(,)π) → ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) = 0)
16144, 160ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) = 0
162 elioore 13351 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (-π(,)π) → 𝑥 ∈ ℝ)
163162recnd 11239 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (-π(,)π) → 𝑥 ∈ ℂ)
164158, 163fmpti 7103 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ
165164a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ)
166165limcdif 25727 . . . . . . . . . . . . . . . . . . 19 (⊤ → ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0) = (((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) lim 0))
167166mptru 1540 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0) = (((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) lim 0)
168 resmpt 6027 . . . . . . . . . . . . . . . . . . . 20 (((-π(,)π) ∖ {0}) ⊆ (-π(,)π) → ((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
16916, 168ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)
170169oveq1i 7411 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) lim 0) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) lim 0)
171167, 170eqtri 2752 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) lim 0)
172156, 161, 1713eltr3i 2837 . . . . . . . . . . . . . . . 16 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) lim 0)
173172a1i 11 . . . . . . . . . . . . . . 15 (⊤ → 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) lim 0))
174 eqid 2724 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℂ ↦ 2) = (𝑥 ∈ ℂ ↦ 2)
175144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 ∈ ℂ → ℂ ⊆ ℂ)
176 2cnd 12287 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 ∈ ℂ → 2 ∈ ℂ)
177175, 176, 175constcncfg 45073 . . . . . . . . . . . . . . . . . . . . . . . 24 (2 ∈ ℂ → (𝑥 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
178102, 177mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → (𝑥 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
179 2cnd 12287 . . . . . . . . . . . . . . . . . . . . . . 23 ((⊤ ∧ 𝑥 ∈ (-π(,)π)) → 2 ∈ ℂ)
180174, 178, 143, 145, 179cncfmptssg 45072 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑥 ∈ (-π(,)π) ↦ 2) ∈ ((-π(,)π)–cn→ℂ))
181 sincn 26298 . . . . . . . . . . . . . . . . . . . . . . . 24 sin ∈ (ℂ–cn→ℂ)
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → sin ∈ (ℂ–cn→ℂ))
183 eqid 2724 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℂ ↦ (𝑥 / 2)) = (𝑥 ∈ ℂ ↦ (𝑥 / 2))
184183divccncf 24748 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ (ℂ–cn→ℂ))
185102, 81, 184mp2an 689 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ (ℂ–cn→ℂ)
186185a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (⊤ → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ (ℂ–cn→ℂ))
187163adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⊤ ∧ 𝑥 ∈ (-π(,)π)) → 𝑥 ∈ ℂ)
188187halfcld 12454 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⊤ ∧ 𝑥 ∈ (-π(,)π)) → (𝑥 / 2) ∈ ℂ)
189183, 186, 143, 145, 188cncfmptssg 45072 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → (𝑥 ∈ (-π(,)π) ↦ (𝑥 / 2)) ∈ ((-π(,)π)–cn→ℂ))
190182, 189cncfmpt1f 24756 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑥 ∈ (-π(,)π) ↦ (sin‘(𝑥 / 2))) ∈ ((-π(,)π)–cn→ℂ))
191180, 190mulcncf 25296 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ∈ ((-π(,)π)–cn→ℂ))
192191mptru 1540 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ∈ ((-π(,)π)–cn→ℂ)
193 cnlimc 25739 . . . . . . . . . . . . . . . . . . . . 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 229 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦))
196195simpri 485 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦)
197 fveq2 6881 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0))
198 oveq2 7409 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦) = ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0))
199197, 198eleq12d 2819 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 0 → (((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦) ↔ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)))
200199rspccva 3603 . . . . . . . . . . . . . . . . . 18 ((∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦) ∧ 0 ∈ (-π(,)π)) → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0))
201196, 44, 200mp2an 689 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)
202 oveq1 7408 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 0 → (𝑥 / 2) = (0 / 2))
203102, 81div0i 11945 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 / 2) = 0
204202, 203eqtrdi 2780 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 0 → (𝑥 / 2) = 0)
205204fveq2d 6885 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 0 → (sin‘(𝑥 / 2)) = (sin‘0))
206 sin0 16089 . . . . . . . . . . . . . . . . . . . . . 22 (sin‘0) = 0
207205, 206eqtrdi 2780 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 0 → (sin‘(𝑥 / 2)) = 0)
208207oveq2d 7417 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 0 → (2 · (sin‘(𝑥 / 2))) = (2 · 0))
209 2t0e0 12378 . . . . . . . . . . . . . . . . . . . 20 (2 · 0) = 0
210208, 209eqtrdi 2780 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → (2 · (sin‘(𝑥 / 2))) = 0)
211 eqid 2724 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))
212210, 211, 159fvmpt 6988 . . . . . . . . . . . . . . . . . 18 (0 ∈ (-π(,)π) → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) = 0)
21344, 212ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) = 0
214 2cnd 12287 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (-π(,)π) → 2 ∈ ℂ)
215163halfcld 12454 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ (-π(,)π) → (𝑥 / 2) ∈ ℂ)
216215sincld 16070 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (-π(,)π) → (sin‘(𝑥 / 2)) ∈ ℂ)
217214, 216mulcld 11231 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (-π(,)π) → (2 · (sin‘(𝑥 / 2))) ∈ ℂ)
218211, 217fmpti 7103 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):(-π(,)π)⟶ℂ
219218a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):(-π(,)π)⟶ℂ)
220219limcdif 25727 . . . . . . . . . . . . . . . . . . 19 (⊤ → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0) = (((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) lim 0))
221220mptru 1540 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0) = (((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) lim 0)
222 resmpt 6027 . . . . . . . . . . . . . . . . . . . 20 (((-π(,)π) ∖ {0}) ⊆ (-π(,)π) → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
22316, 222ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))
224223oveq1i 7411 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) lim 0) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)
225221, 224eqtri 2752 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)
226201, 213, 2253eltr3i 2837 . . . . . . . . . . . . . . . 16 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)
227226a1i 11 . . . . . . . . . . . . . . 15 (⊤ → 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0))
228 eqidd 2725 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
229 oveq1 7408 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑥 / 2) = (𝑦 / 2))
230229fveq2d 6885 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (sin‘(𝑥 / 2)) = (sin‘(𝑦 / 2)))
231230oveq2d 7417 . . . . . . . . . . . . . . . . . . . . . 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 3970 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ ℝ)
236235rehalfcld 12456 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑦 / 2) ∈ ℝ)
237236resincld 16083 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑦 / 2)) ∈ ℝ)
238234, 237remulcld 11241 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (2 · (sin‘(𝑦 / 2))) ∈ ℝ)
239228, 232, 233, 238fvmptd 6995 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = (2 · (sin‘(𝑦 / 2))))
240 2cnd 12287 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℂ)
241237recnd 11239 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑦 / 2)) ∈ ℂ)
24281a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 2 ≠ 0)
243 ioossicc 13407 . . . . . . . . . . . . . . . . . . . . . . 23 (-π(,)π) ⊆ (-π[,]π)
244 eldifi 4118 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ (-π(,)π))
245243, 244sselid 3972 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ (-π[,]π))
246 eldifsni 4785 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ≠ 0)
247 fourierdlem44 45352 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ (-π[,]π) ∧ 𝑦 ≠ 0) → (sin‘(𝑦 / 2)) ≠ 0)
248245, 246, 247syl2anc 583 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑦 / 2)) ≠ 0)
249240, 241, 242, 248mulne0d 11863 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (2 · (sin‘(𝑦 / 2))) ≠ 0)
250239, 249eqnetrd 3000 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ≠ 0)
251250neneqd 2937 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ¬ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0)
252251nrex 3066 . . . . . . . . . . . . . . . . 17 ¬ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0
25325fnmpt 6680 . . . . . . . . . . . . . . . . . . 19 (∀𝑥 ∈ ((-π(,)π) ∖ {0})(2 · (sin‘(𝑥 / 2))) ∈ ℝ → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) Fn ((-π(,)π) ∖ {0}))
254253, 30mprg 3059 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) Fn ((-π(,)π) ∖ {0})
255 ssid 3996 . . . . . . . . . . . . . . . . . 18 ((-π(,)π) ∖ {0}) ⊆ ((-π(,)π) ∖ {0})
256 fvelimab 6954 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) Fn ((-π(,)π) ∖ {0}) ∧ ((-π(,)π) ∖ {0}) ⊆ ((-π(,)π) ∖ {0})) → (0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) “ ((-π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0))
257254, 255, 256mp2an 689 . . . . . . . . . . . . . . . . 17 (0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) “ ((-π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0)
258252, 257mtbir 323 . . . . . . . . . . . . . . . 16 ¬ 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) “ ((-π(,)π) ∖ {0}))
259258a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ¬ 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) “ ((-π(,)π) ∖ {0})))
260 eqidd 2725 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))))
261229fveq2d 6885 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (cos‘(𝑥 / 2)) = (cos‘(𝑦 / 2)))
262261adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑦) → (cos‘(𝑥 / 2)) = (cos‘(𝑦 / 2)))
263235recnd 11239 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ ℂ)
264263halfcld 12454 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑦 / 2) ∈ ℂ)
265264coscld 16071 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑦 / 2)) ∈ ℂ)
266260, 262, 233, 265fvmptd 6995 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = (cos‘(𝑦 / 2)))
267236rered 15168 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (ℜ‘(𝑦 / 2)) = (𝑦 / 2))
268 halfpire 26316 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π / 2) ∈ ℝ
269268renegcli 11518 . . . . . . . . . . . . . . . . . . . . . . . . . 26 -(π / 2) ∈ ℝ
270269a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ)
271270rexrd 11261 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ*)
272268a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (π / 2) ∈ ℝ)
273272rexrd 11261 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (π / 2) ∈ ℝ*)
274 picn 26311 . . . . . . . . . . . . . . . . . . . . . . . . . 26 π ∈ ℂ
275 divneg 11903 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(π / 2) = (-π / 2))
276274, 102, 81, 275mp3an 1457 . . . . . . . . . . . . . . . . . . . . . . . . 25 -(π / 2) = (-π / 2)
27739a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -π ∈ ℝ)
278 2rp 12976 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ∈ ℝ+
279278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ+)
28040a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -π ∈ ℝ*)
28141a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ((-π(,)π) ∖ {0}) → π ∈ ℝ*)
282 ioogtlb 44693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝑦 ∈ (-π(,)π)) → -π < 𝑦)
283280, 281, 244, 282syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -π < 𝑦)
284277, 235, 279, 283ltdiv1dd 13070 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (-π / 2) < (𝑦 / 2))
285276, 284eqbrtrid 5173 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) < (𝑦 / 2))
28638a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → π ∈ ℝ)
287 iooltub 44708 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝑦 ∈ (-π(,)π)) → 𝑦 < π)
288280, 281, 244, 287syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 < π)
289235, 286, 279, 288ltdiv1dd 13070 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑦 / 2) < (π / 2))
290271, 273, 236, 285, 289eliood 44696 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑦 / 2) ∈ (-(π / 2)(,)(π / 2)))
291267, 290eqeltrd 2825 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (ℜ‘(𝑦 / 2)) ∈ (-(π / 2)(,)(π / 2)))
292 cosne0 26380 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 / 2) ∈ ℂ ∧ (ℜ‘(𝑦 / 2)) ∈ (-(π / 2)(,)(π / 2))) → (cos‘(𝑦 / 2)) ≠ 0)
293264, 291, 292syl2anc 583 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑦 / 2)) ≠ 0)
294266, 293eqnetrd 3000 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) ≠ 0)
295294neneqd 2937 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ¬ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0)
296295nrex 3066 . . . . . . . . . . . . . . . . . 18 ¬ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0
29772, 73fnmpti 6683 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) Fn ((-π(,)π) ∖ {0})
298 fvelimab 6954 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) Fn ((-π(,)π) ∖ {0}) ∧ ((-π(,)π) ∖ {0}) ⊆ ((-π(,)π) ∖ {0})) → (0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0))
299297, 255, 298mp2an 689 . . . . . . . . . . . . . . . . . 18 (0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0)
300296, 299mtbir 323 . . . . . . . . . . . . . . . . 17 ¬ 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0}))
301135imaeq1i 6046 . . . . . . . . . . . . . . . . . 18 ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) “ ((-π(,)π) ∖ {0})) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0}))
302301eleq2i 2817 . . . . . . . . . . . . . . . . 17 (0 ∈ ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) “ ((-π(,)π) ∖ {0})) ↔ 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0})))
303300, 302mtbir 323 . . . . . . . . . . . . . . . 16 ¬ 0 ∈ ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) “ ((-π(,)π) ∖ {0}))
304303a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ¬ 0 ∈ ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) “ ((-π(,)π) ∖ {0})))
305 eqid 2724 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑠 / 2))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑠 / 2)))
306 eqid 2724 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2))))
30719sseli 3970 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 ∈ ℝ)
308307recnd 11239 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 ∈ ℂ)
309308halfcld 12454 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑠 / 2) ∈ ℂ)
310309coscld 16071 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ∈ ℂ)
311307rehalfcld 12456 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑠 / 2) ∈ ℝ)
312311rered 15168 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (ℜ‘(𝑠 / 2)) = (𝑠 / 2))
313269a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ)
314313rexrd 11261 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ*)
315268a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (π / 2) ∈ ℝ)
316315rexrd 11261 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (π / 2) ∈ ℝ*)
31738a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ((-π(,)π) ∖ {0}) → π ∈ ℝ)
318317renegcld 11638 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -π ∈ ℝ)
319278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ+)
32040a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -π ∈ ℝ*)
32141a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ((-π(,)π) ∖ {0}) → π ∈ ℝ*)
322 eldifi 4118 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 ∈ (-π(,)π))
323 ioogtlb 44693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝑠 ∈ (-π(,)π)) → -π < 𝑠)
324320, 321, 322, 323syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -π < 𝑠)
325318, 307, 319, 324ltdiv1dd 13070 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (-π / 2) < (𝑠 / 2))
326276, 325eqbrtrid 5173 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) < (𝑠 / 2))
327 iooltub 44708 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝑠 ∈ (-π(,)π)) → 𝑠 < π)
328320, 321, 322, 327syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 < π)
329307, 317, 319, 328ltdiv1dd 13070 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑠 / 2) < (π / 2))
330314, 316, 311, 326, 329eliood 44696 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑠 / 2) ∈ (-(π / 2)(,)(π / 2)))
331312, 330eqeltrd 2825 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (ℜ‘(𝑠 / 2)) ∈ (-(π / 2)(,)(π / 2)))
332 cosne0 26380 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 / 2) ∈ ℂ ∧ (ℜ‘(𝑠 / 2)) ∈ (-(π / 2)(,)(π / 2))) → (cos‘(𝑠 / 2)) ≠ 0)
333309, 331, 332syl2anc 583 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ≠ 0)
334333neneqd 2937 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ¬ (cos‘(𝑠 / 2)) = 0)
335311recoscld 16084 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ∈ ℝ)
336 elsng 4634 . . . . . . . . . . . . . . . . . . . . 21 ((cos‘(𝑠 / 2)) ∈ ℝ → ((cos‘(𝑠 / 2)) ∈ {0} ↔ (cos‘(𝑠 / 2)) = 0))
337335, 336syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((cos‘(𝑠 / 2)) ∈ {0} ↔ (cos‘(𝑠 / 2)) = 0))
338334, 337mtbird 325 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ¬ (cos‘(𝑠 / 2)) ∈ {0})
339310, 338eldifd 3951 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ∈ (ℂ ∖ {0}))
340339adantl 481 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑠 ∈ ((-π(,)π) ∖ {0})) → (cos‘(𝑠 / 2)) ∈ (ℂ ∖ {0}))
341309ad2antrl 725 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ (𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ (𝑠 / 2) ≠ 0)) → (𝑠 / 2) ∈ ℂ)
342 cosf 16065 . . . . . . . . . . . . . . . . . . . 20 cos:ℂ⟶ℂ
343342a1i 11 . . . . . . . . . . . . . . . . . . 19 (⊤ → cos:ℂ⟶ℂ)
344343ffvelcdmda 7076 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ ℂ) → (cos‘𝑥) ∈ ℂ)
345 eqid 2724 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ℂ ↦ (𝑠 / 2)) = (𝑠 ∈ ℂ ↦ (𝑠 / 2))
346345divccncf 24748 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑠 ∈ ℂ ↦ (𝑠 / 2)) ∈ (ℂ–cn→ℂ))
347102, 81, 346mp2an 689 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ℂ ↦ (𝑠 / 2)) ∈ (ℂ–cn→ℂ)
348347a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑠 ∈ ℂ ↦ (𝑠 / 2)) ∈ (ℂ–cn→ℂ))
349141adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑠 ∈ (-π(,)π)) → 𝑠 ∈ ℂ)
350349halfcld 12454 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑠 ∈ (-π(,)π)) → (𝑠 / 2) ∈ ℂ)
351345, 348, 143, 145, 350cncfmptssg 45072 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ∈ ((-π(,)π)–cn→ℂ))
352 oveq1 7408 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 0 → (𝑠 / 2) = (0 / 2))
353352, 203eqtrdi 2780 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → (𝑠 / 2) = 0)
354351, 45, 353cnmptlimc 25741 . . . . . . . . . . . . . . . . . . 19 (⊤ → 0 ∈ ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) lim 0))
355 eqid 2724 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) = (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2))
356141halfcld 12454 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (-π(,)π) → (𝑠 / 2) ∈ ℂ)
357355, 356fmpti 7103 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)):(-π(,)π)⟶ℂ
358357a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)):(-π(,)π)⟶ℂ)
359358limcdif 25727 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) lim 0) = (((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) lim 0))
360359mptru 1540 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) lim 0) = (((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) lim 0)
361 resmpt 6027 . . . . . . . . . . . . . . . . . . . . . 22 (((-π(,)π) ∖ {0}) ⊆ (-π(,)π) → ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2)))
36216, 361ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2))
363362oveq1i 7411 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2)) lim 0)
364360, 363eqtri 2752 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2)) lim 0)
365354, 364eleqtrdi 2835 . . . . . . . . . . . . . . . . . 18 (⊤ → 0 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2)) lim 0))
366 ffn 6707 . . . . . . . . . . . . . . . . . . . . . . 23 (cos:ℂ⟶ℂ → cos Fn ℂ)
367342, 366ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 cos Fn ℂ
368 dffn5 6940 . . . . . . . . . . . . . . . . . . . . . 22 (cos Fn ℂ ↔ cos = (𝑥 ∈ ℂ ↦ (cos‘𝑥)))
369367, 368mpbi 229 . . . . . . . . . . . . . . . . . . . . 21 cos = (𝑥 ∈ ℂ ↦ (cos‘𝑥))
370 coscn 26299 . . . . . . . . . . . . . . . . . . . . 21 cos ∈ (ℂ–cn→ℂ)
371369, 370eqeltrri 2822 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℂ ↦ (cos‘𝑥)) ∈ (ℂ–cn→ℂ)
372371a1i 11 . . . . . . . . . . . . . . . . . . 19 (⊤ → (𝑥 ∈ ℂ ↦ (cos‘𝑥)) ∈ (ℂ–cn→ℂ))
373 0cnd 11204 . . . . . . . . . . . . . . . . . . 19 (⊤ → 0 ∈ ℂ)
374 fveq2 6881 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 0 → (cos‘𝑥) = (cos‘0))
375 cos0 16090 . . . . . . . . . . . . . . . . . . . 20 (cos‘0) = 1
376374, 375eqtrdi 2780 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → (cos‘𝑥) = 1)
377372, 373, 376cnmptlimc 25741 . . . . . . . . . . . . . . . . . 18 (⊤ → 1 ∈ ((𝑥 ∈ ℂ ↦ (cos‘𝑥)) lim 0))
378 fveq2 6881 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑠 / 2) → (cos‘𝑥) = (cos‘(𝑠 / 2)))
379 fveq2 6881 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 / 2) = 0 → (cos‘(𝑠 / 2)) = (cos‘0))
380379, 375eqtrdi 2780 . . . . . . . . . . . . . . . . . . 19 ((𝑠 / 2) = 0 → (cos‘(𝑠 / 2)) = 1)
381380ad2antll 726 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ (𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ (𝑠 / 2) = 0)) → (cos‘(𝑠 / 2)) = 1)
382341, 344, 365, 377, 378, 381limcco 25744 . . . . . . . . . . . . . . . . 17 (⊤ → 1 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑠 / 2))) lim 0))
383 ax-1ne0 11175 . . . . . . . . . . . . . . . . . 18 1 ≠ 0
384383a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → 1 ≠ 0)
385305, 306, 340, 382, 384reclimc 44854 . . . . . . . . . . . . . . . 16 (⊤ → (1 / 1) ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) lim 0))
386 1div1e1 11901 . . . . . . . . . . . . . . . 16 (1 / 1) = 1
38766fveq1i 6882 . . . . . . . . . . . . . . . . . . . 20 ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1)‘𝑠)
388 eqidd 2725 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1))
389 eqidd 2725 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → 1 = 1)
390 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 ∈ ((-π(,)π) ∖ {0}))
391 1red 11212 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 1 ∈ ℝ)
392388, 389, 390, 391fvmptd 6995 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1)‘𝑠) = 1)
393387, 392eqtr2id 2777 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 1 = ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠))
394135a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))))
395 oveq1 7408 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑠 → (𝑥 / 2) = (𝑠 / 2))
396395fveq2d 6885 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑠 → (cos‘(𝑥 / 2)) = (cos‘(𝑠 / 2)))
397396adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (cos‘(𝑥 / 2)) = (cos‘(𝑠 / 2)))
398394, 397, 390, 335fvmptd 6995 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠) = (cos‘(𝑠 / 2)))
399398eqcomd 2730 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) = ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠))
400393, 399oveq12d 7419 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (1 / (cos‘(𝑠 / 2))) = (((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) / ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠)))
401400mpteq2ia 5241 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) / ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠)))
402401oveq1i 7411 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) / ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠))) lim 0)
403385, 386, 4023eltr3g 2841 . . . . . . . . . . . . . . 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 25871 . . . . . . . . . . . . . 14 (⊤ → 1 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) lim 0))
405404mptru 1540 . . . . . . . . . . . . 13 1 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) lim 0)
406 eqidd 2725 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
407 simpr 484 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → 𝑥 = 𝑠)
408406, 407, 390, 307fvmptd 6995 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) = 𝑠)
409 eqidd 2725 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
410407oveq1d 7416 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (𝑥 / 2) = (𝑠 / 2))
411410fveq2d 6885 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (sin‘(𝑥 / 2)) = (sin‘(𝑠 / 2)))
412411oveq2d 7417 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (2 · (sin‘(𝑥 / 2))) = (2 · (sin‘(𝑠 / 2))))
41326a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ)
414311resincld 16083 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑠 / 2)) ∈ ℝ)
415413, 414remulcld 11241 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
416409, 412, 390, 415fvmptd 6995 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠) = (2 · (sin‘(𝑠 / 2))))
417408, 416oveq12d 7419 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠)) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
418417mpteq2ia 5241 . . . . . . . . . . . . . 14 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
419418oveq1i 7411 . . . . . . . . . . . . 13 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim 0)
420405, 419eleqtri 2823 . . . . . . . . . . . 12 1 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim 0)
42110oveq1i 7411 . . . . . . . . . . . . . 14 (𝐾 lim 0) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0)
42210feq1i 6698 . . . . . . . . . . . . . . . . . . 19 (𝐾:(-π[,]π)⟶ℂ ↔ (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π[,]π)⟶ℂ)
42314, 422mpbi 229 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π[,]π)⟶ℂ
424423a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π[,]π)⟶ℂ)
425243a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → (-π(,)π) ⊆ (-π[,]π))
426 iccssre 13403 . . . . . . . . . . . . . . . . . . . 20 ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
42739, 38, 426mp2an 689 . . . . . . . . . . . . . . . . . . 19 (-π[,]π) ⊆ ℝ
428427a1i 11 . . . . . . . . . . . . . . . . . 18 (⊤ → (-π[,]π) ⊆ ℝ)
429428, 12sstrdi 3986 . . . . . . . . . . . . . . . . 17 (⊤ → (-π[,]π) ⊆ ℂ)
430 eqid 2724 . . . . . . . . . . . . . . . . 17 ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})) = ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0}))
43139, 35, 36ltleii 11334 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -π ≤ 0
43235, 38, 37ltleii 11334 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ≤ π
43339, 38elicc2i 13387 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (0 ∈ (-π[,]π) ↔ (0 ∈ ℝ ∧ -π ≤ 0 ∧ 0 ≤ π))
43435, 431, 432, 433mpbir3an 1338 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ∈ (-π[,]π)
435159snss 4781 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 ∈ (-π[,]π) ↔ {0} ⊆ (-π[,]π))
436434, 435mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . 25 {0} ⊆ (-π[,]π)
437 ssequn2 4175 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({0} ⊆ (-π[,]π) ↔ ((-π[,]π) ∪ {0}) = (-π[,]π))
438436, 437mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . 24 ((-π[,]π) ∪ {0}) = (-π[,]π)
439438oveq2i 7412 . . . . . . . . . . . . . . . . . . . . . . 23 ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})) = ((TopOpen‘ℂfld) ↾t (-π[,]π))
440 eqid 2724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (topGen‘ran (,)) = (topGen‘ran (,))
44156, 440rerest 24642 . . . . . . . . . . . . . . . . . . . . . . . 24 ((-π[,]π) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (-π[,]π)) = ((topGen‘ran (,)) ↾t (-π[,]π)))
442427, 441ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((TopOpen‘ℂfld) ↾t (-π[,]π)) = ((topGen‘ran (,)) ↾t (-π[,]π))
443439, 442eqtri 2752 . . . . . . . . . . . . . . . . . . . . . 22 ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})) = ((topGen‘ran (,)) ↾t (-π[,]π))
444443fveq2i 6884 . . . . . . . . . . . . . . . . . . . . 21 (int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0}))) = (int‘((topGen‘ran (,)) ↾t (-π[,]π)))
445159snss 4781 . . . . . . . . . . . . . . . . . . . . . . 23 (0 ∈ (-π(,)π) ↔ {0} ⊆ (-π(,)π))
44644, 445mpbi 229 . . . . . . . . . . . . . . . . . . . . . 22 {0} ⊆ (-π(,)π)
447 ssequn2 4175 . . . . . . . . . . . . . . . . . . . . . 22 ({0} ⊆ (-π(,)π) ↔ ((-π(,)π) ∪ {0}) = (-π(,)π))
448446, 447mpbi 229 . . . . . . . . . . . . . . . . . . . . 21 ((-π(,)π) ∪ {0}) = (-π(,)π)
449444, 448fveq12i 6887 . . . . . . . . . . . . . . . . . . . 20 ((int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})))‘((-π(,)π) ∪ {0})) = ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘(-π(,)π))
450 resttopon 22987 . . . . . . . . . . . . . . . . . . . . . . 23 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (-π[,]π) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (-π[,]π)) ∈ (TopOn‘(-π[,]π)))
45160, 427, 450mp2an 689 . . . . . . . . . . . . . . . . . . . . . 22 ((topGen‘ran (,)) ↾t (-π[,]π)) ∈ (TopOn‘(-π[,]π))
452451topontopi 22739 . . . . . . . . . . . . . . . . . . . . 21 ((topGen‘ran (,)) ↾t (-π[,]π)) ∈ Top
453 retop 24600 . . . . . . . . . . . . . . . . . . . . . . . 24 (topGen‘ran (,)) ∈ Top
454 ovex 7434 . . . . . . . . . . . . . . . . . . . . . . . 24 (-π[,]π) ∈ V
455453, 454pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . . 23 ((topGen‘ran (,)) ∈ Top ∧ (-π[,]π) ∈ V)
456 ssid 3996 . . . . . . . . . . . . . . . . . . . . . . . 24 (-π(,)π) ⊆ (-π(,)π)
45733, 243, 4563pm3.2i 1336 . . . . . . . . . . . . . . . . . . . . . . 23 ((-π(,)π) ∈ (topGen‘ran (,)) ∧ (-π(,)π) ⊆ (-π[,]π) ∧ (-π(,)π) ⊆ (-π(,)π))
458 restopnb 23001 . . . . . . . . . . . . . . . . . . . . . . 23 ((((topGen‘ran (,)) ∈ Top ∧ (-π[,]π) ∈ V) ∧ ((-π(,)π) ∈ (topGen‘ran (,)) ∧ (-π(,)π) ⊆ (-π[,]π) ∧ (-π(,)π) ⊆ (-π(,)π))) → ((-π(,)π) ∈ (topGen‘ran (,)) ↔ (-π(,)π) ∈ ((topGen‘ran (,)) ↾t (-π[,]π))))
459455, 457, 458mp2an 689 . . . . . . . . . . . . . . . . . . . . . 22 ((-π(,)π) ∈ (topGen‘ran (,)) ↔ (-π(,)π) ∈ ((topGen‘ran (,)) ↾t (-π[,]π)))
46033, 459mpbi 229 . . . . . . . . . . . . . . . . . . . . 21 (-π(,)π) ∈ ((topGen‘ran (,)) ↾t (-π[,]π))
461 isopn3i 22908 . . . . . . . . . . . . . . . . . . . . 21 ((((topGen‘ran (,)) ↾t (-π[,]π)) ∈ Top ∧ (-π(,)π) ∈ ((topGen‘ran (,)) ↾t (-π[,]π))) → ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘(-π(,)π)) = (-π(,)π))
462452, 460, 461mp2an 689 . . . . . . . . . . . . . . . . . . . 20 ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘(-π(,)π)) = (-π(,)π)
463 eqid 2724 . . . . . . . . . . . . . . . . . . . 20 (-π(,)π) = (-π(,)π)
464449, 462, 4633eqtrri 2757 . . . . . . . . . . . . . . . . . . 19 (-π(,)π) = ((int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})))‘((-π(,)π) ∪ {0}))
46544, 464eleqtri 2823 . . . . . . . . . . . . . . . . . 18 0 ∈ ((int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})))‘((-π(,)π) ∪ {0}))
466465a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → 0 ∈ ((int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})))‘((-π(,)π) ∪ {0})))
467424, 425, 429, 56, 430, 466limcres 25737 . . . . . . . . . . . . . . . 16 (⊤ → (((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (-π(,)π)) lim 0) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0))
468467mptru 1540 . . . . . . . . . . . . . . 15 (((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (-π(,)π)) lim 0) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0)
469468eqcomi 2733 . . . . . . . . . . . . . 14 ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0) = (((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (-π(,)π)) lim 0)
470 resmpt 6027 . . . . . . . . . . . . . . . 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 7411 . . . . . . . . . . . . . 14 (((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (-π(,)π)) lim 0) = ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0)
473421, 469, 4723eqtri 2756 . . . . . . . . . . . . 13 (𝐾 lim 0) = ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0)
474 eqid 2724 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
475 iftrue 4526 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = 1)
476 1cnd 11206 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → 1 ∈ ℂ)
477475, 476eqeltrd 2825 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 0 → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
478477adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (-π(,)π) ∧ 𝑠 = 0) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
479 iffalse 4529 . . . . . . . . . . . . . . . . . . . 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 12287 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → 2 ∈ ℂ)
483481halfcld 12454 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (𝑠 / 2) ∈ ℂ)
484483sincld 16070 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (sin‘(𝑠 / 2)) ∈ ℂ)
485482, 484mulcld 11231 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
48681a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → 2 ≠ 0)
487243sseli 3970 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ (-π(,)π) → 𝑠 ∈ (-π[,]π))
488 neqne 2940 . . . . . . . . . . . . . . . . . . . . . 22 𝑠 = 0 → 𝑠 ≠ 0)
489 fourierdlem44 45352 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
490487, 488, 489syl2an 595 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (sin‘(𝑠 / 2)) ≠ 0)
491482, 484, 486, 490mulne0d 11863 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
492481, 485, 491divcld 11987 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
493480, 492eqeltrd 2825 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
494478, 493pm2.61dan 810 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (-π(,)π) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
495474, 494fmpti 7103 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π(,)π)⟶ℂ
496495a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π(,)π)⟶ℂ)
497496limcdif 25727 . . . . . . . . . . . . . 14 (⊤ → ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0) = (((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π(,)π) ∖ {0})) lim 0))
498497mptru 1540 . . . . . . . . . . . . 13 ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0) = (((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π(,)π) ∖ {0})) lim 0)
499 resmpt 6027 . . . . . . . . . . . . . . . 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 4119 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ¬ 𝑠 ∈ {0})
502 velsn 4636 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ {0} ↔ 𝑠 = 0)
503501, 502sylnib 328 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ¬ 𝑠 = 0)
504503, 479syl 17 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((-π(,)π) ∖ {0}) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
505504mpteq2ia 5241 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
506500, 505eqtri 2752 . . . . . . . . . . . . . 14 ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π(,)π) ∖ {0})) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
507506oveq1i 7411 . . . . . . . . . . . . 13 (((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π(,)π) ∖ {0})) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim 0)
508473, 498, 5073eqtrri 2757 . . . . . . . . . . . 12 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim 0) = (𝐾 lim 0)
509420, 508eleqtri 2823 . . . . . . . . . . 11 1 ∈ (𝐾 lim 0)
510509a1i 11 . . . . . . . . . 10 (𝑠 = 0 → 1 ∈ (𝐾 lim 0))
511 fveq2 6881 . . . . . . . . . . 11 (𝑠 = 0 → (𝐾𝑠) = (𝐾‘0))
512475, 10, 47fvmpt 6988 . . . . . . . . . . . 12 (0 ∈ (-π[,]π) → (𝐾‘0) = 1)
513434, 512ax-mp 5 . . . . . . . . . . 11 (𝐾‘0) = 1
514511, 513eqtrdi 2780 . . . . . . . . . 10 (𝑠 = 0 → (𝐾𝑠) = 1)
515 oveq2 7409 . . . . . . . . . 10 (𝑠 = 0 → (𝐾 lim 𝑠) = (𝐾 lim 0))
516510, 514, 5153eltr4d 2840 . . . . . . . . 9 (𝑠 = 0 → (𝐾𝑠) ∈ (𝐾 lim 𝑠))
517427, 12sstri 3983 . . . . . . . . . . 11 (-π[,]π) ⊆ ℂ
518517a1i 11 . . . . . . . . . 10 (𝑠 = 0 → (-π[,]π) ⊆ ℂ)
51938a1i 11 . . . . . . . . . . . 12 (𝑠 = 0 → π ∈ ℝ)
520519renegcld 11638 . . . . . . . . . . 11 (𝑠 = 0 → -π ∈ ℝ)
521 id 22 . . . . . . . . . . . 12 (𝑠 = 0 → 𝑠 = 0)
52235a1i 11 . . . . . . . . . . . 12 (𝑠 = 0 → 0 ∈ ℝ)
523521, 522eqeltrd 2825 . . . . . . . . . . 11 (𝑠 = 0 → 𝑠 ∈ ℝ)
524431, 521breqtrrid 5176 . . . . . . . . . . 11 (𝑠 = 0 → -π ≤ 𝑠)
525521, 432eqbrtrdi 5177 . . . . . . . . . . 11 (𝑠 = 0 → 𝑠 ≤ π)
526520, 519, 523, 524, 525eliccd 44702 . . . . . . . . . 10 (𝑠 = 0 → 𝑠 ∈ (-π[,]π))
52757oveq1i 7411 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t (-π[,]π)) = (((TopOpen‘ℂfld) ↾t ℝ) ↾t (-π[,]π))
52856cnfldtop 24622 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) ∈ Top
529 reex 11197 . . . . . . . . . . . . 13 ℝ ∈ V
530 restabs 22991 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ∈ Top ∧ (-π[,]π) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂfld) ↾t ℝ) ↾t (-π[,]π)) = ((TopOpen‘ℂfld) ↾t (-π[,]π)))
531528, 427, 529, 530mp3an 1457 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ↾t ℝ) ↾t (-π[,]π)) = ((TopOpen‘ℂfld) ↾t (-π[,]π))
532527, 531eqtri 2752 . . . . . . . . . . 11 ((topGen‘ran (,)) ↾t (-π[,]π)) = ((TopOpen‘ℂfld) ↾t (-π[,]π))
53356, 532cnplimc 25738 . . . . . . . . . 10 (((-π[,]π) ⊆ ℂ ∧ 𝑠 ∈ (-π[,]π)) → (𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠) ↔ (𝐾:(-π[,]π)⟶ℂ ∧ (𝐾𝑠) ∈ (𝐾 lim 𝑠))))
534518, 526, 533syl2anc 583 . . . . . . . . 9 (𝑠 = 0 → (𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠) ↔ (𝐾:(-π[,]π)⟶ℂ ∧ (𝐾𝑠) ∈ (𝐾 lim 𝑠))))
53515, 516, 534mpbir2and 710 . . . . . . . 8 (𝑠 = 0 → 𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))
536535adantl 481 . . . . . . 7 ((𝑠 ∈ (-π[,]π) ∧ 𝑠 = 0) → 𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))
537 simpl 482 . . . . . . . . . . 11 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ (-π[,]π))
538502notbii 320 . . . . . . . . . . . . 13 𝑠 ∈ {0} ↔ ¬ 𝑠 = 0)
539538biimpri 227 . . . . . . . . . . . 12 𝑠 = 0 → ¬ 𝑠 ∈ {0})
540539adantl 481 . . . . . . . . . . 11 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → ¬ 𝑠 ∈ {0})
541537, 540eldifd 3951 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ((-π[,]π) ∖ {0}))
542 fveq2 6881 . . . . . . . . . . . 12 (𝑥 = 𝑠 → ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥) = ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠))
543542eleq2d 2811 . . . . . . . . . . 11 (𝑥 = 𝑠 → ((𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥) ↔ (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠)))
544429ssdifssd 4134 . . . . . . . . . . . . . . . . 17 (⊤ → ((-π[,]π) ∖ {0}) ⊆ ℂ)
545544, 145idcncfg 45074 . . . . . . . . . . . . . . . 16 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ 𝑠) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
546 eqid 2724 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2))))
547 2cnd 12287 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 2 ∈ ℂ)
548 eldifi 4118 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 𝑠 ∈ (-π[,]π))
549517, 548sselid 3972 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 𝑠 ∈ ℂ)
550549halfcld 12454 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (𝑠 / 2) ∈ ℂ)
551550sincld 16070 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (sin‘(𝑠 / 2)) ∈ ℂ)
552547, 551mulcld 11231 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
55381a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 2 ≠ 0)
554 eldifsni 4785 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 𝑠 ≠ 0)
555548, 554, 489syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (sin‘(𝑠 / 2)) ≠ 0)
556547, 551, 553, 555mulne0d 11863 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
557556neneqd 2937 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π[,]π) ∖ {0}) → ¬ (2 · (sin‘(𝑠 / 2))) = 0)
558 elsng 4634 . . . . . . . . . . . . . . . . . . . . . 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 325 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π[,]π) ∖ {0}) → ¬ (2 · (sin‘(𝑠 / 2))) ∈ {0})
561552, 560eldifd 3951 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
562546, 561fmpti 7103 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))):((-π[,]π) ∖ {0})⟶(ℂ ∖ {0})
563 difss 4123 . . . . . . . . . . . . . . . . . . 19 (ℂ ∖ {0}) ⊆ ℂ
564 eqid 2724 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ℂ ↦ 2) = (𝑠 ∈ ℂ ↦ 2)
565175, 176, 175constcncfg 45073 . . . . . . . . . . . . . . . . . . . . . . 23 (2 ∈ ℂ → (𝑠 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
566102, 565mp1i 13 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑠 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
567 2cnd 12287 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑠 ∈ ((-π[,]π) ∖ {0})) → 2 ∈ ℂ)
568564, 566, 544, 145, 567cncfmptssg 45072 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ 2) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
569549, 547, 553divrecd 11990 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (𝑠 / 2) = (𝑠 · (1 / 2)))
570569mpteq2ia 5241 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / 2)) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 · (1 / 2)))
571 eqid 2724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ℂ ↦ (1 / 2)) = (𝑠 ∈ ℂ ↦ (1 / 2))
572144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 / 2) ∈ ℂ → ℂ ⊆ ℂ)
573 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 / 2) ∈ ℂ → (1 / 2) ∈ ℂ)
574572, 573, 572constcncfg 45073 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 / 2) ∈ ℂ → (𝑠 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
57594, 574mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⊤ → (𝑠 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
57694a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⊤ ∧ 𝑠 ∈ ((-π[,]π) ∖ {0})) → (1 / 2) ∈ ℂ)
577571, 575, 544, 145, 576cncfmptssg 45072 . . . . . . . . . . . . . . . . . . . . . . . 24 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (1 / 2)) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
578545, 577mulcncf 25296 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 · (1 / 2))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
579570, 578eqeltrid 2829 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / 2)) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
580182, 579cncfmpt1f 24756 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (sin‘(𝑠 / 2))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
581568, 580mulcncf 25296 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
582581mptru 1540 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ)
583 cncfcdm 24740 . . . . . . . . . . . . . . . . . . 19 (((ℂ ∖ {0}) ⊆ ℂ ∧ (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ)) → ((𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))):((-π[,]π) ∖ {0})⟶(ℂ ∖ {0})))
584563, 582, 583mp2an 689 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))):((-π[,]π) ∖ {0})⟶(ℂ ∖ {0}))
585562, 584mpbir 230 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→(ℂ ∖ {0}))
586585a1i 11 . . . . . . . . . . . . . . . 16 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→(ℂ ∖ {0})))
587545, 586divcncf 25298 . . . . . . . . . . . . . . 15 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
588587mptru 1540 . . . . . . . . . . . . . 14 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ)
589428ssdifssd 4134 . . . . . . . . . . . . . . . . 17 (⊤ → ((-π[,]π) ∖ {0}) ⊆ ℝ)
590589mptru 1540 . . . . . . . . . . . . . . . 16 ((-π[,]π) ∖ {0}) ⊆ ℝ
591590, 12sstri 3983 . . . . . . . . . . . . . . 15 ((-π[,]π) ∖ {0}) ⊆ ℂ
59257oveq1i 7411 . . . . . . . . . . . . . . . . 17 ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) = (((TopOpen‘ℂfld) ↾t ℝ) ↾t ((-π[,]π) ∖ {0}))
593 restabs 22991 . . . . . . . . . . . . . . . . . 18 (((TopOpen‘ℂfld) ∈ Top ∧ ((-π[,]π) ∖ {0}) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂfld) ↾t ℝ) ↾t ((-π[,]π) ∖ {0})) = ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∖ {0})))
594528, 590, 529, 593mp3an 1457 . . . . . . . . . . . . . . . . 17 (((TopOpen‘ℂfld) ↾t ℝ) ↾t ((-π[,]π) ∖ {0})) = ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∖ {0}))
595592, 594eqtri 2752 . . . . . . . . . . . . . . . 16 ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) = ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∖ {0}))
596 unicntop 24624 . . . . . . . . . . . . . . . . . . 19 ℂ = (TopOpen‘ℂfld)
597596restid 17378 . . . . . . . . . . . . . . . . . 18 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
598528, 597ax-mp 5 . . . . . . . . . . . . . . . . 17 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
599598eqcomi 2733 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
60056, 595, 599cncfcn 24752 . . . . . . . . . . . . . . 15 ((((-π[,]π) ∖ {0}) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (((-π[,]π) ∖ {0})–cn→ℂ) = (((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) Cn (TopOpen‘ℂfld)))
601591, 144, 600mp2an 689 . . . . . . . . . . . . . 14 (((-π[,]π) ∖ {0})–cn→ℂ) = (((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) Cn (TopOpen‘ℂfld))
602588, 601eleqtri 2823 . . . . . . . . . . . . 13 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) Cn (TopOpen‘ℂfld))
603 resttopon 22987 . . . . . . . . . . . . . . 15 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((-π[,]π) ∖ {0}) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) ∈ (TopOn‘((-π[,]π) ∖ {0})))
60460, 590, 603mp2an 689 . . . . . . . . . . . . . 14 ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) ∈ (TopOn‘((-π[,]π) ∖ {0}))
60556cnfldtopon 24621 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
606 cncnp 23106 . . . . . . . . . . . . . 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 689 . . . . . . . . . . . . 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 229 . . . . . . . . . . . 12 ((𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))):((-π[,]π) ∖ {0})⟶ℂ ∧ ∀𝑥 ∈ ((-π[,]π) ∖ {0})(𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥))
609608simpri 485 . . . . . . . . . . 11 𝑥 ∈ ((-π[,]π) ∖ {0})(𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥)
610543, 609vtoclri 3568 . . . . . . . . . 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 5967 . . . . . . . . . 10 (𝐾 ↾ ((-π[,]π) ∖ {0})) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π[,]π) ∖ {0}))
613 difss 4123 . . . . . . . . . . 11 ((-π[,]π) ∖ {0}) ⊆ (-π[,]π)
614 resmpt 6027 . . . . . . . . . . 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 4119 . . . . . . . . . . . . 13 (𝑠 ∈ ((-π[,]π) ∖ {0}) → ¬ 𝑠 ∈ {0})
617616, 502sylnib 328 . . . . . . . . . . . 12 (𝑠 ∈ ((-π[,]π) ∖ {0}) → ¬ 𝑠 = 0)
618617, 479syl 17 . . . . . . . . . . 11 (𝑠 ∈ ((-π[,]π) ∖ {0}) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
619618mpteq2ia 5241 . . . . . . . . . 10 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
620612, 615, 6193eqtri 2756 . . . . . . . . 9 (𝐾 ↾ ((-π[,]π) ∖ {0})) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
621 restabs 22991 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ Top ∧ ((-π[,]π) ∖ {0}) ⊆ (-π[,]π) ∧ (-π[,]π) ∈ V) → (((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) = ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})))
622453, 613, 454, 621mp3an 1457 . . . . . . . . . . 11 (((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) = ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0}))
623622oveq1i 7411 . . . . . . . . . 10 ((((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld)) = (((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))
624623fveq1i 6882 . . . . . . . . 9 (((((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠) = ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠)
625611, 620, 6243eltr4g 2842 . . . . . . . 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 4131 . . . . . . . . . . . . . 14 ((-π[,]π) ⊆ ℝ → ((-π[,]π) ∖ {0}) ⊆ (ℝ ∖ {0}))
629427, 628ax-mp 5 . . . . . . . . . . . . 13 ((-π[,]π) ∖ {0}) ⊆ (ℝ ∖ {0})
630629, 541sselid 3972 . . . . . . . . . . . 12 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ (ℝ ∖ {0}))
631 sscon 4130 . . . . . . . . . . . . . . . . 17 ({0} ⊆ (-π[,]π) → (ℝ ∖ (-π[,]π)) ⊆ (ℝ ∖ {0}))
632436, 631ax-mp 5 . . . . . . . . . . . . . . . 16 (ℝ ∖ (-π[,]π)) ⊆ (ℝ ∖ {0})
633629, 632unssi 4177 . . . . . . . . . . . . . . 15 (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))) ⊆ (ℝ ∖ {0})
634 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (-π[,]π))
635 eldifn 4119 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (ℝ ∖ {0}) → ¬ 𝑠 ∈ {0})
636635adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ (-π[,]π)) → ¬ 𝑠 ∈ {0})
637634, 636eldifd 3951 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ ((-π[,]π) ∖ {0}))
638 elun1 4168 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
639637, 638syl 17 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
640 eldifi 4118 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (ℝ ∖ {0}) → 𝑠 ∈ ℝ)
641640adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ ℝ)
642 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ (-π[,]π)) → ¬ 𝑠 ∈ (-π[,]π))
643641, 642eldifd 3951 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (ℝ ∖ (-π[,]π)))
644 elun2 4169 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (ℝ ∖ (-π[,]π)) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
645643, 644syl 17 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
646639, 645pm2.61dan 810 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (ℝ ∖ {0}) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
647646ssriv 3978 . . . . . . . . . . . . . . 15 (ℝ ∖ {0}) ⊆ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))
648633, 647eqssi 3990 . . . . . . . . . . . . . 14 (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))) = (ℝ ∖ {0})
649648fveq2i 6884 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) = ((int‘(topGen‘ran (,)))‘(ℝ ∖ {0}))
65061cldopn 22857 . . . . . . . . . . . . . . 15 ({0} ∈ (Clsd‘(topGen‘ran (,))) → (ℝ ∖ {0}) ∈ (topGen‘ran (,)))
65159, 650ax-mp 5 . . . . . . . . . . . . . 14 (ℝ ∖ {0}) ∈ (topGen‘ran (,))
652 isopn3i 22908 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ Top ∧ (ℝ ∖ {0}) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘(ℝ ∖ {0})) = (ℝ ∖ {0}))
653453, 651, 652mp2an 689 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘(ℝ ∖ {0})) = (ℝ ∖ {0})
654649, 653eqtri 2752 . . . . . . . . . . . 12 ((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) = (ℝ ∖ {0})
655630, 654eleqtrrdi 2836 . . . . . . . . . . 11 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))))
656655, 537elind 4186 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ (((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) ∩ (-π[,]π)))
657 eqid 2724 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t (-π[,]π)) = ((topGen‘ran (,)) ↾t (-π[,]π))
65861, 657restntr 23008 . . . . . . . . . . 11 (((topGen‘ran (,)) ∈ Top ∧ (-π[,]π) ⊆ ℝ ∧ ((-π[,]π) ∖ {0}) ⊆ (-π[,]π)) → ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘((-π[,]π) ∖ {0})) = (((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) ∩ (-π[,]π)))
659453, 427, 613, 658mp3an 1457 . . . . . . . . . 10 ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘((-π[,]π) ∖ {0})) = (((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) ∩ (-π[,]π))
660656, 659eleqtrrdi 2836 . . . . . . . . 9 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘((-π[,]π) ∖ {0})))
66114a1i 11 . . . . . . . . 9 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝐾:(-π[,]π)⟶ℂ)
662451toponunii 22740 . . . . . . . . . 10 (-π[,]π) = ((topGen‘ran (,)) ↾t (-π[,]π))
663662, 596cnprest 23115 . . . . . . . . 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 834 . . . . . . . 8 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → (𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠) ↔ (𝐾 ↾ ((-π[,]π) ∖ {0})) ∈ (((((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠)))
665625, 664mpbird 257 . . . . . . 7 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))
666536, 665pm2.61dan 810 . . . . . 6 (𝑠 ∈ (-π[,]π) → 𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))
667666rgen 3055 . . . . 5 𝑠 ∈ (-π[,]π)𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠)
668 cncnp 23106 . . . . . 6 ((((topGen‘ran (,)) ↾t (-π[,]π)) ∈ (TopOn‘(-π[,]π)) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → (𝐾 ∈ (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld)) ↔ (𝐾:(-π[,]π)⟶ℂ ∧ ∀𝑠 ∈ (-π[,]π)𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))))
669451, 605, 668mp2an 689 . . . . 5 (𝐾 ∈ (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld)) ↔ (𝐾:(-π[,]π)⟶ℂ ∧ ∀𝑠 ∈ (-π[,]π)𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠)))
67014, 667, 669mpbir2an 708 . . . 4 𝐾 ∈ (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld))
67156, 532, 599cncfcn 24752 . . . . . 6 (((-π[,]π) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((-π[,]π)–cn→ℂ) = (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld)))
672517, 144, 671mp2an 689 . . . . 5 ((-π[,]π)–cn→ℂ) = (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld))
673672eqcomi 2733 . . . 4 (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld)) = ((-π[,]π)–cn→ℂ)
674670, 673eleqtri 2823 . . 3 𝐾 ∈ ((-π[,]π)–cn→ℂ)
675 cncfcdm 24740 . . 3 ((ℝ ⊆ ℂ ∧ 𝐾 ∈ ((-π[,]π)–cn→ℂ)) → (𝐾 ∈ ((-π[,]π)–cn→ℝ) ↔ 𝐾:(-π[,]π)⟶ℝ))
67612, 674, 675mp2an 689 . 2 (𝐾 ∈ ((-π[,]π)–cn→ℝ) ↔ 𝐾:(-π[,]π)⟶ℝ)
67711, 676mpbir 230 1 𝐾 ∈ ((-π[,]π)–cn→ℝ)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 395  w3a 1084   = wceq 1533  wtru 1534  wcel 2098  wne 2932  wral 3053  wrex 3062  Vcvv 3466  cdif 3937  cun 3938  cin 3939  wss 3940  ifcif 4520  {csn 4620  {cpr 4622   class class class wbr 5138  cmpt 5221  dom cdm 5666  ran crn 5667  cres 5668  cima 5669   Fn wfn 6528  wf 6529  cfv 6533  (class class class)co 7401  cc 11104  cr 11105  0cc0 11106  1c1 11107   · cmul 11111  *cxr 11244   < clt 11245  cle 11246  -cneg 11442   / cdiv 11868  2c2 12264  +crp 12971  (,)cioo 13321  [,]cicc 13324  cre 15041  sincsin 16004  cosccos 16005  πcpi 16007  t crest 17365  TopOpenctopn 17366  topGenctg 17382  fldccnfld 21228  Topctop 22717  TopOnctopon 22734  Clsdccld 22842  intcnt 22843   Cn ccn 23050   CnP ccnp 23051  cnccncf 24718   lim climc 25713   D cdv 25714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ioc 13326  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-mod 13832  df-seq 13964  df-exp 14025  df-fac 14231  df-bc 14260  df-hash 14288  df-shft 15011  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-limsup 15412  df-clim 15429  df-rlim 15430  df-sum 15630  df-ef 16008  df-sin 16010  df-cos 16011  df-pi 16013  df-struct 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-rest 17367  df-topn 17368  df-0g 17386  df-gsum 17387  df-topgen 17388  df-pt 17389  df-prds 17392  df-xrs 17447  df-qtop 17452  df-imas 17453  df-xps 17455  df-mre 17529  df-mrc 17530  df-acs 17532  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-submnd 18704  df-mulg 18986  df-cntz 19223  df-cmn 19692  df-psmet 21220  df-xmet 21221  df-met 21222  df-bl 21223  df-mopn 21224  df-fbas 21225  df-fg 21226  df-cnfld 21229  df-top 22718  df-topon 22735  df-topsp 22757  df-bases 22771  df-cld 22845  df-ntr 22846  df-cls 22847  df-nei 22924  df-lp 22962  df-perf 22963  df-cn 23053  df-cnp 23054  df-t1 23140  df-haus 23141  df-cmp 23213  df-tx 23388  df-hmeo 23581  df-fil 23672  df-fm 23764  df-flim 23765  df-flf 23766  df-xms 24148  df-ms 24149  df-tms 24150  df-cncf 24720  df-limc 25717  df-dv 25718
This theorem is referenced by:  fourierdlem77  45384  fourierdlem78  45385  fourierdlem85  45392  fourierdlem88  45395
  Copyright terms: Public domain W3C validator