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\in ℝ\to \left(\mathrm{i}R\in ℝ\leftrightarrow R=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		sn-inelr	$$⊢\neg \mathrm{i}\in ℝ$$
2		ax-icn	$$⊢\mathrm{i}\in ℂ$$
3	2	a1i	$$⊢\left(\left(R\in ℝ\wedge R\ne 0\right)\wedge \mathrm{i}R\in ℝ\right)\to \mathrm{i}\in ℂ$$
4		simpll	$$⊢\left(\left(R\in ℝ\wedge R\ne 0\right)\wedge \mathrm{i}R\in ℝ\right)\to R\in ℝ$$
5	4	recnd	$$⊢\left(\left(R\in ℝ\wedge R\ne 0\right)\wedge \mathrm{i}R\in ℝ\right)\to R\in ℂ$$
6		simplr	$$⊢\left(\left(R\in ℝ\wedge R\ne 0\right)\wedge \mathrm{i}R\in ℝ\right)\to R\ne 0$$
7	4 6	sn-rereccld	Could not format ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( 1 /R R ) e. RR ) : No typesetting found for |- ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( 1 /R R ) e. RR ) with typecode |-
8	7	recnd	Could not format ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( 1 /R R ) e. CC ) : No typesetting found for |- ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( 1 /R R ) e. CC ) with typecode |-
9	3 5 8	mulassd	Could not format ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( ( _i x. R ) x. ( 1 /R R ) ) = ( _i x. ( R x. ( 1 /R R ) ) ) ) : No typesetting found for |- ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( ( _i x. R ) x. ( 1 /R R ) ) = ( _i x. ( R x. ( 1 /R R ) ) ) ) with typecode |-
10	4 6	rerecid	Could not format ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( R x. ( 1 /R R ) ) = 1 ) : No typesetting found for |- ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( R x. ( 1 /R R ) ) = 1 ) with typecode |-
11	10	oveq2d	Could not format ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( _i x. ( R x. ( 1 /R R ) ) ) = ( _i x. 1 ) ) : No typesetting found for |- ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( _i x. ( R x. ( 1 /R R ) ) ) = ( _i x. 1 ) ) with typecode |-
12		sn-it1ei	$$⊢\mathrm{i}\cdot 1=\mathrm{i}$$
13	12	a1i	$$⊢\left(\left(R\in ℝ\wedge R\ne 0\right)\wedge \mathrm{i}R\in ℝ\right)\to \mathrm{i}\cdot 1=\mathrm{i}$$
14	9 11 13	3eqtrd	Could not format ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( ( _i x. R ) x. ( 1 /R R ) ) = _i ) : No typesetting found for |- ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( ( _i x. R ) x. ( 1 /R R ) ) = _i ) with typecode |-
15		simpr	$$⊢\left(\left(R\in ℝ\wedge R\ne 0\right)\wedge \mathrm{i}R\in ℝ\right)\to \mathrm{i}R\in ℝ$$
16	15 7	remulcld	Could not format ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( ( _i x. R ) x. ( 1 /R R ) ) e. RR ) : No typesetting found for |- ( ( ( R e. RR /\ R =/= 0 ) /\ ( _i x. R ) e. RR ) -> ( ( _i x. R ) x. ( 1 /R R ) ) e. RR ) with typecode |-
17	14 16	eqeltrrd	$$⊢\left(\left(R\in ℝ\wedge R\ne 0\right)\wedge \mathrm{i}R\in ℝ\right)\to \mathrm{i}\in ℝ$$
18	17	ex	$$⊢\left(R\in ℝ\wedge R\ne 0\right)\to \left(\mathrm{i}R\in ℝ\to \mathrm{i}\in ℝ\right)$$
19	1 18	mtoi	$$⊢\left(R\in ℝ\wedge R\ne 0\right)\to \neg \mathrm{i}R\in ℝ$$
20	19	ex	$$⊢R\in ℝ\to \left(R\ne 0\to \neg \mathrm{i}R\in ℝ\right)$$
21	20	necon4ad	$$⊢R\in ℝ\to \left(\mathrm{i}R\in ℝ\to R=0\right)$$
22		oveq2	$$⊢R=0\to \mathrm{i}R=\mathrm{i}\cdot 0$$
23		sn-it0e0	$$⊢\mathrm{i}\cdot 0=0$$
24		0re	$$⊢0\in ℝ$$
25	23 24	eqeltri	$$⊢\mathrm{i}\cdot 0\in ℝ$$
26	22 25	eqeltrdi	$$⊢R=0\to \mathrm{i}R\in ℝ$$
27	21 26	impbid1	$$⊢R\in ℝ\to \left(\mathrm{i}R\in ℝ\leftrightarrow R=0\right)$$