Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem sinq12gt0t 8625

Description: The sine of a number strictly between and is positive. (Contributed by Paul Chapman, 15-Mar-2008.)

Assertion

Ref	Expression
sinq12gt0t	(,)

---

Proof of Theorem sinq12gt0t

Step	Hyp	Ref	Expression
1		0re 5412	. . 3
2		pire 8596	. . 3
3		elioo2t 6316	. . . 4 (,)
4		rexrt 5471	. . . 4
5		rexrt 5471	. . . 4
6	3, 4, 5	syl2an 454	. . 3 (,)
7	1, 2, 6	mp2an 695	. 2 (,)
8		sincosq1lem 8620	. . . . 5
9		rehalfclt 5981	. . . . . 6
10	9	3ad2ant1 798	. . . . 5
11		halfpos2t 5984	. . . . . . 7
12	11	biimpa 416	. . . . . 6
13	12	3adant3 797	. . . . 5
14		2re 5926	. . . . . . . 8
15		2pos 5936	. . . . . . . . 9
16		ltdiv1t 5805	. . . . . . . . 9
17	15, 16	mpan2 694	. . . . . . . 8
18	2, 14, 17	mp3an23 905	. . . . . . 7
19	18	adantr 389	. . . . . 6
20	19	biimp3a 916	. . . . 5
21	8, 10, 13, 20	syl3anc 856	. . . 4
22		sincosq1lem 8620	. . . . . 6
23		resubclt 5410	. . . . . . . . 9
24	2, 23	mpan 693	. . . . . . . 8
25		rehalfclt 5981	. . . . . . . 8
26	24, 25	syl 10	. . . . . . 7
27	26	3ad2ant1 798	. . . . . 6
28		posdift 5627	. . . . . . . . . 10
29	2, 28	mpan2 694	. . . . . . . . 9
30		halfpos2t 5984	. . . . . . . . . 10
31	24, 30	syl 10	. . . . . . . . 9
32	29, 31	bitrd 526	. . . . . . . 8
33	32	adantr 389	. . . . . . 7
34	33	biimp3a 916	. . . . . 6
35		ltsubpost 5626	. . . . . . . . . 10
36	2, 35	mpan2 694	. . . . . . . . 9
37		ltdiv1t 5805	. . . . . . . . . . . 12
38	15, 37	mpan2 694	. . . . . . . . . . 11
39	2, 14, 38	mp3an23 905	. . . . . . . . . 10
40	24, 39	syl 10	. . . . . . . . 9
41	36, 40	bitrd 526	. . . . . . . 8
42	41	biimpa 416	. . . . . . 7
43	42	3adant3 797	. . . . . 6
44	22, 27, 34, 43	syl3anc 856	. . . . 5
45		recnt 5285	. . . . . . . . 9
46	2	recn 5286	. . . . . . . . . 10
47		2cn 5927	. . . . . . . . . 10
48		2ne0 5937	. . . . . . . . . . 11
49		divsubdirt 5731	. . . . . . . . . . 11
50	48, 49	mpan2 694	. . . . . . . . . 10
51	46, 47, 50	mp3an13 904	. . . . . . . . 9
52	45, 51	syl 10	. . . . . . . 8
53	52	fveq2d 3713	. . . . . . 7
54	9	recnd 5287	. . . . . . . 8
55		sinhalfpim 8617	. . . . . . . 8
56	54, 55	syl 10	. . . . . . 7
57	53, 56	eqtrd 1499	. . . . . 6
58	57	3ad2ant1 798	. . . . 5
59	44, 58	breqtrd 2629	. . . 4
60		resinclt 7380	. . . . . . . 8
61		recosclt 7381	. . . . . . . 8
62	60, 61	jca 288	. . . . . . 7
63		axmulgt0 5478	. . . . . . 7
64	9, 62, 63	3syl 20	. . . . . 6
65		axmulrcl 5246	. . . . . . . . 9
66	9, 62, 65	3syl 20	. . . . . . . 8
67		axmulgt0 5478	. . . . . . . . 9
68	14, 67	mpan 693	. . . . . . . 8