Metamath Proof Explorer


Theorem irec

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

Ref Expression
Assertion irec
|- ( 1 / _i ) = -u _i

Proof

Step Hyp Ref Expression
1 ax-icn
 |-  _i e. CC
2 1 1 mulneg2i
 |-  ( _i x. -u _i ) = -u ( _i x. _i )
3 ixi
 |-  ( _i x. _i ) = -u 1
4 ax-1cn
 |-  1 e. CC
5 1 1 mulcli
 |-  ( _i x. _i ) e. CC
6 4 5 negcon2i
 |-  ( 1 = -u ( _i x. _i ) <-> ( _i x. _i ) = -u 1 )
7 3 6 mpbir
 |-  1 = -u ( _i x. _i )
8 2 7 eqtr4i
 |-  ( _i x. -u _i ) = 1
9 negicn
 |-  -u _i e. CC
10 ine0
 |-  _i =/= 0
11 4 1 9 10 divmuli
 |-  ( ( 1 / _i ) = -u _i <-> ( _i x. -u _i ) = 1 )
12 8 11 mpbir
 |-  ( 1 / _i ) = -u _i