Metamath Proof Explorer

Theorem sinq12gt0

Description: The sine of a number strictly between 0 and _pi is positive. (Contributed by Paul Chapman, 15-Mar-2008)

Ref Expression
Assertion sinq12gt0 ( 𝐴 ∈ ( 0 (,) π ) → 0 < ( sin ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 0xr ⊢ 0 ∈ ℝ*
2 pire ⊢ π ∈ ℝ
3 2 rexri ⊢ π ∈ ℝ*
4 elioo2 ⊢ ( ( 0 ∈ ℝ* ∧ π ∈ ℝ* ) → ( 𝐴 ∈ ( 0 (,) π ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) ) )
5 1 3 4 mp2an ⊢ ( 𝐴 ∈ ( 0 (,) π ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) )
6 rehalfcl ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 / 2 ) ∈ ℝ )
7 6 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → ( 𝐴 / 2 ) ∈ ℝ )
8 halfpos2 ⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 ↔ 0 < ( 𝐴 / 2 ) ) )
9 8 biimpa ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 < ( 𝐴 / 2 ) )
10 9 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → 0 < ( 𝐴 / 2 ) )
11 2re ⊢ 2 ∈ ℝ
12 2pos ⊢ 0 < 2
13 11 12 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
14 ltdiv1 ⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 𝐴 < π ↔ ( 𝐴 / 2 ) < ( π / 2 ) ) )
15 2 13 14 mp3an23 ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < π ↔ ( 𝐴 / 2 ) < ( π / 2 ) ) )
16 15 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 𝐴 < π ↔ ( 𝐴 / 2 ) < ( π / 2 ) ) )
17 16 biimp3a ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → ( 𝐴 / 2 ) < ( π / 2 ) )
18 sincosq1lem ⊢ ( ( ( 𝐴 / 2 ) ∈ ℝ ∧ 0 < ( 𝐴 / 2 ) ∧ ( 𝐴 / 2 ) < ( π / 2 ) ) → 0 < ( sin ‘ ( 𝐴 / 2 ) ) )
19 7 10 17 18 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → 0 < ( sin ‘ ( 𝐴 / 2 ) ) )
20 resubcl ⊢ ( ( π ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( π − 𝐴 ) ∈ ℝ )
21 2 20 mpan ⊢ ( 𝐴 ∈ ℝ → ( π − 𝐴 ) ∈ ℝ )
22 rehalfcl ⊢ ( ( π − 𝐴 ) ∈ ℝ → ( ( π − 𝐴 ) / 2 ) ∈ ℝ )
23 21 22 syl ⊢ ( 𝐴 ∈ ℝ → ( ( π − 𝐴 ) / 2 ) ∈ ℝ )
24 23 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → ( ( π − 𝐴 ) / 2 ) ∈ ℝ )
25 posdif ⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ ) → ( 𝐴 < π ↔ 0 < ( π − 𝐴 ) ) )
26 2 25 mpan2 ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < π ↔ 0 < ( π − 𝐴 ) ) )
27 halfpos2 ⊢ ( ( π − 𝐴 ) ∈ ℝ → ( 0 < ( π − 𝐴 ) ↔ 0 < ( ( π − 𝐴 ) / 2 ) ) )
28 21 27 syl ⊢ ( 𝐴 ∈ ℝ → ( 0 < ( π − 𝐴 ) ↔ 0 < ( ( π − 𝐴 ) / 2 ) ) )
29 26 28 bitrd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < π ↔ 0 < ( ( π − 𝐴 ) / 2 ) ) )
30 29 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 𝐴 < π ↔ 0 < ( ( π − 𝐴 ) / 2 ) ) )
31 30 biimp3a ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → 0 < ( ( π − 𝐴 ) / 2 ) )
32 ltsubpos ⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ ) → ( 0 < 𝐴 ↔ ( π − 𝐴 ) < π ) )
33 2 32 mpan2 ⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 ↔ ( π − 𝐴 ) < π ) )
34 ltdiv1 ⊢ ( ( ( π − 𝐴 ) ∈ ℝ ∧ π ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( π − 𝐴 ) < π ↔ ( ( π − 𝐴 ) / 2 ) < ( π / 2 ) ) )
35 2 13 34 mp3an23 ⊢ ( ( π − 𝐴 ) ∈ ℝ → ( ( π − 𝐴 ) < π ↔ ( ( π − 𝐴 ) / 2 ) < ( π / 2 ) ) )
36 21 35 syl ⊢ ( 𝐴 ∈ ℝ → ( ( π − 𝐴 ) < π ↔ ( ( π − 𝐴 ) / 2 ) < ( π / 2 ) ) )
37 33 36 bitrd ⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 ↔ ( ( π − 𝐴 ) / 2 ) < ( π / 2 ) ) )
38 37 biimpa ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( ( π − 𝐴 ) / 2 ) < ( π / 2 ) )
39 38 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → ( ( π − 𝐴 ) / 2 ) < ( π / 2 ) )
40 sincosq1lem ⊢ ( ( ( ( π − 𝐴 ) / 2 ) ∈ ℝ ∧ 0 < ( ( π − 𝐴 ) / 2 ) ∧ ( ( π − 𝐴 ) / 2 ) < ( π / 2 ) ) → 0 < ( sin ‘ ( ( π − 𝐴 ) / 2 ) ) )
41 24 31 39 40 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → 0 < ( sin ‘ ( ( π − 𝐴 ) / 2 ) ) )
42 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
43 picn ⊢ π ∈ ℂ
44 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
45 divsubdir ⊢ ( ( π ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( π − 𝐴 ) / 2 ) = ( ( π / 2 ) − ( 𝐴 / 2 ) ) )
46 43 44 45 mp3an13 ⊢ ( 𝐴 ∈ ℂ → ( ( π − 𝐴 ) / 2 ) = ( ( π / 2 ) − ( 𝐴 / 2 ) ) )
47 42 46 syl ⊢ ( 𝐴 ∈ ℝ → ( ( π − 𝐴 ) / 2 ) = ( ( π / 2 ) − ( 𝐴 / 2 ) ) )
48 47 fveq2d ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( ( π − 𝐴 ) / 2 ) ) = ( sin ‘ ( ( π / 2 ) − ( 𝐴 / 2 ) ) ) )
49 6 recnd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 / 2 ) ∈ ℂ )
50 sinhalfpim ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( sin ‘ ( ( π / 2 ) − ( 𝐴 / 2 ) ) ) = ( cos ‘ ( 𝐴 / 2 ) ) )
51 49 50 syl ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( ( π / 2 ) − ( 𝐴 / 2 ) ) ) = ( cos ‘ ( 𝐴 / 2 ) ) )
52 48 51 eqtrd ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( ( π − 𝐴 ) / 2 ) ) = ( cos ‘ ( 𝐴 / 2 ) ) )
53 52 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → ( sin ‘ ( ( π − 𝐴 ) / 2 ) ) = ( cos ‘ ( 𝐴 / 2 ) ) )
54 41 53 breqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → 0 < ( cos ‘ ( 𝐴 / 2 ) ) )
55 resincl ⊢ ( ( 𝐴 / 2 ) ∈ ℝ → ( sin ‘ ( 𝐴 / 2 ) ) ∈ ℝ )
56 recoscl ⊢ ( ( 𝐴 / 2 ) ∈ ℝ → ( cos ‘ ( 𝐴 / 2 ) ) ∈ ℝ )
57 55 56 jca ⊢ ( ( 𝐴 / 2 ) ∈ ℝ → ( ( sin ‘ ( 𝐴 / 2 ) ) ∈ ℝ ∧ ( cos ‘ ( 𝐴 / 2 ) ) ∈ ℝ ) )
58 axmulgt0 ⊢ ( ( ( sin ‘ ( 𝐴 / 2 ) ) ∈ ℝ ∧ ( cos ‘ ( 𝐴 / 2 ) ) ∈ ℝ ) → ( ( 0 < ( sin ‘ ( 𝐴 / 2 ) ) ∧ 0 < ( cos ‘ ( 𝐴 / 2 ) ) ) → 0 < ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) )
59 6 57 58 3syl ⊢ ( 𝐴 ∈ ℝ → ( ( 0 < ( sin ‘ ( 𝐴 / 2 ) ) ∧ 0 < ( cos ‘ ( 𝐴 / 2 ) ) ) → 0 < ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) )
60 remulcl ⊢ ( ( ( sin ‘ ( 𝐴 / 2 ) ) ∈ ℝ ∧ ( cos ‘ ( 𝐴 / 2 ) ) ∈ ℝ ) → ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ∈ ℝ )
61 6 57 60 3syl ⊢ ( 𝐴 ∈ ℝ → ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ∈ ℝ )
62 axmulgt0 ⊢ ( ( 2 ∈ ℝ ∧ ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ∈ ℝ ) → ( ( 0 < 2 ∧ 0 < ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) → 0 < ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) )
63 11 61 62 sylancr ⊢ ( 𝐴 ∈ ℝ → ( ( 0 < 2 ∧ 0 < ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) → 0 < ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) )
64 12 63 mpani ⊢ ( 𝐴 ∈ ℝ → ( 0 < ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) → 0 < ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) )
65 59 64 syld ⊢ ( 𝐴 ∈ ℝ → ( ( 0 < ( sin ‘ ( 𝐴 / 2 ) ) ∧ 0 < ( cos ‘ ( 𝐴 / 2 ) ) ) → 0 < ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) )
66 65 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → ( ( 0 < ( sin ‘ ( 𝐴 / 2 ) ) ∧ 0 < ( cos ‘ ( 𝐴 / 2 ) ) ) → 0 < ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) )
67 19 54 66 mp2and ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → 0 < ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) )
68 2cn ⊢ 2 ∈ ℂ
69 2ne0 ⊢ 2 ≠ 0
70 divcan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 )
71 68 69 70 mp3an23 ⊢ ( 𝐴 ∈ ℂ → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 )
72 42 71 syl ⊢ ( 𝐴 ∈ ℝ → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 )
73 72 fveq2d ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( sin ‘ 𝐴 ) )
74 sin2t ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( sin ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) )
75 49 74 syl ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) )
76 73 75 eqtr3d ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ 𝐴 ) = ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) )
77 76 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → ( sin ‘ 𝐴 ) = ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) )
78 67 77 breqtrrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → 0 < ( sin ‘ 𝐴 ) )
79 5 78 sylbi ⊢ ( 𝐴 ∈ ( 0 (,) π ) → 0 < ( sin ‘ 𝐴 ) )