Metamath Proof Explorer

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 ‘ 𝐴 ) )