Metamath Proof Explorer

Theorem sn-itrere

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

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

Proof

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