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