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 ) ) |
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 ) ) |