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 ‘ 𝐴 ) )