Metamath Proof Explorer

Theorem sincos1sgn

Description: The signs of the sine and cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008)

Ref Expression
Assertion sincos1sgn ⊢ 0 < sin ⁡ 1 ∧ 0 < cos ⁡ 1

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 0lt1 ⊢ 0 < 1
3 1le1 ⊢ 1 ≤ 1
4 0xr ⊢ 0 ∈ ℝ *
5 elioc2 ⊢ 0 ∈ ℝ * ∧ 1 ∈ ℝ → 1 ∈ 0 1 ↔ 1 ∈ ℝ ∧ 0 < 1 ∧ 1 ≤ 1
6 4 1 5 mp2an ⊢ 1 ∈ 0 1 ↔ 1 ∈ ℝ ∧ 0 < 1 ∧ 1 ≤ 1
7 1 2 3 6 mpbir3an ⊢ 1 ∈ 0 1
8 sin01gt0 ⊢ 1 ∈ 0 1 → 0 < sin ⁡ 1
9 cos01gt0 ⊢ 1 ∈ 0 1 → 0 < cos ⁡ 1
10 8 9 jca ⊢ 1 ∈ 0 1 → 0 < sin ⁡ 1 ∧ 0 < cos ⁡ 1
11 7 10 ax-mp ⊢ 0 < sin ⁡ 1 ∧ 0 < cos ⁡ 1