Theorem irec

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

	Ref	Expression
Assertion	irec	⊢ ( 1 / i ) = - i

Proof

Step	Hyp	Ref	Expression
1		ax-icn	⊢ i ∈ ℂ
2	1 1	mulneg2i	⊢ ( i · - i ) = - ( i · i )
3		ixi	⊢ ( i · i ) = - 1
4		ax-1cn	⊢ 1 ∈ ℂ
5	1 1	mulcli	⊢ ( i · i ) ∈ ℂ
6	4 5	negcon2i	⊢ ( 1 = - ( i · i ) ↔ ( i · i ) = - 1 )
7	3 6	mpbir	⊢ 1 = - ( i · i )
8	2 7	eqtr4i	⊢ ( i · - i ) = 1
9		negicn	⊢ - i ∈ ℂ
10		ine0	⊢ i ≠ 0
11	4 1 9 10	divmuli	⊢ ( ( 1 / i ) = - i ↔ ( i · - i ) = 1 )
12	8 11	mpbir	⊢ ( 1 / i ) = - i