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 46123
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 2738 . . . . . 6 (𝑦 = 𝑠 → (𝑦 = 0 ↔ 𝑠 = 0))
3 id 22 . . . . . . 7 (𝑦 = 𝑠𝑦 = 𝑠)
4 oveq1 7437 . . . . . . . . 9 (𝑦 = 𝑠 → (𝑦 / 2) = (𝑠 / 2))
54fveq2d 6910 . . . . . . . 8 (𝑦 = 𝑠 → (sin‘(𝑦 / 2)) = (sin‘(𝑠 / 2)))
65oveq2d 7446 . . . . . . 7 (𝑦 = 𝑠 → (2 · (sin‘(𝑦 / 2))) = (2 · (sin‘(𝑠 / 2))))
73, 6oveq12d 7448 . . . . . 6 (𝑦 = 𝑠 → (𝑦 / (2 · (sin‘(𝑦 / 2)))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
82, 7ifbieq2d 4556 . . . . 5 (𝑦 = 𝑠 → if(𝑦 = 0, 1, (𝑦 / (2 · (sin‘(𝑦 / 2))))) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
98cbvmptv 5260 . . . 4 (𝑦 ∈ (-π[,]π) ↦ if(𝑦 = 0, 1, (𝑦 / (2 · (sin‘(𝑦 / 2)))))) = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
101, 9eqtri 2762 . . 3 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
1110fourierdlem43 46105 . 2 𝐾:(-π[,]π)⟶ℝ
12 ax-resscn 11209 . . 3 ℝ ⊆ ℂ
13 fss 6752 . . . . . 6 ((𝐾:(-π[,]π)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐾:(-π[,]π)⟶ℂ)
1411, 12, 13mp2an 692 . . . . 5 𝐾:(-π[,]π)⟶ℂ
1514a1i 11 . . . . . . . . 9 (𝑠 = 0 → 𝐾:(-π[,]π)⟶ℂ)
16 difss 4145 . . . . . . . . . . . . . . . . 17 ((-π(,)π) ∖ {0}) ⊆ (-π(,)π)
17 elioore 13413 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (-π(,)π) → 𝑠 ∈ ℝ)
1817ssriv 3998 . . . . . . . . . . . . . . . . 17 (-π(,)π) ⊆ ℝ
1916, 18sstri 4004 . . . . . . . . . . . . . . . 16 ((-π(,)π) ∖ {0}) ⊆ ℝ
2019a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ((-π(,)π) ∖ {0}) ⊆ ℝ)
21 eqid 2734 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)
2219sseli 3990 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-π(,)π) ∖ {0}) → 𝑥 ∈ ℝ)
2321, 22fmpti 7131 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥):((-π(,)π) ∖ {0})⟶ℝ
2423a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥):((-π(,)π) ∖ {0})⟶ℝ)
25 eqid 2734 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))
26 2re 12337 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℝ
2726a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ)
2822rehalfcld 12510 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) → (𝑥 / 2) ∈ ℝ)
2928resincld 16175 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑥 / 2)) ∈ ℝ)
3027, 29remulcld 11288 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-π(,)π) ∖ {0}) → (2 · (sin‘(𝑥 / 2))) ∈ ℝ)
3125, 30fmpti 7131 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))):((-π(,)π) ∖ {0})⟶ℝ
3231a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))):((-π(,)π) ∖ {0})⟶ℝ)
33 iooretop 24801 . . . . . . . . . . . . . . . 16 (-π(,)π) ∈ (topGen‘ran (,))
3433a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (-π(,)π) ∈ (topGen‘ran (,)))
35 0re 11260 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
36 negpilt0 45230 . . . . . . . . . . . . . . . . 17 -π < 0
37 pipos 26516 . . . . . . . . . . . . . . . . 17 0 < π
38 pire 26514 . . . . . . . . . . . . . . . . . . . 20 π ∈ ℝ
3938renegcli 11567 . . . . . . . . . . . . . . . . . . 19 -π ∈ ℝ
4039rexri 11316 . . . . . . . . . . . . . . . . . 18 -π ∈ ℝ*
4138rexri 11316 . . . . . . . . . . . . . . . . . 18 π ∈ ℝ*
42 elioo2 13424 . . . . . . . . . . . . . . . . . 18 ((-π ∈ ℝ* ∧ π ∈ ℝ*) → (0 ∈ (-π(,)π) ↔ (0 ∈ ℝ ∧ -π < 0 ∧ 0 < π)))
4340, 41, 42mp2an 692 . . . . . . . . . . . . . . . . 17 (0 ∈ (-π(,)π) ↔ (0 ∈ ℝ ∧ -π < 0 ∧ 0 < π))
4435, 36, 37, 43mpbir3an 1340 . . . . . . . . . . . . . . . 16 0 ∈ (-π(,)π)
4544a1i 11 . . . . . . . . . . . . . . 15 (⊤ → 0 ∈ (-π(,)π))
46 eqid 2734 . . . . . . . . . . . . . . 15 ((-π(,)π) ∖ {0}) = ((-π(,)π) ∖ {0})
47 1ex 11254 . . . . . . . . . . . . . . . . . . 19 1 ∈ V
48 eqid 2734 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1)
4947, 48dmmpti 6712 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = ((-π(,)π) ∖ {0})
50 reelprrecn 11244 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ ∈ {ℝ, ℂ}
5150a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ℝ ∈ {ℝ, ℂ})
5212sseli 3990 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
5352adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
54 1red 11259 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
5551dvmptid 26009 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
56 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . 23 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
5756tgioo2 24838 . . . . . . . . . . . . . . . . . . . . . 22 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
58 sncldre 44981 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 ∈ ℝ → {0} ∈ (Clsd‘(topGen‘ran (,))))
5935, 58ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 {0} ∈ (Clsd‘(topGen‘ran (,)))
60 retopon 24799 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
6160toponunii 22937 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℝ = (topGen‘ran (,))
6261difopn 23057 . . . . . . . . . . . . . . . . . . . . . . . 24 (((-π(,)π) ∈ (topGen‘ran (,)) ∧ {0} ∈ (Clsd‘(topGen‘ran (,)))) → ((-π(,)π) ∖ {0}) ∈ (topGen‘ran (,)))
6333, 59, 62mp2an 692 . . . . . . . . . . . . . . . . . . . . . . 23 ((-π(,)π) ∖ {0}) ∈ (topGen‘ran (,))
6463a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ((-π(,)π) ∖ {0}) ∈ (topGen‘ran (,)))
6551, 53, 54, 55, 20, 57, 56, 64dvmptres 26015 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1))
6665mptru 1543 . . . . . . . . . . . . . . . . . . . 20 (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1)
6766eqcomi 2743 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
6867dmeqi 5917 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
6949, 68eqtr3i 2764 . . . . . . . . . . . . . . . . 17 ((-π(,)π) ∖ {0}) = dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
7069eqimssi 4055 . . . . . . . . . . . . . . . 16 ((-π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
7170a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ((-π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)))
72 fvex 6919 . . . . . . . . . . . . . . . . . . 19 (cos‘(𝑥 / 2)) ∈ V
73 eqid 2734 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))
7472, 73dmmpti 6712 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = ((-π(,)π) ∖ {0})
75 2cnd 12341 . . . . . . . . . . . . . . . . . . . . . . 23 ((⊤ ∧ 𝑥 ∈ ℝ) → 2 ∈ ℂ)
7653halfcld 12508 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⊤ ∧ 𝑥 ∈ ℝ) → (𝑥 / 2) ∈ ℂ)
7776sincld 16162 . . . . . . . . . . . . . . . . . . . . . . 23 ((⊤ ∧ 𝑥 ∈ ℝ) → (sin‘(𝑥 / 2)) ∈ ℂ)
7875, 77mulcld 11278 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → (2 · (sin‘(𝑥 / 2))) ∈ ℂ)
7976coscld 16163 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → (cos‘(𝑥 / 2)) ∈ ℂ)
80 2cnd 12341 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → 2 ∈ ℂ)
81 2ne0 12367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 2 ≠ 0
8281a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → 2 ≠ 0)
8352, 80, 82divrec2d 12044 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → (𝑥 / 2) = ((1 / 2) · 𝑥))
8483fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℝ → (sin‘(𝑥 / 2)) = (sin‘((1 / 2) · 𝑥)))
8584oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ → (2 · (sin‘(𝑥 / 2))) = (2 · (sin‘((1 / 2) · 𝑥))))
8685mpteq2ia 5250 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))
8786oveq2i 7441 . . . . . . . . . . . . . . . . . . . . . . . 24 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2))))) = (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))
88 resmpt 6056 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℝ ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))
8912, 88ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))
9089eqcomi 2743 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) = ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ)
9190oveq2i 7441 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (ℝ D ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ))
92 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) = (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))
93 2cnd 12341 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℂ → 2 ∈ ℂ)
94 halfcn 12478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (1 / 2) ∈ ℂ
9594a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℂ → (1 / 2) ∈ ℂ)
96 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℂ → 𝑥 ∈ ℂ)
9795, 96mulcld 11278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℂ → ((1 / 2) · 𝑥) ∈ ℂ)
9897sincld 16162 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℂ → (sin‘((1 / 2) · 𝑥)) ∈ ℂ)
9993, 98mulcld 11278 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℂ → (2 · (sin‘((1 / 2) · 𝑥))) ∈ ℂ)
10092, 99fmpti 7131 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))):ℂ⟶ℂ
101 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
102 2cn 12338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2 ∈ ℂ
103102, 94mulcli 11265 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (2 · (1 / 2)) ∈ ℂ
104103a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ ℂ → (2 · (1 / 2)) ∈ ℂ)
10597coscld 16163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ ℂ → (cos‘((1 / 2) · 𝑥)) ∈ ℂ)
106104, 105mulcld 11278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ ℂ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) ∈ ℂ)
107106adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((⊤ ∧ 𝑥 ∈ ℂ) → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) ∈ ℂ)
108101, 107dmmptd 6713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⊤ → dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = ℂ)
109108mptru 1543 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = ℂ
11012, 109sseqtrri 4032 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℝ ⊆ dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
111 dvasinbx 45875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))))
112102, 94, 111mp2an 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
113112dmeqi 5917 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 dom (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
114110, 113sseqtrri 4032 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℝ ⊆ dom (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))
115 dvcnre 45871 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))):ℂ⟶ℂ ∧ ℝ ⊆ dom (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))) → (ℝ D ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ)) = ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ))
116100, 114, 115mp2an 692 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℝ D ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ)) = ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ)
117112reseq1i 5995 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ) = ((𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) ↾ ℝ)
118 resmpt 6056 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (2 · (1 / 2)) = 1
121120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → (2 · (1 / 2)) = 1)
12283eqcomd 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℝ → ((1 / 2) · 𝑥) = (𝑥 / 2))
123122fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → (cos‘((1 / 2) · 𝑥)) = (cos‘(𝑥 / 2)))
124121, 123oveq12d 7448 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) = (1 · (cos‘(𝑥 / 2))))
12552halfcld 12508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℝ → (𝑥 / 2) ∈ ℂ)
126125coscld 16163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → (cos‘(𝑥 / 2)) ∈ ℂ)
127126mullidd 11276 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → (1 · (cos‘(𝑥 / 2))) = (cos‘(𝑥 / 2)))
128124, 127eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℝ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) = (cos‘(𝑥 / 2)))
129128mpteq2ia 5250 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
130117, 119, 1293eqtri 2766 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
13191, 116, 1303eqtri 2766 . . . . . . . . . . . . . . . . . . . . . . . 24 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
13287, 131eqtri 2762 . . . . . . . . . . . . . . . . . . . . . . 23 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
133132a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2))))
13451, 78, 79, 133, 20, 57, 56, 64dvmptres 26015 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))))
135134mptru 1543 . . . . . . . . . . . . . . . . . . . 20 (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))
136135eqcomi 2743 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
137136dmeqi 5917 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
13874, 137eqtr3i 2764 . . . . . . . . . . . . . . . . 17 ((-π(,)π) ∖ {0}) = dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
139138eqimssi 4055 . . . . . . . . . . . . . . . 16 ((-π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
140139a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ((-π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))))
14117recnd 11286 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (-π(,)π) → 𝑠 ∈ ℂ)
142141ssriv 3998 . . . . . . . . . . . . . . . . . . . . . . 23 (-π(,)π) ⊆ ℂ
143142a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (-π(,)π) ⊆ ℂ)
144 ssid 4017 . . . . . . . . . . . . . . . . . . . . . . 23 ℂ ⊆ ℂ
145144a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ℂ ⊆ ℂ)
146143, 145idcncfg 45828 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑥 ∈ (-π(,)π) ↦ 𝑥) ∈ ((-π(,)π)–cn→ℂ))
147146mptru 1543 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (-π(,)π) ↦ 𝑥) ∈ ((-π(,)π)–cn→ℂ)
148 cnlimc 25937 . . . . . . . . . . . . . . . . . . . . 21 ((-π(,)π) ⊆ ℂ → ((𝑥 ∈ (-π(,)π) ↦ 𝑥) ∈ ((-π(,)π)–cn→ℂ) ↔ ((𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦))))
149142, 148ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (-π(,)π) ↦ 𝑥) ∈ ((-π(,)π)–cn→ℂ) ↔ ((𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦)))
150147, 149mpbi 230 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦))
151150simpri 485 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦)
152 fveq2 6906 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) = ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0))
153 oveq2 7438 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦) = ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0))
154152, 153eleq12d 2832 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 0 → (((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦) ↔ ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0)))
155154rspccva 3620 . . . . . . . . . . . . . . . . . 18 ((∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦) ∧ 0 ∈ (-π(,)π)) → ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0))
156151, 44, 155mp2an 692 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0)
157 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → 𝑥 = 0)
158 eqid 2734 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (-π(,)π) ↦ 𝑥) = (𝑥 ∈ (-π(,)π) ↦ 𝑥)
159 c0ex 11252 . . . . . . . . . . . . . . . . . . 19 0 ∈ V
160157, 158, 159fvmpt 7015 . . . . . . . . . . . . . . . . . 18 (0 ∈ (-π(,)π) → ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) = 0)
16144, 160ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) = 0
162 elioore 13413 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (-π(,)π) → 𝑥 ∈ ℝ)
163162recnd 11286 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (-π(,)π) → 𝑥 ∈ ℂ)
164158, 163fmpti 7131 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ
165164a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ)
166165limcdif 25925 . . . . . . . . . . . . . . . . . . 19 (⊤ → ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0) = (((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) lim 0))
167166mptru 1543 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0) = (((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) lim 0)
168 resmpt 6056 . . . . . . . . . . . . . . . . . . . 20 (((-π(,)π) ∖ {0}) ⊆ (-π(,)π) → ((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
16916, 168ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)
170169oveq1i 7440 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) lim 0) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) lim 0)
171167, 170eqtri 2762 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) lim 0)
172156, 161, 1713eltr3i 2850 . . . . . . . . . . . . . . . 16 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) lim 0)
173172a1i 11 . . . . . . . . . . . . . . 15 (⊤ → 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) lim 0))
174 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℂ ↦ 2) = (𝑥 ∈ ℂ ↦ 2)
175144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 ∈ ℂ → ℂ ⊆ ℂ)
176 2cnd 12341 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 ∈ ℂ → 2 ∈ ℂ)
177175, 176, 175constcncfg 45827 . . . . . . . . . . . . . . . . . . . . . . . 24 (2 ∈ ℂ → (𝑥 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
178102, 177mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → (𝑥 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
179 2cnd 12341 . . . . . . . . . . . . . . . . . . . . . . 23 ((⊤ ∧ 𝑥 ∈ (-π(,)π)) → 2 ∈ ℂ)
180174, 178, 143, 145, 179cncfmptssg 45826 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑥 ∈ (-π(,)π) ↦ 2) ∈ ((-π(,)π)–cn→ℂ))
181 sincn 26502 . . . . . . . . . . . . . . . . . . . . . . . 24 sin ∈ (ℂ–cn→ℂ)
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → sin ∈ (ℂ–cn→ℂ))
183 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℂ ↦ (𝑥 / 2)) = (𝑥 ∈ ℂ ↦ (𝑥 / 2))
184183divccncf 24945 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ (ℂ–cn→ℂ))
185102, 81, 184mp2an 692 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ (ℂ–cn→ℂ)
186185a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (⊤ → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ (ℂ–cn→ℂ))
187163adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⊤ ∧ 𝑥 ∈ (-π(,)π)) → 𝑥 ∈ ℂ)
188187halfcld 12508 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⊤ ∧ 𝑥 ∈ (-π(,)π)) → (𝑥 / 2) ∈ ℂ)
189183, 186, 143, 145, 188cncfmptssg 45826 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → (𝑥 ∈ (-π(,)π) ↦ (𝑥 / 2)) ∈ ((-π(,)π)–cn→ℂ))
190182, 189cncfmpt1f 24953 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑥 ∈ (-π(,)π) ↦ (sin‘(𝑥 / 2))) ∈ ((-π(,)π)–cn→ℂ))
191180, 190mulcncf 25493 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ∈ ((-π(,)π)–cn→ℂ))
192191mptru 1543 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ∈ ((-π(,)π)–cn→ℂ)
193 cnlimc 25937 . . . . . . . . . . . . . . . . . . . . 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 230 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦))
196195simpri 485 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦)
197 fveq2 6906 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0))
198 oveq2 7438 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦) = ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0))
199197, 198eleq12d 2832 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 0 → (((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦) ↔ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)))
200199rspccva 3620 . . . . . . . . . . . . . . . . . 18 ((∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦) ∧ 0 ∈ (-π(,)π)) → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0))
201196, 44, 200mp2an 692 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)
202 oveq1 7437 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 0 → (𝑥 / 2) = (0 / 2))
203102, 81div0i 11998 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 / 2) = 0
204202, 203eqtrdi 2790 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 0 → (𝑥 / 2) = 0)
205204fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 0 → (sin‘(𝑥 / 2)) = (sin‘0))
206 sin0 16181 . . . . . . . . . . . . . . . . . . . . . 22 (sin‘0) = 0
207205, 206eqtrdi 2790 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 0 → (sin‘(𝑥 / 2)) = 0)
208207oveq2d 7446 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 0 → (2 · (sin‘(𝑥 / 2))) = (2 · 0))
209 2t0e0 12432 . . . . . . . . . . . . . . . . . . . 20 (2 · 0) = 0
210208, 209eqtrdi 2790 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → (2 · (sin‘(𝑥 / 2))) = 0)
211 eqid 2734 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))
212210, 211, 159fvmpt 7015 . . . . . . . . . . . . . . . . . 18 (0 ∈ (-π(,)π) → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) = 0)
21344, 212ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) = 0
214 2cnd 12341 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (-π(,)π) → 2 ∈ ℂ)
215163halfcld 12508 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ (-π(,)π) → (𝑥 / 2) ∈ ℂ)
216215sincld 16162 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (-π(,)π) → (sin‘(𝑥 / 2)) ∈ ℂ)
217214, 216mulcld 11278 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (-π(,)π) → (2 · (sin‘(𝑥 / 2))) ∈ ℂ)
218211, 217fmpti 7131 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):(-π(,)π)⟶ℂ
219218a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):(-π(,)π)⟶ℂ)
220219limcdif 25925 . . . . . . . . . . . . . . . . . . 19 (⊤ → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0) = (((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) lim 0))
221220mptru 1543 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0) = (((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) lim 0)
222 resmpt 6056 . . . . . . . . . . . . . . . . . . . 20 (((-π(,)π) ∖ {0}) ⊆ (-π(,)π) → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
22316, 222ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))
224223oveq1i 7440 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) lim 0) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)
225221, 224eqtri 2762 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)
226201, 213, 2253eltr3i 2850 . . . . . . . . . . . . . . . 16 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)
227226a1i 11 . . . . . . . . . . . . . . 15 (⊤ → 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0))
228 eqidd 2735 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
229 oveq1 7437 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑥 / 2) = (𝑦 / 2))
230229fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (sin‘(𝑥 / 2)) = (sin‘(𝑦 / 2)))
231230oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . 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 3990 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ ℝ)
236235rehalfcld 12510 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑦 / 2) ∈ ℝ)
237236resincld 16175 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑦 / 2)) ∈ ℝ)
238234, 237remulcld 11288 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (2 · (sin‘(𝑦 / 2))) ∈ ℝ)
239228, 232, 233, 238fvmptd 7022 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = (2 · (sin‘(𝑦 / 2))))
240 2cnd 12341 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℂ)
241237recnd 11286 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑦 / 2)) ∈ ℂ)
24281a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 2 ≠ 0)
243 ioossicc 13469 . . . . . . . . . . . . . . . . . . . . . . 23 (-π(,)π) ⊆ (-π[,]π)
244 eldifi 4140 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ (-π(,)π))
245243, 244sselid 3992 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ (-π[,]π))
246 eldifsni 4794 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ≠ 0)
247 fourierdlem44 46106 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ (-π[,]π) ∧ 𝑦 ≠ 0) → (sin‘(𝑦 / 2)) ≠ 0)
248245, 246, 247syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑦 / 2)) ≠ 0)
249240, 241, 242, 248mulne0d 11912 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (2 · (sin‘(𝑦 / 2))) ≠ 0)
250239, 249eqnetrd 3005 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ≠ 0)
251250neneqd 2942 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ¬ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0)
252251nrex 3071 . . . . . . . . . . . . . . . . 17 ¬ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0
25325fnmpt 6708 . . . . . . . . . . . . . . . . . . 19 (∀𝑥 ∈ ((-π(,)π) ∖ {0})(2 · (sin‘(𝑥 / 2))) ∈ ℝ → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) Fn ((-π(,)π) ∖ {0}))
254253, 30mprg 3064 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) Fn ((-π(,)π) ∖ {0})
255 ssid 4017 . . . . . . . . . . . . . . . . . 18 ((-π(,)π) ∖ {0}) ⊆ ((-π(,)π) ∖ {0})
256 fvelimab 6980 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) Fn ((-π(,)π) ∖ {0}) ∧ ((-π(,)π) ∖ {0}) ⊆ ((-π(,)π) ∖ {0})) → (0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) “ ((-π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0))
257254, 255, 256mp2an 692 . . . . . . . . . . . . . . . . 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 2735 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))))
261229fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (cos‘(𝑥 / 2)) = (cos‘(𝑦 / 2)))
262261adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑦) → (cos‘(𝑥 / 2)) = (cos‘(𝑦 / 2)))
263235recnd 11286 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ ℂ)
264263halfcld 12508 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑦 / 2) ∈ ℂ)
265264coscld 16163 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑦 / 2)) ∈ ℂ)
266260, 262, 233, 265fvmptd 7022 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = (cos‘(𝑦 / 2)))
267236rered 15259 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (ℜ‘(𝑦 / 2)) = (𝑦 / 2))
268 halfpire 26520 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π / 2) ∈ ℝ
269268renegcli 11567 . . . . . . . . . . . . . . . . . . . . . . . . . 26 -(π / 2) ∈ ℝ
270269a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ)
271270rexrd 11308 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ*)
272268a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (π / 2) ∈ ℝ)
273272rexrd 11308 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (π / 2) ∈ ℝ*)
274 picn 26515 . . . . . . . . . . . . . . . . . . . . . . . . . 26 π ∈ ℂ
275 divneg 11956 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(π / 2) = (-π / 2))
276274, 102, 81, 275mp3an 1460 . . . . . . . . . . . . . . . . . . . . . . . . 25 -(π / 2) = (-π / 2)
27739a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -π ∈ ℝ)
278 2rp 13036 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ∈ ℝ+
279278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ+)
28040a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -π ∈ ℝ*)
28141a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ((-π(,)π) ∖ {0}) → π ∈ ℝ*)
282 ioogtlb 45447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝑦 ∈ (-π(,)π)) → -π < 𝑦)
283280, 281, 244, 282syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -π < 𝑦)
284277, 235, 279, 283ltdiv1dd 13131 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (-π / 2) < (𝑦 / 2))
285276, 284eqbrtrid 5182 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) < (𝑦 / 2))
28638a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → π ∈ ℝ)
287 iooltub 45462 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝑦 ∈ (-π(,)π)) → 𝑦 < π)
288280, 281, 244, 287syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 < π)
289235, 286, 279, 288ltdiv1dd 13131 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑦 / 2) < (π / 2))
290271, 273, 236, 285, 289eliood 45450 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑦 / 2) ∈ (-(π / 2)(,)(π / 2)))
291267, 290eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (ℜ‘(𝑦 / 2)) ∈ (-(π / 2)(,)(π / 2)))
292 cosne0 26585 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 / 2) ∈ ℂ ∧ (ℜ‘(𝑦 / 2)) ∈ (-(π / 2)(,)(π / 2))) → (cos‘(𝑦 / 2)) ≠ 0)
293264, 291, 292syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑦 / 2)) ≠ 0)
294266, 293eqnetrd 3005 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) ≠ 0)
295294neneqd 2942 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ¬ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0)
296295nrex 3071 . . . . . . . . . . . . . . . . . 18 ¬ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0
29772, 73fnmpti 6711 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) Fn ((-π(,)π) ∖ {0})
298 fvelimab 6980 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) Fn ((-π(,)π) ∖ {0}) ∧ ((-π(,)π) ∖ {0}) ⊆ ((-π(,)π) ∖ {0})) → (0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0))
299297, 255, 298mp2an 692 . . . . . . . . . . . . . . . . . 18 (0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0)
300296, 299mtbir 323 . . . . . . . . . . . . . . . . 17 ¬ 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0}))
301135imaeq1i 6076 . . . . . . . . . . . . . . . . . 18 ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) “ ((-π(,)π) ∖ {0})) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0}))
302301eleq2i 2830 . . . . . . . . . . . . . . . . 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 2734 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑠 / 2))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑠 / 2)))
306 eqid 2734 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2))))
30719sseli 3990 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 ∈ ℝ)
308307recnd 11286 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 ∈ ℂ)
309308halfcld 12508 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑠 / 2) ∈ ℂ)
310309coscld 16163 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ∈ ℂ)
311307rehalfcld 12510 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑠 / 2) ∈ ℝ)
312311rered 15259 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (ℜ‘(𝑠 / 2)) = (𝑠 / 2))
313269a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ)
314313rexrd 11308 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ*)
315268a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (π / 2) ∈ ℝ)
316315rexrd 11308 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (π / 2) ∈ ℝ*)
31738a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ((-π(,)π) ∖ {0}) → π ∈ ℝ)
318317renegcld 11687 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -π ∈ ℝ)
319278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ+)
32040a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -π ∈ ℝ*)
32141a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ((-π(,)π) ∖ {0}) → π ∈ ℝ*)
322 eldifi 4140 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 ∈ (-π(,)π))
323 ioogtlb 45447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝑠 ∈ (-π(,)π)) → -π < 𝑠)
324320, 321, 322, 323syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -π < 𝑠)
325318, 307, 319, 324ltdiv1dd 13131 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (-π / 2) < (𝑠 / 2))
326276, 325eqbrtrid 5182 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) < (𝑠 / 2))
327 iooltub 45462 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝑠 ∈ (-π(,)π)) → 𝑠 < π)
328320, 321, 322, 327syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 < π)
329307, 317, 319, 328ltdiv1dd 13131 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑠 / 2) < (π / 2))
330314, 316, 311, 326, 329eliood 45450 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑠 / 2) ∈ (-(π / 2)(,)(π / 2)))
331312, 330eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (ℜ‘(𝑠 / 2)) ∈ (-(π / 2)(,)(π / 2)))
332 cosne0 26585 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 / 2) ∈ ℂ ∧ (ℜ‘(𝑠 / 2)) ∈ (-(π / 2)(,)(π / 2))) → (cos‘(𝑠 / 2)) ≠ 0)
333309, 331, 332syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ≠ 0)
334333neneqd 2942 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ¬ (cos‘(𝑠 / 2)) = 0)
335311recoscld 16176 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ∈ ℝ)
336 elsng 4644 . . . . . . . . . . . . . . . . . . . . 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 3973 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ∈ (ℂ ∖ {0}))
340339adantl 481 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑠 ∈ ((-π(,)π) ∖ {0})) → (cos‘(𝑠 / 2)) ∈ (ℂ ∖ {0}))
341309ad2antrl 728 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ (𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ (𝑠 / 2) ≠ 0)) → (𝑠 / 2) ∈ ℂ)
342 cosf 16157 . . . . . . . . . . . . . . . . . . . 20 cos:ℂ⟶ℂ
343342a1i 11 . . . . . . . . . . . . . . . . . . 19 (⊤ → cos:ℂ⟶ℂ)
344343ffvelcdmda 7103 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ ℂ) → (cos‘𝑥) ∈ ℂ)
345 eqid 2734 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ℂ ↦ (𝑠 / 2)) = (𝑠 ∈ ℂ ↦ (𝑠 / 2))
346345divccncf 24945 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑠 ∈ ℂ ↦ (𝑠 / 2)) ∈ (ℂ–cn→ℂ))
347102, 81, 346mp2an 692 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ℂ ↦ (𝑠 / 2)) ∈ (ℂ–cn→ℂ)
348347a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑠 ∈ ℂ ↦ (𝑠 / 2)) ∈ (ℂ–cn→ℂ))
349141adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑠 ∈ (-π(,)π)) → 𝑠 ∈ ℂ)
350349halfcld 12508 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑠 ∈ (-π(,)π)) → (𝑠 / 2) ∈ ℂ)
351345, 348, 143, 145, 350cncfmptssg 45826 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ∈ ((-π(,)π)–cn→ℂ))
352 oveq1 7437 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 0 → (𝑠 / 2) = (0 / 2))
353352, 203eqtrdi 2790 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → (𝑠 / 2) = 0)
354351, 45, 353cnmptlimc 25939 . . . . . . . . . . . . . . . . . . 19 (⊤ → 0 ∈ ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) lim 0))
355 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) = (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2))
356141halfcld 12508 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (-π(,)π) → (𝑠 / 2) ∈ ℂ)
357355, 356fmpti 7131 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)):(-π(,)π)⟶ℂ
358357a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)):(-π(,)π)⟶ℂ)
359358limcdif 25925 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) lim 0) = (((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) lim 0))
360359mptru 1543 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) lim 0) = (((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) lim 0)
361 resmpt 6056 . . . . . . . . . . . . . . . . . . . . . 22 (((-π(,)π) ∖ {0}) ⊆ (-π(,)π) → ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2)))
36216, 361ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2))
363362oveq1i 7440 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2)) lim 0)
364360, 363eqtri 2762 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2)) lim 0)
365354, 364eleqtrdi 2848 . . . . . . . . . . . . . . . . . 18 (⊤ → 0 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2)) lim 0))
366 ffn 6736 . . . . . . . . . . . . . . . . . . . . . . 23 (cos:ℂ⟶ℂ → cos Fn ℂ)
367342, 366ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 cos Fn ℂ
368 dffn5 6966 . . . . . . . . . . . . . . . . . . . . . 22 (cos Fn ℂ ↔ cos = (𝑥 ∈ ℂ ↦ (cos‘𝑥)))
369367, 368mpbi 230 . . . . . . . . . . . . . . . . . . . . 21 cos = (𝑥 ∈ ℂ ↦ (cos‘𝑥))
370 coscn 26503 . . . . . . . . . . . . . . . . . . . . 21 cos ∈ (ℂ–cn→ℂ)
371369, 370eqeltrri 2835 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℂ ↦ (cos‘𝑥)) ∈ (ℂ–cn→ℂ)
372371a1i 11 . . . . . . . . . . . . . . . . . . 19 (⊤ → (𝑥 ∈ ℂ ↦ (cos‘𝑥)) ∈ (ℂ–cn→ℂ))
373 0cnd 11251 . . . . . . . . . . . . . . . . . . 19 (⊤ → 0 ∈ ℂ)
374 fveq2 6906 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 0 → (cos‘𝑥) = (cos‘0))
375 cos0 16182 . . . . . . . . . . . . . . . . . . . 20 (cos‘0) = 1
376374, 375eqtrdi 2790 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → (cos‘𝑥) = 1)
377372, 373, 376cnmptlimc 25939 . . . . . . . . . . . . . . . . . 18 (⊤ → 1 ∈ ((𝑥 ∈ ℂ ↦ (cos‘𝑥)) lim 0))
378 fveq2 6906 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑠 / 2) → (cos‘𝑥) = (cos‘(𝑠 / 2)))
379 fveq2 6906 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 / 2) = 0 → (cos‘(𝑠 / 2)) = (cos‘0))
380379, 375eqtrdi 2790 . . . . . . . . . . . . . . . . . . 19 ((𝑠 / 2) = 0 → (cos‘(𝑠 / 2)) = 1)
381380ad2antll 729 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ (𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ (𝑠 / 2) = 0)) → (cos‘(𝑠 / 2)) = 1)
382341, 344, 365, 377, 378, 381limcco 25942 . . . . . . . . . . . . . . . . 17 (⊤ → 1 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑠 / 2))) lim 0))
383 ax-1ne0 11221 . . . . . . . . . . . . . . . . . 18 1 ≠ 0
384383a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → 1 ≠ 0)
385305, 306, 340, 382, 384reclimc 45608 . . . . . . . . . . . . . . . 16 (⊤ → (1 / 1) ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) lim 0))
386 1div1e1 11955 . . . . . . . . . . . . . . . 16 (1 / 1) = 1
38766fveq1i 6907 . . . . . . . . . . . . . . . . . . . 20 ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1)‘𝑠)
388 eqidd 2735 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1))
389 eqidd 2735 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → 1 = 1)
390 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 ∈ ((-π(,)π) ∖ {0}))
391 1red 11259 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 1 ∈ ℝ)
392388, 389, 390, 391fvmptd 7022 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1)‘𝑠) = 1)
393387, 392eqtr2id 2787 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 1 = ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠))
394135a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))))
395 oveq1 7437 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑠 → (𝑥 / 2) = (𝑠 / 2))
396395fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑠 → (cos‘(𝑥 / 2)) = (cos‘(𝑠 / 2)))
397396adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (cos‘(𝑥 / 2)) = (cos‘(𝑠 / 2)))
398394, 397, 390, 335fvmptd 7022 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠) = (cos‘(𝑠 / 2)))
399398eqcomd 2740 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) = ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠))
400393, 399oveq12d 7448 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (1 / (cos‘(𝑠 / 2))) = (((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) / ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠)))
401400mpteq2ia 5250 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) / ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠)))
402401oveq1i 7440 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) / ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠))) lim 0)
403385, 386, 4023eltr3g 2854 . . . . . . . . . . . . . . 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 26069 . . . . . . . . . . . . . 14 (⊤ → 1 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) lim 0))
405404mptru 1543 . . . . . . . . . . . . 13 1 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) lim 0)
406 eqidd 2735 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
407 simpr 484 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → 𝑥 = 𝑠)
408406, 407, 390, 307fvmptd 7022 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) = 𝑠)
409 eqidd 2735 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
410407oveq1d 7445 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (𝑥 / 2) = (𝑠 / 2))
411410fveq2d 6910 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (sin‘(𝑥 / 2)) = (sin‘(𝑠 / 2)))
412411oveq2d 7446 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (2 · (sin‘(𝑥 / 2))) = (2 · (sin‘(𝑠 / 2))))
41326a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ)
414311resincld 16175 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑠 / 2)) ∈ ℝ)
415413, 414remulcld 11288 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
416409, 412, 390, 415fvmptd 7022 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠) = (2 · (sin‘(𝑠 / 2))))
417408, 416oveq12d 7448 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠)) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
418417mpteq2ia 5250 . . . . . . . . . . . . . 14 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
419418oveq1i 7440 . . . . . . . . . . . . 13 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim 0)
420405, 419eleqtri 2836 . . . . . . . . . . . 12 1 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim 0)
42110oveq1i 7440 . . . . . . . . . . . . . 14 (𝐾 lim 0) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0)
42210feq1i 6727 . . . . . . . . . . . . . . . . . . 19 (𝐾:(-π[,]π)⟶ℂ ↔ (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π[,]π)⟶ℂ)
42314, 422mpbi 230 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π[,]π)⟶ℂ
424423a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π[,]π)⟶ℂ)
425243a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → (-π(,)π) ⊆ (-π[,]π))
426 iccssre 13465 . . . . . . . . . . . . . . . . . . . 20 ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
42739, 38, 426mp2an 692 . . . . . . . . . . . . . . . . . . 19 (-π[,]π) ⊆ ℝ
428427a1i 11 . . . . . . . . . . . . . . . . . 18 (⊤ → (-π[,]π) ⊆ ℝ)
429428, 12sstrdi 4007 . . . . . . . . . . . . . . . . 17 (⊤ → (-π[,]π) ⊆ ℂ)
430 eqid 2734 . . . . . . . . . . . . . . . . 17 ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})) = ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0}))
43139, 35, 36ltleii 11381 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -π ≤ 0
43235, 38, 37ltleii 11381 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ≤ π
43339, 38elicc2i 13449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (0 ∈ (-π[,]π) ↔ (0 ∈ ℝ ∧ -π ≤ 0 ∧ 0 ≤ π))
43435, 431, 432, 433mpbir3an 1340 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ∈ (-π[,]π)
435159snss 4789 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 ∈ (-π[,]π) ↔ {0} ⊆ (-π[,]π))
436434, 435mpbi 230 . . . . . . . . . . . . . . . . . . . . . . . . 25 {0} ⊆ (-π[,]π)
437 ssequn2 4198 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({0} ⊆ (-π[,]π) ↔ ((-π[,]π) ∪ {0}) = (-π[,]π))
438436, 437mpbi 230 . . . . . . . . . . . . . . . . . . . . . . . 24 ((-π[,]π) ∪ {0}) = (-π[,]π)
439438oveq2i 7441 . . . . . . . . . . . . . . . . . . . . . . 23 ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})) = ((TopOpen‘ℂfld) ↾t (-π[,]π))
440 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . . . 25 (topGen‘ran (,)) = (topGen‘ran (,))
44156, 440rerest 24839 . . . . . . . . . . . . . . . . . . . . . . . 24 ((-π[,]π) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (-π[,]π)) = ((topGen‘ran (,)) ↾t (-π[,]π)))
442427, 441ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((TopOpen‘ℂfld) ↾t (-π[,]π)) = ((topGen‘ran (,)) ↾t (-π[,]π))
443439, 442eqtri 2762 . . . . . . . . . . . . . . . . . . . . . 22 ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})) = ((topGen‘ran (,)) ↾t (-π[,]π))
444443fveq2i 6909 . . . . . . . . . . . . . . . . . . . . 21 (int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0}))) = (int‘((topGen‘ran (,)) ↾t (-π[,]π)))
445159snss 4789 . . . . . . . . . . . . . . . . . . . . . . 23 (0 ∈ (-π(,)π) ↔ {0} ⊆ (-π(,)π))
44644, 445mpbi 230 . . . . . . . . . . . . . . . . . . . . . 22 {0} ⊆ (-π(,)π)
447 ssequn2 4198 . . . . . . . . . . . . . . . . . . . . . 22 ({0} ⊆ (-π(,)π) ↔ ((-π(,)π) ∪ {0}) = (-π(,)π))
448446, 447mpbi 230 . . . . . . . . . . . . . . . . . . . . 21 ((-π(,)π) ∪ {0}) = (-π(,)π)
449444, 448fveq12i 6912 . . . . . . . . . . . . . . . . . . . 20 ((int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})))‘((-π(,)π) ∪ {0})) = ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘(-π(,)π))
450 resttopon 23184 . . . . . . . . . . . . . . . . . . . . . . 23 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (-π[,]π) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (-π[,]π)) ∈ (TopOn‘(-π[,]π)))
45160, 427, 450mp2an 692 . . . . . . . . . . . . . . . . . . . . . 22 ((topGen‘ran (,)) ↾t (-π[,]π)) ∈ (TopOn‘(-π[,]π))
452451topontopi 22936 . . . . . . . . . . . . . . . . . . . . 21 ((topGen‘ran (,)) ↾t (-π[,]π)) ∈ Top
453 retop 24797 . . . . . . . . . . . . . . . . . . . . . . . 24 (topGen‘ran (,)) ∈ Top
454 ovex 7463 . . . . . . . . . . . . . . . . . . . . . . . 24 (-π[,]π) ∈ V
455453, 454pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . . 23 ((topGen‘ran (,)) ∈ Top ∧ (-π[,]π) ∈ V)
456 ssid 4017 . . . . . . . . . . . . . . . . . . . . . . . 24 (-π(,)π) ⊆ (-π(,)π)
45733, 243, 4563pm3.2i 1338 . . . . . . . . . . . . . . . . . . . . . . 23 ((-π(,)π) ∈ (topGen‘ran (,)) ∧ (-π(,)π) ⊆ (-π[,]π) ∧ (-π(,)π) ⊆ (-π(,)π))
458 restopnb 23198 . . . . . . . . . . . . . . . . . . . . . . 23 ((((topGen‘ran (,)) ∈ Top ∧ (-π[,]π) ∈ V) ∧ ((-π(,)π) ∈ (topGen‘ran (,)) ∧ (-π(,)π) ⊆ (-π[,]π) ∧ (-π(,)π) ⊆ (-π(,)π))) → ((-π(,)π) ∈ (topGen‘ran (,)) ↔ (-π(,)π) ∈ ((topGen‘ran (,)) ↾t (-π[,]π))))
459455, 457, 458mp2an 692 . . . . . . . . . . . . . . . . . . . . . 22 ((-π(,)π) ∈ (topGen‘ran (,)) ↔ (-π(,)π) ∈ ((topGen‘ran (,)) ↾t (-π[,]π)))
46033, 459mpbi 230 . . . . . . . . . . . . . . . . . . . . 21 (-π(,)π) ∈ ((topGen‘ran (,)) ↾t (-π[,]π))
461 isopn3i 23105 . . . . . . . . . . . . . . . . . . . . 21 ((((topGen‘ran (,)) ↾t (-π[,]π)) ∈ Top ∧ (-π(,)π) ∈ ((topGen‘ran (,)) ↾t (-π[,]π))) → ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘(-π(,)π)) = (-π(,)π))
462452, 460, 461mp2an 692 . . . . . . . . . . . . . . . . . . . 20 ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘(-π(,)π)) = (-π(,)π)
463 eqid 2734 . . . . . . . . . . . . . . . . . . . 20 (-π(,)π) = (-π(,)π)
464449, 462, 4633eqtrri 2767 . . . . . . . . . . . . . . . . . . 19 (-π(,)π) = ((int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})))‘((-π(,)π) ∪ {0}))
46544, 464eleqtri 2836 . . . . . . . . . . . . . . . . . 18 0 ∈ ((int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})))‘((-π(,)π) ∪ {0}))
466465a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → 0 ∈ ((int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})))‘((-π(,)π) ∪ {0})))
467424, 425, 429, 56, 430, 466limcres 25935 . . . . . . . . . . . . . . . 16 (⊤ → (((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (-π(,)π)) lim 0) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0))
468467mptru 1543 . . . . . . . . . . . . . . 15 (((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (-π(,)π)) lim 0) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0)
469468eqcomi 2743 . . . . . . . . . . . . . 14 ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0) = (((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (-π(,)π)) lim 0)
470 resmpt 6056 . . . . . . . . . . . . . . . 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 7440 . . . . . . . . . . . . . 14 (((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (-π(,)π)) lim 0) = ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0)
473421, 469, 4723eqtri 2766 . . . . . . . . . . . . 13 (𝐾 lim 0) = ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0)
474 eqid 2734 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
475 iftrue 4536 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = 1)
476 1cnd 11253 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → 1 ∈ ℂ)
477475, 476eqeltrd 2838 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 0 → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
478477adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (-π(,)π) ∧ 𝑠 = 0) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
479 iffalse 4539 . . . . . . . . . . . . . . . . . . . 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 12341 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → 2 ∈ ℂ)
483481halfcld 12508 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (𝑠 / 2) ∈ ℂ)
484483sincld 16162 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (sin‘(𝑠 / 2)) ∈ ℂ)
485482, 484mulcld 11278 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
48681a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → 2 ≠ 0)
487243sseli 3990 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ (-π(,)π) → 𝑠 ∈ (-π[,]π))
488 neqne 2945 . . . . . . . . . . . . . . . . . . . . . 22 𝑠 = 0 → 𝑠 ≠ 0)
489 fourierdlem44 46106 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
490487, 488, 489syl2an 596 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (sin‘(𝑠 / 2)) ≠ 0)
491482, 484, 486, 490mulne0d 11912 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
492481, 485, 491divcld 12040 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
493480, 492eqeltrd 2838 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
494478, 493pm2.61dan 813 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (-π(,)π) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
495474, 494fmpti 7131 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π(,)π)⟶ℂ
496495a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π(,)π)⟶ℂ)
497496limcdif 25925 . . . . . . . . . . . . . 14 (⊤ → ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0) = (((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π(,)π) ∖ {0})) lim 0))
498497mptru 1543 . . . . . . . . . . . . 13 ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0) = (((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π(,)π) ∖ {0})) lim 0)
499 resmpt 6056 . . . . . . . . . . . . . . . 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 4141 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ¬ 𝑠 ∈ {0})
502 velsn 4646 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ {0} ↔ 𝑠 = 0)
503501, 502sylnib 328 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ¬ 𝑠 = 0)
504503, 479syl 17 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((-π(,)π) ∖ {0}) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
505504mpteq2ia 5250 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
506500, 505eqtri 2762 . . . . . . . . . . . . . 14 ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π(,)π) ∖ {0})) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
507506oveq1i 7440 . . . . . . . . . . . . 13 (((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π(,)π) ∖ {0})) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim 0)
508473, 498, 5073eqtrri 2767 . . . . . . . . . . . 12 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim 0) = (𝐾 lim 0)
509420, 508eleqtri 2836 . . . . . . . . . . 11 1 ∈ (𝐾 lim 0)
510509a1i 11 . . . . . . . . . 10 (𝑠 = 0 → 1 ∈ (𝐾 lim 0))
511 fveq2 6906 . . . . . . . . . . 11 (𝑠 = 0 → (𝐾𝑠) = (𝐾‘0))
512475, 10, 47fvmpt 7015 . . . . . . . . . . . 12 (0 ∈ (-π[,]π) → (𝐾‘0) = 1)
513434, 512ax-mp 5 . . . . . . . . . . 11 (𝐾‘0) = 1
514511, 513eqtrdi 2790 . . . . . . . . . 10 (𝑠 = 0 → (𝐾𝑠) = 1)
515 oveq2 7438 . . . . . . . . . 10 (𝑠 = 0 → (𝐾 lim 𝑠) = (𝐾 lim 0))
516510, 514, 5153eltr4d 2853 . . . . . . . . 9 (𝑠 = 0 → (𝐾𝑠) ∈ (𝐾 lim 𝑠))
517427, 12sstri 4004 . . . . . . . . . . 11 (-π[,]π) ⊆ ℂ
518517a1i 11 . . . . . . . . . 10 (𝑠 = 0 → (-π[,]π) ⊆ ℂ)
51938a1i 11 . . . . . . . . . . . 12 (𝑠 = 0 → π ∈ ℝ)
520519renegcld 11687 . . . . . . . . . . 11 (𝑠 = 0 → -π ∈ ℝ)
521 id 22 . . . . . . . . . . . 12 (𝑠 = 0 → 𝑠 = 0)
52235a1i 11 . . . . . . . . . . . 12 (𝑠 = 0 → 0 ∈ ℝ)
523521, 522eqeltrd 2838 . . . . . . . . . . 11 (𝑠 = 0 → 𝑠 ∈ ℝ)
524431, 521breqtrrid 5185 . . . . . . . . . . 11 (𝑠 = 0 → -π ≤ 𝑠)
525521, 432eqbrtrdi 5186 . . . . . . . . . . 11 (𝑠 = 0 → 𝑠 ≤ π)
526520, 519, 523, 524, 525eliccd 45456 . . . . . . . . . 10 (𝑠 = 0 → 𝑠 ∈ (-π[,]π))
52757oveq1i 7440 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t (-π[,]π)) = (((TopOpen‘ℂfld) ↾t ℝ) ↾t (-π[,]π))
52856cnfldtop 24819 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) ∈ Top
529 reex 11243 . . . . . . . . . . . . 13 ℝ ∈ V
530 restabs 23188 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ∈ Top ∧ (-π[,]π) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂfld) ↾t ℝ) ↾t (-π[,]π)) = ((TopOpen‘ℂfld) ↾t (-π[,]π)))
531528, 427, 529, 530mp3an 1460 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ↾t ℝ) ↾t (-π[,]π)) = ((TopOpen‘ℂfld) ↾t (-π[,]π))
532527, 531eqtri 2762 . . . . . . . . . . 11 ((topGen‘ran (,)) ↾t (-π[,]π)) = ((TopOpen‘ℂfld) ↾t (-π[,]π))
53356, 532cnplimc 25936 . . . . . . . . . 10 (((-π[,]π) ⊆ ℂ ∧ 𝑠 ∈ (-π[,]π)) → (𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠) ↔ (𝐾:(-π[,]π)⟶ℂ ∧ (𝐾𝑠) ∈ (𝐾 lim 𝑠))))
534518, 526, 533syl2anc 584 . . . . . . . . 9 (𝑠 = 0 → (𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠) ↔ (𝐾:(-π[,]π)⟶ℂ ∧ (𝐾𝑠) ∈ (𝐾 lim 𝑠))))
53515, 516, 534mpbir2and 713 . . . . . . . 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 228 . . . . . . . . . . . 12 𝑠 = 0 → ¬ 𝑠 ∈ {0})
540539adantl 481 . . . . . . . . . . 11 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → ¬ 𝑠 ∈ {0})
541537, 540eldifd 3973 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ((-π[,]π) ∖ {0}))
542 fveq2 6906 . . . . . . . . . . . 12 (𝑥 = 𝑠 → ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥) = ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠))
543542eleq2d 2824 . . . . . . . . . . 11 (𝑥 = 𝑠 → ((𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥) ↔ (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠)))
544429ssdifssd 4156 . . . . . . . . . . . . . . . . 17 (⊤ → ((-π[,]π) ∖ {0}) ⊆ ℂ)
545544, 145idcncfg 45828 . . . . . . . . . . . . . . . 16 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ 𝑠) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
546 eqid 2734 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2))))
547 2cnd 12341 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 2 ∈ ℂ)
548 eldifi 4140 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 𝑠 ∈ (-π[,]π))
549517, 548sselid 3992 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 𝑠 ∈ ℂ)
550549halfcld 12508 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (𝑠 / 2) ∈ ℂ)
551550sincld 16162 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (sin‘(𝑠 / 2)) ∈ ℂ)
552547, 551mulcld 11278 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
55381a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 2 ≠ 0)
554 eldifsni 4794 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 𝑠 ≠ 0)
555548, 554, 489syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (sin‘(𝑠 / 2)) ≠ 0)
556547, 551, 553, 555mulne0d 11912 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
557556neneqd 2942 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π[,]π) ∖ {0}) → ¬ (2 · (sin‘(𝑠 / 2))) = 0)
558 elsng 4644 . . . . . . . . . . . . . . . . . . . . . 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 3973 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
562546, 561fmpti 7131 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))):((-π[,]π) ∖ {0})⟶(ℂ ∖ {0})
563 difss 4145 . . . . . . . . . . . . . . . . . . 19 (ℂ ∖ {0}) ⊆ ℂ
564 eqid 2734 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ℂ ↦ 2) = (𝑠 ∈ ℂ ↦ 2)
565175, 176, 175constcncfg 45827 . . . . . . . . . . . . . . . . . . . . . . 23 (2 ∈ ℂ → (𝑠 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
566102, 565mp1i 13 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑠 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
567 2cnd 12341 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑠 ∈ ((-π[,]π) ∖ {0})) → 2 ∈ ℂ)
568564, 566, 544, 145, 567cncfmptssg 45826 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ 2) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
569549, 547, 553divrecd 12043 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (𝑠 / 2) = (𝑠 · (1 / 2)))
570569mpteq2ia 5250 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / 2)) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 · (1 / 2)))
571 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ℂ ↦ (1 / 2)) = (𝑠 ∈ ℂ ↦ (1 / 2))
572144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 / 2) ∈ ℂ → ℂ ⊆ ℂ)
573 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 / 2) ∈ ℂ → (1 / 2) ∈ ℂ)
574572, 573, 572constcncfg 45827 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 / 2) ∈ ℂ → (𝑠 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
57594, 574mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⊤ → (𝑠 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
57694a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⊤ ∧ 𝑠 ∈ ((-π[,]π) ∖ {0})) → (1 / 2) ∈ ℂ)
577571, 575, 544, 145, 576cncfmptssg 45826 . . . . . . . . . . . . . . . . . . . . . . . 24 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (1 / 2)) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
578545, 577mulcncf 25493 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 · (1 / 2))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
579570, 578eqeltrid 2842 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / 2)) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
580182, 579cncfmpt1f 24953 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (sin‘(𝑠 / 2))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
581568, 580mulcncf 25493 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
582581mptru 1543 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ)
583 cncfcdm 24937 . . . . . . . . . . . . . . . . . . 19 (((ℂ ∖ {0}) ⊆ ℂ ∧ (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ)) → ((𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))):((-π[,]π) ∖ {0})⟶(ℂ ∖ {0})))
584563, 582, 583mp2an 692 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))):((-π[,]π) ∖ {0})⟶(ℂ ∖ {0}))
585562, 584mpbir 231 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→(ℂ ∖ {0}))
586585a1i 11 . . . . . . . . . . . . . . . 16 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→(ℂ ∖ {0})))
587545, 586divcncf 25495 . . . . . . . . . . . . . . 15 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
588587mptru 1543 . . . . . . . . . . . . . 14 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ)
589428ssdifssd 4156 . . . . . . . . . . . . . . . . 17 (⊤ → ((-π[,]π) ∖ {0}) ⊆ ℝ)
590589mptru 1543 . . . . . . . . . . . . . . . 16 ((-π[,]π) ∖ {0}) ⊆ ℝ
591590, 12sstri 4004 . . . . . . . . . . . . . . 15 ((-π[,]π) ∖ {0}) ⊆ ℂ
59257oveq1i 7440 . . . . . . . . . . . . . . . . 17 ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) = (((TopOpen‘ℂfld) ↾t ℝ) ↾t ((-π[,]π) ∖ {0}))
593 restabs 23188 . . . . . . . . . . . . . . . . . 18 (((TopOpen‘ℂfld) ∈ Top ∧ ((-π[,]π) ∖ {0}) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂfld) ↾t ℝ) ↾t ((-π[,]π) ∖ {0})) = ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∖ {0})))
594528, 590, 529, 593mp3an 1460 . . . . . . . . . . . . . . . . 17 (((TopOpen‘ℂfld) ↾t ℝ) ↾t ((-π[,]π) ∖ {0})) = ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∖ {0}))
595592, 594eqtri 2762 . . . . . . . . . . . . . . . 16 ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) = ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∖ {0}))
596 unicntop 24821 . . . . . . . . . . . . . . . . . . 19 ℂ = (TopOpen‘ℂfld)
597596restid 17479 . . . . . . . . . . . . . . . . . 18 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
598528, 597ax-mp 5 . . . . . . . . . . . . . . . . 17 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
599598eqcomi 2743 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
60056, 595, 599cncfcn 24949 . . . . . . . . . . . . . . 15 ((((-π[,]π) ∖ {0}) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (((-π[,]π) ∖ {0})–cn→ℂ) = (((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) Cn (TopOpen‘ℂfld)))
601591, 144, 600mp2an 692 . . . . . . . . . . . . . 14 (((-π[,]π) ∖ {0})–cn→ℂ) = (((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) Cn (TopOpen‘ℂfld))
602588, 601eleqtri 2836 . . . . . . . . . . . . 13 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) Cn (TopOpen‘ℂfld))
603 resttopon 23184 . . . . . . . . . . . . . . 15 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((-π[,]π) ∖ {0}) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) ∈ (TopOn‘((-π[,]π) ∖ {0})))
60460, 590, 603mp2an 692 . . . . . . . . . . . . . 14 ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) ∈ (TopOn‘((-π[,]π) ∖ {0}))
60556cnfldtopon 24818 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
606 cncnp 23303 . . . . . . . . . . . . . 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 692 . . . . . . . . . . . . 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 230 . . . . . . . . . . . 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 3589 . . . . . . . . . 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 5995 . . . . . . . . . 10 (𝐾 ↾ ((-π[,]π) ∖ {0})) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π[,]π) ∖ {0}))
613 difss 4145 . . . . . . . . . . 11 ((-π[,]π) ∖ {0}) ⊆ (-π[,]π)
614 resmpt 6056 . . . . . . . . . . 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 4141 . . . . . . . . . . . . 13 (𝑠 ∈ ((-π[,]π) ∖ {0}) → ¬ 𝑠 ∈ {0})
617616, 502sylnib 328 . . . . . . . . . . . 12 (𝑠 ∈ ((-π[,]π) ∖ {0}) → ¬ 𝑠 = 0)
618617, 479syl 17 . . . . . . . . . . 11 (𝑠 ∈ ((-π[,]π) ∖ {0}) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
619618mpteq2ia 5250 . . . . . . . . . 10 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
620612, 615, 6193eqtri 2766 . . . . . . . . 9 (𝐾 ↾ ((-π[,]π) ∖ {0})) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
621 restabs 23188 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ Top ∧ ((-π[,]π) ∖ {0}) ⊆ (-π[,]π) ∧ (-π[,]π) ∈ V) → (((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) = ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})))
622453, 613, 454, 621mp3an 1460 . . . . . . . . . . 11 (((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) = ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0}))
623622oveq1i 7440 . . . . . . . . . 10 ((((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld)) = (((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))
624623fveq1i 6907 . . . . . . . . 9 (((((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠) = ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠)
625611, 620, 6243eltr4g 2855 . . . . . . . 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 4153 . . . . . . . . . . . . . 14 ((-π[,]π) ⊆ ℝ → ((-π[,]π) ∖ {0}) ⊆ (ℝ ∖ {0}))
629427, 628ax-mp 5 . . . . . . . . . . . . 13 ((-π[,]π) ∖ {0}) ⊆ (ℝ ∖ {0})
630629, 541sselid 3992 . . . . . . . . . . . 12 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ (ℝ ∖ {0}))
631 sscon 4152 . . . . . . . . . . . . . . . . 17 ({0} ⊆ (-π[,]π) → (ℝ ∖ (-π[,]π)) ⊆ (ℝ ∖ {0}))
632436, 631ax-mp 5 . . . . . . . . . . . . . . . 16 (ℝ ∖ (-π[,]π)) ⊆ (ℝ ∖ {0})
633629, 632unssi 4200 . . . . . . . . . . . . . . 15 (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))) ⊆ (ℝ ∖ {0})
634 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (-π[,]π))
635 eldifn 4141 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (ℝ ∖ {0}) → ¬ 𝑠 ∈ {0})
636635adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ (-π[,]π)) → ¬ 𝑠 ∈ {0})
637634, 636eldifd 3973 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ ((-π[,]π) ∖ {0}))
638 elun1 4191 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
639637, 638syl 17 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
640 eldifi 4140 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (ℝ ∖ {0}) → 𝑠 ∈ ℝ)
641640adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ ℝ)
642 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ (-π[,]π)) → ¬ 𝑠 ∈ (-π[,]π))
643641, 642eldifd 3973 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (ℝ ∖ (-π[,]π)))
644 elun2 4192 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (ℝ ∖ (-π[,]π)) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
645643, 644syl 17 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
646639, 645pm2.61dan 813 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (ℝ ∖ {0}) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
647646ssriv 3998 . . . . . . . . . . . . . . 15 (ℝ ∖ {0}) ⊆ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))
648633, 647eqssi 4011 . . . . . . . . . . . . . 14 (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))) = (ℝ ∖ {0})
649648fveq2i 6909 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) = ((int‘(topGen‘ran (,)))‘(ℝ ∖ {0}))
65061cldopn 23054 . . . . . . . . . . . . . . 15 ({0} ∈ (Clsd‘(topGen‘ran (,))) → (ℝ ∖ {0}) ∈ (topGen‘ran (,)))
65159, 650ax-mp 5 . . . . . . . . . . . . . 14 (ℝ ∖ {0}) ∈ (topGen‘ran (,))
652 isopn3i 23105 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ Top ∧ (ℝ ∖ {0}) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘(ℝ ∖ {0})) = (ℝ ∖ {0}))
653453, 651, 652mp2an 692 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘(ℝ ∖ {0})) = (ℝ ∖ {0})
654649, 653eqtri 2762 . . . . . . . . . . . 12 ((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) = (ℝ ∖ {0})
655630, 654eleqtrrdi 2849 . . . . . . . . . . 11 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))))
656655, 537elind 4209 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ (((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) ∩ (-π[,]π)))
657 eqid 2734 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t (-π[,]π)) = ((topGen‘ran (,)) ↾t (-π[,]π))
65861, 657restntr 23205 . . . . . . . . . . 11 (((topGen‘ran (,)) ∈ Top ∧ (-π[,]π) ⊆ ℝ ∧ ((-π[,]π) ∖ {0}) ⊆ (-π[,]π)) → ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘((-π[,]π) ∖ {0})) = (((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) ∩ (-π[,]π)))
659453, 427, 613, 658mp3an 1460 . . . . . . . . . 10 ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘((-π[,]π) ∖ {0})) = (((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) ∩ (-π[,]π))
660656, 659eleqtrrdi 2849 . . . . . . . . 9 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘((-π[,]π) ∖ {0})))
66114a1i 11 . . . . . . . . 9 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝐾:(-π[,]π)⟶ℂ)
662451toponunii 22937 . . . . . . . . . 10 (-π[,]π) = ((topGen‘ran (,)) ↾t (-π[,]π))
663662, 596cnprest 23312 . . . . . . . . 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 837 . . . . . . . 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 813 . . . . . 6 (𝑠 ∈ (-π[,]π) → 𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))
667666rgen 3060 . . . . 5 𝑠 ∈ (-π[,]π)𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠)
668 cncnp 23303 . . . . . 6 ((((topGen‘ran (,)) ↾t (-π[,]π)) ∈ (TopOn‘(-π[,]π)) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → (𝐾 ∈ (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld)) ↔ (𝐾:(-π[,]π)⟶ℂ ∧ ∀𝑠 ∈ (-π[,]π)𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))))
669451, 605, 668mp2an 692 . . . . 5 (𝐾 ∈ (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld)) ↔ (𝐾:(-π[,]π)⟶ℂ ∧ ∀𝑠 ∈ (-π[,]π)𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠)))
67014, 667, 669mpbir2an 711 . . . 4 𝐾 ∈ (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld))
67156, 532, 599cncfcn 24949 . . . . . 6 (((-π[,]π) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((-π[,]π)–cn→ℂ) = (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld)))
672517, 144, 671mp2an 692 . . . . 5 ((-π[,]π)–cn→ℂ) = (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld))
673672eqcomi 2743 . . . 4 (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld)) = ((-π[,]π)–cn→ℂ)
674670, 673eleqtri 2836 . . 3 𝐾 ∈ ((-π[,]π)–cn→ℂ)
675 cncfcdm 24937 . . 3 ((ℝ ⊆ ℂ ∧ 𝐾 ∈ ((-π[,]π)–cn→ℂ)) → (𝐾 ∈ ((-π[,]π)–cn→ℝ) ↔ 𝐾:(-π[,]π)⟶ℝ))
67612, 674, 675mp2an 692 . 2 (𝐾 ∈ ((-π[,]π)–cn→ℝ) ↔ 𝐾:(-π[,]π)⟶ℝ)
67711, 676mpbir 231 1 𝐾 ∈ ((-π[,]π)–cn→ℝ)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wa 395  w3a 1086   = wceq 1536  wtru 1537  wcel 2105  wne 2937  wral 3058  wrex 3067  Vcvv 3477  cdif 3959  cun 3960  cin 3961  wss 3962  ifcif 4530  {csn 4630  {cpr 4632   class class class wbr 5147  cmpt 5230  dom cdm 5688  ran crn 5689  cres 5690  cima 5691   Fn wfn 6557  wf 6558  cfv 6562  (class class class)co 7430  cc 11150  cr 11151  0cc0 11152  1c1 11153   · cmul 11157  *cxr 11291   < clt 11292  cle 11293  -cneg 11490   / cdiv 11917  2c2 12318  +crp 13031  (,)cioo 13383  [,]cicc 13386  cre 15132  sincsin 16095  cosccos 16096  πcpi 16098  t crest 17466  TopOpenctopn 17467  topGenctg 17483  fldccnfld 21381  Topctop 22914  TopOnctopon 22931  Clsdccld 23039  intcnt 23040   Cn ccn 23247   CnP ccnp 23248  cnccncf 24915   lim climc 25911   D cdv 25912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230  ax-addf 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-pm 8867  df-ixp 8936  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-fi 9448  df-sup 9479  df-inf 9480  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-q 12988  df-rp 13032  df-xneg 13151  df-xadd 13152  df-xmul 13153  df-ioo 13387  df-ioc 13388  df-ico 13389  df-icc 13390  df-fz 13544  df-fzo 13691  df-fl 13828  df-mod 13906  df-seq 14039  df-exp 14099  df-fac 14309  df-bc 14338  df-hash 14366  df-shft 15102  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-limsup 15503  df-clim 15520  df-rlim 15521  df-sum 15719  df-ef 16099  df-sin 16101  df-cos 16102  df-pi 16104  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17468  df-topn 17469  df-0g 17487  df-gsum 17488  df-topgen 17489  df-pt 17490  df-prds 17493  df-xrs 17548  df-qtop 17553  df-imas 17554  df-xps 17556  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-submnd 18809  df-mulg 19098  df-cntz 19347  df-cmn 19814  df-psmet 21373  df-xmet 21374  df-met 21375  df-bl 21376  df-mopn 21377  df-fbas 21378  df-fg 21379  df-cnfld 21382  df-top 22915  df-topon 22932  df-topsp 22954  df-bases 22968  df-cld 23042  df-ntr 23043  df-cls 23044  df-nei 23121  df-lp 23159  df-perf 23160  df-cn 23250  df-cnp 23251  df-t1 23337  df-haus 23338  df-cmp 23410  df-tx 23585  df-hmeo 23778  df-fil 23869  df-fm 23961  df-flim 23962  df-flf 23963  df-xms 24345  df-ms 24346  df-tms 24347  df-cncf 24917  df-limc 25915  df-dv 25916
This theorem is referenced by:  fourierdlem77  46138  fourierdlem78  46139  fourierdlem85  46146  fourierdlem88  46149
  Copyright terms: Public domain W3C validator