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