dvsincos - Metamath Proof Explorer

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

Theorem dvsincos 26334

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.

Step	Hyp	Ref	Expression
1		cnelprrecn 11323	. . . . . 6 ⊢ ℂ ∈ {ℝ, ℂ}
2	1	a1i 11	. . . . 5 ⊢ (⊤ → ℂ ∈ {ℝ, ℂ})
3		ax-icn 11289	. . . . . . . . . 10 ⊢ i ∈ ℂ
4	3	a1i 11	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → i ∈ ℂ)
5		simpr 490	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
6	4, 5	mulcld 11359	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
7		efcl 16280	. . . . . . . 8 ⊢ ((i · 𝑥) ∈ ℂ → (exp‘(i · 𝑥)) ∈ ℂ)
8	6, 7	syl 18	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (exp‘(i · 𝑥)) ∈ ℂ)
9		ine0 11781	. . . . . . . 8 ⊢ i ≠ 0
10	9	a1i 11	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → i ≠ 0)
11	8, 4, 10	divcld 12123	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → ((exp‘(i · 𝑥)) / i) ∈ ℂ)
12		negicn 11588	. . . . . . . . . 10 ⊢ -i ∈ ℂ
13		mulcl 11314	. . . . . . . . . 10 ⊢ (( -i ∈ ℂ ∧ 𝑥 ∈ ℂ) → ( -i · 𝑥) ∈ ℂ)
14	12, 5, 13	sylancr 599	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → ( -i · 𝑥) ∈ ℂ)
15		efcl 16280	. . . . . . . . 9 ⊢ (( -i · 𝑥) ∈ ℂ → (exp‘( -i · 𝑥)) ∈ ℂ)
16	14, 15	syl 18	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (exp‘( -i · 𝑥)) ∈ ℂ)
17	16, 4, 10	divcld 12123	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → ((exp‘( -i · 𝑥)) / i) ∈ ℂ)
18	17	negcld 11686	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → -((exp‘( -i · 𝑥)) / i) ∈ ℂ)
19	11, 18	addcld 11358	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) / i) + -((exp‘( -i · 𝑥)) / i)) ∈ ℂ)
20	8, 16	addcld 11358	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → ((exp‘(i · 𝑥)) + (exp‘( -i · 𝑥))) ∈ ℂ)
21	8, 4	mulcld 11359	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → ((exp‘(i · 𝑥)) · i) ∈ ℂ)
22		efcl 16280	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℂ → (exp‘𝑦) ∈ ℂ)
23	22	adantl 487	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑦 ∈ ℂ) → (exp‘𝑦) ∈ ℂ)
24		1cnd 11332	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ)
25	2	dvmptid 26310	. . . . . . . . . . 11 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1))
26	3	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → i ∈ ℂ)
27	2, 5, 24, 25, 26	dvmptcmul 26317	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (i · 𝑥))) = (𝑥 ∈ ℂ ↦ (i · 1)))
28	3	mulridi 11343	. . . . . . . . . . 11 ⊢ (i · 1) = i
29	28	mpteq2i 5205	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℂ ↦ (i · 1)) = (𝑥 ∈ ℂ ↦ i)
30	27, 29	eqtrdi 2814	. . . . . . . . 9 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (i · 𝑥))) = (𝑥 ∈ ℂ ↦ i))
31		eff 16279	. . . . . . . . . . . . 13 ⊢ exp:ℂ⟶ℂ
32	31	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → exp:ℂ⟶ℂ)
33	32	feqmptd 6979	. . . . . . . . . . 11 ⊢ (⊤ → exp = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
34	33	oveq2d 7462	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D exp) = (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦))))
35		dvef 26333	. . . . . . . . . . 11 ⊢ (ℂ D exp) = exp
36	35, 33	eqtrid 2810	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D exp) = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
37	34, 36	eqtr3d 2800	. . . . . . . . 9 ⊢ (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
38		fveq2 6911	. . . . . . . . 9 ⊢ (𝑦 = (i · 𝑥) → (exp‘𝑦) = (exp‘(i · 𝑥)))
39	2, 2, 6, 4, 23, 23, 30, 37, 38, 38	dvmptco 26325	. . . . . . . 8 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (exp‘(i · 𝑥)))) = (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) · i)))
40	9	a1i 11	. . . . . . . 8 ⊢ (⊤ → i ≠ 0)
41	2, 8, 21, 39, 26, 40	dvmptdivc 26318	. . . . . . 7 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) / i))) = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) · i) / i)))
42	8, 4, 10	divcan4d 12129	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) · i) / i) = (exp‘(i · 𝑥)))
43	42	mpteq2dva 5202	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) · i) / i)) = (𝑥 ∈ ℂ ↦ (exp‘(i · 𝑥))))
44	41, 43	eqtrd 2798	. . . . . 6 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) / i))) = (𝑥 ∈ ℂ ↦ (exp‘(i · 𝑥))))
45		mulcl 11314	. . . . . . . . . 10 ⊢ (((exp‘( -i · 𝑥)) ∈ ℂ ∧ -i ∈ ℂ) → ((exp‘( -i · 𝑥)) · -i) ∈ ℂ)
46	16, 12, 45	sylancl 598	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → ((exp‘( -i · 𝑥)) · -i) ∈ ℂ)
47	46, 4, 10	divcld 12123	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘( -i · 𝑥)) · -i) / i) ∈ ℂ)
48	12	a1i 11	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → -i ∈ ℂ)
49	12	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → -i ∈ ℂ)
50	2, 5, 24, 25, 49	dvmptcmul 26317	. . . . . . . . . . 11 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ ( -i · 𝑥))) = (𝑥 ∈ ℂ ↦ ( -i · 1)))
51	12	mulridi 11343	. . . . . . . . . . . 12 ⊢ ( -i · 1) = -i
52	51	mpteq2i 5205	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℂ ↦ ( -i · 1)) = (𝑥 ∈ ℂ ↦ -i)
53	50, 52	eqtrdi 2814	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ ( -i · 𝑥))) = (𝑥 ∈ ℂ ↦ -i))
54		fveq2 6911	. . . . . . . . . 10 ⊢ (𝑦 = ( -i · 𝑥) → (exp‘𝑦) = (exp‘( -i · 𝑥)))
55	2, 2, 14, 48, 23, 23, 53, 37, 54, 54	dvmptco 26325	. . . . . . . . 9 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (exp‘( -i · 𝑥)))) = (𝑥 ∈ ℂ ↦ ((exp‘( -i · 𝑥)) · -i)))
56	2, 16, 46, 55, 26, 40	dvmptdivc 26318	. . . . . . . 8 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ ((exp‘( -i · 𝑥)) / i))) = (𝑥 ∈ ℂ ↦ (((exp‘( -i · 𝑥)) · -i) / i)))
57	2, 17, 47, 56	dvmptneg 26319	. . . . . . 7 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ -((exp‘( -i · 𝑥)) / i))) = (𝑥 ∈ ℂ ↦ -(((exp‘( -i · 𝑥)) · -i) / i)))
58	46, 4, 10	divneg2d 12137	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → -(((exp‘( -i · 𝑥)) · -i) / i) = (((exp‘( -i · 𝑥)) · -i) / -i))
59	3, 9	negne0i 11663	. . . . . . . . . . 11 ⊢ -i ≠ 0
60	59	a1i 11	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → -i ≠ 0)
61	16, 48, 60	divcan4d 12129	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘( -i · 𝑥)) · -i) / -i) = (exp‘( -i · 𝑥)))
62	58, 61	eqtrd 2798	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → -(((exp‘( -i · 𝑥)) · -i) / i) = (exp‘( -i · 𝑥)))
63	62	mpteq2dva 5202	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ ℂ ↦ -(((exp‘( -i · 𝑥)) · -i) / i)) = (𝑥 ∈ ℂ ↦ (exp‘( -i · 𝑥))))
64	57, 63	eqtrd 2798	. . . . . 6 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ -((exp‘( -i · 𝑥)) / i))) = (𝑥 ∈ ℂ ↦ (exp‘( -i · 𝑥))))
65	2, 11, 8, 44, 18, 16, 64	dvmptadd 26313	. . . . 5 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) / i) + -((exp‘( -i · 𝑥)) / i)))) = (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) + (exp‘( -i · 𝑥)))))
66		2cnd 12451	. . . . 5 ⊢ (⊤ → 2 ∈ ℂ)
67		2ne0 12479	. . . . . 6 ⊢ 2 ≠ 0
68	67	a1i 11	. . . . 5 ⊢ (⊤ → 2 ≠ 0)
69	2, 19, 20, 65, 66, 68	dvmptdivc 26318	. . . 4 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ ((((exp‘(i · 𝑥)) / i) + -((exp‘( -i · 𝑥)) / i)) / 2))) = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘( -i · 𝑥))) / 2)))
70		df-sin 16267	. . . . . 6 ⊢ sin = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / (2 · i)))
71	8, 16	subcld 11699	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → ((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) ∈ ℂ)
72		2cnd 12451	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 2 ∈ ℂ)
73	67	a1i 11	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 2 ≠ 0)
74	71, 4, 72, 10, 73	divdiv1d 12154	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → ((((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / i) / 2) = (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / (i · 2)))
75		2cn 12448	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
76	3, 75	mulcomi 11347	. . . . . . . . . 10 ⊢ (i · 2) = (2 · i)
77	76	oveq2i 7457	. . . . . . . . 9 ⊢ (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / (i · 2)) = (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / (2 · i))
78	74, 77	eqtrdi 2814	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → ((((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / i) / 2) = (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / (2 · i)))
79	8, 16, 4, 10	divsubdird 12162	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / i) = (((exp‘(i · 𝑥)) / i) − ((exp‘( -i · 𝑥)) / i)))
80	11, 17	negsubd 11705	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) / i) + -((exp‘( -i · 𝑥)) / i)) = (((exp‘(i · 𝑥)) / i) − ((exp‘( -i · 𝑥)) / i)))
81	79, 80	eqtr4d 2801	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / i) = (((exp‘(i · 𝑥)) / i) + -((exp‘( -i · 𝑥)) / i)))
82	81	oveq1d 7461	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → ((((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / i) / 2) = ((((exp‘(i · 𝑥)) / i) + -((exp‘( -i · 𝑥)) / i)) / 2))
83	78, 82	eqtr3d 2800	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / (2 · i)) = ((((exp‘(i · 𝑥)) / i) + -((exp‘( -i · 𝑥)) / i)) / 2))
84	83	mpteq2dva 5202	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / (2 · i))) = (𝑥 ∈ ℂ ↦ ((((exp‘(i · 𝑥)) / i) + -((exp‘( -i · 𝑥)) / i)) / 2)))
85	70, 84	eqtrid 2810	. . . . 5 ⊢ (⊤ → sin = (𝑥 ∈ ℂ ↦ ((((exp‘(i · 𝑥)) / i) + -((exp‘( -i · 𝑥)) / i)) / 2)))
86	85	oveq2d 7462	. . . 4 ⊢ (⊤ → (ℂ D sin) = (ℂ D (𝑥 ∈ ℂ ↦ ((((exp‘(i · 𝑥)) / i) + -((exp‘( -i · 𝑥)) / i)) / 2))))
87		df-cos 16268	. . . . 5 ⊢ cos = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘( -i · 𝑥))) / 2))
88	87	a1i 11	. . . 4 ⊢ (⊤ → cos = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘( -i · 𝑥))) / 2)))
89	69, 86, 88	3eqtr4d 2808	. . 3 ⊢ (⊤ → (ℂ D sin) = cos)
90	21, 46	addcld 11358	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) · i) + ((exp‘( -i · 𝑥)) · -i)) ∈ ℂ)
91	2, 8, 21, 39, 16, 46, 55	dvmptadd 26313	. . . . 5 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) + (exp‘( -i · 𝑥))))) = (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) · i) + ((exp‘( -i · 𝑥)) · -i))))
92	2, 20, 90, 91, 66, 68	dvmptdivc 26318	. . . 4 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘( -i · 𝑥))) / 2))) = (𝑥 ∈ ℂ ↦ ((((exp‘(i · 𝑥)) · i) + ((exp‘( -i · 𝑥)) · -i)) / 2)))
93	88	oveq2d 7462	. . . 4 ⊢ (⊤ → (ℂ D cos) = (ℂ D (𝑥 ∈ ℂ ↦ (((exp‘(i · 𝑥)) + (exp‘( -i · 𝑥))) / 2))))
94	71, 4, 10	divcld 12123	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / i) ∈ ℂ)
95	94, 72, 73	divnegd 12136	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → -((((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / i) / 2) = ( -(((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / i) / 2))
96		sinval 16322	. . . . . . . . 9 ⊢ (𝑥 ∈ ℂ → (sin‘𝑥) = (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / (2 · i)))
97	96	adantl 487	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (sin‘𝑥) = (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / (2 · i)))
98	97, 78	eqtr4d 2801	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (sin‘𝑥) = ((((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / i) / 2))
99	98	negeqd 11581	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → -(sin‘𝑥) = -((((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / i) / 2))
100	3	negnegi 11658	. . . . . . . . . 10 ⊢ - -i = i
101	100	oveq2i 7457	. . . . . . . . 9 ⊢ (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) · - -i) = (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) · i)
102		mulneg2 11783	. . . . . . . . . 10 ⊢ ((((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) ∈ ℂ ∧ -i ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) · - -i) = -(((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) · -i))
103	71, 12, 102	sylancl 598	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) · - -i) = -(((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) · -i))
104	101, 103	eqtr3id 2812	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) · i) = -(((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) · -i))
105		mulcl 11314	. . . . . . . . . . 11 ⊢ (((exp‘( -i · 𝑥)) ∈ ℂ ∧ i ∈ ℂ) → ((exp‘( -i · 𝑥)) · i) ∈ ℂ)
106	16, 3, 105	sylancl 598	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → ((exp‘( -i · 𝑥)) · i) ∈ ℂ)
107	21, 106	negsubd 11705	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) · i) + -((exp‘( -i · 𝑥)) · i)) = (((exp‘(i · 𝑥)) · i) − ((exp‘( -i · 𝑥)) · i)))
108		mulneg2 11783	. . . . . . . . . . 11 ⊢ (((exp‘( -i · 𝑥)) ∈ ℂ ∧ i ∈ ℂ) → ((exp‘( -i · 𝑥)) · -i) = -((exp‘( -i · 𝑥)) · i))
109	16, 3, 108	sylancl 598	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → ((exp‘( -i · 𝑥)) · -i) = -((exp‘( -i · 𝑥)) · i))
110	109	oveq2d 7462	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) · i) + ((exp‘( -i · 𝑥)) · -i)) = (((exp‘(i · 𝑥)) · i) + -((exp‘( -i · 𝑥)) · i)))
111	8, 16, 4	subdird 11803	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) · i) = (((exp‘(i · 𝑥)) · i) − ((exp‘( -i · 𝑥)) · i)))
112	107, 110, 111	3eqtr4d 2808	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) · i) + ((exp‘( -i · 𝑥)) · -i)) = (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) · i))
113	71, 4, 10	divrecd 12126	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / i) = (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) · (1 / i)))
114		irec 14375	. . . . . . . . . . 11 ⊢ (1 / i) = -i
115	114	oveq2i 7457	. . . . . . . . . 10 ⊢ (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) · (1 / i)) = (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) · -i)
116	113, 115	eqtrdi 2814	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / i) = (((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) · -i))
117	116	negeqd 11581	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → -(((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / i) = -(((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) · -i))
118	104, 112, 117	3eqtr4d 2808	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (((exp‘(i · 𝑥)) · i) + ((exp‘( -i · 𝑥)) · -i)) = -(((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / i))
119	118	oveq1d 7461	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → ((((exp‘(i · 𝑥)) · i) + ((exp‘( -i · 𝑥)) · -i)) / 2) = ( -(((exp‘(i · 𝑥)) − (exp‘( -i · 𝑥))) / i) / 2))
120	95, 99, 119	3eqtr4d 2808	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → -(sin‘𝑥) = ((((exp‘(i · 𝑥)) · i) + ((exp‘( -i · 𝑥)) · -i)) / 2))
121	120	mpteq2dva 5202	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℂ ↦ -(sin‘𝑥)) = (𝑥 ∈ ℂ ↦ ((((exp‘(i · 𝑥)) · i) + ((exp‘( -i · 𝑥)) · -i)) / 2)))
122	92, 93, 121	3eqtr4d 2808	. . 3 ⊢ (⊤ → (ℂ D cos) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥)))
123	89, 122	jca 521	. 2 ⊢ (⊤ → ((ℂ D sin) = cos ∧ (ℂ D cos) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥))))
124	123	mptru 1577	1 ⊢ ((ℂ D sin) = cos ∧ (ℂ D cos) = (𝑥 ∈ ℂ ↦ -(sin‘𝑥)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∧ wa 401 = wceq 1570 ⊤wtru 1571 ∈ wcel 2147 ≠ wne 2959 {cpr 4590 ↦ cmpt 5190 ⟶wf 6557 ‘cfv 6561 (class class class)co 7446 ℂcc 11228 ℝcr 11229 0cc0 11230 1c1 11231 ici 11232 + caddc 11233 · cmul 11235 − cmin 11571 -cneg 11572 / cdiv 12003 2c2 12427 expce 16259 sincsin 16261 cosccos 16262 D cdv 26216

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-inf2 9672 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307 ax-pre-sup 11308 ax-addf 11309

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-of 7720 df-om 7905 df-1st 8028 df-2nd 8029 df-supp 8208 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-1o 8507 df-2o 8508 df-er 8748 df-map 8880 df-pm 8881 df-ixp 8957 df-en 9005 df-dom 9006 df-sdom 9007 df-fin 9008 df-fsupp 9385 df-fi 9433 df-sup 9464 df-inf 9465 df-oi 9534 df-card 10050 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-div 12004 df-nn 12366 df-2 12435 df-3 12436 df-4 12437 df-5 12438 df-6 12439 df-7 12440 df-8 12441 df-9 12442 df-n0 12637 df-z 12724 df-dec 12845 df-uz 12996 df-q 13106 df-rp 13151 df-xneg 13271 df-xadd 13272 df-xmul 13273 df-ico 13512 df-icc 13513 df-fz 13670 df-fzo 13819 df-fl 13962 df-seq 14175 df-exp 14235 df-fac 14448 df-bc 14477 df-hash 14505 df-shft 15252 df-cj 15298 df-re 15299 df-im 15300 df-sqrt 15434 df-abs 15435 df-limsup 15670 df-clim 15687 df-rlim 15688 df-sum 15886 df-ef 16265 df-sin 16267 df-cos 16268 df-struct 17357 df-sets 17374 df-slot 17392 df-ndx 17404 df-base 17420 df-ress 17441 df-plusg 17473 df-mulr 17474 df-starv 17475 df-sca 17476 df-vsca 17477 df-ip 17478 df-tset 17479 df-ple 17480 df-ds 17482 df-unif 17483 df-hom 17484 df-cco 17485 df-rest 17625 df-topn 17626 df-0g 17644 df-gsum 17645 df-topgen 17646 df-pt 17647 df-prds 17650 df-xrs 17706 df-qtop 17711 df-imas 17712 df-xps 17714 df-mre 17788 df-mrc 17789 df-acs 17791 df-mgm 18848 df-sgrp 18940 df-mnd 18956 df-submnd 19011 df-mulg 19310 df-cntz 19564 df-cmn 20029 df-psmet 21703 df-xmet 21704 df-met 21705 df-bl 21706 df-mopn 21707 df-fbas 21708 df-fg 21709 df-cnfld 21712 df-top 23245 df-topon 23262 df-topsp 23284 df-bases 23297 df-cld 23370 df-ntr 23371 df-cls 23372 df-nei 23449 df-lp 23487 df-perf 23488 df-cn 23578 df-cnp 23579 df-haus 23666 df-tx 23914 df-hmeo 24107 df-fil 24198 df-fm 24290 df-flim 24291 df-flf 24292 df-xms 24672 df-ms 24673 df-tms 24674 df-cncf 25232 df-limc 26219 df-dv 26220

This theorem is used by: dvsin 26335 dvcos 26336

W3C validator