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 ( ( 𝐴 ∈ ( 0 [,] π ) ∧ 𝐵 ∈ ( 0 [,] π ) ) → ( 𝐴 = 𝐵 ↔ ( cos ‘ 𝐴 ) = ( cos ‘ 𝐵 ) ) )

Proof

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