Metamath Proof Explorer


Theorem cosord

Description: Cosine is decreasing over the closed interval from 0 to _pi . (Contributed by Paul Chapman, 16-Mar-2008) (Proof shortened by Mario Carneiro, 10-May-2014)

Ref Expression
Assertion cosord ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) → ( 𝐴 < 𝐵 ↔ ( cos ‘ 𝐵 ) < ( cos ‘ 𝐴 ) ) )

Proof

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