Metamath Proof Explorer

Theorem acoscosb

Description: Relationship between cosine and arccosine. (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion acoscosb ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ 0 π → arccos ⁡ A = B ↔ cos ⁡ B = A

Proof

Step Hyp Ref Expression
1 cosacos ⊢ A ∈ ℂ → cos ⁡ arccos ⁡ A = A
2 1 3ad2ant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ 0 π → cos ⁡ arccos ⁡ A = A
3 fveqeq2 ⊢ arccos ⁡ A = B → cos ⁡ arccos ⁡ A = A ↔ cos ⁡ B = A
4 2 3 syl5ibcom ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ 0 π → arccos ⁡ A = B → cos ⁡ B = A
5 acoscos ⊢ B ∈ ℂ ∧ ℜ ⁡ B ∈ 0 π → arccos ⁡ cos ⁡ B = B
6 5 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ 0 π → arccos ⁡ cos ⁡ B = B
7 fveqeq2 ⊢ cos ⁡ B = A → arccos ⁡ cos ⁡ B = B ↔ arccos ⁡ A = B
8 6 7 syl5ibcom ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ 0 π → cos ⁡ B = A → arccos ⁡ A = B
9 4 8 impbid ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ ℜ ⁡ B ∈ 0 π → arccos ⁡ A = B ↔ cos ⁡ B = A