Metamath Proof Explorer


Theorem retire

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

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

Proof

Step Hyp Ref Expression
1 recn
 |-  ( R e. RR -> R e. CC )
2 ax-icn
 |-  _i e. CC
3 2 a1i
 |-  ( R e. RR -> _i e. CC )
4 1 3 mulcomd
 |-  ( R e. RR -> ( R x. _i ) = ( _i x. R ) )
5 4 eleq1d
 |-  ( R e. RR -> ( ( R x. _i ) e. RR <-> ( _i x. R ) e. RR ) )
6 itrere
 |-  ( R e. RR -> ( ( _i x. R ) e. RR <-> R = 0 ) )
7 5 6 bitrd
 |-  ( R e. RR -> ( ( R x. _i ) e. RR <-> R = 0 ) )