Metamath Proof Explorer


Theorem retire

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

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

Proof

Step Hyp Ref Expression
1 recn ( 𝑅 ∈ ℝ → 𝑅 ∈ ℂ )
2 ax-icn i ∈ ℂ
3 2 a1i ( 𝑅 ∈ ℝ → i ∈ ℂ )
4 1 3 mulcomd ( 𝑅 ∈ ℝ → ( 𝑅 · i ) = ( i · 𝑅 ) )
5 4 eleq1d ( 𝑅 ∈ ℝ → ( ( 𝑅 · i ) ∈ ℝ ↔ ( i · 𝑅 ) ∈ ℝ ) )
6 itrere ( 𝑅 ∈ ℝ → ( ( i · 𝑅 ) ∈ ℝ ↔ 𝑅 = 0 ) )
7 5 6 bitrd ( 𝑅 ∈ ℝ → ( ( 𝑅 · i ) ∈ ℝ ↔ 𝑅 = 0 ) )