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

Theorem fourierdlem62 42736
 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 2828 . . . . . 6 (𝑦 = 𝑠 → (𝑦 = 0 ↔ 𝑠 = 0))
3 id 22 . . . . . . 7 (𝑦 = 𝑠𝑦 = 𝑠)
4 oveq1 7156 . . . . . . . . 9 (𝑦 = 𝑠 → (𝑦 / 2) = (𝑠 / 2))
54fveq2d 6665 . . . . . . . 8 (𝑦 = 𝑠 → (sin‘(𝑦 / 2)) = (sin‘(𝑠 / 2)))
65oveq2d 7165 . . . . . . 7 (𝑦 = 𝑠 → (2 · (sin‘(𝑦 / 2))) = (2 · (sin‘(𝑠 / 2))))
73, 6oveq12d 7167 . . . . . 6 (𝑦 = 𝑠 → (𝑦 / (2 · (sin‘(𝑦 / 2)))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
82, 7ifbieq2d 4475 . . . . 5 (𝑦 = 𝑠 → if(𝑦 = 0, 1, (𝑦 / (2 · (sin‘(𝑦 / 2))))) = if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
98cbvmptv 5155 . . . 4 (𝑦 ∈ (-π[,]π) ↦ if(𝑦 = 0, 1, (𝑦 / (2 · (sin‘(𝑦 / 2)))))) = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
101, 9eqtri 2847 . . 3 𝐾 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
1110fourierdlem43 42718 . 2 𝐾:(-π[,]π)⟶ℝ
12 ax-resscn 10592 . . 3 ℝ ⊆ ℂ
13 fss 6517 . . . . . 6 ((𝐾:(-π[,]π)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐾:(-π[,]π)⟶ℂ)
1411, 12, 13mp2an 691 . . . . 5 𝐾:(-π[,]π)⟶ℂ
1514a1i 11 . . . . . . . . 9 (𝑠 = 0 → 𝐾:(-π[,]π)⟶ℂ)
16 difss 4094 . . . . . . . . . . . . . . . . 17 ((-π(,)π) ∖ {0}) ⊆ (-π(,)π)
17 elioore 12765 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (-π(,)π) → 𝑠 ∈ ℝ)
1817ssriv 3957 . . . . . . . . . . . . . . . . 17 (-π(,)π) ⊆ ℝ
1916, 18sstri 3962 . . . . . . . . . . . . . . . 16 ((-π(,)π) ∖ {0}) ⊆ ℝ
2019a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ((-π(,)π) ∖ {0}) ⊆ ℝ)
21 eqid 2824 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)
2219sseli 3949 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-π(,)π) ∖ {0}) → 𝑥 ∈ ℝ)
2321, 22fmpti 6867 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥):((-π(,)π) ∖ {0})⟶ℝ
2423a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥):((-π(,)π) ∖ {0})⟶ℝ)
25 eqid 2824 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))
26 2re 11708 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℝ
2726a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ)
2822rehalfcld 11881 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) → (𝑥 / 2) ∈ ℝ)
2928resincld 15496 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑥 / 2)) ∈ ℝ)
3027, 29remulcld 10669 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((-π(,)π) ∖ {0}) → (2 · (sin‘(𝑥 / 2))) ∈ ℝ)
3125, 30fmpti 6867 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))):((-π(,)π) ∖ {0})⟶ℝ
3231a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))):((-π(,)π) ∖ {0})⟶ℝ)
33 iooretop 23374 . . . . . . . . . . . . . . . 16 (-π(,)π) ∈ (topGen‘ran (,))
3433a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (-π(,)π) ∈ (topGen‘ran (,)))
35 0re 10641 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
36 negpilt0 41837 . . . . . . . . . . . . . . . . 17 -π < 0
37 pipos 25056 . . . . . . . . . . . . . . . . 17 0 < π
38 pire 25054 . . . . . . . . . . . . . . . . . . . 20 π ∈ ℝ
3938renegcli 10945 . . . . . . . . . . . . . . . . . . 19 -π ∈ ℝ
4039rexri 10697 . . . . . . . . . . . . . . . . . 18 -π ∈ ℝ*
4138rexri 10697 . . . . . . . . . . . . . . . . . 18 π ∈ ℝ*
42 elioo2 12776 . . . . . . . . . . . . . . . . . 18 ((-π ∈ ℝ* ∧ π ∈ ℝ*) → (0 ∈ (-π(,)π) ↔ (0 ∈ ℝ ∧ -π < 0 ∧ 0 < π)))
4340, 41, 42mp2an 691 . . . . . . . . . . . . . . . . 17 (0 ∈ (-π(,)π) ↔ (0 ∈ ℝ ∧ -π < 0 ∧ 0 < π))
4435, 36, 37, 43mpbir3an 1338 . . . . . . . . . . . . . . . 16 0 ∈ (-π(,)π)
4544a1i 11 . . . . . . . . . . . . . . 15 (⊤ → 0 ∈ (-π(,)π))
46 eqid 2824 . . . . . . . . . . . . . . 15 ((-π(,)π) ∖ {0}) = ((-π(,)π) ∖ {0})
47 1ex 10635 . . . . . . . . . . . . . . . . . . 19 1 ∈ V
48 eqid 2824 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1)
4947, 48dmmpti 6481 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = ((-π(,)π) ∖ {0})
50 reelprrecn 10627 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ ∈ {ℝ, ℂ}
5150a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ℝ ∈ {ℝ, ℂ})
5212sseli 3949 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
5352adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
54 1red 10640 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
5551dvmptid 24563 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
56 eqid 2824 . . . . . . . . . . . . . . . . . . . . . . 23 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
5756tgioo2 23411 . . . . . . . . . . . . . . . . . . . . . 22 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
58 sncldre 41596 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 ∈ ℝ → {0} ∈ (Clsd‘(topGen‘ran (,))))
5935, 58ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 {0} ∈ (Clsd‘(topGen‘ran (,)))
60 retopon 23372 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
6160toponunii 21524 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℝ = (topGen‘ran (,))
6261difopn 21642 . . . . . . . . . . . . . . . . . . . . . . . 24 (((-π(,)π) ∈ (topGen‘ran (,)) ∧ {0} ∈ (Clsd‘(topGen‘ran (,)))) → ((-π(,)π) ∖ {0}) ∈ (topGen‘ran (,)))
6333, 59, 62mp2an 691 . . . . . . . . . . . . . . . . . . . . . . 23 ((-π(,)π) ∖ {0}) ∈ (topGen‘ran (,))
6463a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ((-π(,)π) ∖ {0}) ∈ (topGen‘ran (,)))
6551, 53, 54, 55, 20, 57, 56, 64dvmptres 24569 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1))
6665mptru 1545 . . . . . . . . . . . . . . . . . . . 20 (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1)
6766eqcomi 2833 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
6867dmeqi 5760 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
6949, 68eqtr3i 2849 . . . . . . . . . . . . . . . . 17 ((-π(,)π) ∖ {0}) = dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
7069eqimssi 4011 . . . . . . . . . . . . . . . 16 ((-π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
7170a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ((-π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)))
72 fvex 6674 . . . . . . . . . . . . . . . . . . 19 (cos‘(𝑥 / 2)) ∈ V
73 eqid 2824 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))
7472, 73dmmpti 6481 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = ((-π(,)π) ∖ {0})
75 2cnd 11712 . . . . . . . . . . . . . . . . . . . . . . 23 ((⊤ ∧ 𝑥 ∈ ℝ) → 2 ∈ ℂ)
7653halfcld 11879 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⊤ ∧ 𝑥 ∈ ℝ) → (𝑥 / 2) ∈ ℂ)
7776sincld 15483 . . . . . . . . . . . . . . . . . . . . . . 23 ((⊤ ∧ 𝑥 ∈ ℝ) → (sin‘(𝑥 / 2)) ∈ ℂ)
7875, 77mulcld 10659 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → (2 · (sin‘(𝑥 / 2))) ∈ ℂ)
7976coscld 15484 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → (cos‘(𝑥 / 2)) ∈ ℂ)
80 2cnd 11712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → 2 ∈ ℂ)
81 2ne0 11738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 2 ≠ 0
8281a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → 2 ≠ 0)
8352, 80, 82divrec2d 11418 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → (𝑥 / 2) = ((1 / 2) · 𝑥))
8483fveq2d 6665 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℝ → (sin‘(𝑥 / 2)) = (sin‘((1 / 2) · 𝑥)))
8584oveq2d 7165 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ → (2 · (sin‘(𝑥 / 2))) = (2 · (sin‘((1 / 2) · 𝑥))))
8685mpteq2ia 5143 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))
8786oveq2i 7160 . . . . . . . . . . . . . . . . . . . . . . . 24 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2))))) = (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))
88 resmpt 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℝ ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))
8912, 88ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))
9089eqcomi 2833 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) = ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ)
9190oveq2i 7160 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (ℝ D ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ))
92 eqid 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) = (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))
93 2cnd 11712 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℂ → 2 ∈ ℂ)
94 halfcn 11849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (1 / 2) ∈ ℂ
9594a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℂ → (1 / 2) ∈ ℂ)
96 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℂ → 𝑥 ∈ ℂ)
9795, 96mulcld 10659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℂ → ((1 / 2) · 𝑥) ∈ ℂ)
9897sincld 15483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℂ → (sin‘((1 / 2) · 𝑥)) ∈ ℂ)
9993, 98mulcld 10659 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℂ → (2 · (sin‘((1 / 2) · 𝑥))) ∈ ℂ)
10092, 99fmpti 6867 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))):ℂ⟶ℂ
101 eqid 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
102 2cn 11709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2 ∈ ℂ
103102, 94mulcli 10646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (2 · (1 / 2)) ∈ ℂ
104103a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ ℂ → (2 · (1 / 2)) ∈ ℂ)
10597coscld 15484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ ℂ → (cos‘((1 / 2) · 𝑥)) ∈ ℂ)
106104, 105mulcld 10659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ ℂ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) ∈ ℂ)
107106adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((⊤ ∧ 𝑥 ∈ ℂ) → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) ∈ ℂ)
108101, 107dmmptd 6482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (⊤ → dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = ℂ)
109108mptru 1545 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = ℂ
11012, 109sseqtrri 3990 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℝ ⊆ dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
111 dvasinbx 42488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((2 ∈ ℂ ∧ (1 / 2) ∈ ℂ) → (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))))
112102, 94, 111mp2an 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
113112dmeqi 5760 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 dom (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = dom (𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))))
114110, 113sseqtrri 3990 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℝ ⊆ dom (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))
115 dvcnre 42484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))):ℂ⟶ℂ ∧ ℝ ⊆ dom (ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))))) → (ℝ D ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ)) = ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ))
116100, 114, 115mp2an 691 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℝ D ((𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥)))) ↾ ℝ)) = ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ)
117112reseq1i 5836 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ) = ((𝑥 ∈ ℂ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) ↾ ℝ)
118 resmpt 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (2 · (1 / 2)) = 1
121120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → (2 · (1 / 2)) = 1)
12283eqcomd 2830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℝ → ((1 / 2) · 𝑥) = (𝑥 / 2))
123122fveq2d 6665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → (cos‘((1 / 2) · 𝑥)) = (cos‘(𝑥 / 2)))
124121, 123oveq12d 7167 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) = (1 · (cos‘(𝑥 / 2))))
12552halfcld 11879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑥 ∈ ℝ → (𝑥 / 2) ∈ ℂ)
126125coscld 15484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ ℝ → (cos‘(𝑥 / 2)) ∈ ℂ)
127126mulid2d 10657 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → (1 · (cos‘(𝑥 / 2))) = (cos‘(𝑥 / 2)))
128124, 127eqtrd 2859 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ℝ → ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥))) = (cos‘(𝑥 / 2)))
129128mpteq2ia 5143 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ ↦ ((2 · (1 / 2)) · (cos‘((1 / 2) · 𝑥)))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
130117, 119, 1293eqtri 2851 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℂ D (𝑥 ∈ ℂ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) ↾ ℝ) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
13191, 116, 1303eqtri 2851 . . . . . . . . . . . . . . . . . . . . . . . 24 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘((1 / 2) · 𝑥))))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
13287, 131eqtri 2847 . . . . . . . . . . . . . . . . . . . . . . 23 (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2)))
133132a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ℝ ↦ (cos‘(𝑥 / 2))))
13451, 78, 79, 133, 20, 57, 56, 64dvmptres 24569 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))))
135134mptru 1545 . . . . . . . . . . . . . . . . . . . 20 (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))
136135eqcomi 2833 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
137136dmeqi 5760 . . . . . . . . . . . . . . . . . 18 dom (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
13874, 137eqtr3i 2849 . . . . . . . . . . . . . . . . 17 ((-π(,)π) ∖ {0}) = dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
139138eqimssi 4011 . . . . . . . . . . . . . . . 16 ((-π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
140139a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ((-π(,)π) ∖ {0}) ⊆ dom (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))))
14117recnd 10667 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (-π(,)π) → 𝑠 ∈ ℂ)
142141ssriv 3957 . . . . . . . . . . . . . . . . . . . . . . 23 (-π(,)π) ⊆ ℂ
143142a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (-π(,)π) ⊆ ℂ)
144 ssid 3975 . . . . . . . . . . . . . . . . . . . . . . 23 ℂ ⊆ ℂ
145144a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ℂ ⊆ ℂ)
146143, 145idcncfg 42441 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑥 ∈ (-π(,)π) ↦ 𝑥) ∈ ((-π(,)π)–cn→ℂ))
147146mptru 1545 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (-π(,)π) ↦ 𝑥) ∈ ((-π(,)π)–cn→ℂ)
148 cnlimc 24494 . . . . . . . . . . . . . . . . . . . . 21 ((-π(,)π) ⊆ ℂ → ((𝑥 ∈ (-π(,)π) ↦ 𝑥) ∈ ((-π(,)π)–cn→ℂ) ↔ ((𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦))))
149142, 148ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (-π(,)π) ↦ 𝑥) ∈ ((-π(,)π)–cn→ℂ) ↔ ((𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦)))
150147, 149mpbi 233 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦))
151150simpri 489 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦)
152 fveq2 6661 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) = ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0))
153 oveq2 7157 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦) = ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0))
154152, 153eleq12d 2910 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 0 → (((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦) ↔ ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0)))
155154rspccva 3608 . . . . . . . . . . . . . . . . . 18 ((∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 𝑦) ∧ 0 ∈ (-π(,)π)) → ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0))
156151, 44, 155mp2an 691 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0)
157 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → 𝑥 = 0)
158 eqid 2824 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (-π(,)π) ↦ 𝑥) = (𝑥 ∈ (-π(,)π) ↦ 𝑥)
159 c0ex 10633 . . . . . . . . . . . . . . . . . . 19 0 ∈ V
160157, 158, 159fvmpt 6759 . . . . . . . . . . . . . . . . . 18 (0 ∈ (-π(,)π) → ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) = 0)
16144, 160ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ 𝑥)‘0) = 0
162 elioore 12765 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (-π(,)π) → 𝑥 ∈ ℝ)
163162recnd 10667 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (-π(,)π) → 𝑥 ∈ ℂ)
164158, 163fmpti 6867 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ
165164a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (-π(,)π) ↦ 𝑥):(-π(,)π)⟶ℂ)
166165limcdif 24482 . . . . . . . . . . . . . . . . . . 19 (⊤ → ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0) = (((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) lim 0))
167166mptru 1545 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0) = (((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) lim 0)
168 resmpt 5892 . . . . . . . . . . . . . . . . . . . 20 (((-π(,)π) ∖ {0}) ⊆ (-π(,)π) → ((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
16916, 168ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)
170169oveq1i 7159 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ (-π(,)π) ↦ 𝑥) ↾ ((-π(,)π) ∖ {0})) lim 0) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) lim 0)
171167, 170eqtri 2847 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ 𝑥) lim 0) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) lim 0)
172156, 161, 1713eltr3i 2928 . . . . . . . . . . . . . . . 16 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) lim 0)
173172a1i 11 . . . . . . . . . . . . . . 15 (⊤ → 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) lim 0))
174 eqid 2824 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℂ ↦ 2) = (𝑥 ∈ ℂ ↦ 2)
175144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 ∈ ℂ → ℂ ⊆ ℂ)
176 2cnd 11712 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 ∈ ℂ → 2 ∈ ℂ)
177175, 176, 175constcncfg 42440 . . . . . . . . . . . . . . . . . . . . . . . 24 (2 ∈ ℂ → (𝑥 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
178102, 177mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → (𝑥 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
179 2cnd 11712 . . . . . . . . . . . . . . . . . . . . . . 23 ((⊤ ∧ 𝑥 ∈ (-π(,)π)) → 2 ∈ ℂ)
180174, 178, 143, 145, 179cncfmptssg 42439 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑥 ∈ (-π(,)π) ↦ 2) ∈ ((-π(,)π)–cn→ℂ))
181 sincn 25042 . . . . . . . . . . . . . . . . . . . . . . . 24 sin ∈ (ℂ–cn→ℂ)
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → sin ∈ (ℂ–cn→ℂ))
183 eqid 2824 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℂ ↦ (𝑥 / 2)) = (𝑥 ∈ ℂ ↦ (𝑥 / 2))
184183divccncf 23514 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ (ℂ–cn→ℂ))
185102, 81, 184mp2an 691 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ (ℂ–cn→ℂ)
186185a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (⊤ → (𝑥 ∈ ℂ ↦ (𝑥 / 2)) ∈ (ℂ–cn→ℂ))
187163adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⊤ ∧ 𝑥 ∈ (-π(,)π)) → 𝑥 ∈ ℂ)
188187halfcld 11879 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⊤ ∧ 𝑥 ∈ (-π(,)π)) → (𝑥 / 2) ∈ ℂ)
189183, 186, 143, 145, 188cncfmptssg 42439 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → (𝑥 ∈ (-π(,)π) ↦ (𝑥 / 2)) ∈ ((-π(,)π)–cn→ℂ))
190182, 189cncfmpt1f 23522 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑥 ∈ (-π(,)π) ↦ (sin‘(𝑥 / 2))) ∈ ((-π(,)π)–cn→ℂ))
191180, 190mulcncf 24053 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ∈ ((-π(,)π)–cn→ℂ))
192191mptru 1545 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ∈ ((-π(,)π)–cn→ℂ)
193 cnlimc 24494 . . . . . . . . . . . . . . . . . . . . 21 ((-π(,)π) ⊆ ℂ → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ∈ ((-π(,)π)–cn→ℂ) ↔ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦))))
194142, 193ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ∈ ((-π(,)π)–cn→ℂ) ↔ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦)))
195192, 194mpbi 233 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):(-π(,)π)⟶ℂ ∧ ∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦))
196195simpri 489 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦)
197 fveq2 6661 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0))
198 oveq2 7157 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 0 → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦) = ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0))
199197, 198eleq12d 2910 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 0 → (((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦) ↔ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)))
200199rspccva 3608 . . . . . . . . . . . . . . . . . 18 ((∀𝑦 ∈ (-π(,)π)((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 𝑦) ∧ 0 ∈ (-π(,)π)) → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0))
201196, 44, 200mp2an 691 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) ∈ ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)
202 oveq1 7156 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 0 → (𝑥 / 2) = (0 / 2))
203102, 81div0i 11372 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 / 2) = 0
204202, 203syl6eq 2875 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 0 → (𝑥 / 2) = 0)
205204fveq2d 6665 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 0 → (sin‘(𝑥 / 2)) = (sin‘0))
206 sin0 15502 . . . . . . . . . . . . . . . . . . . . . 22 (sin‘0) = 0
207205, 206syl6eq 2875 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 0 → (sin‘(𝑥 / 2)) = 0)
208207oveq2d 7165 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 0 → (2 · (sin‘(𝑥 / 2))) = (2 · 0))
209 2t0e0 11803 . . . . . . . . . . . . . . . . . . . 20 (2 · 0) = 0
210208, 209syl6eq 2875 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → (2 · (sin‘(𝑥 / 2))) = 0)
211 eqid 2824 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))
212210, 211, 159fvmpt 6759 . . . . . . . . . . . . . . . . . 18 (0 ∈ (-π(,)π) → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) = 0)
21344, 212ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2))))‘0) = 0
214 2cnd 11712 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (-π(,)π) → 2 ∈ ℂ)
215163halfcld 11879 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ (-π(,)π) → (𝑥 / 2) ∈ ℂ)
216215sincld 15483 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (-π(,)π) → (sin‘(𝑥 / 2)) ∈ ℂ)
217214, 216mulcld 10659 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (-π(,)π) → (2 · (sin‘(𝑥 / 2))) ∈ ℂ)
218211, 217fmpti 6867 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):(-π(,)π)⟶ℂ
219218a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))):(-π(,)π)⟶ℂ)
220219limcdif 24482 . . . . . . . . . . . . . . . . . . 19 (⊤ → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0) = (((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) lim 0))
221220mptru 1545 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0) = (((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) lim 0)
222 resmpt 5892 . . . . . . . . . . . . . . . . . . . 20 (((-π(,)π) ∖ {0}) ⊆ (-π(,)π) → ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
22316, 222ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))
224223oveq1i 7159 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) ↾ ((-π(,)π) ∖ {0})) lim 0) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)
225221, 224eqtri 2847 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (-π(,)π) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)
226201, 213, 2253eltr3i 2928 . . . . . . . . . . . . . . . 16 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0)
227226a1i 11 . . . . . . . . . . . . . . 15 (⊤ → 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) lim 0))
228 eqidd 2825 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
229 oveq1 7156 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑥 / 2) = (𝑦 / 2))
230229fveq2d 6665 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (sin‘(𝑥 / 2)) = (sin‘(𝑦 / 2)))
231230oveq2d 7165 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → (2 · (sin‘(𝑥 / 2))) = (2 · (sin‘(𝑦 / 2))))
232231adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑦) → (2 · (sin‘(𝑥 / 2))) = (2 · (sin‘(𝑦 / 2))))
233 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ ((-π(,)π) ∖ {0}))
23426a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ)
23519sseli 3949 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ ℝ)
236235rehalfcld 11881 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑦 / 2) ∈ ℝ)
237236resincld 15496 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑦 / 2)) ∈ ℝ)
238234, 237remulcld 10669 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (2 · (sin‘(𝑦 / 2))) ∈ ℝ)
239228, 232, 233, 238fvmptd 6766 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = (2 · (sin‘(𝑦 / 2))))
240 2cnd 11712 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℂ)
241237recnd 10667 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑦 / 2)) ∈ ℂ)
24281a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 2 ≠ 0)
243 ioossicc 12820 . . . . . . . . . . . . . . . . . . . . . . 23 (-π(,)π) ⊆ (-π[,]π)
244 eldifi 4089 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ (-π(,)π))
245243, 244sseldi 3951 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ (-π[,]π))
246 eldifsni 4707 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ≠ 0)
247 fourierdlem44 42719 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ (-π[,]π) ∧ 𝑦 ≠ 0) → (sin‘(𝑦 / 2)) ≠ 0)
248245, 246, 247syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑦 / 2)) ≠ 0)
249240, 241, 242, 248mulne0d 11290 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (2 · (sin‘(𝑦 / 2))) ≠ 0)
250239, 249eqnetrd 3081 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) ≠ 0)
251250neneqd 3019 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ¬ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0)
252251nrex 3261 . . . . . . . . . . . . . . . . 17 ¬ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0
25325fnmpt 6477 . . . . . . . . . . . . . . . . . . 19 (∀𝑥 ∈ ((-π(,)π) ∖ {0})(2 · (sin‘(𝑥 / 2))) ∈ ℝ → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) Fn ((-π(,)π) ∖ {0}))
254253, 30mprg 3147 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) Fn ((-π(,)π) ∖ {0})
255 ssid 3975 . . . . . . . . . . . . . . . . . 18 ((-π(,)π) ∖ {0}) ⊆ ((-π(,)π) ∖ {0})
256 fvelimab 6728 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) Fn ((-π(,)π) ∖ {0}) ∧ ((-π(,)π) ∖ {0}) ⊆ ((-π(,)π) ∖ {0})) → (0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) “ ((-π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0))
257254, 255, 256mp2an 691 . . . . . . . . . . . . . . . . 17 (0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) “ ((-π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑦) = 0)
258252, 257mtbir 326 . . . . . . . . . . . . . . . 16 ¬ 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) “ ((-π(,)π) ∖ {0}))
259258a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ¬ 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) “ ((-π(,)π) ∖ {0})))
260 eqidd 2825 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))))
261229fveq2d 6665 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (cos‘(𝑥 / 2)) = (cos‘(𝑦 / 2)))
262261adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑦) → (cos‘(𝑥 / 2)) = (cos‘(𝑦 / 2)))
263235recnd 10667 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 ∈ ℂ)
264263halfcld 11879 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑦 / 2) ∈ ℂ)
265264coscld 15484 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑦 / 2)) ∈ ℂ)
266260, 262, 233, 265fvmptd 6766 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = (cos‘(𝑦 / 2)))
267236rered 14583 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (ℜ‘(𝑦 / 2)) = (𝑦 / 2))
268 halfpire 25060 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π / 2) ∈ ℝ
269268renegcli 10945 . . . . . . . . . . . . . . . . . . . . . . . . . 26 -(π / 2) ∈ ℝ
270269a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ)
271270rexrd 10689 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ*)
272268a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (π / 2) ∈ ℝ)
273272rexrd 10689 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (π / 2) ∈ ℝ*)
274 picn 25055 . . . . . . . . . . . . . . . . . . . . . . . . . 26 π ∈ ℂ
275 divneg 11330 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(π / 2) = (-π / 2))
276274, 102, 81, 275mp3an 1458 . . . . . . . . . . . . . . . . . . . . . . . . 25 -(π / 2) = (-π / 2)
27739a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -π ∈ ℝ)
278 2rp 12391 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ∈ ℝ+
279278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ+)
28040a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -π ∈ ℝ*)
28141a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ((-π(,)π) ∖ {0}) → π ∈ ℝ*)
282 ioogtlb 42058 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝑦 ∈ (-π(,)π)) → -π < 𝑦)
283280, 281, 244, 282syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -π < 𝑦)
284277, 235, 279, 283ltdiv1dd 12485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (-π / 2) < (𝑦 / 2))
285276, 284eqbrtrid 5087 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) < (𝑦 / 2))
28638a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → π ∈ ℝ)
287 iooltub 42073 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝑦 ∈ (-π(,)π)) → 𝑦 < π)
288280, 281, 244, 287syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ((-π(,)π) ∖ {0}) → 𝑦 < π)
289235, 286, 279, 288ltdiv1dd 12485 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑦 / 2) < (π / 2))
290271, 273, 236, 285, 289eliood 42061 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (𝑦 / 2) ∈ (-(π / 2)(,)(π / 2)))
291267, 290eqeltrd 2916 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (ℜ‘(𝑦 / 2)) ∈ (-(π / 2)(,)(π / 2)))
292 cosne0 25124 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 / 2) ∈ ℂ ∧ (ℜ‘(𝑦 / 2)) ∈ (-(π / 2)(,)(π / 2))) → (cos‘(𝑦 / 2)) ≠ 0)
293264, 291, 292syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑦 / 2)) ≠ 0)
294266, 293eqnetrd 3081 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) ≠ 0)
295294neneqd 3019 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ((-π(,)π) ∖ {0}) → ¬ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0)
296295nrex 3261 . . . . . . . . . . . . . . . . . 18 ¬ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0
29772, 73fnmpti 6480 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) Fn ((-π(,)π) ∖ {0})
298 fvelimab 6728 . . . . . . . . . . . . . . . . . . 19 (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) Fn ((-π(,)π) ∖ {0}) ∧ ((-π(,)π) ∖ {0}) ⊆ ((-π(,)π) ∖ {0})) → (0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0))
299297, 255, 298mp2an 691 . . . . . . . . . . . . . . . . . 18 (0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0})) ↔ ∃𝑦 ∈ ((-π(,)π) ∖ {0})((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2)))‘𝑦) = 0)
300296, 299mtbir 326 . . . . . . . . . . . . . . . . 17 ¬ 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0}))
301135imaeq1i 5913 . . . . . . . . . . . . . . . . . 18 ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) “ ((-π(,)π) ∖ {0})) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0}))
302301eleq2i 2907 . . . . . . . . . . . . . . . . 17 (0 ∈ ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) “ ((-π(,)π) ∖ {0})) ↔ 0 ∈ ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))) “ ((-π(,)π) ∖ {0})))
303300, 302mtbir 326 . . . . . . . . . . . . . . . 16 ¬ 0 ∈ ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) “ ((-π(,)π) ∖ {0}))
304303a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ¬ 0 ∈ ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) “ ((-π(,)π) ∖ {0})))
305 eqid 2824 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑠 / 2))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑠 / 2)))
306 eqid 2824 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2))))
30719sseli 3949 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 ∈ ℝ)
308307recnd 10667 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 ∈ ℂ)
309308halfcld 11879 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑠 / 2) ∈ ℂ)
310309coscld 15484 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ∈ ℂ)
311307rehalfcld 11881 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑠 / 2) ∈ ℝ)
312311rered 14583 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (ℜ‘(𝑠 / 2)) = (𝑠 / 2))
313269a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ)
314313rexrd 10689 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) ∈ ℝ*)
315268a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (π / 2) ∈ ℝ)
316315rexrd 10689 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (π / 2) ∈ ℝ*)
31738a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ((-π(,)π) ∖ {0}) → π ∈ ℝ)
318317renegcld 11065 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -π ∈ ℝ)
319278a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ+)
32040a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -π ∈ ℝ*)
32141a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ((-π(,)π) ∖ {0}) → π ∈ ℝ*)
322 eldifi 4089 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 ∈ (-π(,)π))
323 ioogtlb 42058 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝑠 ∈ (-π(,)π)) → -π < 𝑠)
324320, 321, 322, 323syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -π < 𝑠)
325318, 307, 319, 324ltdiv1dd 12485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (-π / 2) < (𝑠 / 2))
326276, 325eqbrtrid 5087 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → -(π / 2) < (𝑠 / 2))
327 iooltub 42073 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((-π ∈ ℝ* ∧ π ∈ ℝ*𝑠 ∈ (-π(,)π)) → 𝑠 < π)
328320, 321, 322, 327syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 < π)
329307, 317, 319, 328ltdiv1dd 12485 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑠 / 2) < (π / 2))
330314, 316, 311, 326, 329eliood 42061 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑠 / 2) ∈ (-(π / 2)(,)(π / 2)))
331312, 330eqeltrd 2916 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (ℜ‘(𝑠 / 2)) ∈ (-(π / 2)(,)(π / 2)))
332 cosne0 25124 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑠 / 2) ∈ ℂ ∧ (ℜ‘(𝑠 / 2)) ∈ (-(π / 2)(,)(π / 2))) → (cos‘(𝑠 / 2)) ≠ 0)
333309, 331, 332syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ≠ 0)
334333neneqd 3019 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ¬ (cos‘(𝑠 / 2)) = 0)
335311recoscld 15497 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ∈ ℝ)
336 elsng 4564 . . . . . . . . . . . . . . . . . . . . 21 ((cos‘(𝑠 / 2)) ∈ ℝ → ((cos‘(𝑠 / 2)) ∈ {0} ↔ (cos‘(𝑠 / 2)) = 0))
337335, 336syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((cos‘(𝑠 / 2)) ∈ {0} ↔ (cos‘(𝑠 / 2)) = 0))
338334, 337mtbird 328 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ¬ (cos‘(𝑠 / 2)) ∈ {0})
339310, 338eldifd 3930 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) ∈ (ℂ ∖ {0}))
340339adantl 485 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑠 ∈ ((-π(,)π) ∖ {0})) → (cos‘(𝑠 / 2)) ∈ (ℂ ∖ {0}))
341309ad2antrl 727 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ (𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ (𝑠 / 2) ≠ 0)) → (𝑠 / 2) ∈ ℂ)
342 cosf 15478 . . . . . . . . . . . . . . . . . . . 20 cos:ℂ⟶ℂ
343342a1i 11 . . . . . . . . . . . . . . . . . . 19 (⊤ → cos:ℂ⟶ℂ)
344343ffvelrnda 6842 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑥 ∈ ℂ) → (cos‘𝑥) ∈ ℂ)
345 eqid 2824 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ℂ ↦ (𝑠 / 2)) = (𝑠 ∈ ℂ ↦ (𝑠 / 2))
346345divccncf 23514 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 ∈ ℂ ∧ 2 ≠ 0) → (𝑠 ∈ ℂ ↦ (𝑠 / 2)) ∈ (ℂ–cn→ℂ))
347102, 81, 346mp2an 691 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ℂ ↦ (𝑠 / 2)) ∈ (ℂ–cn→ℂ)
348347a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑠 ∈ ℂ ↦ (𝑠 / 2)) ∈ (ℂ–cn→ℂ))
349141adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑠 ∈ (-π(,)π)) → 𝑠 ∈ ℂ)
350349halfcld 11879 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑠 ∈ (-π(,)π)) → (𝑠 / 2) ∈ ℂ)
351345, 348, 143, 145, 350cncfmptssg 42439 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ∈ ((-π(,)π)–cn→ℂ))
352 oveq1 7156 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 0 → (𝑠 / 2) = (0 / 2))
353352, 203syl6eq 2875 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → (𝑠 / 2) = 0)
354351, 45, 353cnmptlimc 24496 . . . . . . . . . . . . . . . . . . 19 (⊤ → 0 ∈ ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) lim 0))
355 eqid 2824 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) = (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2))
356141halfcld 11879 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ (-π(,)π) → (𝑠 / 2) ∈ ℂ)
357355, 356fmpti 6867 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)):(-π(,)π)⟶ℂ
358357a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)):(-π(,)π)⟶ℂ)
359358limcdif 24482 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) lim 0) = (((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) lim 0))
360359mptru 1545 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) lim 0) = (((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) lim 0)
361 resmpt 5892 . . . . . . . . . . . . . . . . . . . . . 22 (((-π(,)π) ∖ {0}) ⊆ (-π(,)π) → ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2)))
36216, 361ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2))
363362oveq1i 7159 . . . . . . . . . . . . . . . . . . . 20 (((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) ↾ ((-π(,)π) ∖ {0})) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2)) lim 0)
364360, 363eqtri 2847 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (-π(,)π) ↦ (𝑠 / 2)) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2)) lim 0)
365354, 364eleqtrdi 2926 . . . . . . . . . . . . . . . . . 18 (⊤ → 0 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / 2)) lim 0))
366 ffn 6503 . . . . . . . . . . . . . . . . . . . . . . 23 (cos:ℂ⟶ℂ → cos Fn ℂ)
367342, 366ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 cos Fn ℂ
368 dffn5 6715 . . . . . . . . . . . . . . . . . . . . . 22 (cos Fn ℂ ↔ cos = (𝑥 ∈ ℂ ↦ (cos‘𝑥)))
369367, 368mpbi 233 . . . . . . . . . . . . . . . . . . . . 21 cos = (𝑥 ∈ ℂ ↦ (cos‘𝑥))
370 coscn 25043 . . . . . . . . . . . . . . . . . . . . 21 cos ∈ (ℂ–cn→ℂ)
371369, 370eqeltrri 2913 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℂ ↦ (cos‘𝑥)) ∈ (ℂ–cn→ℂ)
372371a1i 11 . . . . . . . . . . . . . . . . . . 19 (⊤ → (𝑥 ∈ ℂ ↦ (cos‘𝑥)) ∈ (ℂ–cn→ℂ))
373 0cnd 10632 . . . . . . . . . . . . . . . . . . 19 (⊤ → 0 ∈ ℂ)
374 fveq2 6661 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 0 → (cos‘𝑥) = (cos‘0))
375 cos0 15503 . . . . . . . . . . . . . . . . . . . 20 (cos‘0) = 1
376374, 375syl6eq 2875 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 0 → (cos‘𝑥) = 1)
377372, 373, 376cnmptlimc 24496 . . . . . . . . . . . . . . . . . 18 (⊤ → 1 ∈ ((𝑥 ∈ ℂ ↦ (cos‘𝑥)) lim 0))
378 fveq2 6661 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑠 / 2) → (cos‘𝑥) = (cos‘(𝑠 / 2)))
379 fveq2 6661 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 / 2) = 0 → (cos‘(𝑠 / 2)) = (cos‘0))
380379, 375syl6eq 2875 . . . . . . . . . . . . . . . . . . 19 ((𝑠 / 2) = 0 → (cos‘(𝑠 / 2)) = 1)
381380ad2antll 728 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ (𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ (𝑠 / 2) = 0)) → (cos‘(𝑠 / 2)) = 1)
382341, 344, 365, 377, 378, 381limcco 24499 . . . . . . . . . . . . . . . . 17 (⊤ → 1 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑠 / 2))) lim 0))
383 ax-1ne0 10604 . . . . . . . . . . . . . . . . . 18 1 ≠ 0
384383a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → 1 ≠ 0)
385305, 306, 340, 382, 384reclimc 42221 . . . . . . . . . . . . . . . 16 (⊤ → (1 / 1) ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) lim 0))
386 1div1e1 11328 . . . . . . . . . . . . . . . 16 (1 / 1) = 1
38766fveq1i 6662 . . . . . . . . . . . . . . . . . . . 20 ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) = ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1)‘𝑠)
388 eqidd 2825 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1))
389 eqidd 2825 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → 1 = 1)
390 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 𝑠 ∈ ((-π(,)π) ∖ {0}))
391 1red 10640 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 1 ∈ ℝ)
392388, 389, 390, 391fvmptd 6766 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 1)‘𝑠) = 1)
393387, 392syl5req 2872 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 1 = ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠))
394135a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (cos‘(𝑥 / 2))))
395 oveq1 7156 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑠 → (𝑥 / 2) = (𝑠 / 2))
396395fveq2d 6665 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑠 → (cos‘(𝑥 / 2)) = (cos‘(𝑠 / 2)))
397396adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (cos‘(𝑥 / 2)) = (cos‘(𝑠 / 2)))
398394, 397, 390, 335fvmptd 6766 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠) = (cos‘(𝑠 / 2)))
399398eqcomd 2830 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (cos‘(𝑠 / 2)) = ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠))
400393, 399oveq12d 7167 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (1 / (cos‘(𝑠 / 2))) = (((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) / ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠)))
401400mpteq2ia 5143 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) / ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠)))
402401oveq1i 7159 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (1 / (cos‘(𝑠 / 2)))) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))‘𝑠) / ((ℝ D (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))‘𝑠))) lim 0)
403385, 386, 4023eltr3g 2932 . . . . . . . . . . . . . . 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 24622 . . . . . . . . . . . . . 14 (⊤ → 1 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) lim 0))
405404mptru 1545 . . . . . . . . . . . . 13 1 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) lim 0)
406 eqidd 2825 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥))
407 simpr 488 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → 𝑥 = 𝑠)
408406, 407, 390, 307fvmptd 6766 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) = 𝑠)
409 eqidd 2825 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))) = (𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2)))))
410407oveq1d 7164 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (𝑥 / 2) = (𝑠 / 2))
411410fveq2d 6665 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (sin‘(𝑥 / 2)) = (sin‘(𝑠 / 2)))
412411oveq2d 7165 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ∧ 𝑥 = 𝑠) → (2 · (sin‘(𝑥 / 2))) = (2 · (sin‘(𝑠 / 2))))
41326a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → 2 ∈ ℝ)
414311resincld 15496 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (sin‘(𝑠 / 2)) ∈ ℝ)
415413, 414remulcld 10669 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ∈ ℝ)
416409, 412, 390, 415fvmptd 6766 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠) = (2 · (sin‘(𝑠 / 2))))
417408, 416oveq12d 7167 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((-π(,)π) ∖ {0}) → (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠)) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
418417mpteq2ia 5143 . . . . . . . . . . . . . 14 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
419418oveq1i 7159 . . . . . . . . . . . . 13 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ 𝑥)‘𝑠) / ((𝑥 ∈ ((-π(,)π) ∖ {0}) ↦ (2 · (sin‘(𝑥 / 2))))‘𝑠))) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim 0)
420405, 419eleqtri 2914 . . . . . . . . . . . 12 1 ∈ ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim 0)
42110oveq1i 7159 . . . . . . . . . . . . . 14 (𝐾 lim 0) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0)
42210feq1i 6494 . . . . . . . . . . . . . . . . . . 19 (𝐾:(-π[,]π)⟶ℂ ↔ (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π[,]π)⟶ℂ)
42314, 422mpbi 233 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π[,]π)⟶ℂ
424423a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π[,]π)⟶ℂ)
425243a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → (-π(,)π) ⊆ (-π[,]π))
426 iccssre 12816 . . . . . . . . . . . . . . . . . . . 20 ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
42739, 38, 426mp2an 691 . . . . . . . . . . . . . . . . . . 19 (-π[,]π) ⊆ ℝ
428427a1i 11 . . . . . . . . . . . . . . . . . 18 (⊤ → (-π[,]π) ⊆ ℝ)
429428, 12sstrdi 3965 . . . . . . . . . . . . . . . . 17 (⊤ → (-π[,]π) ⊆ ℂ)
430 eqid 2824 . . . . . . . . . . . . . . . . 17 ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})) = ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0}))
43139, 35, 36ltleii 10761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -π ≤ 0
43235, 38, 37ltleii 10761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ≤ π
43339, 38elicc2i 12800 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (0 ∈ (-π[,]π) ↔ (0 ∈ ℝ ∧ -π ≤ 0 ∧ 0 ≤ π))
43435, 431, 432, 433mpbir3an 1338 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ∈ (-π[,]π)
435159snss 4703 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 ∈ (-π[,]π) ↔ {0} ⊆ (-π[,]π))
436434, 435mpbi 233 . . . . . . . . . . . . . . . . . . . . . . . . 25 {0} ⊆ (-π[,]π)
437 ssequn2 4145 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({0} ⊆ (-π[,]π) ↔ ((-π[,]π) ∪ {0}) = (-π[,]π))
438436, 437mpbi 233 . . . . . . . . . . . . . . . . . . . . . . . 24 ((-π[,]π) ∪ {0}) = (-π[,]π)
439438oveq2i 7160 . . . . . . . . . . . . . . . . . . . . . . 23 ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})) = ((TopOpen‘ℂfld) ↾t (-π[,]π))
440 eqid 2824 . . . . . . . . . . . . . . . . . . . . . . . . 25 (topGen‘ran (,)) = (topGen‘ran (,))
44156, 440rerest 23412 . . . . . . . . . . . . . . . . . . . . . . . 24 ((-π[,]π) ⊆ ℝ → ((TopOpen‘ℂfld) ↾t (-π[,]π)) = ((topGen‘ran (,)) ↾t (-π[,]π)))
442427, 441ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((TopOpen‘ℂfld) ↾t (-π[,]π)) = ((topGen‘ran (,)) ↾t (-π[,]π))
443439, 442eqtri 2847 . . . . . . . . . . . . . . . . . . . . . 22 ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})) = ((topGen‘ran (,)) ↾t (-π[,]π))
444443fveq2i 6664 . . . . . . . . . . . . . . . . . . . . 21 (int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0}))) = (int‘((topGen‘ran (,)) ↾t (-π[,]π)))
445159snss 4703 . . . . . . . . . . . . . . . . . . . . . . 23 (0 ∈ (-π(,)π) ↔ {0} ⊆ (-π(,)π))
44644, 445mpbi 233 . . . . . . . . . . . . . . . . . . . . . 22 {0} ⊆ (-π(,)π)
447 ssequn2 4145 . . . . . . . . . . . . . . . . . . . . . 22 ({0} ⊆ (-π(,)π) ↔ ((-π(,)π) ∪ {0}) = (-π(,)π))
448446, 447mpbi 233 . . . . . . . . . . . . . . . . . . . . 21 ((-π(,)π) ∪ {0}) = (-π(,)π)
449444, 448fveq12i 6667 . . . . . . . . . . . . . . . . . . . 20 ((int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})))‘((-π(,)π) ∪ {0})) = ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘(-π(,)π))
450 resttopon 21769 . . . . . . . . . . . . . . . . . . . . . . 23 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ (-π[,]π) ⊆ ℝ) → ((topGen‘ran (,)) ↾t (-π[,]π)) ∈ (TopOn‘(-π[,]π)))
45160, 427, 450mp2an 691 . . . . . . . . . . . . . . . . . . . . . 22 ((topGen‘ran (,)) ↾t (-π[,]π)) ∈ (TopOn‘(-π[,]π))
452451topontopi 21523 . . . . . . . . . . . . . . . . . . . . 21 ((topGen‘ran (,)) ↾t (-π[,]π)) ∈ Top
453 retop 23370 . . . . . . . . . . . . . . . . . . . . . . . 24 (topGen‘ran (,)) ∈ Top
454 ovex 7182 . . . . . . . . . . . . . . . . . . . . . . . 24 (-π[,]π) ∈ V
455453, 454pm3.2i 474 . . . . . . . . . . . . . . . . . . . . . . 23 ((topGen‘ran (,)) ∈ Top ∧ (-π[,]π) ∈ V)
456 ssid 3975 . . . . . . . . . . . . . . . . . . . . . . . 24 (-π(,)π) ⊆ (-π(,)π)
45733, 243, 4563pm3.2i 1336 . . . . . . . . . . . . . . . . . . . . . . 23 ((-π(,)π) ∈ (topGen‘ran (,)) ∧ (-π(,)π) ⊆ (-π[,]π) ∧ (-π(,)π) ⊆ (-π(,)π))
458 restopnb 21783 . . . . . . . . . . . . . . . . . . . . . . 23 ((((topGen‘ran (,)) ∈ Top ∧ (-π[,]π) ∈ V) ∧ ((-π(,)π) ∈ (topGen‘ran (,)) ∧ (-π(,)π) ⊆ (-π[,]π) ∧ (-π(,)π) ⊆ (-π(,)π))) → ((-π(,)π) ∈ (topGen‘ran (,)) ↔ (-π(,)π) ∈ ((topGen‘ran (,)) ↾t (-π[,]π))))
459455, 457, 458mp2an 691 . . . . . . . . . . . . . . . . . . . . . 22 ((-π(,)π) ∈ (topGen‘ran (,)) ↔ (-π(,)π) ∈ ((topGen‘ran (,)) ↾t (-π[,]π)))
46033, 459mpbi 233 . . . . . . . . . . . . . . . . . . . . 21 (-π(,)π) ∈ ((topGen‘ran (,)) ↾t (-π[,]π))
461 isopn3i 21690 . . . . . . . . . . . . . . . . . . . . 21 ((((topGen‘ran (,)) ↾t (-π[,]π)) ∈ Top ∧ (-π(,)π) ∈ ((topGen‘ran (,)) ↾t (-π[,]π))) → ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘(-π(,)π)) = (-π(,)π))
462452, 460, 461mp2an 691 . . . . . . . . . . . . . . . . . . . 20 ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘(-π(,)π)) = (-π(,)π)
463 eqid 2824 . . . . . . . . . . . . . . . . . . . 20 (-π(,)π) = (-π(,)π)
464449, 462, 4633eqtrri 2852 . . . . . . . . . . . . . . . . . . 19 (-π(,)π) = ((int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})))‘((-π(,)π) ∪ {0}))
46544, 464eleqtri 2914 . . . . . . . . . . . . . . . . . 18 0 ∈ ((int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})))‘((-π(,)π) ∪ {0}))
466465a1i 11 . . . . . . . . . . . . . . . . 17 (⊤ → 0 ∈ ((int‘((TopOpen‘ℂfld) ↾t ((-π[,]π) ∪ {0})))‘((-π(,)π) ∪ {0})))
467424, 425, 429, 56, 430, 466limcres 24492 . . . . . . . . . . . . . . . 16 (⊤ → (((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (-π(,)π)) lim 0) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0))
468467mptru 1545 . . . . . . . . . . . . . . 15 (((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (-π(,)π)) lim 0) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0)
469468eqcomi 2833 . . . . . . . . . . . . . 14 ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0) = (((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (-π(,)π)) lim 0)
470 resmpt 5892 . . . . . . . . . . . . . . . 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 7159 . . . . . . . . . . . . . 14 (((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ (-π(,)π)) lim 0) = ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0)
473421, 469, 4723eqtri 2851 . . . . . . . . . . . . 13 (𝐾 lim 0) = ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0)
474 eqid 2824 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))))
475 iftrue 4456 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = 1)
476 1cnd 10634 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 0 → 1 ∈ ℂ)
477475, 476eqeltrd 2916 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 0 → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
478477adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (-π(,)π) ∧ 𝑠 = 0) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
479 iffalse 4459 . . . . . . . . . . . . . . . . . . . 20 𝑠 = 0 → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
480479adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
481141adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ℂ)
482 2cnd 11712 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → 2 ∈ ℂ)
483481halfcld 11879 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (𝑠 / 2) ∈ ℂ)
484483sincld 15483 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (sin‘(𝑠 / 2)) ∈ ℂ)
485482, 484mulcld 10659 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
48681a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → 2 ≠ 0)
487243sseli 3949 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ (-π(,)π) → 𝑠 ∈ (-π[,]π))
488 neqne 3022 . . . . . . . . . . . . . . . . . . . . . 22 𝑠 = 0 → 𝑠 ≠ 0)
489 fourierdlem44 42719 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠 ∈ (-π[,]π) ∧ 𝑠 ≠ 0) → (sin‘(𝑠 / 2)) ≠ 0)
490487, 488, 489syl2an 598 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (sin‘(𝑠 / 2)) ≠ 0)
491482, 484, 486, 490mulne0d 11290 . . . . . . . . . . . . . . . . . . . 20 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
492481, 485, 491divcld 11414 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → (𝑠 / (2 · (sin‘(𝑠 / 2)))) ∈ ℂ)
493480, 492eqeltrd 2916 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (-π(,)π) ∧ ¬ 𝑠 = 0) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
494478, 493pm2.61dan 812 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ (-π(,)π) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ℂ)
495474, 494fmpti 6867 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π(,)π)⟶ℂ
496495a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))):(-π(,)π)⟶ℂ)
497496limcdif 24482 . . . . . . . . . . . . . 14 (⊤ → ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0) = (((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π(,)π) ∖ {0})) lim 0))
498497mptru 1545 . . . . . . . . . . . . 13 ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) lim 0) = (((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π(,)π) ∖ {0})) lim 0)
499 resmpt 5892 . . . . . . . . . . . . . . . 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 4090 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ¬ 𝑠 ∈ {0})
502 velsn 4566 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ {0} ↔ 𝑠 = 0)
503501, 502sylnib 331 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π(,)π) ∖ {0}) → ¬ 𝑠 = 0)
504503, 479syl 17 . . . . . . . . . . . . . . . 16 (𝑠 ∈ ((-π(,)π) ∖ {0}) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
505504mpteq2ia 5143 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
506500, 505eqtri 2847 . . . . . . . . . . . . . 14 ((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π(,)π) ∖ {0})) = (𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
507506oveq1i 7159 . . . . . . . . . . . . 13 (((𝑠 ∈ (-π(,)π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π(,)π) ∖ {0})) lim 0) = ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim 0)
508473, 498, 5073eqtrri 2852 . . . . . . . . . . . 12 ((𝑠 ∈ ((-π(,)π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) lim 0) = (𝐾 lim 0)
509420, 508eleqtri 2914 . . . . . . . . . . 11 1 ∈ (𝐾 lim 0)
510509a1i 11 . . . . . . . . . 10 (𝑠 = 0 → 1 ∈ (𝐾 lim 0))
511 fveq2 6661 . . . . . . . . . . 11 (𝑠 = 0 → (𝐾𝑠) = (𝐾‘0))
512475, 10, 47fvmpt 6759 . . . . . . . . . . . 12 (0 ∈ (-π[,]π) → (𝐾‘0) = 1)
513434, 512ax-mp 5 . . . . . . . . . . 11 (𝐾‘0) = 1
514511, 513syl6eq 2875 . . . . . . . . . 10 (𝑠 = 0 → (𝐾𝑠) = 1)
515 oveq2 7157 . . . . . . . . . 10 (𝑠 = 0 → (𝐾 lim 𝑠) = (𝐾 lim 0))
516510, 514, 5153eltr4d 2931 . . . . . . . . 9 (𝑠 = 0 → (𝐾𝑠) ∈ (𝐾 lim 𝑠))
517427, 12sstri 3962 . . . . . . . . . . 11 (-π[,]π) ⊆ ℂ
518517a1i 11 . . . . . . . . . 10 (𝑠 = 0 → (-π[,]π) ⊆ ℂ)
51938a1i 11 . . . . . . . . . . . 12 (𝑠 = 0 → π ∈ ℝ)
520519renegcld 11065 . . . . . . . . . . 11 (𝑠 = 0 → -π ∈ ℝ)
521 id 22 . . . . . . . . . . . 12 (𝑠 = 0 → 𝑠 = 0)
52235a1i 11 . . . . . . . . . . . 12 (𝑠 = 0 → 0 ∈ ℝ)
523521, 522eqeltrd 2916 . . . . . . . . . . 11 (𝑠 = 0 → 𝑠 ∈ ℝ)
524431, 521breqtrrid 5090 . . . . . . . . . . 11 (𝑠 = 0 → -π ≤ 𝑠)
525521, 432eqbrtrdi 5091 . . . . . . . . . . 11 (𝑠 = 0 → 𝑠 ≤ π)
526520, 519, 523, 524, 525eliccd 42067 . . . . . . . . . 10 (𝑠 = 0 → 𝑠 ∈ (-π[,]π))
52757oveq1i 7159 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t (-π[,]π)) = (((TopOpen‘ℂfld) ↾t ℝ) ↾t (-π[,]π))
52856cnfldtop 23392 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) ∈ Top
529 reex 10626 . . . . . . . . . . . . 13 ℝ ∈ V
530 restabs 21773 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ∈ Top ∧ (-π[,]π) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂfld) ↾t ℝ) ↾t (-π[,]π)) = ((TopOpen‘ℂfld) ↾t (-π[,]π)))
531528, 427, 529, 530mp3an 1458 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ↾t ℝ) ↾t (-π[,]π)) = ((TopOpen‘ℂfld) ↾t (-π[,]π))
532527, 531eqtri 2847 . . . . . . . . . . 11 ((topGen‘ran (,)) ↾t (-π[,]π)) = ((TopOpen‘ℂfld) ↾t (-π[,]π))
53356, 532cnplimc 24493 . . . . . . . . . 10 (((-π[,]π) ⊆ ℂ ∧ 𝑠 ∈ (-π[,]π)) → (𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠) ↔ (𝐾:(-π[,]π)⟶ℂ ∧ (𝐾𝑠) ∈ (𝐾 lim 𝑠))))
534518, 526, 533syl2anc 587 . . . . . . . . 9 (𝑠 = 0 → (𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠) ↔ (𝐾:(-π[,]π)⟶ℂ ∧ (𝐾𝑠) ∈ (𝐾 lim 𝑠))))
53515, 516, 534mpbir2and 712 . . . . . . . 8 (𝑠 = 0 → 𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))
536535adantl 485 . . . . . . 7 ((𝑠 ∈ (-π[,]π) ∧ 𝑠 = 0) → 𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))
537 simpl 486 . . . . . . . . . . 11 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ (-π[,]π))
538502notbii 323 . . . . . . . . . . . . 13 𝑠 ∈ {0} ↔ ¬ 𝑠 = 0)
539538biimpri 231 . . . . . . . . . . . 12 𝑠 = 0 → ¬ 𝑠 ∈ {0})
540539adantl 485 . . . . . . . . . . 11 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → ¬ 𝑠 ∈ {0})
541537, 540eldifd 3930 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ((-π[,]π) ∖ {0}))
542 fveq2 6661 . . . . . . . . . . . 12 (𝑥 = 𝑠 → ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥) = ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠))
543542eleq2d 2901 . . . . . . . . . . 11 (𝑥 = 𝑠 → ((𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥) ↔ (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠)))
544429ssdifssd 4105 . . . . . . . . . . . . . . . . 17 (⊤ → ((-π[,]π) ∖ {0}) ⊆ ℂ)
545544, 145idcncfg 42441 . . . . . . . . . . . . . . . 16 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ 𝑠) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
546 eqid 2824 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2))))
547 2cnd 11712 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 2 ∈ ℂ)
548 eldifi 4089 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 𝑠 ∈ (-π[,]π))
549517, 548sseldi 3951 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 𝑠 ∈ ℂ)
550549halfcld 11879 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (𝑠 / 2) ∈ ℂ)
551550sincld 15483 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (sin‘(𝑠 / 2)) ∈ ℂ)
552547, 551mulcld 10659 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ∈ ℂ)
55381a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 2 ≠ 0)
554 eldifsni 4707 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 𝑠 ≠ 0)
555548, 554, 489syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (sin‘(𝑠 / 2)) ≠ 0)
556547, 551, 553, 555mulne0d 11290 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ≠ 0)
557556neneqd 3019 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ ((-π[,]π) ∖ {0}) → ¬ (2 · (sin‘(𝑠 / 2))) = 0)
558 elsng 4564 . . . . . . . . . . . . . . . . . . . . . 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 328 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ((-π[,]π) ∖ {0}) → ¬ (2 · (sin‘(𝑠 / 2))) ∈ {0})
561552, 560eldifd 3930 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (2 · (sin‘(𝑠 / 2))) ∈ (ℂ ∖ {0}))
562546, 561fmpti 6867 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))):((-π[,]π) ∖ {0})⟶(ℂ ∖ {0})
563 difss 4094 . . . . . . . . . . . . . . . . . . 19 (ℂ ∖ {0}) ⊆ ℂ
564 eqid 2824 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 ∈ ℂ ↦ 2) = (𝑠 ∈ ℂ ↦ 2)
565175, 176, 175constcncfg 42440 . . . . . . . . . . . . . . . . . . . . . . 23 (2 ∈ ℂ → (𝑠 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
566102, 565mp1i 13 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑠 ∈ ℂ ↦ 2) ∈ (ℂ–cn→ℂ))
567 2cnd 11712 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑠 ∈ ((-π[,]π) ∖ {0})) → 2 ∈ ℂ)
568564, 566, 544, 145, 567cncfmptssg 42439 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ 2) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
569549, 547, 553divrecd 11417 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 ∈ ((-π[,]π) ∖ {0}) → (𝑠 / 2) = (𝑠 · (1 / 2)))
570569mpteq2ia 5143 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / 2)) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 · (1 / 2)))
571 eqid 2824 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 ∈ ℂ ↦ (1 / 2)) = (𝑠 ∈ ℂ ↦ (1 / 2))
572144a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 / 2) ∈ ℂ → ℂ ⊆ ℂ)
573 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((1 / 2) ∈ ℂ → (1 / 2) ∈ ℂ)
574572, 573, 572constcncfg 42440 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 / 2) ∈ ℂ → (𝑠 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
57594, 574mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⊤ → (𝑠 ∈ ℂ ↦ (1 / 2)) ∈ (ℂ–cn→ℂ))
57694a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⊤ ∧ 𝑠 ∈ ((-π[,]π) ∖ {0})) → (1 / 2) ∈ ℂ)
577571, 575, 544, 145, 576cncfmptssg 42439 . . . . . . . . . . . . . . . . . . . . . . . 24 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (1 / 2)) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
578545, 577mulcncf 24053 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 · (1 / 2))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
579570, 578eqeltrid 2920 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / 2)) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
580182, 579cncfmpt1f 23522 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (sin‘(𝑠 / 2))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
581568, 580mulcncf 24053 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
582581mptru 1545 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ)
583 cncffvrn 23506 . . . . . . . . . . . . . . . . . . 19 (((ℂ ∖ {0}) ⊆ ℂ ∧ (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ)) → ((𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))):((-π[,]π) ∖ {0})⟶(ℂ ∖ {0})))
584563, 582, 583mp2an 691 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→(ℂ ∖ {0})) ↔ (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))):((-π[,]π) ∖ {0})⟶(ℂ ∖ {0}))
585562, 584mpbir 234 . . . . . . . . . . . . . . . . 17 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→(ℂ ∖ {0}))
586585a1i 11 . . . . . . . . . . . . . . . 16 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (2 · (sin‘(𝑠 / 2)))) ∈ (((-π[,]π) ∖ {0})–cn→(ℂ ∖ {0})))
587545, 586divcncf 24054 . . . . . . . . . . . . . . 15 (⊤ → (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ))
588587mptru 1545 . . . . . . . . . . . . . 14 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((-π[,]π) ∖ {0})–cn→ℂ)
589428ssdifssd 4105 . . . . . . . . . . . . . . . . 17 (⊤ → ((-π[,]π) ∖ {0}) ⊆ ℝ)
590589mptru 1545 . . . . . . . . . . . . . . . 16 ((-π[,]π) ∖ {0}) ⊆ ℝ
591590, 12sstri 3962 . . . . . . . . . . . . . . 15 ((-π[,]π) ∖ {0}) ⊆ ℂ
59257oveq1i 7159 . . . . . . . . . . . . . . . . 17 ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) = (((TopOpen‘ℂfld) ↾t ℝ) ↾t ((-π[,]π) ∖ {0}))
593 restabs 21773 . . . . . . . . . . . . . . . . . 18 (((TopOpen‘ℂfld) ∈ Top ∧ ((-π[,]π) ∖ {0}) ⊆ ℝ ∧ ℝ ∈ V) → (((TopOpen‘ℂfld) ↾t ℝ) ↾t ((-π[,]π) ∖ {0})) = ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∖ {0})))
594528, 590, 529, 593mp3an 1458 . . . . . . . . . . . . . . . . 17 (((TopOpen‘ℂfld) ↾t ℝ) ↾t ((-π[,]π) ∖ {0})) = ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∖ {0}))
595592, 594eqtri 2847 . . . . . . . . . . . . . . . 16 ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) = ((TopOpen‘ℂfld) ↾t ((-π[,]π) ∖ {0}))
596 unicntop 23394 . . . . . . . . . . . . . . . . . . 19 ℂ = (TopOpen‘ℂfld)
597596restid 16707 . . . . . . . . . . . . . . . . . 18 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
598528, 597ax-mp 5 . . . . . . . . . . . . . . . . 17 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
599598eqcomi 2833 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
60056, 595, 599cncfcn 23518 . . . . . . . . . . . . . . 15 ((((-π[,]π) ∖ {0}) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (((-π[,]π) ∖ {0})–cn→ℂ) = (((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) Cn (TopOpen‘ℂfld)))
601591, 144, 600mp2an 691 . . . . . . . . . . . . . 14 (((-π[,]π) ∖ {0})–cn→ℂ) = (((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) Cn (TopOpen‘ℂfld))
602588, 601eleqtri 2914 . . . . . . . . . . . . 13 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ (((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) Cn (TopOpen‘ℂfld))
603 resttopon 21769 . . . . . . . . . . . . . . 15 (((topGen‘ran (,)) ∈ (TopOn‘ℝ) ∧ ((-π[,]π) ∖ {0}) ⊆ ℝ) → ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) ∈ (TopOn‘((-π[,]π) ∖ {0})))
60460, 590, 603mp2an 691 . . . . . . . . . . . . . 14 ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) ∈ (TopOn‘((-π[,]π) ∖ {0}))
60556cnfldtopon 23391 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
606 cncnp 21888 . . . . . . . . . . . . . 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 691 . . . . . . . . . . . . 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 233 . . . . . . . . . . . 12 ((𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))):((-π[,]π) ∖ {0})⟶ℂ ∧ ∀𝑥 ∈ ((-π[,]π) ∖ {0})(𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥))
609608simpri 489 . . . . . . . . . . 11 𝑥 ∈ ((-π[,]π) ∖ {0})(𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2))))) ∈ ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑥)
610543, 609vtoclri 3571 . . . . . . . . . 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 5836 . . . . . . . . . 10 (𝐾 ↾ ((-π[,]π) ∖ {0})) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) ↾ ((-π[,]π) ∖ {0}))
613 difss 4094 . . . . . . . . . . 11 ((-π[,]π) ∖ {0}) ⊆ (-π[,]π)
614 resmpt 5892 . . . . . . . . . . 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 4090 . . . . . . . . . . . . 13 (𝑠 ∈ ((-π[,]π) ∖ {0}) → ¬ 𝑠 ∈ {0})
617616, 502sylnib 331 . . . . . . . . . . . 12 (𝑠 ∈ ((-π[,]π) ∖ {0}) → ¬ 𝑠 = 0)
618617, 479syl 17 . . . . . . . . . . 11 (𝑠 ∈ ((-π[,]π) ∖ {0}) → if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2))))) = (𝑠 / (2 · (sin‘(𝑠 / 2)))))
619618mpteq2ia 5143 . . . . . . . . . 10 (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ if(𝑠 = 0, 1, (𝑠 / (2 · (sin‘(𝑠 / 2)))))) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
620612, 615, 6193eqtri 2851 . . . . . . . . 9 (𝐾 ↾ ((-π[,]π) ∖ {0})) = (𝑠 ∈ ((-π[,]π) ∖ {0}) ↦ (𝑠 / (2 · (sin‘(𝑠 / 2)))))
621 restabs 21773 . . . . . . . . . . . 12 (((topGen‘ran (,)) ∈ Top ∧ ((-π[,]π) ∖ {0}) ⊆ (-π[,]π) ∧ (-π[,]π) ∈ V) → (((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) = ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})))
622453, 613, 454, 621mp3an 1458 . . . . . . . . . . 11 (((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) = ((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0}))
623622oveq1i 7159 . . . . . . . . . 10 ((((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld)) = (((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))
624623fveq1i 6662 . . . . . . . . 9 (((((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠) = ((((topGen‘ran (,)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠)
625611, 620, 6243eltr4g 2933 . . . . . . . 8 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → (𝐾 ↾ ((-π[,]π) ∖ {0})) ∈ (((((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠))
626452, 613pm3.2i 474 . . . . . . . . . 10 (((topGen‘ran (,)) ↾t (-π[,]π)) ∈ Top ∧ ((-π[,]π) ∖ {0}) ⊆ (-π[,]π))
627626a1i 11 . . . . . . . . 9 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → (((topGen‘ran (,)) ↾t (-π[,]π)) ∈ Top ∧ ((-π[,]π) ∖ {0}) ⊆ (-π[,]π)))
628 ssdif 4102 . . . . . . . . . . . . . 14 ((-π[,]π) ⊆ ℝ → ((-π[,]π) ∖ {0}) ⊆ (ℝ ∖ {0}))
629427, 628ax-mp 5 . . . . . . . . . . . . 13 ((-π[,]π) ∖ {0}) ⊆ (ℝ ∖ {0})
630629, 541sseldi 3951 . . . . . . . . . . . 12 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ (ℝ ∖ {0}))
631 sscon 4101 . . . . . . . . . . . . . . . . 17 ({0} ⊆ (-π[,]π) → (ℝ ∖ (-π[,]π)) ⊆ (ℝ ∖ {0}))
632436, 631ax-mp 5 . . . . . . . . . . . . . . . 16 (ℝ ∖ (-π[,]π)) ⊆ (ℝ ∖ {0})
633629, 632unssi 4147 . . . . . . . . . . . . . . 15 (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))) ⊆ (ℝ ∖ {0})
634 simpr 488 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (-π[,]π))
635 eldifn 4090 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (ℝ ∖ {0}) → ¬ 𝑠 ∈ {0})
636635adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ (-π[,]π)) → ¬ 𝑠 ∈ {0})
637634, 636eldifd 3930 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ ((-π[,]π) ∖ {0}))
638 elun1 4138 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ ((-π[,]π) ∖ {0}) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
639637, 638syl 17 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (ℝ ∖ {0}) ∧ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
640 eldifi 4089 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (ℝ ∖ {0}) → 𝑠 ∈ ℝ)
641640adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ ℝ)
642 simpr 488 . . . . . . . . . . . . . . . . . . 19 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ (-π[,]π)) → ¬ 𝑠 ∈ (-π[,]π))
643641, 642eldifd 3930 . . . . . . . . . . . . . . . . . 18 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (ℝ ∖ (-π[,]π)))
644 elun2 4139 . . . . . . . . . . . . . . . . . 18 (𝑠 ∈ (ℝ ∖ (-π[,]π)) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
645643, 644syl 17 . . . . . . . . . . . . . . . . 17 ((𝑠 ∈ (ℝ ∖ {0}) ∧ ¬ 𝑠 ∈ (-π[,]π)) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
646639, 645pm2.61dan 812 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (ℝ ∖ {0}) → 𝑠 ∈ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))))
647646ssriv 3957 . . . . . . . . . . . . . . 15 (ℝ ∖ {0}) ⊆ (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))
648633, 647eqssi 3969 . . . . . . . . . . . . . 14 (((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π))) = (ℝ ∖ {0})
649648fveq2i 6664 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) = ((int‘(topGen‘ran (,)))‘(ℝ ∖ {0}))
65061cldopn 21639 . . . . . . . . . . . . . . 15 ({0} ∈ (Clsd‘(topGen‘ran (,))) → (ℝ ∖ {0}) ∈ (topGen‘ran (,)))
65159, 650ax-mp 5 . . . . . . . . . . . . . 14 (ℝ ∖ {0}) ∈ (topGen‘ran (,))
652 isopn3i 21690 . . . . . . . . . . . . . 14 (((topGen‘ran (,)) ∈ Top ∧ (ℝ ∖ {0}) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘(ℝ ∖ {0})) = (ℝ ∖ {0}))
653453, 651, 652mp2an 691 . . . . . . . . . . . . 13 ((int‘(topGen‘ran (,)))‘(ℝ ∖ {0})) = (ℝ ∖ {0})
654649, 653eqtri 2847 . . . . . . . . . . . 12 ((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) = (ℝ ∖ {0})
655630, 654eleqtrrdi 2927 . . . . . . . . . . 11 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))))
656655, 537elind 4156 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ (((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) ∩ (-π[,]π)))
657 eqid 2824 . . . . . . . . . . . 12 ((topGen‘ran (,)) ↾t (-π[,]π)) = ((topGen‘ran (,)) ↾t (-π[,]π))
65861, 657restntr 21790 . . . . . . . . . . 11 (((topGen‘ran (,)) ∈ Top ∧ (-π[,]π) ⊆ ℝ ∧ ((-π[,]π) ∖ {0}) ⊆ (-π[,]π)) → ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘((-π[,]π) ∖ {0})) = (((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) ∩ (-π[,]π)))
659453, 427, 613, 658mp3an 1458 . . . . . . . . . 10 ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘((-π[,]π) ∖ {0})) = (((int‘(topGen‘ran (,)))‘(((-π[,]π) ∖ {0}) ∪ (ℝ ∖ (-π[,]π)))) ∩ (-π[,]π))
660656, 659eleqtrrdi 2927 . . . . . . . . 9 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝑠 ∈ ((int‘((topGen‘ran (,)) ↾t (-π[,]π)))‘((-π[,]π) ∖ {0})))
66114a1i 11 . . . . . . . . 9 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝐾:(-π[,]π)⟶ℂ)
662451toponunii 21524 . . . . . . . . . 10 (-π[,]π) = ((topGen‘ran (,)) ↾t (-π[,]π))
663662, 596cnprest 21897 . . . . . . . . 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 835 . . . . . . . 8 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → (𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠) ↔ (𝐾 ↾ ((-π[,]π) ∖ {0})) ∈ (((((topGen‘ran (,)) ↾t (-π[,]π)) ↾t ((-π[,]π) ∖ {0})) CnP (TopOpen‘ℂfld))‘𝑠)))
665625, 664mpbird 260 . . . . . . 7 ((𝑠 ∈ (-π[,]π) ∧ ¬ 𝑠 = 0) → 𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))
666536, 665pm2.61dan 812 . . . . . 6 (𝑠 ∈ (-π[,]π) → 𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))
667666rgen 3143 . . . . 5 𝑠 ∈ (-π[,]π)𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠)
668 cncnp 21888 . . . . . 6 ((((topGen‘ran (,)) ↾t (-π[,]π)) ∈ (TopOn‘(-π[,]π)) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → (𝐾 ∈ (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld)) ↔ (𝐾:(-π[,]π)⟶ℂ ∧ ∀𝑠 ∈ (-π[,]π)𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠))))
669451, 605, 668mp2an 691 . . . . 5 (𝐾 ∈ (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld)) ↔ (𝐾:(-π[,]π)⟶ℂ ∧ ∀𝑠 ∈ (-π[,]π)𝐾 ∈ ((((topGen‘ran (,)) ↾t (-π[,]π)) CnP (TopOpen‘ℂfld))‘𝑠)))
67014, 667, 669mpbir2an 710 . . . 4 𝐾 ∈ (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld))
67156, 532, 599cncfcn 23518 . . . . . 6 (((-π[,]π) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((-π[,]π)–cn→ℂ) = (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld)))
672517, 144, 671mp2an 691 . . . . 5 ((-π[,]π)–cn→ℂ) = (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld))
673672eqcomi 2833 . . . 4 (((topGen‘ran (,)) ↾t (-π[,]π)) Cn (TopOpen‘ℂfld)) = ((-π[,]π)–cn→ℂ)
674670, 673eleqtri 2914 . . 3 𝐾 ∈ ((-π[,]π)–cn→ℂ)
675 cncffvrn 23506 . . 3 ((ℝ ⊆ ℂ ∧ 𝐾 ∈ ((-π[,]π)–cn→ℂ)) → (𝐾 ∈ ((-π[,]π)–cn→ℝ) ↔ 𝐾:(-π[,]π)⟶ℝ))
67612, 674, 675mp2an 691 . 2 (𝐾 ∈ ((-π[,]π)–cn→ℝ) ↔ 𝐾:(-π[,]π)⟶ℝ)
67711, 676mpbir 234 1 𝐾 ∈ ((-π[,]π)–cn→ℝ)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ⊤wtru 1539   ∈ wcel 2115   ≠ wne 3014  ∀wral 3133  ∃wrex 3134  Vcvv 3480   ∖ cdif 3916   ∪ cun 3917   ∩ cin 3918   ⊆ wss 3919  ifcif 4450  {csn 4550  {cpr 4552   class class class wbr 5052   ↦ cmpt 5132  dom cdm 5542  ran crn 5543   ↾ cres 5544   “ cima 5545   Fn wfn 6338  ⟶wf 6339  ‘cfv 6343  (class class class)co 7149  ℂcc 10533  ℝcr 10534  0cc0 10535  1c1 10536   · cmul 10540  ℝ*cxr 10672   < clt 10673   ≤ cle 10674  -cneg 10869   / cdiv 11295  2c2 11689  ℝ+crp 12386  (,)cioo 12735  [,]cicc 12738  ℜcre 14456  sincsin 15417  cosccos 15418  πcpi 15420   ↾t crest 16694  TopOpenctopn 16695  topGenctg 16711  ℂfldccnfld 20545  Topctop 21501  TopOnctopon 21518  Clsdccld 21624  intcnt 21625   Cn ccn 21832   CnP ccnp 21833  –cn→ccncf 23484   limℂ climc 24468   D cdv 24469 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-inf2 9101  ax-cnex 10591  ax-resscn 10592  ax-1cn 10593  ax-icn 10594  ax-addcl 10595  ax-addrcl 10596  ax-mulcl 10597  ax-mulrcl 10598  ax-mulcom 10599  ax-addass 10600  ax-mulass 10601  ax-distr 10602  ax-i2m1 10603  ax-1ne0 10604  ax-1rid 10605  ax-rnegex 10606  ax-rrecex 10607  ax-cnre 10608  ax-pre-lttri 10609  ax-pre-lttrn 10610  ax-pre-ltadd 10611  ax-pre-mulgt0 10612  ax-pre-sup 10613  ax-addf 10614  ax-mulf 10615 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-of 7403  df-om 7575  df-1st 7684  df-2nd 7685  df-supp 7827  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-er 8285  df-map 8404  df-pm 8405  df-ixp 8458  df-en 8506  df-dom 8507  df-sdom 8508  df-fin 8509  df-fsupp 8831  df-fi 8872  df-sup 8903  df-inf 8904  df-oi 8971  df-card 9365  df-pnf 10675  df-mnf 10676  df-xr 10677  df-ltxr 10678  df-le 10679  df-sub 10870  df-neg 10871  df-div 11296  df-nn 11635  df-2 11697  df-3 11698  df-4 11699  df-5 11700  df-6 11701  df-7 11702  df-8 11703  df-9 11704  df-n0 11895  df-z 11979  df-dec 12096  df-uz 12241  df-q 12346  df-rp 12387  df-xneg 12504  df-xadd 12505  df-xmul 12506  df-ioo 12739  df-ioc 12740  df-ico 12741  df-icc 12742  df-fz 12895  df-fzo 13038  df-fl 13166  df-mod 13242  df-seq 13374  df-exp 13435  df-fac 13639  df-bc 13668  df-hash 13696  df-shft 14426  df-cj 14458  df-re 14459  df-im 14460  df-sqrt 14594  df-abs 14595  df-limsup 14828  df-clim 14845  df-rlim 14846  df-sum 15043  df-ef 15421  df-sin 15423  df-cos 15424  df-pi 15426  df-struct 16485  df-ndx 16486  df-slot 16487  df-base 16489  df-sets 16490  df-ress 16491  df-plusg 16578  df-mulr 16579  df-starv 16580  df-sca 16581  df-vsca 16582  df-ip 16583  df-tset 16584  df-ple 16585  df-ds 16587  df-unif 16588  df-hom 16589  df-cco 16590  df-rest 16696  df-topn 16697  df-0g 16715  df-gsum 16716  df-topgen 16717  df-pt 16718  df-prds 16721  df-xrs 16775  df-qtop 16780  df-imas 16781  df-xps 16783  df-mre 16857  df-mrc 16858  df-acs 16860  df-mgm 17852  df-sgrp 17901  df-mnd 17912  df-submnd 17957  df-mulg 18225  df-cntz 18447  df-cmn 18908  df-psmet 20537  df-xmet 20538  df-met 20539  df-bl 20540  df-mopn 20541  df-fbas 20542  df-fg 20543  df-cnfld 20546  df-top 21502  df-topon 21519  df-topsp 21541  df-bases 21554  df-cld 21627  df-ntr 21628  df-cls 21629  df-nei 21706  df-lp 21744  df-perf 21745  df-cn 21835  df-cnp 21836  df-t1 21922  df-haus 21923  df-cmp 21995  df-tx 22170  df-hmeo 22363  df-fil 22454  df-fm 22546  df-flim 22547  df-flf 22548  df-xms 22930  df-ms 22931  df-tms 22932  df-cncf 23486  df-limc 24472  df-dv 24473 This theorem is referenced by:  fourierdlem77  42751  fourierdlem78  42752  fourierdlem85  42759  fourierdlem88  42762
 Copyright terms: Public domain W3C validator