Theorem sincosq2sgn 8657

Description: The signs of the sine and cosine functions in the second quadrant. (Contributed by Paul Chapman, 24-Jan-2008.)

Assertion

Ref	Expression
sincosq2sgn	|- (A e. ((pi / 2)(,)pi) -> (0 < (sin` A) /\ (cos` A) < 0))

Proof of Theorem sincosq2sgn

Step	Hyp	Ref	Expression
1		pire 8631	. . . 4 |- pi e. RR
2		2re 5936	. . . 4 |- 2 e. RR
3		2ne0 5947	. . . 4 |- 2 =/= 0
4	1, 2, 3	redivcl 5764	. . 3 |- (pi / 2) e. RR
5		elioo2t 6329	. . . 4 |- (((pi / 2) e. RR* /\ pi e. RR*) -> (A e. ((pi / 2)(,)pi) <-> (A e. RR /\ (pi / 2) < A /\ A < pi)))
6		rexrt 5482	. . . 4 |- ((pi / 2) e. RR -> (pi / 2) e. RR*)
7		rexrt 5482	. . . 4 |- (pi e. RR -> pi e. RR*)
8	5, 6, 7	syl2an 454	. . 3 |- (((pi / 2) e. RR /\ pi e. RR) -> (A e. ((pi / 2)(,)pi) <-> (A e. RR /\ (pi / 2) < A /\ A < pi)))
9	4, 1, 8	mp2an 696	. 2 |- (A e. ((pi / 2)(,)pi) <-> (A e. RR /\ (pi / 2) < A /\ A < pi))
10		0re 5423	. . . . . . . . . 10 |- 0 e. RR
11		elioo2t 6329	. . . . . . . . . . 11 |- ((0 e. RR* /\ (pi / 2) e. RR*) -> ((A - (pi / 2)) e. (0(,)(pi / 2)) <-> ((A - (pi / 2)) e. RR /\ 0 < (A - (pi / 2)) /\ (A - (pi / 2)) < (pi / 2))))
12		rexrt 5482	. . . . . . . . . . 11 |- (0 e. RR -> 0 e. RR*)
13	11, 12, 6	syl2an 454	. . . . . . . . . 10 |- ((0 e. RR /\ (pi / 2) e. RR) -> ((A - (pi / 2)) e. (0(,)(pi / 2)) <-> ((A - (pi / 2)) e. RR /\ 0 < (A - (pi / 2)) /\ (A - (pi / 2)) < (pi / 2))))
14	10, 4, 13	mp2an 696	. . . . . . . . 9 |- ((A - (pi / 2)) e. (0(,)(pi / 2)) <-> ((A - (pi / 2)) e. RR /\ 0 < (A - (pi / 2)) /\ (A - (pi / 2)) < (pi / 2)))
15		sincosq1sgn 8656	. . . . . . . . 9 |- ((A - (pi / 2)) e. (0(,)(pi / 2)) -> (0 < (sin` (A - (pi / 2))) /\ 0 < (cos` (A - (pi / 2)))))
16	14, 15	sylbir 201	. . . . . . . 8 |- (((A - (pi / 2)) e. RR /\ 0 < (A - (pi / 2)) /\ (A - (pi / 2)) < (pi / 2)) -> (0 < (sin` (A - (pi / 2))) /\ 0 < (cos` (A - (pi / 2)))))
17		resubclt 5421	. . . . . . . . 9 |- ((A e. RR /\ (pi / 2) e. RR) -> (A - (pi / 2)) e. RR)
18	4, 17	mpan2 695	. . . . . . . 8 |- (A e. RR -> (A - (pi / 2)) e. RR)
19	16, 18	syl3an1 858	. . . . . . 7 |- ((A e. RR /\ 0 < (A - (pi / 2)) /\ (A - (pi / 2)) < (pi / 2)) -> (0 < (sin` (A - (pi / 2))) /\ 0 < (cos` (A - (pi / 2)))))
20	19	3expib 835	. . . . . 6 |- (A e. RR -> ((0 < (A - (pi / 2)) /\ (A - (pi / 2)) < (pi / 2)) -> (0 < (sin` (A - (pi / 2))) /\ 0 < (cos` (A - (pi / 2))))))
21		ltsub13t 5626	. . . . . . . . 9 |- ((0 e. RR /\ A e. RR /\ (pi / 2) e. RR) -> (0 < (A - (pi / 2)) <-> (pi / 2) < (A - 0)))
22	10, 4, 21	mp3an13 906	. . . . . . . 8 |- (A e. RR -> (0 < (A - (pi / 2)) <-> (pi / 2) < (A - 0)))
23		recnt 5296	. . . . . . . . . 10 |- (A e. RR -> A e. CC)
24		subid1t 5379	. . . . . . . . . 10 |- (A e. CC -> (A - 0) = A)
25	23, 24	syl 10	. . . . . . . . 9 |- (A e. RR -> (A - 0) = A)
26	25	breq2d 2626	. . . . . . . 8 |- (A e. RR -> ((pi / 2) < (A - 0) <-> (pi / 2) < A))
27	22, 26	bitrd 527	. . . . . . 7 |- (A e. RR -> (0 < (A - (pi / 2)) <-> (pi / 2) < A))
28		ltsubaddt 5611	. . . . . . . . 9 |- ((A e. RR /\ (pi / 2) e. RR /\ (pi / 2) e. RR) -> ((A - (pi / 2)) < (pi / 2) <-> A < ((pi / 2) + (pi / 2))))
29	4, 4, 28	mp3an23 907	. . . . . . . 8 |- (A e. RR -> ((A - (pi / 2)) < (pi / 2) <-> A < ((pi / 2) + (pi / 2))))
30	1	recn 5297	. . . . . . . . . 10 |- pi e. CC
31		2halvest 5996	. . . . . . . . . 10 |- (pi e. CC -> ((pi / 2) + (pi / 2)) = pi)
32	30, 31	ax-mp 7	. . . . . . . . 9 |- ((pi / 2) + (pi / 2)) = pi
33	32	breq2i 2623	. . . . . . . 8 |- (A < ((pi / 2) + (pi / 2)) <-> A < pi)
34	29, 33	syl6bb 535	. . . . . . 7 |- (A e. RR -> ((A - (pi / 2)) < (pi / 2) <-> A < pi))
35	27, 34	anbi12d 627	. . . . . 6 |- (A e. RR -> ((0 < (A - (pi / 2)) /\ (A - (pi / 2)) < (pi / 2)) <-> ((pi / 2) < A /\ A < pi)))
36		resinclt 7397	. . . . . . . 8 |- ((A - (pi / 2)) e. RR -> (sin` (A - (pi / 2))) e. RR)
37		lt0neg2t 5652	. . . . . . . 8 |- ((sin` (A - (pi / 2))) e. RR -> (0 < (sin` (A - (pi / 2))) <-> -u(sin` (A - (pi / 2))) < 0))
38	18, 36, 37	3syl 20	. . . . . . 7 |- (A e. RR -> (0 < (sin` (A - (pi / 2))) <-> -u(sin` (A - (pi / 2))) < 0))
39	38	anbi1d 616	. . . . . 6 |- (A e. RR -> ((0 < (sin` (A - (pi / 2))) /\ 0 < (cos` (A - (pi / 2)))) <-> (-u(sin` (A - (pi / 2))) < 0 /\ 0 < (cos` (A - (pi / 2))))))
40	20, 35, 39	3imtr3d 541	. . . . 5 |- (A e. RR -> (((pi / 2) < A /\ A < pi) -> (-u(sin` (A - (pi / 2))) < 0 /\ 0 < (cos` (A - (pi / 2))))))
41	4	recn 5297	. . . . . . . . . . 11 |- (pi / 2) e. CC
42		pncan3t 5360	. . . . . . . . . . 11 |- (((pi / 2) e. CC /\ A e. CC) -> ((pi / 2) + (A - (pi / 2))) = A)
43	41, 42	mpan 694	. . . . . . . . . 10 |- (A e. CC -> ((pi / 2) + (A - (pi / 2))) = A)
44	23, 43	syl 10	. . . . . . . . 9 |- (A e. RR -> ((pi / 2) + (A - (pi / 2))) = A)
45	44	fveq2d 3723	. . . . . . . 8 |- (A e. RR -> (cos` ((pi / 2) + (A - (pi / 2)))) = (cos` A))
46	18	recnd 5298	. . . . . . . . 9 |- (A e. RR -> (A - (pi / 2)) e. CC)
47		coshalfpip 8653	. . . . . . . . 9 |- ((A - (pi / 2)) e. CC -> (cos` ((pi / 2) + (A - (pi / 2)))) = -u(sin` (A - (pi / 2))))
48	46, 47	syl 10	. . . . . . . 8 |- (A e. RR -> (cos` ((pi / 2) + (A - (pi / 2)))) = -u(sin` (A - (pi / 2))))
49	45, 48	eqtr3d 1507	. . . . . . 7 |- (A e. RR -> (cos` A) = -u(sin` (A - (pi / 2))))
50	49	breq1d 2625	. . . . . 6 |- (A e. RR -> ((cos` A) < 0 <-> -u(sin` (A - (pi / 2))) < 0))
51	44	fveq2d 3723	. . . . . . . 8 |- (A e. RR -> (sin` ((pi / 2) + (A - (pi / 2)))) = (sin` A))
52		sinhalfpip 8651	. . . . . . . . 9 |- ((A - (pi / 2)) e. CC -> (sin` ((pi / 2) + (A - (pi / 2)))) = (cos` (A - (pi / 2))))
53	46, 52	syl 10	. . . . . . . 8 |- (A e. RR -> (sin` ((pi / 2) + (A - (pi / 2)))) = (cos` (A - (pi / 2))))
54	51, 53	eqtr3d 1507	. . . . . . 7 |- (A e. RR -> (sin` A) = (cos` (A - (pi / 2))))
55	54	breq2d 2626	. . . . . 6 |- (A e. RR -> (0 < (sin` A) <-> 0 < (cos` (A - (pi / 2)))))
56	50, 55	anbi12d 627	. . . . 5 |- (A e. RR -> (((cos` A) < 0 /\ 0 < (sin` A)) <-> (-u(sin` (A - (pi / 2))) < 0 /\ 0 < (cos` (A - (pi / 2))))))
57	40, 56	sylibrd 204	. . . 4 |- (A e. RR -> (((pi / 2) < A /\ A < pi) -> ((cos` A) < 0 /\ 0 < (sin` A))))
58	57	3impib 830	. . 3 |- ((A e. RR