Theorem sinq12gt0t 8644

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

Assertion

Ref	Expression
sinq12gt0t	|- (A e. (0(,)pi) -> 0 < (sin` A))

Proof of Theorem sinq12gt0t

Step	Hyp	Ref	Expression
1		0re 5420	. . 3 |- 0 e. RR
2		pire 8615	. . 3 |- pi e. RR
3		elioo2t 6324	. . . 4 |- ((0 e. RR* /\ pi e. RR*) -> (A e. (0(,)pi) <-> (A e. RR /\ 0 < A /\ A < pi)))
4		rexrt 5479	. . . 4 |- (0 e. RR -> 0 e. RR*)
5		rexrt 5479	. . . 4 |- (pi e. RR -> pi e. RR*)
6	3, 4, 5	syl2an 454	. . 3 |- ((0 e. RR /\ pi e. RR) -> (A e. (0(,)pi) <-> (A e. RR /\ 0 < A /\ A < pi)))
7	1, 2, 6	mp2an 696	. 2 |- (A e. (0(,)pi) <-> (A e. RR /\ 0 < A /\ A < pi))
8		sincosq1lem 8639	. . . . 5 |- (((A / 2) e. RR /\ 0 < (A / 2) /\ (A / 2) < (pi / 2)) -> 0 < (sin` (A / 2)))
9		rehalfclt 5989	. . . . . 6 |- (A e. RR -> (A / 2) e. RR)
10	9	3ad2ant1 799	. . . . 5 |- ((A e. RR /\ 0 < A /\ A < pi) -> (A / 2) e. RR)
11		halfpos2t 5992	. . . . . . 7 |- (A e. RR -> (0 < A <-> 0 < (A / 2)))
12	11	biimpa 416	. . . . . 6 |- ((A e. RR /\ 0 < A) -> 0 < (A / 2))
13	12	3adant3 798	. . . . 5 |- ((A e. RR /\ 0 < A /\ A < pi) -> 0 < (A / 2))
14		2re 5934	. . . . . . . 8 |- 2 e. RR
15		2pos 5944	. . . . . . . . 9 |- 0 < 2
16		ltdiv1t 5813	. . . . . . . . 9 |- (((A e. RR /\ pi e. RR /\ 2 e. RR) /\ 0 < 2) -> (A < pi <-> (A / 2) < (pi / 2)))
17	15, 16	mpan2 695	. . . . . . . 8 |- ((A e. RR /\ pi e. RR /\ 2 e. RR) -> (A < pi <-> (A / 2) < (pi / 2)))
18	2, 14, 17	mp3an23 906	. . . . . . 7 |- (A e. RR -> (A < pi <-> (A / 2) < (pi / 2)))
19	18	adantr 389	. . . . . 6 |- ((A e. RR /\ 0 < A) -> (A < pi <-> (A / 2) < (pi / 2)))
20	19	biimp3a 917	. . . . 5 |- ((A e. RR /\ 0 < A /\ A < pi) -> (A / 2) < (pi / 2))
21	8, 10, 13, 20	syl3anc 857	. . . 4 |- ((A e. RR /\ 0 < A /\ A < pi) -> 0 < (sin` (A / 2)))
22		sincosq1lem 8639	. . . . . 6 |- ((((pi - A) / 2) e. RR /\ 0 < ((pi - A) / 2) /\ ((pi - A) / 2) < (pi / 2)) -> 0 < (sin` ((pi - A) / 2)))
23		resubclt 5418	. . . . . . . . 9 |- ((pi e. RR /\ A e. RR) -> (pi - A) e. RR)
24	2, 23	mpan 694	. . . . . . . 8 |- (A e. RR -> (pi - A) e. RR)
25		rehalfclt 5989	. . . . . . . 8 |- ((pi - A) e. RR -> ((pi - A) / 2) e. RR)
26	24, 25	syl 10	. . . . . . 7 |- (A e. RR -> ((pi - A) / 2) e. RR)
27	26	3ad2ant1 799	. . . . . 6 |- ((A e. RR /\ 0 < A /\ A < pi) -> ((pi - A) / 2) e. RR)
28		posdift 5635	. . . . . . . . . 10 |- ((A e. RR /\ pi e. RR) -> (A < pi <-> 0 < (pi - A)))
29	2, 28	mpan2 695	. . . . . . . . 9 |- (A e. RR -> (A < pi <-> 0 < (pi - A)))
30		halfpos2t 5992	. . . . . . . . . 10 |- ((pi - A) e. RR -> (0 < (pi - A) <-> 0 < ((pi - A) / 2)))
31	24, 30	syl 10	. . . . . . . . 9 |- (A e. RR -> (0 < (pi - A) <-> 0 < ((pi - A) / 2)))
32	29, 31	bitrd 527	. . . . . . . 8 |- (A e. RR -> (A < pi <-> 0 < ((pi - A) / 2)))
33	32	adantr 389	. . . . . . 7 |- ((A e. RR /\ 0 < A) -> (A < pi <-> 0 < ((pi - A) / 2)))
34	33	biimp3a 917	. . . . . 6 |- ((A e. RR /\ 0 < A /\ A < pi) -> 0 < ((pi - A) / 2))
35		ltsubpost 5634	. . . . . . . . . 10 |- ((A e. RR /\ pi e. RR) -> (0 < A <-> (pi - A) < pi))
36	2, 35	mpan2 695	. . . . . . . . 9 |- (A e. RR -> (0 < A <-> (pi - A) < pi))
37		ltdiv1t 5813	. . . . . . . . . . . 12 |- ((((pi - A) e. RR /\ pi e. RR /\ 2 e. RR) /\ 0 < 2) -> ((pi - A) < pi <-> ((pi - A) / 2) < (pi / 2)))
38	15, 37	mpan2 695	. . . . . . . . . . 11 |- (((pi - A) e. RR /\ pi e. RR /\ 2 e. RR) -> ((pi - A) < pi <-> ((pi - A) / 2) < (pi / 2)))
39	2, 14, 38	mp3an23 906	. . . . . . . . . 10 |- ((pi - A) e. RR -> ((pi - A) < pi <-> ((pi - A) / 2) < (pi / 2)))
40	24, 39	syl 10	. . . . . . . . 9 |- (A e. RR -> ((pi - A) < pi <-> ((pi - A) / 2) < (pi / 2)))
41	36, 40	bitrd 527	. . . . . . . 8 |- (A e. RR -> (0 < A <-> ((pi - A) / 2) < (pi / 2)))
42	41	biimpa 416	. . . . . . 7 |- ((A e. RR /\ 0 < A) -> ((pi - A) / 2) < (pi / 2))
43	42	3adant3 798	. . . . . 6 |- ((A e. RR /\ 0 < A /\ A < pi) -> ((pi - A) / 2) < (pi / 2))
44	22, 27, 34, 43	syl3anc 857	. . . . 5 |- ((A e. RR /\ 0 < A /\ A < pi) -> 0 < (sin` ((pi - A) / 2)))
45		recnt 5293	. . . . . . . . 9 |- (A e. RR -> A e. CC)
46	2	recn 5294	. . . . . . . . . 10 |- pi e. CC
47		2cn 5935	. . . . . . . . . 10 |- 2 e. CC
48		2ne0 5945	. . . . . . . . . . 11 |- 2 =/= 0
49		divsubdirt 5739	. . . . . . . . . . 11 |- (((pi e. CC /\ A e. CC /\ 2 e. CC) /\ 2 =/= 0) -> ((pi - A) / 2) = ((pi / 2) - (A / 2)))
50	48, 49	mpan2 695	. . . . . . . . . 10 |- ((pi e. CC /\ A e. CC /\ 2 e. CC) -> ((pi - A) / 2) = ((pi / 2) - (A / 2)))
51	46, 47, 50	mp3an13 905	. . . . . . . . 9 |- (A e. CC -> ((pi - A) / 2) = ((pi / 2) - (A / 2)))
52	45, 51	syl 10	. . . . . . . 8 |- (A e. RR -> ((pi - A) / 2) = ((pi / 2) - (A / 2)))
53	52	fveq2d 3719	. . . . . . 7 |- (A e. RR -> (sin` ((pi - A) / 2)) = (sin` ((pi / 2) - (A / 2))))
54	9	recnd 5295	. . . . . . . 8 |- (A e. RR -> (A / 2) e. CC)
55		sinhalfpim 8636	. . . . . . . 8 |- ((A / 2) e. CC -> (sin` ((pi / 2) - (A / 2))) = (cos` (A / 2)))
56	54, 55	syl 10	. . . . . . 7 |- (A e. RR -> (sin` ((pi / 2) - (A / 2))) = (cos` (A / 2)))
57	53, 56	eqtrd 1504	. . . . . 6 |- (A e. RR -> (sin` ((pi - A) / 2)) = (cos` (A / 2)))
58	57	3ad2ant1 799	. . . . 5 |- ((A e. RR /\ 0 < A /\ A < pi) -> (sin` ((pi - A) / 2)) = (cos` (A / 2)))
59	44, 58	breqtrd 2634	. . . 4 |- ((A e. RR /\ 0 < A /\ A < pi) -> 0 < (cos` (A / 2)))
60		resinclt 7388	. . . . . . . 8 |- ((A / 2) e. RR -> (sin` (A / 2)) e. RR)
61		recosclt 7389	. . . . . . . 8 |- ((A / 2) e. RR -> (cos` (A / 2)) e. RR)
62	60, 61	jca 288	. . . . . . 7 |- ((A / 2) e. RR -> ((sin` (A / 2)) e. RR /\ (cos` (A / 2)) e. RR))
63		axmulgt0 5486	. . . . . . 7 |- (((sin` (A / 2)) e. RR /\ (cos` (A / 2)) e. RR) -> ((0 < (sin` (A / 2)) /\ 0 < (cos` (A / 2))) -> 0 < ((sin` (A / 2)) x. (cos` (A / 2)))))
64	9, 62, 63	3syl 20	. . . . . 6 |- (A e. RR -> ((0 < (sin` (A / 2)) /\ 0 < (cos` (A / 2))) -> 0 < ((sin` (A / 2)) x. (cos` (A / 2)))))
65		axmulrcl 5254	. . . . . . . . 9 |- (((sin` (A / 2)) e. RR /\ (cos` (A / 2)) e. RR) -> ((sin` (A / 2)) x. (cos` (A / 2))) e. RR)
66	9, 62, 65	3syl 20	. . . . . . . 8 |- (A e. RR -> ((sin` (A / 2)) x. (cos` (A / 2))) e. RR)
67		axmulgt0 5486	. . . . . . . . 9 |- ((2 e. RR /\ ((sin` (A / 2)) x. (cos` (A / 2))) e. RR) -> ((0 < 2 /\ 0 < ((sin` (A / 2)) x. (cos` (A / 2)))) -> 0 < (2 x. ((sin` (A / 2)) x. (cos` (A / 2))))))
68	14, 67	mpan 694	. . . . . . . 8 |- (((sin` (A / 2)) x. (cos` (A / 2))) e. RR -> ((0 < 2 /\ 0 < ((sin