Theorem sin02gt0

Description: The sine of a positive real number less than or equal to 2 is positive. (Contributed by Paul Chapman, 19-Jan-2008)

	Ref	Expression
Assertion	sin02gt0	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) → 0 < ( sin ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		0xr	⊢ 0 ∈ ℝ*
2		2re	⊢ 2 ∈ ℝ
3		elioc2	⊢ ( ( 0 ∈ ℝ* ∧ 2 ∈ ℝ ) → ( 𝐴 ∈ ( 0 (,] 2 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 2 ) ) )
4	1 2 3	mp2an	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 2 ) )
5		rehalfcl	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 / 2 ) ∈ ℝ )
6	5	3ad2ant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 2 ) → ( 𝐴 / 2 ) ∈ ℝ )
7	4 6	sylbi	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) → ( 𝐴 / 2 ) ∈ ℝ )
8		resincl	⊢ ( ( 𝐴 / 2 ) ∈ ℝ → ( sin ‘ ( 𝐴 / 2 ) ) ∈ ℝ )
9		recoscl	⊢ ( ( 𝐴 / 2 ) ∈ ℝ → ( cos ‘ ( 𝐴 / 2 ) ) ∈ ℝ )
10	8 9	remulcld	⊢ ( ( 𝐴 / 2 ) ∈ ℝ → ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ∈ ℝ )
11	7 10	syl	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) → ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ∈ ℝ )
12		2pos	⊢ 0 < 2
13		divgt0	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → 0 < ( 𝐴 / 2 ) )
14	2 12 13	mpanr12	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 < ( 𝐴 / 2 ) )
15	14	3adant3	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 2 ) → 0 < ( 𝐴 / 2 ) )
16	2 12	pm3.2i	⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
17		lediv1	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 𝐴 ≤ 2 ↔ ( 𝐴 / 2 ) ≤ ( 2 / 2 ) ) )
18	2 16 17	mp3an23	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ≤ 2 ↔ ( 𝐴 / 2 ) ≤ ( 2 / 2 ) ) )
19	18	biimpa	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 2 ) → ( 𝐴 / 2 ) ≤ ( 2 / 2 ) )
20		2div2e1	⊢ ( 2 / 2 ) = 1
21	19 20	breqtrdi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 2 ) → ( 𝐴 / 2 ) ≤ 1 )
22	21	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 2 ) → ( 𝐴 / 2 ) ≤ 1 )
23	6 15 22	3jca	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 2 ) → ( ( 𝐴 / 2 ) ∈ ℝ ∧ 0 < ( 𝐴 / 2 ) ∧ ( 𝐴 / 2 ) ≤ 1 ) )
24		1re	⊢ 1 ∈ ℝ
25		elioc2	⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ ) → ( ( 𝐴 / 2 ) ∈ ( 0 (,] 1 ) ↔ ( ( 𝐴 / 2 ) ∈ ℝ ∧ 0 < ( 𝐴 / 2 ) ∧ ( 𝐴 / 2 ) ≤ 1 ) ) )
26	1 24 25	mp2an	⊢ ( ( 𝐴 / 2 ) ∈ ( 0 (,] 1 ) ↔ ( ( 𝐴 / 2 ) ∈ ℝ ∧ 0 < ( 𝐴 / 2 ) ∧ ( 𝐴 / 2 ) ≤ 1 ) )
27	23 4 26	3imtr4i	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) → ( 𝐴 / 2 ) ∈ ( 0 (,] 1 ) )
28		sin01gt0	⊢ ( ( 𝐴 / 2 ) ∈ ( 0 (,] 1 ) → 0 < ( sin ‘ ( 𝐴 / 2 ) ) )
29	27 28	syl	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) → 0 < ( sin ‘ ( 𝐴 / 2 ) ) )
30		cos01gt0	⊢ ( ( 𝐴 / 2 ) ∈ ( 0 (,] 1 ) → 0 < ( cos ‘ ( 𝐴 / 2 ) ) )
31	27 30	syl	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) → 0 < ( cos ‘ ( 𝐴 / 2 ) ) )
32		axmulgt0	⊢ ( ( ( sin ‘ ( 𝐴 / 2 ) ) ∈ ℝ ∧ ( cos ‘ ( 𝐴 / 2 ) ) ∈ ℝ ) → ( ( 0 < ( sin ‘ ( 𝐴 / 2 ) ) ∧ 0 < ( cos ‘ ( 𝐴 / 2 ) ) ) → 0 < ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) )
33	8 9 32	syl2anc	⊢ ( ( 𝐴 / 2 ) ∈ ℝ → ( ( 0 < ( sin ‘ ( 𝐴 / 2 ) ) ∧ 0 < ( cos ‘ ( 𝐴 / 2 ) ) ) → 0 < ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) )
34	7 33	syl	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) → ( ( 0 < ( sin ‘ ( 𝐴 / 2 ) ) ∧ 0 < ( cos ‘ ( 𝐴 / 2 ) ) ) → 0 < ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) )
35	29 31 34	mp2and	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) → 0 < ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) )
36		axmulgt0	⊢ ( ( 2 ∈ ℝ ∧ ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ∈ ℝ ) → ( ( 0 < 2 ∧ 0 < ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) → 0 < ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) )
37	2 36	mpan	⊢ ( ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ∈ ℝ → ( ( 0 < 2 ∧ 0 < ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) → 0 < ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) )
38	12 37	mpani	⊢ ( ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ∈ ℝ → ( 0 < ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) → 0 < ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) )
39	11 35 38	sylc	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) → 0 < ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) )
40	7	recnd	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) → ( 𝐴 / 2 ) ∈ ℂ )
41		sin2t	⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( sin ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) )
42	40 41	syl	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) → ( sin ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) )
43	39 42	breqtrrd	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) → 0 < ( sin ‘ ( 2 · ( 𝐴 / 2 ) ) ) )
44	4	simp1bi	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) → 𝐴 ∈ ℝ )
45	44	recnd	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) → 𝐴 ∈ ℂ )
46		2cn	⊢ 2 ∈ ℂ
47		2ne0	⊢ 2 ≠ 0
48		divcan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 )
49	46 47 48	mp3an23	⊢ ( 𝐴 ∈ ℂ → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 )
50	45 49	syl	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 )
51	50	fveq2d	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) → ( sin ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( sin ‘ 𝐴 ) )
52	43 51	breqtrd	⊢ ( 𝐴 ∈ ( 0 (,] 2 ) → 0 < ( sin ‘ 𝐴 ) )