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 ⊢ A ∈ 0 π ∧ B ∈ 0 π → A < B ↔ cos ⁡ B < cos ⁡ A

Proof

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