Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem efivalt 7389

Description: The exponential function in terms of sine and cosine.

Assertion

Ref	Expression
efivalt

---

Proof of Theorem efivalt

Step	Hyp	Ref	Expression
1		2cn 5927	. . . 4
2		2ne0 5937	. . . . 5
3		divdirt 5713	. . . . 5
4	2, 3	mpan2 694	. . . 4
5	1, 4	mp3an3 902	. . 3
6		axaddcl 5243	. . . 4
7		axicn 5242	. . . . . 6
8		axmulcl 5245	. . . . . 6
9	7, 8	mpan 693	. . . . 5
10		efclt 7254	. . . . 5
11	9, 10	syl 10	. . . 4
12	7	negcl 5341	. . . . . 6
13		axmulcl 5245	. . . . . 6
14	12, 13	mpan 693	. . . . 5
15		efclt 7254	. . . . 5
16	14, 15	syl 10	. . . 4
17	6, 11, 16	sylanc 471	. . 3
18		subclt 5339	. . . 4
19	18, 11, 16	sylanc 471	. . 3
20	5, 17, 19	sylanc 471	. 2
21		pncan3t 5349	. . . . . . 7
22	21, 16, 11	sylanc 471	. . . . . 6
23	22	opreq2d 3961	. . . . 5
24		axaddass 5249	. . . . . 6
25	24, 11, 16, 19	syl3anc 856	. . . . 5
26		2timest 5951	. . . . . 6
27	11, 26	syl 10	. . . . 5
28	23, 25, 27	3eqtr4d 1509	. . . 4
29	28	opreq1d 3960	. . 3
30		divcan3t 5718	. . . . 5
31	1, 2, 30	mp3an13 904	. . . 4
32	11, 31	syl 10	. . 3
33	29, 32	eqtr2d 1500	. 2
34		cosvalt 7372	. . 3
35	1, 7	mulcl 5293	. . . . . 6
36		ine0 5406	. . . . . . . 8
37	1, 7, 2, 36	muln0 5668	. . . . . . 7
38		div12t 5707	. . . . . . 7
39	37, 38	mpan2 694	. . . . . 6