Metamath Proof Explorer


Theorem itrere

Description: _i times a real is real iff the real is zero. (Contributed by SN, 25-Apr-2025)

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

Proof

Step Hyp Ref Expression
1 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 3 5 6 divcan4d ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( i · 𝑅 ) ∈ ℝ ) → ( ( i · 𝑅 ) / 𝑅 ) = i )
8 simpr ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( i · 𝑅 ) ∈ ℝ ) → ( i · 𝑅 ) ∈ ℝ )
9 8 4 6 redivcld ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( i · 𝑅 ) ∈ ℝ ) → ( ( i · 𝑅 ) / 𝑅 ) ∈ ℝ )
10 7 9 eqeltrrd ( ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) ∧ ( i · 𝑅 ) ∈ ℝ ) → i ∈ ℝ )
11 10 ex ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) → ( ( i · 𝑅 ) ∈ ℝ → i ∈ ℝ ) )
12 1 11 mtoi ( ( 𝑅 ∈ ℝ ∧ 𝑅 ≠ 0 ) → ¬ ( i · 𝑅 ) ∈ ℝ )
13 12 ex ( 𝑅 ∈ ℝ → ( 𝑅 ≠ 0 → ¬ ( i · 𝑅 ) ∈ ℝ ) )
14 13 necon4ad ( 𝑅 ∈ ℝ → ( ( i · 𝑅 ) ∈ ℝ → 𝑅 = 0 ) )
15 oveq2 ( 𝑅 = 0 → ( i · 𝑅 ) = ( i · 0 ) )
16 it0e0 ( i · 0 ) = 0
17 0re 0 ∈ ℝ
18 16 17 eqeltri ( i · 0 ) ∈ ℝ
19 15 18 eqeltrdi ( 𝑅 = 0 → ( i · 𝑅 ) ∈ ℝ )
20 14 19 impbid1 ( 𝑅 ∈ ℝ → ( ( i · 𝑅 ) ∈ ℝ ↔ 𝑅 = 0 ) )