Metamath Proof Explorer

Theorem retire

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

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

Proof

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