sincos4thpi - Metamath Proof Explorer

Home

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem sincos4thpi 8627

Description: The sine and cosine of

. (Contributed by Paul Chapman, 25-Jan-2008.)

**Assertion**
Ref	Expression
sincos4thpi	$/\$

**Proof of Theorem sincos4thpi**
Step	Hyp	Ref	Expression
1		2re 5926	. . . . . . . . . . . 12
2		2ne0 5937	. . . . . . . . . . . 12
3	1, 2	rereccl 5757	. . . . . . . . . . 11
4	3	recn 5286	. . . . . . . . . 10
5		ax1cn 5241	. . . . . . . . . . 11
6		2halvest 5986	. . . . . . . . . . 11
7	5, 6	ax-mp 7	. . . . . . . . . 10
8		sincosq1eq 8626	. . . . . . . . . 10 $/\$ $/\$
9	4, 4, 7, 8	mp3an 913	. . . . . . . . 9
10	9	opreq2i 3957	. . . . . . . 8
11	10	opreq2i 3957	. . . . . . 7
12		2cn 5927	. . . . . . . . . . . 12
13		pire 8596	. . . . . . . . . . . . 13
14	13	recn 5286	. . . . . . . . . . . 12
15	5, 12, 14, 12, 2, 2	divmuldiv 5742	. . . . . . . . . . 11
16	14	mulid2 5305	. . . . . . . . . . . 12
17		2t2e4 5969	. . . . . . . . . . . 12
18	16, 17	opreq12i 3958	. . . . . . . . . . 11
19	15, 18	eqtr 1487	. . . . . . . . . 10
20	19	fveq2i 3712	. . . . . . . . 9
21	20, 20	opreq12i 3958	. . . . . . . 8
22	21	opreq2i 3957	. . . . . . 7
23	12, 2	recid 5696	. . . . . . . . . . 11
24	23	opreq1i 3956	. . . . . . . . . 10
25	13, 1, 2	redivcl 5754	. . . . . . . . . . . 12
26	25	recn 5286	. . . . . . . . . . 11
27	12, 4, 26	mulass 5297	. . . . . . . . . 10
28	26	mulid2 5305	. . . . . . . . . 10
29	24, 27, 28	3eqtr3 1495	. . . . . . . . 9
30	29	fveq2i 3712	. . . . . . . 8
31	4, 26	mulcl 5293	. . . . . . . . 9
32		sin2tt 7404	. . . . . . . . 9
33	31, 32	ax-mp 7	. . . . . . . 8
34		sinhalfpi 8599	. . . . . . . 8
35	30, 33, 34	3eqtr3 1495	. . . . . . 7
36	11, 22, 35	3eqtr3 1495	. . . . . 6
37	36	fveq2i 3712	. . . . 5
38		4re 5929	. . . . . . . . 9
39		4pos 5939	. . . . . . . . . 10
40	38, 39	gt0ne0i 5591	. . . . . . . . 9
41	13, 38, 40	redivcl 5754	. . . . . . . 8
42		resinclt 7380	. . . . . . . 8
43	41, 42	ax-mp 7	. . . . . . 7
44	43, 43	remulcl 5307	. . . . . 6
45		0re 5412	. . . . . . 7
46		2pos 5936	. . . . . . 7
47	45, 1, 46	ltlei 5554	. . . . . 6
48	43	msqge0 5588	. . . . . 6
49	1, 44, 47, 48	sqrmuli 6634	. . . . 5
50		sqr1 6646	. . . . 5
51	37, 49, 50	3eqtr3r 1496	. . . 4
52		sqr2re 6660	. . . . . 6
53	52	recn 5286	. . . . 5
54		sqrclt 6640	. . . . . . 7 $/\$
55	44, 48, 54	mp2an 695	. . . . . 6
56	55	recn 5286	. . . . 5
57		sqr00t 6644	. . . . . . . . 9 $/\$
58	1, 47, 57	mp2an 695	. . . . . . . 8
59	58	necon3bii 1590	. . . . . . 7
60	2, 59	mpbir 190	. . . . . 6
61		divmul2t 5677	. . . . . 6 $/\$ $/\$ $/\$
62	60, 61	mpan2 694	. . . . 5 $/\$ $/\$
63	5, 53, 56, 62	mp3an 913	. . . 4
64	51, 63	mpbir 190	. . 3
65		pipos 8597	. . . . . . . 8
66	13, 38, 65, 39	divgt0i 5814	. . . . . . 7
67		1re 5407	. . . . . . . 8
68		pigt2lt4 8594	. . . . . . . . . . 11 $/\$
69	68	pm3.27i 324	. . . . . . . . . 10
70	13, 38, 38, 39	ltdiv1i 5779	. . . . . . . . . 10
71	69, 70	mpbi 189	. . . . . . . . 9
72	38	recn 5286	. . . . . . . . . 10
73	72, 40	divid 5726	. . . . . . . . 9
74	71, 73	breqtr 2628	. . . . . . . 8
75	41, 67, 74	ltlei 5554	. . . . . . 7
76		elioc2t 6322	. . . . . . . . 9