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