Theorem irec

Description: The reciprocal of _i . (Contributed by NM, 11-Oct-1999)

	Ref	Expression
Assertion	irec	$$⊢\frac{1}{\mathrm{i}}=-\mathrm{i}$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2	1 1	mulneg2i	$$⊢\mathrm{i}\left(-\mathrm{i}\right)=-\mathrm{i}\mathrm{i}$$
3		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
4		ax-1cn	$$⊢1\in ℂ$$
5	1 1	mulcli	$$⊢\mathrm{i}\mathrm{i}\in ℂ$$
6	4 5	negcon2i	$$⊢1=-\mathrm{i}\mathrm{i}\leftrightarrow \mathrm{i}\mathrm{i}=-1$$
7	3 6	mpbir	$$⊢1=-\mathrm{i}\mathrm{i}$$
8	2 7	eqtr4i	$$⊢\mathrm{i}\left(-\mathrm{i}\right)=1$$
9		negicn	$$⊢-\mathrm{i}\in ℂ$$
10		ine0	$$⊢\mathrm{i}\ne 0$$
11	4 1 9 10	divmuli	$$⊢\frac{1}{\mathrm{i}}=-\mathrm{i}\leftrightarrow \mathrm{i}\left(-\mathrm{i}\right)=1$$
12	8 11	mpbir	$$⊢\frac{1}{\mathrm{i}}=-\mathrm{i}$$