Theorem atantanb

Description: Relationship between tangent and arctangent. (Contributed by Mario Carneiro, 5-Apr-2015)

	Ref	Expression
Assertion	atantanb	$$⊢\left(A\in \mathrm{dom}arctan\wedge B\in ℂ\wedge \Re \left(B\right)\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\right)\to \left(arctan\left(A\right)=B\leftrightarrow \tan B=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		tanatan	$$⊢A\in \mathrm{dom}arctan\to \tan arctan\left(A\right)=A$$
2	1	3ad2ant1	$$⊢\left(A\in \mathrm{dom}arctan\wedge B\in ℂ\wedge \Re \left(B\right)\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\right)\to \tan arctan\left(A\right)=A$$
3		fveqeq2	$$⊢arctan\left(A\right)=B\to \left(\tan arctan\left(A\right)=A\leftrightarrow \tan B=A\right)$$
4	2 3	syl5ibcom	$$⊢\left(A\in \mathrm{dom}arctan\wedge B\in ℂ\wedge \Re \left(B\right)\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\right)\to \left(arctan\left(A\right)=B\to \tan B=A\right)$$
5		atantan	$$⊢\left(B\in ℂ\wedge \Re \left(B\right)\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\right)\to arctan\left(\tan B\right)=B$$
6	5	3adant1	$$⊢\left(A\in \mathrm{dom}arctan\wedge B\in ℂ\wedge \Re \left(B\right)\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\right)\to arctan\left(\tan B\right)=B$$
7		fveqeq2	$$⊢\tan B=A\to \left(arctan\left(\tan B\right)=B\leftrightarrow arctan\left(A\right)=B\right)$$
8	6 7	syl5ibcom	$$⊢\left(A\in \mathrm{dom}arctan\wedge B\in ℂ\wedge \Re \left(B\right)\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\right)\to \left(\tan B=A\to arctan\left(A\right)=B\right)$$
9	4 8	impbid	$$⊢\left(A\in \mathrm{dom}arctan\wedge B\in ℂ\wedge \Re \left(B\right)\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\right)\to \left(arctan\left(A\right)=B\leftrightarrow \tan B=A\right)$$