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