sinq12gt0

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

		Ref	Expression
	Assertion	sinq12gt0	$⊢ A \in (0, π) \to 0 < \sin A$

Proof

Step	Hyp	Ref	Expression
1		0xr	$⊢ 0 \in ℝ^{*}$
2		pire	$⊢ π \in ℝ$
3	2	rexri	$⊢ π \in ℝ^{*}$
4		elioo2	$⊢ (0 \in ℝ^{} \land π \in ℝ^{}) \to (A \in (0, π) \leftrightarrow (A \in ℝ \land 0 < A \land A < π))$
5	1 3 4	mp2an	$⊢ A \in (0, π) \leftrightarrow (A \in ℝ \land 0 < A \land A < π)$
6		rehalfcl	$⊢ A \in ℝ \to \frac{A}{2} \in ℝ$
7	6	3ad2ant1	$⊢ (A \in ℝ \land 0 < A \land A < π) \to \frac{A}{2} \in ℝ$
8		halfpos2	$⊢ A \in ℝ \to (0 < A \leftrightarrow 0 < \frac{A}{2})$
9	8	biimpa	$⊢ (A \in ℝ \land 0 < A) \to 0 < \frac{A}{2}$
10	9	3adant3	$⊢ (A \in ℝ \land 0 < A \land A < π) \to 0 < \frac{A}{2}$
11		2re	$⊢ 2 \in ℝ$
12		2pos	$⊢ 0 < 2$
13	11 12	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
14		ltdiv1	$⊢ (A \in ℝ \land π \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (A < π \leftrightarrow \frac{A}{2} < \frac{π}{2})$
15	2 13 14	mp3an23	$⊢ A \in ℝ \to (A < π \leftrightarrow \frac{A}{2} < \frac{π}{2})$
16	15	adantr	$⊢ (A \in ℝ \land 0 < A) \to (A < π \leftrightarrow \frac{A}{2} < \frac{π}{2})$
17	16	biimp3a	$⊢ (A \in ℝ \land 0 < A \land A < π) \to \frac{A}{2} < \frac{π}{2}$
18		sincosq1lem	$⊢ (\frac{A}{2} \in ℝ \land 0 < \frac{A}{2} \land \frac{A}{2} < \frac{π}{2}) \to 0 < \sin (\frac{A}{2})$
19	7 10 17 18	syl3anc	$⊢ (A \in ℝ \land 0 < A \land A < π) \to 0 < \sin (\frac{A}{2})$
20		resubcl	$⊢ (π \in ℝ \land A \in ℝ) \to π - A \in ℝ$
21	2 20	mpan	$⊢ A \in ℝ \to π - A \in ℝ$
22		rehalfcl	$⊢ π - A \in ℝ \to \frac{π - A}{2} \in ℝ$
23	21 22	syl	$⊢ A \in ℝ \to \frac{π - A}{2} \in ℝ$
24	23	3ad2ant1	$⊢ (A \in ℝ \land 0 < A \land A < π) \to \frac{π - A}{2} \in ℝ$
25		posdif	$⊢ (A \in ℝ \land π \in ℝ) \to (A < π \leftrightarrow 0 < π - A)$
26	2 25	mpan2	$⊢ A \in ℝ \to (A < π \leftrightarrow 0 < π - A)$
27		halfpos2	$⊢ π - A \in ℝ \to (0 < π - A \leftrightarrow 0 < \frac{π - A}{2})$
28	21 27	syl	$⊢ A \in ℝ \to (0 < π - A \leftrightarrow 0 < \frac{π - A}{2})$
29	26 28	bitrd	$⊢ A \in ℝ \to (A < π \leftrightarrow 0 < \frac{π - A}{2})$
30	29	adantr	$⊢ (A \in ℝ \land 0 < A) \to (A < π \leftrightarrow 0 < \frac{π - A}{2})$
31	30	biimp3a	$⊢ (A \in ℝ \land 0 < A \land A < π) \to 0 < \frac{π - A}{2}$
32		ltsubpos	$⊢ (A \in ℝ \land π \in ℝ) \to (0 < A \leftrightarrow π - A < π)$
33	2 32	mpan2	$⊢ A \in ℝ \to (0 < A \leftrightarrow π - A < π)$
34		ltdiv1	$⊢ (π - A \in ℝ \land π \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (π - A < π \leftrightarrow \frac{π - A}{2} < \frac{π}{2})$
35	2 13 34	mp3an23	$⊢ π - A \in ℝ \to (π - A < π \leftrightarrow \frac{π - A}{2} < \frac{π}{2})$
36	21 35	syl	$⊢ A \in ℝ \to (π - A < π \leftrightarrow \frac{π - A}{2} < \frac{π}{2})$
37	33 36	bitrd	$⊢ A \in ℝ \to (0 < A \leftrightarrow \frac{π - A}{2} < \frac{π}{2})$
38	37	biimpa	$⊢ (A \in ℝ \land 0 < A) \to \frac{π - A}{2} < \frac{π}{2}$
39	38	3adant3	$⊢ (A \in ℝ \land 0 < A \land A < π) \to \frac{π - A}{2} < \frac{π}{2}$
40		sincosq1lem	$⊢ (\frac{π - A}{2} \in ℝ \land 0 < \frac{π - A}{2} \land \frac{π - A}{2} < \frac{π}{2}) \to 0 < \sin (\frac{π - A}{2})$
41	24 31 39 40	syl3anc	$⊢ (A \in ℝ \land 0 < A \land A < π) \to 0 < \sin (\frac{π - A}{2})$
42		recn	$⊢ A \in ℝ \to A \in ℂ$
43		picn	$⊢ π \in ℂ$
44		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
45		divsubdir	$⊢ (π \in ℂ \land A \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{π - A}{2} = (\frac{π}{2}) - (\frac{A}{2})$
46	43 44 45	mp3an13	$⊢ A \in ℂ \to \frac{π - A}{2} = (\frac{π}{2}) - (\frac{A}{2})$
47	42 46	syl	$⊢ A \in ℝ \to \frac{π - A}{2} = (\frac{π}{2}) - (\frac{A}{2})$
48	47	fveq2d	$⊢ A \in ℝ \to \sin (\frac{π - A}{2}) = \sin ((\frac{π}{2}) - (\frac{A}{2}))$
49	6	recnd	$⊢ A \in ℝ \to \frac{A}{2} \in ℂ$
50		sinhalfpim	$⊢ \frac{A}{2} \in ℂ \to \sin ((\frac{π}{2}) - (\frac{A}{2})) = \cos (\frac{A}{2})$
51	49 50	syl	$⊢ A \in ℝ \to \sin ((\frac{π}{2}) - (\frac{A}{2})) = \cos (\frac{A}{2})$
52	48 51	eqtrd	$⊢ A \in ℝ \to \sin (\frac{π - A}{2}) = \cos (\frac{A}{2})$
53	52	3ad2ant1	$⊢ (A \in ℝ \land 0 < A \land A < π) \to \sin (\frac{π - A}{2}) = \cos (\frac{A}{2})$
54	41 53	breqtrd	$⊢ (A \in ℝ \land 0 < A \land A < π) \to 0 < \cos (\frac{A}{2})$
55		resincl	$⊢ \frac{A}{2} \in ℝ \to \sin (\frac{A}{2}) \in ℝ$
56		recoscl	$⊢ \frac{A}{2} \in ℝ \to \cos (\frac{A}{2}) \in ℝ$
57	55 56	jca	$⊢ \frac{A}{2} \in ℝ \to (\sin (\frac{A}{2}) \in ℝ \land \cos (\frac{A}{2}) \in ℝ)$
58		axmulgt0	$⊢ (\sin (\frac{A}{2}) \in ℝ \land \cos (\frac{A}{2}) \in ℝ) \to ((0 < \sin (\frac{A}{2}) \land 0 < \cos (\frac{A}{2})) \to 0 < \sin (\frac{A}{2}) \cos (\frac{A}{2}))$
59	6 57 58	3syl	$⊢ A \in ℝ \to ((0 < \sin (\frac{A}{2}) \land 0 < \cos (\frac{A}{2})) \to 0 < \sin (\frac{A}{2}) \cos (\frac{A}{2}))$
60		remulcl	$⊢ (\sin (\frac{A}{2}) \in ℝ \land \cos (\frac{A}{2}) \in ℝ) \to \sin (\frac{A}{2}) \cos (\frac{A}{2}) \in ℝ$
61	6 57 60	3syl	$⊢ A \in ℝ \to \sin (\frac{A}{2}) \cos (\frac{A}{2}) \in ℝ$
62		axmulgt0	$⊢ (2 \in ℝ \land \sin (\frac{A}{2}) \cos (\frac{A}{2}) \in ℝ) \to ((0 < 2 \land 0 < \sin (\frac{A}{2}) \cos (\frac{A}{2})) \to 0 < 2 \sin (\frac{A}{2}) \cos (\frac{A}{2}))$
63	11 61 62	sylancr	$⊢ A \in ℝ \to ((0 < 2 \land 0 < \sin (\frac{A}{2}) \cos (\frac{A}{2})) \to 0 < 2 \sin (\frac{A}{2}) \cos (\frac{A}{2}))$
64	12 63	mpani	$⊢ A \in ℝ \to (0 < \sin (\frac{A}{2}) \cos (\frac{A}{2}) \to 0 < 2 \sin (\frac{A}{2}) \cos (\frac{A}{2}))$
65	59 64	syld	$⊢ A \in ℝ \to ((0 < \sin (\frac{A}{2}) \land 0 < \cos (\frac{A}{2})) \to 0 < 2 \sin (\frac{A}{2}) \cos (\frac{A}{2}))$
66	65	3ad2ant1	$⊢ (A \in ℝ \land 0 < A \land A < π) \to ((0 < \sin (\frac{A}{2}) \land 0 < \cos (\frac{A}{2})) \to 0 < 2 \sin (\frac{A}{2}) \cos (\frac{A}{2}))$
67	19 54 66	mp2and	$⊢ (A \in ℝ \land 0 < A \land A < π) \to 0 < 2 \sin (\frac{A}{2}) \cos (\frac{A}{2})$
68		2cn	$⊢ 2 \in ℂ$
69		2ne0	$⊢ 2 \neq 0$
70		divcan2	$⊢ (A \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to 2 (\frac{A}{2}) = A$
71	68 69 70	mp3an23	$⊢ A \in ℂ \to 2 (\frac{A}{2}) = A$
72	42 71	syl	$⊢ A \in ℝ \to 2 (\frac{A}{2}) = A$
73	72	fveq2d	$⊢ A \in ℝ \to \sin 2 (\frac{A}{2}) = \sin A$
74		sin2t	$⊢ \frac{A}{2} \in ℂ \to \sin 2 (\frac{A}{2}) = 2 \sin (\frac{A}{2}) \cos (\frac{A}{2})$
75	49 74	syl	$⊢ A \in ℝ \to \sin 2 (\frac{A}{2}) = 2 \sin (\frac{A}{2}) \cos (\frac{A}{2})$
76	73 75	eqtr3d	$⊢ A \in ℝ \to \sin A = 2 \sin (\frac{A}{2}) \cos (\frac{A}{2})$
77	76	3ad2ant1	$⊢ (A \in ℝ \land 0 < A \land A < π) \to \sin A = 2 \sin (\frac{A}{2}) \cos (\frac{A}{2})$
78	67 77	breqtrrd	$⊢ (A \in ℝ \land 0 < A \land A < π) \to 0 < \sin A$
79	5 78	sylbi	$⊢ A \in (0, π) \to 0 < \sin A$

Metamath Proof Explorer

Theorem sinq12gt0

Proof