Metamath Proof Explorer

Theorem sin01gt0

Description: The sine of a positive real number less than or equal to 1 is positive. (Contributed by Paul Chapman, 19-Jan-2008) (Revised by Wolf Lammen, 25-Sep-2020)

Ref Expression
Assertion sin01gt0 ⊢ A ∈ 0 1 → 0 < sin ⁡ A

Proof

Step Hyp Ref Expression
1 0xr ⊢ 0 ∈ ℝ *
2 1re ⊢ 1 ∈ ℝ
3 elioc2 ⊢ 0 ∈ ℝ * ∧ 1 ∈ ℝ → A ∈ 0 1 ↔ A ∈ ℝ ∧ 0 < A ∧ A ≤ 1
4 1 2 3 mp2an ⊢ A ∈ 0 1 ↔ A ∈ ℝ ∧ 0 < A ∧ A ≤ 1
5 4 simp1bi ⊢ A ∈ 0 1 → A ∈ ℝ
6 3nn0 ⊢ 3 ∈ ℕ 0
7 reexpcl ⊢ A ∈ ℝ ∧ 3 ∈ ℕ 0 → A 3 ∈ ℝ
8 5 6 7 sylancl ⊢ A ∈ 0 1 → A 3 ∈ ℝ
9 3re ⊢ 3 ∈ ℝ
10 3ne0 ⊢ 3 ≠ 0
11 redivcl ⊢ A 3 ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0 → A 3 3 ∈ ℝ
12 9 10 11 mp3an23 ⊢ A 3 ∈ ℝ → A 3 3 ∈ ℝ
13 8 12 syl ⊢ A ∈ 0 1 → A 3 3 ∈ ℝ
14 3z ⊢ 3 ∈ ℤ
15 expgt0 ⊢ A ∈ ℝ ∧ 3 ∈ ℤ ∧ 0 < A → 0 < A 3
16 14 15 mp3an2 ⊢ A ∈ ℝ ∧ 0 < A → 0 < A 3
17 16 3adant3 ⊢ A ∈ ℝ ∧ 0 < A ∧ A ≤ 1 → 0 < A 3
18 4 17 sylbi ⊢ A ∈ 0 1 → 0 < A 3
19 0lt1 ⊢ 0 < 1
20 2 19 pm3.2i ⊢ 1 ∈ ℝ ∧ 0 < 1
21 3pos ⊢ 0 < 3
22 9 21 pm3.2i ⊢ 3 ∈ ℝ ∧ 0 < 3
23 1lt3 ⊢ 1 < 3
24 ltdiv2 ⊢ 1 ∈ ℝ ∧ 0 < 1 ∧ 3 ∈ ℝ ∧ 0 < 3 ∧ A 3 ∈ ℝ ∧ 0 < A 3 → 1 < 3 ↔ A 3 3 < A 3 1
25 23 24 mpbii ⊢ 1 ∈ ℝ ∧ 0 < 1 ∧ 3 ∈ ℝ ∧ 0 < 3 ∧ A 3 ∈ ℝ ∧ 0 < A 3 → A 3 3 < A 3 1
26 20 22 25 mp3an12 ⊢ A 3 ∈ ℝ ∧ 0 < A 3 → A 3 3 < A 3 1
27 8 18 26 syl2anc ⊢ A ∈ 0 1 → A 3 3 < A 3 1
28 8 recnd ⊢ A ∈ 0 1 → A 3 ∈ ℂ
29 28 div1d ⊢ A ∈ 0 1 → A 3 1 = A 3
30 27 29 breqtrd ⊢ A ∈ 0 1 → A 3 3 < A 3
31 1nn0 ⊢ 1 ∈ ℕ 0
32 31 a1i ⊢ A ∈ 0 1 → 1 ∈ ℕ 0
33 1le3 ⊢ 1 ≤ 3
34 1z ⊢ 1 ∈ ℤ
35 34 eluz1i ⊢ 3 ∈ ℤ ≥ 1 ↔ 3 ∈ ℤ ∧ 1 ≤ 3
36 14 33 35 mpbir2an ⊢ 3 ∈ ℤ ≥ 1
37 36 a1i ⊢ A ∈ 0 1 → 3 ∈ ℤ ≥ 1
38 4 simp2bi ⊢ A ∈ 0 1 → 0 < A
39 0re ⊢ 0 ∈ ℝ
40 ltle ⊢ 0 ∈ ℝ ∧ A ∈ ℝ → 0 < A → 0 ≤ A
41 39 5 40 sylancr ⊢ A ∈ 0 1 → 0 < A → 0 ≤ A
42 38 41 mpd ⊢ A ∈ 0 1 → 0 ≤ A
43 4 simp3bi ⊢ A ∈ 0 1 → A ≤ 1
44 5 32 37 42 43 leexp2rd ⊢ A ∈ 0 1 → A 3 ≤ A 1
45 5 recnd ⊢ A ∈ 0 1 → A ∈ ℂ
46 45 exp1d ⊢ A ∈ 0 1 → A 1 = A
47 44 46 breqtrd ⊢ A ∈ 0 1 → A 3 ≤ A
48 13 8 5 30 47 ltletrd ⊢ A ∈ 0 1 → A 3 3 < A
49 13 5 posdifd ⊢ A ∈ 0 1 → A 3 3 < A ↔ 0 < A − A 3 3
50 48 49 mpbid ⊢ A ∈ 0 1 → 0 < A − A 3 3
51 sin01bnd ⊢ A ∈ 0 1 → A − A 3 3 < sin ⁡ A ∧ sin ⁡ A < A
52 51 simpld ⊢ A ∈ 0 1 → A − A 3 3 < sin ⁡ A
53 5 13 resubcld ⊢ A ∈ 0 1 → A − A 3 3 ∈ ℝ
54 5 resincld ⊢ A ∈ 0 1 → sin ⁡ A ∈ ℝ
55 lttr ⊢ 0 ∈ ℝ ∧ A − A 3 3 ∈ ℝ ∧ sin ⁡ A ∈ ℝ → 0 < A − A 3 3 ∧ A − A 3 3 < sin ⁡ A → 0 < sin ⁡ A
56 39 53 54 55 mp3an2i ⊢ A ∈ 0 1 → 0 < A − A 3 3 ∧ A − A 3 3 < sin ⁡ A → 0 < sin ⁡ A
57 50 52 56 mp2and ⊢ A ∈ 0 1 → 0 < sin ⁡ A