sincos4thpi - Metamath Proof Explorer

Home

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem sincos4thpi 8705

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 5981	. . . . . . . . . . . 12
2		2ne0 5992	. . . . . . . . . . . 12
3	1, 2	rereccl 5803	. . . . . . . . . . 11
4	3	recn 5326	. . . . . . . . . 10
5		ax1cn 5281	. . . . . . . . . . 11
6		2halvest 6041	. . . . . . . . . . 11
7	5, 6	ax-mp 7	. . . . . . . . . 10
8		sincosq1eq 8704	. . . . . . . . . 10 $/\$ $/\$
9	4, 4, 7, 8	mp3an 918	. . . . . . . . 9
10	9	opreq2i 3978	. . . . . . . 8
11	10	opreq2i 3978	. . . . . . 7
12		2cn 5982	. . . . . . . . . . . 12
13		pire 8672	. . . . . . . . . . . . 13
14	13	recn 5326	. . . . . . . . . . . 12
15	5, 12, 14, 12, 2, 2	divmuldiv 5788	. . . . . . . . . . 11
16	14	mulid2 5345	. . . . . . . . . . . 12
17		2t2e4 6024	. . . . . . . . . . . 12
18	16, 17	opreq12i 3979	. . . . . . . . . . 11
19	15, 18	eqtr 1498	. . . . . . . . . 10
20	19	fveq2i 3733	. . . . . . . . 9
21	20, 20	opreq12i 3979	. . . . . . . 8
22	21	opreq2i 3978	. . . . . . 7
23	12, 2	recid 5740	. . . . . . . . . . 11
24	23	opreq1i 3977	. . . . . . . . . 10
25	13, 1, 2	redivcl 5800	. . . . . . . . . . . 12
26	25	recn 5326	. . . . . . . . . . 11
27	12, 4, 26	mulass 5337	. . . . . . . . . 10
28	26	mulid2 5345	. . . . . . . . . 10
29	24, 27, 28	3eqtr3 1506	. . . . . . . . 9
30	29	fveq2i 3733	. . . . . . . 8
31	4, 26	mulcl 5333	. . . . . . . . 9
32		sin2tt 7462	. . . . . . . . 9
33	31, 32	ax-mp 7	. . . . . . . 8
34		sinhalfpi 8675	. . . . . . . 8
35	30, 33, 34	3eqtr3 1506	. . . . . . 7
36	11, 22, 35	3eqtr3 1506	. . . . . 6
37	36	fveq2i 3733	. . . . 5
38		4re 5984	. . . . . . . . 9
39		4pos 5994	. . . . . . . . . 10
40	38, 39	gt0ne0i 5629	. . . . . . . . 9
41	13, 38, 40	redivcl 5800	. . . . . . . 8
42		resinclt 7438	. . . . . . . 8
43	41, 42	ax-mp 7	. . . . . . 7
44	43, 43	remulcl 5347	. . . . . 6
45		0re 5452	. . . . . . 7
46		2pos 5991	. . . . . . 7
47	45, 1, 46	ltlei 5593	. . . . . 6
48	43	msqge0 5626	. . . . . 6
49	1, 44, 47, 48	sqrmuli 6705	. . . . 5
50		sqr1 6717	. . . . 5
51	37, 49, 50	3eqtr3r 1507	. . . 4
52		sqr2re 6731	. . . . . 6
53	52	recn 5326	. . . . 5
54		sqrclt 6711	. . . . . . 7 $/\$
55	44, 48, 54	mp2an 699	. . . . . 6
56	55	recn 5326	. . . . 5
57		sqr00t 6715	. . . . . . . . 9 $/\$
58	1, 47, 57	mp2an 699	. . . . . . . 8
59	58	necon3bii 1601	. . . . . . 7
60	2, 59	mpbir 190	. . . . . 6
61		divmul2t 5720	. . . . . 6 $/\$ $/\$ $/\$
62	60, 61	mpan2 698	. . . . 5 $/\$ $/\$
63	5, 53, 56, 62	mp3an 918	. . . 4
64	51, 63	mpbir 190	. . 3
65		pipos 8673	. . . . . . . 8
66	13, 38, 65, 39	divgt0i 5862	. . . . . . 7
67		1re 5447	. . . . . . . 8
68		pigt2lt4 8670	. . . . . . . . . . 11 $/\$
69	68	pm3.27i 324	. . . . . . . . . 10
70	13, 38, 38, 39	ltdiv1i 5825	. . . . . . . . . 10
71	69, 70	mpbi 189	. . . . . . . . 9
72	38	recn 5326	. . . . . . . . . 10
73	72, 40	divid 5771	. . . . . . . . 9
74	71, 73	breqtr 2643	. . . . . . . 8
75	41, 67, 74	ltlei 5593	. . . . . . 7
76		elioc2t 6391	. . . . . . . . 9