This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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