Theorem retire

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

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

Proof

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