Metamath Proof Explorer


Theorem acoscosb

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

Ref Expression
Assertion acoscosb ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( 0 (,) π ) ) → ( ( arccos ‘ 𝐴 ) = 𝐵 ↔ ( cos ‘ 𝐵 ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 cosacos ( 𝐴 ∈ ℂ → ( cos ‘ ( arccos ‘ 𝐴 ) ) = 𝐴 )
2 1 3ad2ant1 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( 0 (,) π ) ) → ( cos ‘ ( arccos ‘ 𝐴 ) ) = 𝐴 )
3 fveqeq2 ( ( arccos ‘ 𝐴 ) = 𝐵 → ( ( cos ‘ ( arccos ‘ 𝐴 ) ) = 𝐴 ↔ ( cos ‘ 𝐵 ) = 𝐴 ) )
4 2 3 syl5ibcom ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( 0 (,) π ) ) → ( ( arccos ‘ 𝐴 ) = 𝐵 → ( cos ‘ 𝐵 ) = 𝐴 ) )
5 acoscos ( ( 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( 0 (,) π ) ) → ( arccos ‘ ( cos ‘ 𝐵 ) ) = 𝐵 )
6 5 3adant1 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( 0 (,) π ) ) → ( arccos ‘ ( cos ‘ 𝐵 ) ) = 𝐵 )
7 fveqeq2 ( ( cos ‘ 𝐵 ) = 𝐴 → ( ( arccos ‘ ( cos ‘ 𝐵 ) ) = 𝐵 ↔ ( arccos ‘ 𝐴 ) = 𝐵 ) )
8 6 7 syl5ibcom ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( 0 (,) π ) ) → ( ( cos ‘ 𝐵 ) = 𝐴 → ( arccos ‘ 𝐴 ) = 𝐵 ) )
9 4 8 impbid ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ( 0 (,) π ) ) → ( ( arccos ‘ 𝐴 ) = 𝐵 ↔ ( cos ‘ 𝐵 ) = 𝐴 ) )