MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvsincos Structured version   Visualization version   GIF version

Theorem dvsincos 23985
Description: Derivative of the sine and cosine functions. (Contributed by Mario Carneiro, 21-May-2016.)
Assertion
Ref Expression
dvsincos ((ℂ D sin) = cos ∧ (ℂ D cos) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥)))

Proof of Theorem dvsincos
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 cnelprrecn 10252 . . . . . 6 ℂ ∈ {ℝ, ℂ}
21a1i 11 . . . . 5 (⊤ → ℂ ∈ {ℝ, ℂ})
3 ax-icn 10218 . . . . . . . . . 10 i ∈ ℂ
43a1i 11 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℂ) → i ∈ ℂ)
5 simpr 472 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
64, 5mulcld 10283 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
7 efcl 15041 . . . . . . . 8 ((i · 𝑥) ∈ ℂ → (exp‘(i · 𝑥)) ∈ ℂ)
86, 7syl 17 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℂ) → (exp‘(i · 𝑥)) ∈ ℂ)
9 ine0 10688 . . . . . . . 8 i ≠ 0
109a1i 11 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℂ) → i ≠ 0)
118, 4, 10divcld 11024 . . . . . 6 ((⊤ ∧ 𝑥 ∈ ℂ) → ((exp‘(i · 𝑥)) / i) ∈ ℂ)
12 negicn 10505 . . . . . . . . . 10 -i ∈ ℂ
13 mulcl 10243 . . . . . . . . . 10 ((-i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (-i · 𝑥) ∈ ℂ)
1412, 5, 13sylancr 576 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℂ) → (-i · 𝑥) ∈ ℂ)
15 efcl 15041 . . . . . . . . 9 ((-i · 𝑥) ∈ ℂ → (exp‘(-i · 𝑥)) ∈ ℂ)
1614, 15syl 17 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℂ) → (exp‘(-i · 𝑥)) ∈ ℂ)
1716, 4, 10divcld 11024 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℂ) → ((exp‘(-i · 𝑥)) / i) ∈ ℂ)
1817negcld 10602 . . . . . 6 ((⊤ ∧ 𝑥 ∈ ℂ) → -((exp‘(-i · 𝑥)) / i) ∈ ℂ)
1911, 18addcld 10282 . . . . 5 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) / i) + -((exp‘(-i · 𝑥)) / i)) ∈ ℂ)
208, 16addcld 10282 . . . . 5 ((⊤ ∧ 𝑥 ∈ ℂ) → ((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) ∈ ℂ)
218, 4mulcld 10283 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℂ) → ((exp‘(i · 𝑥)) · i) ∈ ℂ)
22 efcl 15041 . . . . . . . . . 10 (𝑦 ∈ ℂ → (exp‘𝑦) ∈ ℂ)
2322adantl 468 . . . . . . . . 9 ((⊤ ∧ 𝑦 ∈ ℂ) → (exp‘𝑦) ∈ ℂ)
24 1cnd 10279 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ)
252dvmptid 23961 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1))
263a1i 11 . . . . . . . . . . 11 (⊤ → i ∈ ℂ)
272, 5, 24, 25, 26dvmptcmul 23968 . . . . . . . . . 10 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (i · 𝑥))) = (𝑥 ∈ ℂ ↦ (i · 1)))
283mulid1i 10265 . . . . . . . . . . 11 (i · 1) = i
2928mpteq2i 4888 . . . . . . . . . 10 (𝑥 ∈ ℂ ↦ (i · 1)) = (𝑥 ∈ ℂ ↦ i)
3027, 29syl6eq 2824 . . . . . . . . 9 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (i · 𝑥))) = (𝑥 ∈ ℂ ↦ i))
31 eff 15040 . . . . . . . . . . . . 13 exp:ℂ⟶ℂ
3231a1i 11 . . . . . . . . . . . 12 (⊤ → exp:ℂ⟶ℂ)
3332feqmptd 6408 . . . . . . . . . . 11 (⊤ → exp = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
3433oveq2d 6828 . . . . . . . . . 10 (⊤ → (ℂ D exp) = (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦))))
35 dvef 23984 . . . . . . . . . . 11 (ℂ D exp) = exp
3635, 33syl5eq 2820 . . . . . . . . . 10 (⊤ → (ℂ D exp) = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
3734, 36eqtr3d 2810 . . . . . . . . 9 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
38 fveq2 6348 . . . . . . . . 9 (𝑦 = (i · 𝑥) → (exp‘𝑦) = (exp‘(i · 𝑥)))
392, 2, 6, 4, 23, 23, 30, 37, 38, 38dvmptco 23976 . . . . . . . 8 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (exp‘(i · 𝑥)))) = (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) · i)))
409a1i 11 . . . . . . . 8 (⊤ → i ≠ 0)
412, 8, 21, 39, 26, 40dvmptdivc 23969 . . . . . . 7 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) / i))) = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) · i) / i)))
428, 4, 10divcan4d 11030 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) · i) / i) = (exp‘(i · 𝑥)))
4342mpteq2dva 4891 . . . . . . 7 (⊤ → (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) · i) / i)) = (𝑥 ∈ ℂ ↦ (exp‘(i · 𝑥))))
4441, 43eqtrd 2808 . . . . . 6 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) / i))) = (𝑥 ∈ ℂ ↦ (exp‘(i · 𝑥))))
45 mulcl 10243 . . . . . . . . . 10 (((exp‘(-i · 𝑥)) ∈ ℂ ∧ -i ∈ ℂ) → ((exp‘(-i · 𝑥)) · -i) ∈ ℂ)
4616, 12, 45sylancl 575 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℂ) → ((exp‘(-i · 𝑥)) · -i) ∈ ℂ)
4746, 4, 10divcld 11024 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(-i · 𝑥)) · -i) / i) ∈ ℂ)
4812a1i 11 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℂ) → -i ∈ ℂ)
4912a1i 11 . . . . . . . . . . . 12 (⊤ → -i ∈ ℂ)
502, 5, 24, 25, 49dvmptcmul 23968 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (-i · 𝑥))) = (𝑥 ∈ ℂ ↦ (-i · 1)))
5112mulid1i 10265 . . . . . . . . . . . 12 (-i · 1) = -i
5251mpteq2i 4888 . . . . . . . . . . 11 (𝑥 ∈ ℂ ↦ (-i · 1)) = (𝑥 ∈ ℂ ↦ -i)
5350, 52syl6eq 2824 . . . . . . . . . 10 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (-i · 𝑥))) = (𝑥 ∈ ℂ ↦ -i))
54 fveq2 6348 . . . . . . . . . 10 (𝑦 = (-i · 𝑥) → (exp‘𝑦) = (exp‘(-i · 𝑥)))
552, 2, 14, 48, 23, 23, 53, 37, 54, 54dvmptco 23976 . . . . . . . . 9 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (exp‘(-i · 𝑥)))) = (𝑥 ∈ ℂ ↦ ((exp‘(-i · 𝑥)) · -i)))
562, 16, 46, 55, 26, 40dvmptdivc 23969 . . . . . . . 8 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ ((exp‘(-i · 𝑥)) / i))) = (𝑥 ∈ ℂ ↦ (((exp‘(-i · 𝑥)) · -i) / i)))
572, 17, 47, 56dvmptneg 23970 . . . . . . 7 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ -((exp‘(-i · 𝑥)) / i))) = (𝑥 ∈ ℂ ↦ -(((exp‘(-i · 𝑥)) · -i) / i)))
5846, 4, 10divneg2d 11038 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℂ) → -(((exp‘(-i · 𝑥)) · -i) / i) = (((exp‘(-i · 𝑥)) · -i) / -i))
593, 9negne0i 10579 . . . . . . . . . . 11 -i ≠ 0
6059a1i 11 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℂ) → -i ≠ 0)
6116, 48, 60divcan4d 11030 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(-i · 𝑥)) · -i) / -i) = (exp‘(-i · 𝑥)))
6258, 61eqtrd 2808 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℂ) → -(((exp‘(-i · 𝑥)) · -i) / i) = (exp‘(-i · 𝑥)))
6362mpteq2dva 4891 . . . . . . 7 (⊤ → (𝑥 ∈ ℂ ↦ -(((exp‘(-i · 𝑥)) · -i) / i)) = (𝑥 ∈ ℂ ↦ (exp‘(-i · 𝑥))))
6457, 63eqtrd 2808 . . . . . 6 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ -((exp‘(-i · 𝑥)) / i))) = (𝑥 ∈ ℂ ↦ (exp‘(-i · 𝑥))))
652, 11, 8, 44, 18, 16, 64dvmptadd 23964 . . . . 5 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) / i) + -((exp‘(-i · 𝑥)) / i)))) = (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥)))))
66 2cnd 11316 . . . . 5 (⊤ → 2 ∈ ℂ)
67 2ne0 11336 . . . . . 6 2 ≠ 0
6867a1i 11 . . . . 5 (⊤ → 2 ≠ 0)
692, 19, 20, 65, 66, 68dvmptdivc 23969 . . . 4 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ ((((exp‘(i · 𝑥)) / i) + -((exp‘(-i · 𝑥)) / i)) / 2))) = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) / 2)))
70 df-sin 15028 . . . . . 6 sin = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i)))
718, 16subcld 10615 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℂ) → ((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) ∈ ℂ)
72 2cnd 11316 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℂ) → 2 ∈ ℂ)
7367a1i 11 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℂ) → 2 ≠ 0)
7471, 4, 72, 10, 73divdiv1d 11055 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℂ) → ((((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / i) / 2) = (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (i · 2)))
75 2cn 11314 . . . . . . . . . . 11 2 ∈ ℂ
763, 75mulcomi 10269 . . . . . . . . . 10 (i · 2) = (2 · i)
7776oveq2i 6823 . . . . . . . . 9 (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (i · 2)) = (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i))
7874, 77syl6eq 2824 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℂ) → ((((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / i) / 2) = (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i)))
798, 16, 4, 10divsubdird 11063 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / i) = (((exp‘(i · 𝑥)) / i) − ((exp‘(-i · 𝑥)) / i)))
8011, 17negsubd 10621 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) / i) + -((exp‘(-i · 𝑥)) / i)) = (((exp‘(i · 𝑥)) / i) − ((exp‘(-i · 𝑥)) / i)))
8179, 80eqtr4d 2811 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / i) = (((exp‘(i · 𝑥)) / i) + -((exp‘(-i · 𝑥)) / i)))
8281oveq1d 6827 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℂ) → ((((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / i) / 2) = ((((exp‘(i · 𝑥)) / i) + -((exp‘(-i · 𝑥)) / i)) / 2))
8378, 82eqtr3d 2810 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i)) = ((((exp‘(i · 𝑥)) / i) + -((exp‘(-i · 𝑥)) / i)) / 2))
8483mpteq2dva 4891 . . . . . 6 (⊤ → (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i))) = (𝑥 ∈ ℂ ↦ ((((exp‘(i · 𝑥)) / i) + -((exp‘(-i · 𝑥)) / i)) / 2)))
8570, 84syl5eq 2820 . . . . 5 (⊤ → sin = (𝑥 ∈ ℂ ↦ ((((exp‘(i · 𝑥)) / i) + -((exp‘(-i · 𝑥)) / i)) / 2)))
8685oveq2d 6828 . . . 4 (⊤ → (ℂ D sin) = (ℂ D (𝑥 ∈ ℂ ↦ ((((exp‘(i · 𝑥)) / i) + -((exp‘(-i · 𝑥)) / i)) / 2))))
87 df-cos 15029 . . . . 5 cos = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) / 2))
8887a1i 11 . . . 4 (⊤ → cos = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) / 2)))
8969, 86, 883eqtr4d 2818 . . 3 (⊤ → (ℂ D sin) = cos)
9021, 46addcld 10282 . . . . 5 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) · i) + ((exp‘(-i · 𝑥)) · -i)) ∈ ℂ)
912, 8, 21, 39, 16, 46, 55dvmptadd 23964 . . . . 5 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))))) = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) · i) + ((exp‘(-i · 𝑥)) · -i))))
922, 20, 90, 91, 66, 68dvmptdivc 23969 . . . 4 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) / 2))) = (𝑥 ∈ ℂ ↦ ((((exp‘(i · 𝑥)) · i) + ((exp‘(-i · 𝑥)) · -i)) / 2)))
9388oveq2d 6828 . . . 4 (⊤ → (ℂ D cos) = (ℂ D (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘(-i · 𝑥))) / 2))))
9471, 4, 10divcld 11024 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / i) ∈ ℂ)
9594, 72, 73divnegd 11037 . . . . . 6 ((⊤ ∧ 𝑥 ∈ ℂ) → -((((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / i) / 2) = (-(((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / i) / 2))
96 sinval 15080 . . . . . . . . 9 (𝑥 ∈ ℂ → (sin‘𝑥) = (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i)))
9796adantl 468 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℂ) → (sin‘𝑥) = (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / (2 · i)))
9897, 78eqtr4d 2811 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℂ) → (sin‘𝑥) = ((((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / i) / 2))
9998negeqd 10498 . . . . . 6 ((⊤ ∧ 𝑥 ∈ ℂ) → -(sin‘𝑥) = -((((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / i) / 2))
1003negnegi 10574 . . . . . . . . . 10 --i = i
101100oveq2i 6823 . . . . . . . . 9 (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) · --i) = (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) · i)
102 mulneg2 10690 . . . . . . . . . 10 ((((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) ∈ ℂ ∧ -i ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) · --i) = -(((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) · -i))
10371, 12, 102sylancl 575 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) · --i) = -(((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) · -i))
104101, 103syl5eqr 2822 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) · i) = -(((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) · -i))
105 mulcl 10243 . . . . . . . . . . 11 (((exp‘(-i · 𝑥)) ∈ ℂ ∧ i ∈ ℂ) → ((exp‘(-i · 𝑥)) · i) ∈ ℂ)
10616, 3, 105sylancl 575 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℂ) → ((exp‘(-i · 𝑥)) · i) ∈ ℂ)
10721, 106negsubd 10621 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) · i) + -((exp‘(-i · 𝑥)) · i)) = (((exp‘(i · 𝑥)) · i) − ((exp‘(-i · 𝑥)) · i)))
108 mulneg2 10690 . . . . . . . . . . 11 (((exp‘(-i · 𝑥)) ∈ ℂ ∧ i ∈ ℂ) → ((exp‘(-i · 𝑥)) · -i) = -((exp‘(-i · 𝑥)) · i))
10916, 3, 108sylancl 575 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℂ) → ((exp‘(-i · 𝑥)) · -i) = -((exp‘(-i · 𝑥)) · i))
110109oveq2d 6828 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) · i) + ((exp‘(-i · 𝑥)) · -i)) = (((exp‘(i · 𝑥)) · i) + -((exp‘(-i · 𝑥)) · i)))
1118, 16, 4subdird 10710 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) · i) = (((exp‘(i · 𝑥)) · i) − ((exp‘(-i · 𝑥)) · i)))
112107, 110, 1113eqtr4d 2818 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) · i) + ((exp‘(-i · 𝑥)) · -i)) = (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) · i))
11371, 4, 10divrecd 11027 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / i) = (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) · (1 / i)))
114 irec 13193 . . . . . . . . . . 11 (1 / i) = -i
115114oveq2i 6823 . . . . . . . . . 10 (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) · (1 / i)) = (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) · -i)
116113, 115syl6eq 2824 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / i) = (((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) · -i))
117116negeqd 10498 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℂ) → -(((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / i) = -(((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) · -i))
118104, 112, 1173eqtr4d 2818 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) · i) + ((exp‘(-i · 𝑥)) · -i)) = -(((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / i))
119118oveq1d 6827 . . . . . 6 ((⊤ ∧ 𝑥 ∈ ℂ) → ((((exp‘(i · 𝑥)) · i) + ((exp‘(-i · 𝑥)) · -i)) / 2) = (-(((exp‘(i · 𝑥)) − (exp‘(-i · 𝑥))) / i) / 2))
12095, 99, 1193eqtr4d 2818 . . . . 5 ((⊤ ∧ 𝑥 ∈ ℂ) → -(sin‘𝑥) = ((((exp‘(i · 𝑥)) · i) + ((exp‘(-i · 𝑥)) · -i)) / 2))
121120mpteq2dva 4891 . . . 4 (⊤ → (𝑥 ∈ ℂ ↦ -(sin‘𝑥)) = (𝑥 ∈ ℂ ↦ ((((exp‘(i · 𝑥)) · i) + ((exp‘(-i · 𝑥)) · -i)) / 2)))
12292, 93, 1213eqtr4d 2818 . . 3 (⊤ → (ℂ D cos) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥)))
12389, 122jca 502 . 2 (⊤ → ((ℂ D sin) = cos ∧ (ℂ D cos) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥))))
124123trud 1644 1 ((ℂ D sin) = cos ∧ (ℂ D cos) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1634  wtru 1635  wcel 2148  wne 2946  {cpr 4328  cmpt 4876  wf 6038  cfv 6042  (class class class)co 6812  cc 10157  cr 10158  0cc0 10159  1c1 10160  ici 10161   + caddc 10162   · cmul 10164  cmin 10489  -cneg 10490   / cdiv 10907  2c2 11293  expce 15020  sincsin 15022  cosccos 15023   D cdv 23868
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-rep 4917  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117  ax-inf2 8723  ax-cnex 10215  ax-resscn 10216  ax-1cn 10217  ax-icn 10218  ax-addcl 10219  ax-addrcl 10220  ax-mulcl 10221  ax-mulrcl 10222  ax-mulcom 10223  ax-addass 10224  ax-mulass 10225  ax-distr 10226  ax-i2m1 10227  ax-1ne0 10228  ax-1rid 10229  ax-rnegex 10230  ax-rrecex 10231  ax-cnre 10232  ax-pre-lttri 10233  ax-pre-lttrn 10234  ax-pre-ltadd 10235  ax-pre-mulgt0 10236  ax-pre-sup 10237  ax-addf 10238  ax-mulf 10239
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-fal 1640  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-pss 3745  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-tp 4331  df-op 4333  df-uni 4586  df-int 4623  df-iun 4667  df-iin 4668  df-br 4798  df-opab 4860  df-mpt 4877  df-tr 4900  df-id 5171  df-eprel 5176  df-po 5184  df-so 5185  df-fr 5222  df-se 5223  df-we 5224  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-pred 5834  df-ord 5880  df-on 5881  df-lim 5882  df-suc 5883  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-isom 6051  df-riota 6773  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-of 7065  df-om 7234  df-1st 7336  df-2nd 7337  df-supp 7468  df-wrecs 7580  df-recs 7642  df-rdg 7680  df-1o 7734  df-2o 7735  df-oadd 7738  df-er 7917  df-map 8032  df-pm 8033  df-ixp 8084  df-en 8131  df-dom 8132  df-sdom 8133  df-fin 8134  df-fsupp 8453  df-fi 8494  df-sup 8525  df-inf 8526  df-oi 8592  df-card 8986  df-cda 9213  df-pnf 10299  df-mnf 10300  df-xr 10301  df-ltxr 10302  df-le 10303  df-sub 10491  df-neg 10492  df-div 10908  df-nn 11244  df-2 11302  df-3 11303  df-4 11304  df-5 11305  df-6 11306  df-7 11307  df-8 11308  df-9 11309  df-n0 11517  df-z 11602  df-dec 11718  df-uz 11911  df-q 12014  df-rp 12053  df-xneg 12168  df-xadd 12169  df-xmul 12170  df-ico 12405  df-icc 12406  df-fz 12556  df-fzo 12696  df-fl 12823  df-seq 13031  df-exp 13090  df-fac 13287  df-bc 13316  df-hash 13344  df-shft 14037  df-cj 14069  df-re 14070  df-im 14071  df-sqrt 14205  df-abs 14206  df-limsup 14432  df-clim 14449  df-rlim 14450  df-sum 14647  df-ef 15026  df-sin 15028  df-cos 15029  df-struct 16086  df-ndx 16087  df-slot 16088  df-base 16090  df-sets 16091  df-ress 16092  df-plusg 16182  df-mulr 16183  df-starv 16184  df-sca 16185  df-vsca 16186  df-ip 16187  df-tset 16188  df-ple 16189  df-ds 16192  df-unif 16193  df-hom 16194  df-cco 16195  df-rest 16311  df-topn 16312  df-0g 16330  df-gsum 16331  df-topgen 16332  df-pt 16333  df-prds 16336  df-xrs 16390  df-qtop 16395  df-imas 16396  df-xps 16398  df-mre 16474  df-mrc 16475  df-acs 16477  df-mgm 17470  df-sgrp 17512  df-mnd 17523  df-submnd 17564  df-mulg 17769  df-cntz 17977  df-cmn 18422  df-psmet 19973  df-xmet 19974  df-met 19975  df-bl 19976  df-mopn 19977  df-fbas 19978  df-fg 19979  df-cnfld 19982  df-top 20939  df-topon 20956  df-topsp 20978  df-bases 20991  df-cld 21064  df-ntr 21065  df-cls 21066  df-nei 21143  df-lp 21181  df-perf 21182  df-cn 21272  df-cnp 21273  df-haus 21360  df-tx 21606  df-hmeo 21799  df-fil 21890  df-fm 21982  df-flim 21983  df-flf 21984  df-xms 22365  df-ms 22366  df-tms 22367  df-cncf 22921  df-limc 23871  df-dv 23872
This theorem is referenced by:  dvsin  23986  dvcos  23987
  Copyright terms: Public domain W3C validator