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