Theorem acoscosb

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

	Ref	Expression
Assertion	acoscosb	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge \Re \left(B\right)\in \left(0,\mathrm{\pi }\right)\right)\to \left(arccos\left(A\right)=B\leftrightarrow \cos B=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		cosacos	$$⊢A\in ℂ\to \cos arccos\left(A\right)=A$$
2	1	3ad2ant1	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge \Re \left(B\right)\in \left(0,\mathrm{\pi }\right)\right)\to \cos arccos\left(A\right)=A$$
3		fveqeq2	$$⊢arccos\left(A\right)=B\to \left(\cos arccos\left(A\right)=A\leftrightarrow \cos B=A\right)$$
4	2 3	syl5ibcom	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge \Re \left(B\right)\in \left(0,\mathrm{\pi }\right)\right)\to \left(arccos\left(A\right)=B\to \cos B=A\right)$$
5		acoscos	$$⊢\left(B\in ℂ\wedge \Re \left(B\right)\in \left(0,\mathrm{\pi }\right)\right)\to arccos\left(\cos B\right)=B$$
6	5	3adant1	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge \Re \left(B\right)\in \left(0,\mathrm{\pi }\right)\right)\to arccos\left(\cos B\right)=B$$
7		fveqeq2	$$⊢\cos B=A\to \left(arccos\left(\cos B\right)=B\leftrightarrow arccos\left(A\right)=B\right)$$
8	6 7	syl5ibcom	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge \Re \left(B\right)\in \left(0,\mathrm{\pi }\right)\right)\to \left(\cos B=A\to arccos\left(A\right)=B\right)$$
9	4 8	impbid	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge \Re \left(B\right)\in \left(0,\mathrm{\pi }\right)\right)\to \left(arccos\left(A\right)=B\leftrightarrow \cos B=A\right)$$