Theorem atanval

Description: Value of the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015)

	Ref	Expression
Assertion	atanval	$$⊢A\in \mathrm{dom}arctan\to arctan\left(A\right)=\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢x=A\to \mathrm{i}x=\mathrm{i}A$$
2	1	oveq2d	$$⊢x=A\to 1-\mathrm{i}x=1-\mathrm{i}A$$
3	2	fveq2d	$$⊢x=A\to \log \left(1-\mathrm{i}x\right)=\log \left(1-\mathrm{i}A\right)$$
4	1	oveq2d	$$⊢x=A\to 1+\mathrm{i}x=1+\mathrm{i}A$$
5	4	fveq2d	$$⊢x=A\to \log \left(1+\mathrm{i}x\right)=\log \left(1+\mathrm{i}A\right)$$
6	3 5	oveq12d	$$⊢x=A\to \log \left(1-\mathrm{i}x\right)-\log \left(1+\mathrm{i}x\right)=\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)$$
7	6	oveq2d	$$⊢x=A\to \left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}x\right)-\log \left(1+\mathrm{i}x\right)\right)=\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)$$
8		df-atan	$$⊢arctan=\left(x\in \left(ℂ\setminus \left\{-\mathrm{i},\mathrm{i}\right\}\right)⟼\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}x\right)-\log \left(1+\mathrm{i}x\right)\right)\right)$$
9		ovex	$$⊢\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)\in \mathrm{V}$$
10	7 8 9	fvmpt	$$⊢A\in \left(ℂ\setminus \left\{-\mathrm{i},\mathrm{i}\right\}\right)\to arctan\left(A\right)=\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)$$
11		atanf	$$⊢arctan:ℂ\setminus \left\{-\mathrm{i},\mathrm{i}\right\}⟶ℂ$$
12	11	fdmi	$$⊢\mathrm{dom}arctan=ℂ\setminus \left\{-\mathrm{i},\mathrm{i}\right\}$$
13	10 12	eleq2s	$$⊢A\in \mathrm{dom}arctan\to arctan\left(A\right)=\left(\frac{\mathrm{i}}{2}\right)\left(\log \left(1-\mathrm{i}A\right)-\log \left(1+\mathrm{i}A\right)\right)$$