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

Metamath Proof Explorer

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 ( 𝑅 ∈ ℝ → ( ( i · 𝑅 ) ∈ ℝ ↔ 𝑅 = 0 ) )

Proof

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