Step |
Hyp |
Ref |
Expression |
1 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ( 0 [,] π ) ) |
2 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ( 0 [,] π ) ) |
3 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) ∧ 𝐴 < 𝐵 ) → 𝐴 < 𝐵 ) |
4 |
1 2 3
|
cosordlem |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) ∧ 𝐴 < 𝐵 ) → ( cos ‘ 𝐵 ) < ( cos ‘ 𝐴 ) ) |
5 |
4
|
ex |
⊢ ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) → ( 𝐴 < 𝐵 → ( cos ‘ 𝐵 ) < ( cos ‘ 𝐴 ) ) ) |
6 |
|
fveq2 |
⊢ ( 𝐴 = 𝐵 → ( cos ‘ 𝐴 ) = ( cos ‘ 𝐵 ) ) |
7 |
6
|
eqcomd |
⊢ ( 𝐴 = 𝐵 → ( cos ‘ 𝐵 ) = ( cos ‘ 𝐴 ) ) |
8 |
7
|
a1i |
⊢ ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) → ( 𝐴 = 𝐵 → ( cos ‘ 𝐵 ) = ( cos ‘ 𝐴 ) ) ) |
9 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) ∧ 𝐵 < 𝐴 ) → 𝐵 ∈ ( 0 [,] π ) ) |
10 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) ∧ 𝐵 < 𝐴 ) → 𝐴 ∈ ( 0 [,] π ) ) |
11 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) ∧ 𝐵 < 𝐴 ) → 𝐵 < 𝐴 ) |
12 |
9 10 11
|
cosordlem |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) ∧ 𝐵 < 𝐴 ) → ( cos ‘ 𝐴 ) < ( cos ‘ 𝐵 ) ) |
13 |
12
|
ex |
⊢ ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) → ( 𝐵 < 𝐴 → ( cos ‘ 𝐴 ) < ( cos ‘ 𝐵 ) ) ) |
14 |
8 13
|
orim12d |
⊢ ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) → ( ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) → ( ( cos ‘ 𝐵 ) = ( cos ‘ 𝐴 ) ∨ ( cos ‘ 𝐴 ) < ( cos ‘ 𝐵 ) ) ) ) |
15 |
14
|
con3d |
⊢ ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) → ( ¬ ( ( cos ‘ 𝐵 ) = ( cos ‘ 𝐴 ) ∨ ( cos ‘ 𝐴 ) < ( cos ‘ 𝐵 ) ) → ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ) ) |
16 |
|
0re |
⊢ 0 ∈ ℝ |
17 |
|
pire |
⊢ π ∈ ℝ |
18 |
16 17
|
elicc2i |
⊢ ( 𝐴 ∈ ( 0 [,] π ) ↔ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ π ) ) |
19 |
18
|
simp1bi |
⊢ ( 𝐴 ∈ ( 0 [,] π ) → 𝐴 ∈ ℝ ) |
20 |
16 17
|
elicc2i |
⊢ ( 𝐵 ∈ ( 0 [,] π ) ↔ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ∧ 𝐵 ≤ π ) ) |
21 |
20
|
simp1bi |
⊢ ( 𝐵 ∈ ( 0 [,] π ) → 𝐵 ∈ ℝ ) |
22 |
|
recoscl |
⊢ ( 𝐵 ∈ ℝ → ( cos ‘ 𝐵 ) ∈ ℝ ) |
23 |
|
recoscl |
⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ∈ ℝ ) |
24 |
|
axlttri |
⊢ ( ( ( cos ‘ 𝐵 ) ∈ ℝ ∧ ( cos ‘ 𝐴 ) ∈ ℝ ) → ( ( cos ‘ 𝐵 ) < ( cos ‘ 𝐴 ) ↔ ¬ ( ( cos ‘ 𝐵 ) = ( cos ‘ 𝐴 ) ∨ ( cos ‘ 𝐴 ) < ( cos ‘ 𝐵 ) ) ) ) |
25 |
22 23 24
|
syl2anr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( cos ‘ 𝐵 ) < ( cos ‘ 𝐴 ) ↔ ¬ ( ( cos ‘ 𝐵 ) = ( cos ‘ 𝐴 ) ∨ ( cos ‘ 𝐴 ) < ( cos ‘ 𝐵 ) ) ) ) |
26 |
19 21 25
|
syl2an |
⊢ ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) → ( ( cos ‘ 𝐵 ) < ( cos ‘ 𝐴 ) ↔ ¬ ( ( cos ‘ 𝐵 ) = ( cos ‘ 𝐴 ) ∨ ( cos ‘ 𝐴 ) < ( cos ‘ 𝐵 ) ) ) ) |
27 |
|
axlttri |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ) ) |
28 |
19 21 27
|
syl2an |
⊢ ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) → ( 𝐴 < 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ) ) |
29 |
15 26 28
|
3imtr4d |
⊢ ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) → ( ( cos ‘ 𝐵 ) < ( cos ‘ 𝐴 ) → 𝐴 < 𝐵 ) ) |
30 |
5 29
|
impbid |
⊢ ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) → ( 𝐴 < 𝐵 ↔ ( cos ‘ 𝐵 ) < ( cos ‘ 𝐴 ) ) ) |