Metamath Proof Explorer

Theorem itrere

Description: _i times a real is real iff the real is zero. (Contributed by SN, 25-Apr-2025)

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

Proof

Step Hyp Ref Expression
1 inelr 
 |-  -. _i e. RR
2 ax-icn 
 |-  _i e. CC
3 2 a1i 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> _i e. CC )
4 simpll 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> R e. RR )
5 4 recnd 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> R e. CC )
6 simplr 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> R =/= 0 )
7 3 5 6 divcan4d 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( ( _i x. R ) / R ) = _i )
8 simpr 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( _i x. R ) e. RR )
9 8 4 6 redivcld 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( ( _i x. R ) / R ) e. RR )
10 7 9 eqeltrrd 
 |-  ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> _i e. RR )
11 10 ex 
 |-  ( ( R e. RR /\ R =/= 0 ) -> ( ( _i x. R ) e. RR -> _i e. RR ) )
12 1 11 mtoi 
 |-  ( ( R e. RR /\ R =/= 0 ) -> -. ( _i x. R ) e. RR )
13 12 ex 
 |-  ( R e. RR -> ( R =/= 0 -> -. ( _i x. R ) e. RR ) )
14 13 necon4ad 
 |-  ( R e. RR -> ( ( _i x. R ) e. RR -> R = 0 ) )
15 oveq2 
 |-  ( R = 0 -> ( _i x. R ) = ( _i x. 0 ) )
16 it0e0 
 |-  ( _i x. 0 ) = 0
17 0re 
 |-  0 e. RR
18 16 17 eqeltri 
 |-  ( _i x. 0 ) e. RR
19 15 18 eqeltrdi 
 |-  ( R = 0 -> ( _i x. R ) e. RR )
20 14 19 impbid1 
 |-  ( R e. RR -> ( ( _i x. R ) e. RR <-> R = 0 ) )