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		rimul	|- ( ( R e. RR /\ ( _i x. R ) e. RR ) -> R = 0 )
2	1	ex	|- ( R e. RR -> ( ( _i x. R ) e. RR -> R = 0 ) )
3		oveq2	|- ( R = 0 -> ( _i x. R ) = ( _i x. 0 ) )
4		it0e0	|- ( _i x. 0 ) = 0
5		0re	|- 0 e. RR
6	4 5	eqeltri	|- ( _i x. 0 ) e. RR
7	3 6	eqeltrdi	|- ( R = 0 -> ( _i x. R ) e. RR )
8	2 7	impbid1	|- ( R e. RR -> ( ( _i x. R ) e. RR <-> R = 0 ) )