Metamath Proof Explorer


Theorem sinord

Description: Sine is increasing over the closed interval from -u (pi / 2 ) to ( pi / 2 ) . (Contributed by Mario Carneiro, 29-Jul-2014)

Ref Expression
Assertion sinord ( ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ∧ 𝐵 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ) → ( 𝐴 < 𝐵 ↔ ( sin ‘ 𝐴 ) < ( sin ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 neghalfpire - ( π / 2 ) ∈ ℝ
2 halfpire ( π / 2 ) ∈ ℝ
3 iccssre ( ( - ( π / 2 ) ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( - ( π / 2 ) [,] ( π / 2 ) ) ⊆ ℝ )
4 1 2 3 mp2an ( - ( π / 2 ) [,] ( π / 2 ) ) ⊆ ℝ
5 4 sseli ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 𝐴 ∈ ℝ )
6 4 sseli ( 𝐵 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 𝐵 ∈ ℝ )
7 ltsub2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( ( π / 2 ) − 𝐵 ) < ( ( π / 2 ) − 𝐴 ) ) )
8 2 7 mp3an3 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( ( π / 2 ) − 𝐵 ) < ( ( π / 2 ) − 𝐴 ) ) )
9 5 6 8 syl2an ( ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ∧ 𝐵 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ) → ( 𝐴 < 𝐵 ↔ ( ( π / 2 ) − 𝐵 ) < ( ( π / 2 ) − 𝐴 ) ) )
10 oveq2 ( 𝑥 = 𝐵 → ( ( π / 2 ) − 𝑥 ) = ( ( π / 2 ) − 𝐵 ) )
11 10 eleq1d ( 𝑥 = 𝐵 → ( ( ( π / 2 ) − 𝑥 ) ∈ ( 0 [,] π ) ↔ ( ( π / 2 ) − 𝐵 ) ∈ ( 0 [,] π ) ) )
12 4 sseli ( 𝑥 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 𝑥 ∈ ℝ )
13 resubcl ( ( ( π / 2 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( π / 2 ) − 𝑥 ) ∈ ℝ )
14 2 12 13 sylancr ( 𝑥 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( ( π / 2 ) − 𝑥 ) ∈ ℝ )
15 1 2 elicc2i ( 𝑥 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ↔ ( 𝑥 ∈ ℝ ∧ - ( π / 2 ) ≤ 𝑥𝑥 ≤ ( π / 2 ) ) )
16 15 simp3bi ( 𝑥 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 𝑥 ≤ ( π / 2 ) )
17 subge0 ( ( ( π / 2 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 0 ≤ ( ( π / 2 ) − 𝑥 ) ↔ 𝑥 ≤ ( π / 2 ) ) )
18 2 12 17 sylancr ( 𝑥 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( 0 ≤ ( ( π / 2 ) − 𝑥 ) ↔ 𝑥 ≤ ( π / 2 ) ) )
19 16 18 mpbird ( 𝑥 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 0 ≤ ( ( π / 2 ) − 𝑥 ) )
20 15 simp2bi ( 𝑥 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → - ( π / 2 ) ≤ 𝑥 )
21 lesub2 ( ( - ( π / 2 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( - ( π / 2 ) ≤ 𝑥 ↔ ( ( π / 2 ) − 𝑥 ) ≤ ( ( π / 2 ) − - ( π / 2 ) ) ) )
22 1 2 21 mp3an13 ( 𝑥 ∈ ℝ → ( - ( π / 2 ) ≤ 𝑥 ↔ ( ( π / 2 ) − 𝑥 ) ≤ ( ( π / 2 ) − - ( π / 2 ) ) ) )
23 12 22 syl ( 𝑥 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( - ( π / 2 ) ≤ 𝑥 ↔ ( ( π / 2 ) − 𝑥 ) ≤ ( ( π / 2 ) − - ( π / 2 ) ) ) )
24 20 23 mpbid ( 𝑥 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( ( π / 2 ) − 𝑥 ) ≤ ( ( π / 2 ) − - ( π / 2 ) ) )
25 2 recni ( π / 2 ) ∈ ℂ
26 25 25 subnegi ( ( π / 2 ) − - ( π / 2 ) ) = ( ( π / 2 ) + ( π / 2 ) )
27 pidiv2halves ( ( π / 2 ) + ( π / 2 ) ) = π
28 26 27 eqtri ( ( π / 2 ) − - ( π / 2 ) ) = π
29 24 28 breqtrdi ( 𝑥 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( ( π / 2 ) − 𝑥 ) ≤ π )
30 0re 0 ∈ ℝ
31 pire π ∈ ℝ
32 30 31 elicc2i ( ( ( π / 2 ) − 𝑥 ) ∈ ( 0 [,] π ) ↔ ( ( ( π / 2 ) − 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( π / 2 ) − 𝑥 ) ∧ ( ( π / 2 ) − 𝑥 ) ≤ π ) )
33 14 19 29 32 syl3anbrc ( 𝑥 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( ( π / 2 ) − 𝑥 ) ∈ ( 0 [,] π ) )
34 11 33 vtoclga ( 𝐵 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( ( π / 2 ) − 𝐵 ) ∈ ( 0 [,] π ) )
35 oveq2 ( 𝑥 = 𝐴 → ( ( π / 2 ) − 𝑥 ) = ( ( π / 2 ) − 𝐴 ) )
36 35 eleq1d ( 𝑥 = 𝐴 → ( ( ( π / 2 ) − 𝑥 ) ∈ ( 0 [,] π ) ↔ ( ( π / 2 ) − 𝐴 ) ∈ ( 0 [,] π ) ) )
37 36 33 vtoclga ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( ( π / 2 ) − 𝐴 ) ∈ ( 0 [,] π ) )
38 cosord ( ( ( ( π / 2 ) − 𝐵 ) ∈ ( 0 [,] π ) ∧ ( ( π / 2 ) − 𝐴 ) ∈ ( 0 [,] π ) ) → ( ( ( π / 2 ) − 𝐵 ) < ( ( π / 2 ) − 𝐴 ) ↔ ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) < ( cos ‘ ( ( π / 2 ) − 𝐵 ) ) ) )
39 34 37 38 syl2anr ( ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ∧ 𝐵 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ) → ( ( ( π / 2 ) − 𝐵 ) < ( ( π / 2 ) − 𝐴 ) ↔ ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) < ( cos ‘ ( ( π / 2 ) − 𝐵 ) ) ) )
40 5 recnd ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 𝐴 ∈ ℂ )
41 coshalfpim ( 𝐴 ∈ ℂ → ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) = ( sin ‘ 𝐴 ) )
42 40 41 syl ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) = ( sin ‘ 𝐴 ) )
43 6 recnd ( 𝐵 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 𝐵 ∈ ℂ )
44 coshalfpim ( 𝐵 ∈ ℂ → ( cos ‘ ( ( π / 2 ) − 𝐵 ) ) = ( sin ‘ 𝐵 ) )
45 43 44 syl ( 𝐵 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( cos ‘ ( ( π / 2 ) − 𝐵 ) ) = ( sin ‘ 𝐵 ) )
46 42 45 breqan12d ( ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ∧ 𝐵 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ) → ( ( cos ‘ ( ( π / 2 ) − 𝐴 ) ) < ( cos ‘ ( ( π / 2 ) − 𝐵 ) ) ↔ ( sin ‘ 𝐴 ) < ( sin ‘ 𝐵 ) ) )
47 9 39 46 3bitrd ( ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ∧ 𝐵 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ) → ( 𝐴 < 𝐵 ↔ ( sin ‘ 𝐴 ) < ( sin ‘ 𝐵 ) ) )