Metamath Proof Explorer

Theorem cos11

Description: Cosine is one-to-one 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 cos11 ⊢A∈0π∧B∈0π→A=B↔cos⁡A=cos⁡B

Proof

Step Hyp Ref Expression
1 ancom ⊢¬A<B∧¬B<A↔¬B<A∧¬A<B
2 cosord ⊢B∈0π∧A∈0π→B<A↔cos⁡A<cos⁡B
3 2 ancoms ⊢A∈0π∧B∈0π→B<A↔cos⁡A<cos⁡B
4 3 notbid ⊢A∈0π∧B∈0π→¬B<A↔¬cos⁡A<cos⁡B
5 cosord ⊢A∈0π∧B∈0π→A<B↔cos⁡B<cos⁡A
6 5 notbid ⊢A∈0π∧B∈0π→¬A<B↔¬cos⁡B<cos⁡A
7 4 6 anbi12d ⊢A∈0π∧B∈0π→¬B<A∧¬A<B↔¬cos⁡A<cos⁡B∧¬cos⁡B<cos⁡A
8 1 7 bitrid ⊢A∈0π∧B∈0π→¬A<B∧¬B<A↔¬cos⁡A<cos⁡B∧¬cos⁡B<cos⁡A
9 0re ⊢0∈ℝ
10 pire ⊢π∈ℝ
11 9 10 elicc2i ⊢A∈0π↔A∈ℝ∧0≤A∧A≤π
12 11 simp1bi ⊢A∈0π→A∈ℝ
13 9 10 elicc2i ⊢B∈0π↔B∈ℝ∧0≤B∧B≤π
14 13 simp1bi ⊢B∈0π→B∈ℝ
15 lttri3 ⊢A∈ℝ∧B∈ℝ→A=B↔¬A<B∧¬B<A
16 12 14 15 syl2an ⊢A∈0π∧B∈0π→A=B↔¬A<B∧¬B<A
17 recoscl ⊢A∈ℝ→cos⁡A∈ℝ
18 recoscl ⊢B∈ℝ→cos⁡B∈ℝ
19 lttri3 ⊢cos⁡A∈ℝ∧cos⁡B∈ℝ→cos⁡A=cos⁡B↔¬cos⁡A<cos⁡B∧¬cos⁡B<cos⁡A
20 17 18 19 syl2an ⊢A∈ℝ∧B∈ℝ→cos⁡A=cos⁡B↔¬cos⁡A<cos⁡B∧¬cos⁡B<cos⁡A
21 12 14 20 syl2an ⊢A∈0π∧B∈0π→cos⁡A=cos⁡B↔¬cos⁡A<cos⁡B∧¬cos⁡B<cos⁡A
22 8 16 21 3bitr4d ⊢A∈0π∧B∈0π→A=B↔cos⁡A=cos⁡B