Metamath Proof Explorer

Theorem reixi

Description: ixi without ax-mulcom . (Contributed by SN, 5-May-2024)

Ref Expression
Assertion reixi 
|- ( _i x. _i ) = ( 0 -R 1 )

Proof

Step Hyp Ref Expression
1 ax-i2m1 
 |-  ( ( _i x. _i ) + 1 ) = 0
2 1re 
 |-  1 e. RR
3 renegid2 
 |-  ( 1 e. RR -> ( ( 0 -R 1 ) + 1 ) = 0 )
4 2 3 ax-mp 
 |-  ( ( 0 -R 1 ) + 1 ) = 0
5 1 4 eqtr4i 
 |-  ( ( _i x. _i ) + 1 ) = ( ( 0 -R 1 ) + 1 )
6 ax-icn 
 |-  _i e. CC
7 6 6 mulcli 
 |-  ( _i x. _i ) e. CC
8 7 a1i 
 |-  ( T. -> ( _i x. _i ) e. CC )
9 rernegcl 
 |-  ( 1 e. RR -> ( 0 -R 1 ) e. RR )
10 9 recnd 
 |-  ( 1 e. RR -> ( 0 -R 1 ) e. CC )
11 2 10 mp1i 
 |-  ( T. -> ( 0 -R 1 ) e. CC )
12 1cnd 
 |-  ( T. -> 1 e. CC )
13 8 11 12 sn-addcan2d 
 |-  ( T. -> ( ( ( _i x. _i ) + 1 ) = ( ( 0 -R 1 ) + 1 ) <-> ( _i x. _i ) = ( 0 -R 1 ) ) )
14 5 13 mpbii 
 |-  ( T. -> ( _i x. _i ) = ( 0 -R 1 ) )
15 14 mptru 
 |-  ( _i x. _i ) = ( 0 -R 1 )