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

Metamath Proof Explorer

Theorem sinltx

Description: The sine of a positive real number is less than its argument. (Contributed by Mario Carneiro, 29-Jul-2014)

Ref Expression
Assertion sinltx ( 𝐴 ∈ ℝ+ → ( sin ‘ 𝐴 ) < 𝐴 )

Proof

Step Hyp Ref Expression
1 rpre ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
2 1 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ )
3 2 resincld ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 < 𝐴 ) → ( sin ‘ 𝐴 ) ∈ ℝ )
4 1red ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 < 𝐴 ) → 1 ∈ ℝ )
5 sinbnd ⊢ ( 𝐴 ∈ ℝ → ( - 1 ≤ ( sin ‘ 𝐴 ) ∧ ( sin ‘ 𝐴 ) ≤ 1 ) )
6 5 simprd ⊢ ( 𝐴 ∈ ℝ → ( sin ‘ 𝐴 ) ≤ 1 )
7 1 6 syl ⊢ ( 𝐴 ∈ ℝ+ → ( sin ‘ 𝐴 ) ≤ 1 )
8 7 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 < 𝐴 ) → ( sin ‘ 𝐴 ) ≤ 1 )
9 simpr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 < 𝐴 ) → 1 < 𝐴 )
10 3 4 2 8 9 lelttrd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 1 < 𝐴 ) → ( sin ‘ 𝐴 ) < 𝐴 )
11 df-3an ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1 ) ↔ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ 𝐴 ≤ 1 ) )
12 0xr ⊢ 0 ∈ ℝ*
13 1re ⊢ 1 ∈ ℝ
14 elioc2 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ ) → ( 𝐴 ∈ ( 0 (,] 1 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1 ) ) )
15 12 13 14 mp2an ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1 ) )
16 elrp ⊢ ( 𝐴 ∈ ℝ+ ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
17 16 anbi1i ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) ↔ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ 𝐴 ≤ 1 ) )
18 11 15 17 3bitr4i ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) ↔ ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) )
19 sin01bnd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 3 ) ) < ( sin ‘ 𝐴 ) ∧ ( sin ‘ 𝐴 ) < 𝐴 ) )
20 19 simprd ⊢ ( 𝐴 ∈ ( 0 (,] 1 ) → ( sin ‘ 𝐴 ) < 𝐴 )
21 18 20 sylbir ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ≤ 1 ) → ( sin ‘ 𝐴 ) < 𝐴 )
22 1red ⊢ ( 𝐴 ∈ ℝ+ → 1 ∈ ℝ )
23 10 21 22 1 ltlecasei ⊢ ( 𝐴 ∈ ℝ+ → ( sin ‘ 𝐴 ) < 𝐴 )