This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 rerecid2d ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 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 ) )