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

Proof

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