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 ⊢A∈02→0<sin⁡A

Proof

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