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