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

Proof

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