Theorem imval2

Description: The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005)

	Ref	Expression
Assertion	imval2	$$⊢A\in ℂ\to \Im \left(A\right)=\frac{A-\bar{A}}{2\mathrm{i}}$$

Proof

Step	Hyp	Ref	Expression
1		imcl	$$⊢A\in ℂ\to \Im \left(A\right)\in ℝ$$
2	1	recnd	$$⊢A\in ℂ\to \Im \left(A\right)\in ℂ$$
3		2mulicn	$$⊢2\mathrm{i}\in ℂ$$
4		2muline0	$$⊢2\mathrm{i}\ne 0$$
5		divcan4	$$⊢\left(\Im \left(A\right)\in ℂ\wedge 2\mathrm{i}\in ℂ\wedge 2\mathrm{i}\ne 0\right)\to \frac{\Im \left(A\right)2\mathrm{i}}{2\mathrm{i}}=\Im \left(A\right)$$
6	3 4 5	mp3an23	$$⊢\Im \left(A\right)\in ℂ\to \frac{\Im \left(A\right)2\mathrm{i}}{2\mathrm{i}}=\Im \left(A\right)$$
7	2 6	syl	$$⊢A\in ℂ\to \frac{\Im \left(A\right)2\mathrm{i}}{2\mathrm{i}}=\Im \left(A\right)$$
8		recl	$$⊢A\in ℂ\to \Re \left(A\right)\in ℝ$$
9	8	recnd	$$⊢A\in ℂ\to \Re \left(A\right)\in ℂ$$
10		ax-icn	$$⊢\mathrm{i}\in ℂ$$
11		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge \Im \left(A\right)\in ℂ\right)\to \mathrm{i}\Im \left(A\right)\in ℂ$$
12	10 2 11	sylancr	$$⊢A\in ℂ\to \mathrm{i}\Im \left(A\right)\in ℂ$$
13	9 12	addcld	$$⊢A\in ℂ\to \Re \left(A\right)+\mathrm{i}\Im \left(A\right)\in ℂ$$
14	13 9 12	subsubd	$$⊢A\in ℂ\to \Re \left(A\right)+\mathrm{i}\Im \left(A\right)-\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)=\left(\Re \left(A\right)+\mathrm{i}\Im \left(A\right)\right)-\Re \left(A\right)+\mathrm{i}\Im \left(A\right)$$
15		replim	$$⊢A\in ℂ\to A=\Re \left(A\right)+\mathrm{i}\Im \left(A\right)$$
16		remim	$$⊢A\in ℂ\to \bar{A}=\Re \left(A\right)-\mathrm{i}\Im \left(A\right)$$
17	15 16	oveq12d	$$⊢A\in ℂ\to A-\bar{A}=\Re \left(A\right)+\mathrm{i}\Im \left(A\right)-\left(\Re \left(A\right)-\mathrm{i}\Im \left(A\right)\right)$$
18	12	2timesd	$$⊢A\in ℂ\to 2\mathrm{i}\Im \left(A\right)=\mathrm{i}\Im \left(A\right)+\mathrm{i}\Im \left(A\right)$$
19		mulcom	$$⊢\left(\Im \left(A\right)\in ℂ\wedge 2\mathrm{i}\in ℂ\right)\to \Im \left(A\right)2\mathrm{i}=2\mathrm{i}\Im \left(A\right)$$
20	3 19	mpan2	$$⊢\Im \left(A\right)\in ℂ\to \Im \left(A\right)2\mathrm{i}=2\mathrm{i}\Im \left(A\right)$$
21		2cn	$$⊢2\in ℂ$$
22		mulass	$$⊢\left(2\in ℂ\wedge \mathrm{i}\in ℂ\wedge \Im \left(A\right)\in ℂ\right)\to 2\mathrm{i}\Im \left(A\right)=2\mathrm{i}\Im \left(A\right)$$
23	21 10 22	mp3an12	$$⊢\Im \left(A\right)\in ℂ\to 2\mathrm{i}\Im \left(A\right)=2\mathrm{i}\Im \left(A\right)$$
24	20 23	eqtrd	$$⊢\Im \left(A\right)\in ℂ\to \Im \left(A\right)2\mathrm{i}=2\mathrm{i}\Im \left(A\right)$$
25	2 24	syl	$$⊢A\in ℂ\to \Im \left(A\right)2\mathrm{i}=2\mathrm{i}\Im \left(A\right)$$
26	9 12	pncan2d	$$⊢A\in ℂ\to \Re \left(A\right)+\mathrm{i}\Im \left(A\right)-\Re \left(A\right)=\mathrm{i}\Im \left(A\right)$$
27	26	oveq1d	$$⊢A\in ℂ\to \left(\Re \left(A\right)+\mathrm{i}\Im \left(A\right)\right)-\Re \left(A\right)+\mathrm{i}\Im \left(A\right)=\mathrm{i}\Im \left(A\right)+\mathrm{i}\Im \left(A\right)$$
28	18 25 27	3eqtr4d	$$⊢A\in ℂ\to \Im \left(A\right)2\mathrm{i}=\left(\Re \left(A\right)+\mathrm{i}\Im \left(A\right)\right)-\Re \left(A\right)+\mathrm{i}\Im \left(A\right)$$
29	14 17 28	3eqtr4rd	$$⊢A\in ℂ\to \Im \left(A\right)2\mathrm{i}=A-\bar{A}$$
30	29	oveq1d	$$⊢A\in ℂ\to \frac{\Im \left(A\right)2\mathrm{i}}{2\mathrm{i}}=\frac{A-\bar{A}}{2\mathrm{i}}$$
31	7 30	eqtr3d	$$⊢A\in ℂ\to \Im \left(A\right)=\frac{A-\bar{A}}{2\mathrm{i}}$$