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 ⊢A∈−π2π2∧B∈−π2π2→A<B↔sin⁡A<sin⁡B

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 ⊢A∈−π2π2→A∈ℝ
6 4 sseli ⊢B∈−π2π2→B∈ℝ
7 ltsub2 ⊢A∈ℝ∧B∈ℝ∧π2∈ℝ→A<B↔π2−B<π2−A
8 2 7 mp3an3 ⊢A∈ℝ∧B∈ℝ→A<B↔π2−B<π2−A
9 5 6 8 syl2an ⊢A∈−π2π2∧B∈−π2π2→A<B↔π2−B<π2−A
10 oveq2 ⊢x=B→π2−x=π2−B
11 10 eleq1d ⊢x=B→π2−x∈0π↔π2−B∈0π
12 4 sseli ⊢x∈−π2π2→x∈ℝ
13 resubcl ⊢π2∈ℝ∧x∈ℝ→π2−x∈ℝ
14 2 12 13 sylancr ⊢x∈−π2π2→π2−x∈ℝ
15 1 2 elicc2i ⊢x∈−π2π2↔x∈ℝ∧−π2≤x∧x≤π2
16 15 simp3bi ⊢x∈−π2π2→x≤π2
17 subge0 ⊢π2∈ℝ∧x∈ℝ→0≤π2−x↔x≤π2
18 2 12 17 sylancr ⊢x∈−π2π2→0≤π2−x↔x≤π2
19 16 18 mpbird ⊢x∈−π2π2→0≤π2−x
20 15 simp2bi ⊢x∈−π2π2→−π2≤x
21 lesub2 ⊢−π2∈ℝ∧x∈ℝ∧π2∈ℝ→−π2≤x↔π2−x≤π2−−π2
22 1 2 21 mp3an13 ⊢x∈ℝ→−π2≤x↔π2−x≤π2−−π2
23 12 22 syl ⊢x∈−π2π2→−π2≤x↔π2−x≤π2−−π2
24 20 23 mpbid ⊢x∈−π2π2→π2−x≤π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 ⊢x∈−π2π2→π2−x≤π
30 0re ⊢0∈ℝ
31 pire ⊢π∈ℝ
32 30 31 elicc2i ⊢π2−x∈0π↔π2−x∈ℝ∧0≤π2−x∧π2−x≤π
33 14 19 29 32 syl3anbrc ⊢x∈−π2π2→π2−x∈0π
34 11 33 vtoclga ⊢B∈−π2π2→π2−B∈0π
35 oveq2 ⊢x=A→π2−x=π2−A
36 35 eleq1d ⊢x=A→π2−x∈0π↔π2−A∈0π
37 36 33 vtoclga ⊢A∈−π2π2→π2−A∈0π
38 cosord ⊢π2−B∈0π∧π2−A∈0π→π2−B<π2−A↔cos⁡π2−A<cos⁡π2−B
39 34 37 38 syl2anr ⊢A∈−π2π2∧B∈−π2π2→π2−B<π2−A↔cos⁡π2−A<cos⁡π2−B
40 5 recnd ⊢A∈−π2π2→A∈ℂ
41 coshalfpim ⊢A∈ℂ→cos⁡π2−A=sin⁡A
42 40 41 syl ⊢A∈−π2π2→cos⁡π2−A=sin⁡A
43 6 recnd ⊢B∈−π2π2→B∈ℂ
44 coshalfpim ⊢B∈ℂ→cos⁡π2−B=sin⁡B
45 43 44 syl ⊢B∈−π2π2→cos⁡π2−B=sin⁡B
46 42 45 breqan12d ⊢A∈−π2π2∧B∈−π2π2→cos⁡π2−A<cos⁡π2−B↔sin⁡A<sin⁡B
47 9 39 46 3bitrd ⊢A∈−π2π2∧B∈−π2π2→A<B↔sin⁡A<sin⁡B