Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic trigonometry
Inverse trigonometric functions
acoscosb
Next ⟩
asinbnd
Metamath Proof Explorer
Ascii
Unicode
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