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