Metamath Proof Explorer

Theorem itrere

Description: _i times a real is real iff the real is zero. (Contributed by SN, 27-Jun-2024)

Ref Expression
Assertion itrere 
|- ( R e. RR -> ( ( _i x. R ) 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 ax-icn 
 |-  _i e. CC
4 3 a1i 
 |-  ( ( ( ( R e. RR /\ R =/= 0 ) /\ ( x e. RR /\ ( R x. x ) = 1 ) ) /\ ( _i x. R ) e. RR ) -> _i e. CC )
5 simplll 
 |-  ( ( ( ( R e. RR /\ R =/= 0 ) /\ ( x e. RR /\ ( R x. x ) = 1 ) ) /\ ( _i x. R ) e. RR ) -> R e. RR )
6 5 recnd 
 |-  ( ( ( ( R e. RR /\ R =/= 0 ) /\ ( x e. RR /\ ( R x. x ) = 1 ) ) /\ ( _i x. R ) e. RR ) -> R e. CC )
7 simplrl 
 |-  ( ( ( ( R e. RR /\ R =/= 0 ) /\ ( x e. RR /\ ( R x. x ) = 1 ) ) /\ ( _i x. R ) e. RR ) -> x e. RR )
8 7 recnd 
 |-  ( ( ( ( R e. RR /\ R =/= 0 ) /\ ( x e. RR /\ ( R x. x ) = 1 ) ) /\ ( _i x. R ) e. RR ) -> x e. CC )
9 4 6 8 mulassd 
 |-  ( ( ( ( R e. RR /\ R =/= 0 ) /\ ( x e. RR /\ ( R x. x ) = 1 ) ) /\ ( _i x. R ) e. RR ) -> ( ( _i x. R ) x. x ) = ( _i x. ( R x. x ) ) )
10 simplrr 
 |-  ( ( ( ( R e. RR /\ R =/= 0 ) /\ ( x e. RR /\ ( R x. x ) = 1 ) ) /\ ( _i x. R ) e. RR ) -> ( R x. x ) = 1 )
11 10 oveq2d 
 |-  ( ( ( ( R e. RR /\ R =/= 0 ) /\ ( x e. RR /\ ( R x. x ) = 1 ) ) /\ ( _i x. R ) e. RR ) -> ( _i x. ( R x. x ) ) = ( _i x. 1 ) )
12 it1ei 
 |-  ( _i x. 1 ) = _i
13 12 a1i 
 |-  ( ( ( ( R e. RR /\ R =/= 0 ) /\ ( x e. RR /\ ( R x. x ) = 1 ) ) /\ ( _i x. R ) e. RR ) -> ( _i x. 1 ) = _i )
14 9 11 13 3eqtrd 
 |-  ( ( ( ( R e. RR /\ R =/= 0 ) /\ ( x e. RR /\ ( R x. x ) = 1 ) ) /\ ( _i x. R ) e. RR ) -> ( ( _i x. R ) x. x ) = _i )
15 simpr 
 |-  ( ( ( ( R e. RR /\ R =/= 0 ) /\ ( x e. RR /\ ( R x. x ) = 1 ) ) /\ ( _i x. R ) e. RR ) -> ( _i x. R ) e. RR )
16 15 7 remulcld 
 |-  ( ( ( ( R e. RR /\ R =/= 0 ) /\ ( x e. RR /\ ( R x. x ) = 1 ) ) /\ ( _i x. R ) e. RR ) -> ( ( _i x. R ) x. x ) e. RR )
17 14 16 eqeltrrd 
 |-  ( ( ( ( R e. RR /\ R =/= 0 ) /\ ( x e. RR /\ ( R x. x ) = 1 ) ) /\ ( _i x. R ) e. RR ) -> _i e. RR )
18 17 ex 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( x e. RR /\ ( R x. x ) = 1 ) ) -> ( ( _i x. R ) e. RR -> _i e. RR ) )
19 2 18 mtoi 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( x e. RR /\ ( R x. x ) = 1 ) ) -> -. ( _i x. R ) e. RR )
20 1 19 rexlimddv 
 |-  ( ( R e. RR /\ R =/= 0 ) -> -. ( _i x. R ) e. RR )
21 20 ex 
 |-  ( R e. RR -> ( R =/= 0 -> -. ( _i x. R ) e. RR ) )
22 21 necon4ad 
 |-  ( R e. RR -> ( ( _i x. R ) e. RR -> R = 0 ) )
23 oveq2 
 |-  ( R = 0 -> ( _i x. R ) = ( _i x. 0 ) )
24 sn-it0e0 
 |-  ( _i x. 0 ) = 0
25 0re 
 |-  0 e. RR
26 24 25 eqeltri 
 |-  ( _i x. 0 ) e. RR
27 23 26 eqeltrdi 
 |-  ( R = 0 -> ( _i x. R ) e. RR )
28 22 27 impbid1 
 |-  ( R e. RR -> ( ( _i x. R ) e. RR <-> R = 0 ) )