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