Metamath Proof Explorer

Theorem sincosq1lem

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

Ref Expression
Assertion sincosq1lem ⊢ A ∈ ℝ ∧ 0 < A ∧ A < π 2 → 0 < sin ⁡ A

Proof

Step Hyp Ref Expression
1 halfpire ⊢ π 2 ∈ ℝ
2 ltle ⊢ A ∈ ℝ ∧ π 2 ∈ ℝ → A < π 2 → A ≤ π 2
3 1 2 mpan2 ⊢ A ∈ ℝ → A < π 2 → A ≤ π 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 ⊢ A ∈ ℝ ∧ π 2 ∈ ℝ ∧ 2 ∈ ℝ → A ≤ π 2 ∧ π 2 ≤ 2 → A ≤ 2
19 1 9 18 mp3an23 ⊢ A ∈ ℝ → A ≤ π 2 ∧ π 2 ≤ 2 → A ≤ 2
20 17 19 mpan2i ⊢ A ∈ ℝ → A ≤ π 2 → A ≤ 2
21 3 20 syld ⊢ A ∈ ℝ → A < π 2 → A ≤ 2
22 21 adantr ⊢ A ∈ ℝ ∧ 0 < A → A < π 2 → A ≤ 2
23 22 3impia ⊢ A ∈ ℝ ∧ 0 < A ∧ A < π 2 → A ≤ 2
24 0xr ⊢ 0 ∈ ℝ *
25 elioc2 ⊢ 0 ∈ ℝ * ∧ 2 ∈ ℝ → A ∈ 0 2 ↔ A ∈ ℝ ∧ 0 < A ∧ A ≤ 2
26 24 9 25 mp2an ⊢ A ∈ 0 2 ↔ A ∈ ℝ ∧ 0 < A ∧ A ≤ 2
27 sin02gt0 ⊢ A ∈ 0 2 → 0 < sin ⁡ A
28 26 27 sylbir ⊢ A ∈ ℝ ∧ 0 < A ∧ A ≤ 2 → 0 < sin ⁡ A
29 23 28 syld3an3 ⊢ A ∈ ℝ ∧ 0 < A ∧ A < π 2 → 0 < sin ⁡ A