Theorem sn-retire

Description: Commuted version of sn-itrere . (Contributed by SN, 27-Jun-2024)

	Ref	Expression
Assertion	sn-retire	$$⊢R\in ℝ\to \left(R\mathrm{i}\in ℝ\leftrightarrow R=0\right)$$

Proof

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