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