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