irec

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

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

Metamath Proof Explorer