Theorem sn-retire

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

	Ref	Expression
Assertion	sn-retire	⊢ ( 𝑅 ∈ ℝ → ( ( 𝑅 · i ) ∈ ℝ ↔ 𝑅 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		sn-inelr	⊢ ¬ i ∈ ℝ
2		simpll	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( 𝑅 · i ) ∈ ℝ ) → 𝑅 ∈ ℝ )
3		simplr	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( 𝑅 · i ) ∈ ℝ ) → 𝑅 ≠ 0 )
4	2 3	rerecid2	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( 𝑅 · i ) ∈ ℝ ) → ( ( 1 /ℝ 𝑅 ) · 𝑅 ) = 1 )
5	4	oveq1d	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( 𝑅 · i ) ∈ ℝ ) → ( ( ( 1 /ℝ 𝑅 ) · 𝑅 ) · i ) = ( 1 · i ) )
6	2 3	sn-rereccld	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( 𝑅 · i ) ∈ ℝ ) → ( 1 /ℝ 𝑅 ) ∈ ℝ )
7	6	recnd	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( 𝑅 · i ) ∈ ℝ ) → ( 1 /ℝ 𝑅 ) ∈ ℂ )
8	2	recnd	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( 𝑅 · i ) ∈ ℝ ) → 𝑅 ∈ ℂ )
9		ax-icn	⊢ i ∈ ℂ
10	9	a1i	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( 𝑅 · i ) ∈ ℝ ) → i ∈ ℂ )
11	7 8 10	mulassd	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( 𝑅 · i ) ∈ ℝ ) → ( ( ( 1 /ℝ 𝑅 ) · 𝑅 ) · i ) = ( ( 1 /ℝ 𝑅 ) · ( 𝑅 · i ) ) )
12		sn-1ticom	⊢ ( 1 · i ) = ( i · 1 )
13		sn-it1ei	⊢ ( i · 1 ) = i
14	12 13	eqtri	⊢ ( 1 · i ) = i
15	14	a1i	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( 𝑅 · i ) ∈ ℝ ) → ( 1 · i ) = i )
16	5 11 15	3eqtr3d	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( 𝑅 · i ) ∈ ℝ ) → ( ( 1 /ℝ 𝑅 ) · ( 𝑅 · i ) ) = i )
17		simpr	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( 𝑅 · i ) ∈ ℝ ) → ( 𝑅 · i ) ∈ ℝ )
18	6 17	remulcld	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( 𝑅 · i ) ∈ ℝ ) → ( ( 1 /ℝ 𝑅 ) · ( 𝑅 · i ) ) ∈ ℝ )
19	16 18	eqeltrrd	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( 𝑅 · i ) ∈ ℝ ) → i ∈ ℝ )
20	19	ex	⊢ ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) → ( ( 𝑅 · i ) ∈ ℝ → i ∈ ℝ ) )
21	1 20	mtoi	⊢ ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) → ¬ ( 𝑅 · i ) ∈ ℝ )
22	21	ex	⊢ ( 𝑅 ∈ ℝ → ( 𝑅 ≠ 0 → ¬ ( 𝑅 · i ) ∈ ℝ ) )
23	22	necon4ad	⊢ ( 𝑅 ∈ ℝ → ( ( 𝑅 · i ) ∈ ℝ → 𝑅 = 0 ) )
24		oveq1	⊢ ( 𝑅 = 0 → ( 𝑅 · i ) = ( 0 · i ) )
25		sn-0tie0	⊢ ( 0 · i ) = 0
26		0re	⊢ 0 ∈ ℝ
27	25 26	eqeltri	⊢ ( 0 · i ) ∈ ℝ
28	24 27	eqeltrdi	⊢ ( 𝑅 = 0 → ( 𝑅 · i ) ∈ ℝ )
29	23 28	impbid1	⊢ ( 𝑅 ∈ ℝ → ( ( 𝑅 · i ) ∈ ℝ ↔ 𝑅 = 0 ) )