Metamath Proof Explorer


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