Metamath Proof Explorer

Theorem ipiiie0

Description: The multiplicative inverse of _i (per i4 ) is also its additive inverse. (Contributed by SN, 30-Jun-2024)

Ref Expression
Assertion ipiiie0 
|- ( _i + ( _i x. ( _i x. _i ) ) ) = 0

Proof

Step Hyp Ref Expression
1 it1ei 
 |-  ( _i x. 1 ) = _i
2 1 eqcomi 
 |-  _i = ( _i x. 1 )
3 reixi 
 |-  ( _i x. _i ) = ( 0 -R 1 )
4 3 oveq2i 
 |-  ( _i x. ( _i x. _i ) ) = ( _i x. ( 0 -R 1 ) )
5 2 4 oveq12i 
 |-  ( _i + ( _i x. ( _i x. _i ) ) ) = ( ( _i x. 1 ) + ( _i x. ( 0 -R 1 ) ) )
6 ax-icn 
 |-  _i e. CC
7 ax-1cn 
 |-  1 e. CC
8 1re 
 |-  1 e. RR
9 rernegcl 
 |-  ( 1 e. RR -> ( 0 -R 1 ) e. RR )
10 8 9 ax-mp 
 |-  ( 0 -R 1 ) e. RR
11 10 recni 
 |-  ( 0 -R 1 ) e. CC
12 6 7 11 adddii 
 |-  ( _i x. ( 1 + ( 0 -R 1 ) ) ) = ( ( _i x. 1 ) + ( _i x. ( 0 -R 1 ) ) )
13 renegid 
 |-  ( 1 e. RR -> ( 1 + ( 0 -R 1 ) ) = 0 )
14 8 13 ax-mp 
 |-  ( 1 + ( 0 -R 1 ) ) = 0
15 14 oveq2i 
 |-  ( _i x. ( 1 + ( 0 -R 1 ) ) ) = ( _i x. 0 )
16 sn-it0e0 
 |-  ( _i x. 0 ) = 0
17 15 16 eqtri 
 |-  ( _i x. ( 1 + ( 0 -R 1 ) ) ) = 0
18 5 12 17 3eqtr2i 
 |-  ( _i + ( _i x. ( _i x. _i ) ) ) = 0