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 ( 𝐴 ∈ ( 0 (,] 1 ) → 0 < ( sin ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 0xr ⊢ 0 ∈ ℝ*
2 1re ⊢ 1 ∈ ℝ
3 elioc2 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ ) → ( 𝐴 ∈ ( 0 (,] 1 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1 ) ) )
4 1 2 3 mp2an ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1 ) )
5 4 simp1bi ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 𝐴 ∈ ℝ )
6 3nn0 ⊢ 3 ∈ ℕ0
7 reexpcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 3 ∈ ℕ0 ) → ( 𝐴 ↑ 3 ) ∈ ℝ )
8 5 6 7 sylancl ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 3 ) ∈ ℝ )
9 3re ⊢ 3 ∈ ℝ
10 3ne0 ⊢ 3 ≠ 0
11 redivcl ⊢ ( ( ( 𝐴 ↑ 3 ) ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0 ) → ( ( 𝐴 ↑ 3 ) / 3 ) ∈ ℝ )
12 9 10 11 mp3an23 ⊢ ( ( 𝐴 ↑ 3 ) ∈ ℝ → ( ( 𝐴 ↑ 3 ) / 3 ) ∈ ℝ )
13 8 12 syl ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 3 ) / 3 ) ∈ ℝ )
14 3z ⊢ 3 ∈ ℤ
15 expgt0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 3 ∈ ℤ ∧ 0 < 𝐴 ) → 0 < ( 𝐴 ↑ 3 ) )
16 14 15 mp3an2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 < ( 𝐴 ↑ 3 ) )
17 16 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1 ) → 0 < ( 𝐴 ↑ 3 ) )
18 4 17 sylbi ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 0 < ( 𝐴 ↑ 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 ) ∧ ( ( 𝐴 ↑ 3 ) ∈ ℝ ∧ 0 < ( 𝐴 ↑ 3 ) ) ) → ( 1 < 3 ↔ ( ( 𝐴 ↑ 3 ) / 3 ) < ( ( 𝐴 ↑ 3 ) / 1 ) ) )
25 23 24 mpbii ⊢ ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ∧ ( ( 𝐴 ↑ 3 ) ∈ ℝ ∧ 0 < ( 𝐴 ↑ 3 ) ) ) → ( ( 𝐴 ↑ 3 ) / 3 ) < ( ( 𝐴 ↑ 3 ) / 1 ) )
26 20 22 25 mp3an12 ⊢ ( ( ( 𝐴 ↑ 3 ) ∈ ℝ ∧ 0 < ( 𝐴 ↑ 3 ) ) → ( ( 𝐴 ↑ 3 ) / 3 ) < ( ( 𝐴 ↑ 3 ) / 1 ) )
27 8 18 26 syl2anc ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 3 ) / 3 ) < ( ( 𝐴 ↑ 3 ) / 1 ) )
28 8 recnd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 3 ) ∈ ℂ )
29 28 div1d ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 3 ) / 1 ) = ( 𝐴 ↑ 3 ) )
30 27 29 breqtrd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 3 ) / 3 ) < ( 𝐴 ↑ 3 ) )
31 1nn0 ⊢ 1 ∈ ℕ0
32 31 a1i ⊢ ( 𝐴 ∈ ( 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 ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 3 ∈ ( ℤ≥ ‘ 1 ) )
38 4 simp2bi ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 0 < 𝐴 )
39 0re ⊢ 0 ∈ ℝ
40 ltle ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 < 𝐴 → 0 ≤ 𝐴 ) )
41 39 5 40 sylancr ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 0 < 𝐴 → 0 ≤ 𝐴 ) )
42 38 41 mpd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 0 ≤ 𝐴 )
43 4 simp3bi ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 𝐴 ≤ 1 )
44 5 32 37 42 43 leexp2rd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 3 ) ≤ ( 𝐴 ↑ 1 ) )
45 5 recnd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 𝐴 ∈ ℂ )
46 45 exp1d ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 1 ) = 𝐴 )
47 44 46 breqtrd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 ↑ 3 ) ≤ 𝐴 )
48 13 8 5 30 47 ltletrd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 ↑ 3 ) / 3 ) < 𝐴 )
49 13 5 posdifd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( ( 𝐴 ↑ 3 ) / 3 ) < 𝐴 ↔ 0 < ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) ) )
50 48 49 mpbid ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 0 < ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) )
51 sin01bnd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) < ( sin ‘ 𝐴 ) ∧ ( sin ‘ 𝐴 ) < 𝐴 ) )
52 51 simpld ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) < ( sin ‘ 𝐴 ) )
53 5 13 resubcld ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) ∈ ℝ )
54 5 resincld ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( sin ‘ 𝐴 ) ∈ ℝ )
55 lttr ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) ∈ ℝ ∧ ( sin ‘ 𝐴 ) ∈ ℝ ) → ( ( 0 < ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) ∧ ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) < ( sin ‘ 𝐴 ) ) → 0 < ( sin ‘ 𝐴 ) ) )
56 39 53 54 55 mp3an2i ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 0 < ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) ∧ ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) < ( sin ‘ 𝐴 ) ) → 0 < ( sin ‘ 𝐴 ) ) )
57 50 52 56 mp2and ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → 0 < ( sin ‘ 𝐴 ) )