Metamath Proof Explorer

Theorem sn-retire

Description: Commuted version of sn-itrere . (Contributed by SN, 27-Jun-2024)

Ref Expression
Assertion sn-retire 
|- ( R e. RR -> ( ( R x. _i ) e. RR <-> R = 0 ) )

Proof

Step Hyp Ref Expression
1 sn-inelr 
 |-  -. _i e. RR
2 simpll 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( R x. _i ) e. RR ) -> R e. RR )
3 simplr 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( R x. _i ) e. RR ) -> R =/= 0 )
4 2 3 rerecid2 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( R x. _i ) e. RR ) -> ( ( 1 /R R ) x. R ) = 1 )
5 4 oveq1d 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( R x. _i ) e. RR ) -> ( ( ( 1 /R R ) x. R ) x. _i ) = ( 1 x. _i ) )
6 2 3 sn-rereccld 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( R x. _i ) e. RR ) -> ( 1 /R R ) e. RR )
7 6 recnd 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( R x. _i ) e. RR ) -> ( 1 /R R ) e. CC )
8 2 recnd 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( R x. _i ) e. RR ) -> R e. CC )
9 ax-icn 
 |-  _i e. CC
10 9 a1i 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( R x. _i ) e. RR ) -> _i e. CC )
11 7 8 10 mulassd 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( R x. _i ) e. RR ) -> ( ( ( 1 /R R ) x. R ) x. _i ) = ( ( 1 /R R ) x. ( R x. _i ) ) )
12 sn-1ticom 
 |-  ( 1 x. _i ) = ( _i x. 1 )
13 sn-it1ei 
 |-  ( _i x. 1 ) = _i
14 12 13 eqtri 
 |-  ( 1 x. _i ) = _i
15 14 a1i 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( R x. _i ) e. RR ) -> ( 1 x. _i ) = _i )
16 5 11 15 3eqtr3d 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( R x. _i ) e. RR ) -> ( ( 1 /R R ) x. ( R x. _i ) ) = _i )
17 simpr 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( R x. _i ) e. RR ) -> ( R x. _i ) e. RR )
18 6 17 remulcld 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( R x. _i ) e. RR ) -> ( ( 1 /R R ) x. ( R x. _i ) ) e. RR )
19 16 18 eqeltrrd 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( R x. _i ) e. RR ) -> _i e. RR )
20 19 ex 
 |-  ( ( R e. RR /\ R =/= 0 ) -> ( ( R x. _i ) e. RR -> _i e. RR ) )
21 1 20 mtoi 
 |-  ( ( R e. RR /\ R =/= 0 ) -> -. ( R x. _i ) e. RR )
22 21 ex 
 |-  ( R e. RR -> ( R =/= 0 -> -. ( R x. _i ) e. RR ) )
23 22 necon4ad 
 |-  ( R e. RR -> ( ( R x. _i ) e. RR -> R = 0 ) )
24 oveq1 
 |-  ( R = 0 -> ( R x. _i ) = ( 0 x. _i ) )
25 sn-0tie0 
 |-  ( 0 x. _i ) = 0
26 0re 
 |-  0 e. RR
27 25 26 eqeltri 
 |-  ( 0 x. _i ) e. RR
28 24 27 eqeltrdi 
 |-  ( R = 0 -> ( R x. _i ) e. RR )
29 23 28 impbid1 
 |-  ( R e. RR -> ( ( R x. _i ) e. RR <-> R = 0 ) )