Metamath Proof Explorer


Theorem sincosq1lem

Description: Lemma for sincosq1sgn . (Contributed by Paul Chapman, 24-Jan-2008)

Ref Expression
Assertion sincosq1lem ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴𝐴 < ( π / 2 ) ) → 0 < ( sin ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 halfpire ( π / 2 ) ∈ ℝ
2 ltle ( ( 𝐴 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( 𝐴 < ( π / 2 ) → 𝐴 ≤ ( π / 2 ) ) )
3 1 2 mpan2 ( 𝐴 ∈ ℝ → ( 𝐴 < ( π / 2 ) → 𝐴 ≤ ( π / 2 ) ) )
4 pire π ∈ ℝ
5 4re 4 ∈ ℝ
6 pigt2lt4 ( 2 < π ∧ π < 4 )
7 6 simpri π < 4
8 4 5 7 ltleii π ≤ 4
9 2re 2 ∈ ℝ
10 2pos 0 < 2
11 9 10 pm3.2i ( 2 ∈ ℝ ∧ 0 < 2 )
12 ledivmul ( ( π ∈ ℝ ∧ 2 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( π / 2 ) ≤ 2 ↔ π ≤ ( 2 · 2 ) ) )
13 4 9 11 12 mp3an ( ( π / 2 ) ≤ 2 ↔ π ≤ ( 2 · 2 ) )
14 2t2e4 ( 2 · 2 ) = 4
15 14 breq2i ( π ≤ ( 2 · 2 ) ↔ π ≤ 4 )
16 13 15 bitri ( ( π / 2 ) ≤ 2 ↔ π ≤ 4 )
17 8 16 mpbir ( π / 2 ) ≤ 2
18 letr ( ( 𝐴 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( 𝐴 ≤ ( π / 2 ) ∧ ( π / 2 ) ≤ 2 ) → 𝐴 ≤ 2 ) )
19 1 9 18 mp3an23 ( 𝐴 ∈ ℝ → ( ( 𝐴 ≤ ( π / 2 ) ∧ ( π / 2 ) ≤ 2 ) → 𝐴 ≤ 2 ) )
20 17 19 mpan2i ( 𝐴 ∈ ℝ → ( 𝐴 ≤ ( π / 2 ) → 𝐴 ≤ 2 ) )
21 3 20 syld ( 𝐴 ∈ ℝ → ( 𝐴 < ( π / 2 ) → 𝐴 ≤ 2 ) )
22 21 adantr ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 𝐴 < ( π / 2 ) → 𝐴 ≤ 2 ) )
23 22 3impia ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴𝐴 < ( π / 2 ) ) → 𝐴 ≤ 2 )
24 0xr 0 ∈ ℝ*
25 elioc2 ( ( 0 ∈ ℝ* ∧ 2 ∈ ℝ ) → ( 𝐴 ∈ ( 0 (,] 2 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴𝐴 ≤ 2 ) ) )
26 24 9 25 mp2an ( 𝐴 ∈ ( 0 (,] 2 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴𝐴 ≤ 2 ) )
27 sin02gt0 ( 𝐴 ∈ ( 0 (,] 2 ) → 0 < ( sin ‘ 𝐴 ) )
28 26 27 sylbir ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴𝐴 ≤ 2 ) → 0 < ( sin ‘ 𝐴 ) )
29 23 28 syld3an3 ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴𝐴 < ( π / 2 ) ) → 0 < ( sin ‘ 𝐴 ) )