Description: A real times _i is real iff the real is zero. (Contributed by SN, 25-Apr-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | retire | ⊢ ( 𝑅 ∈ ℝ → ( ( 𝑅 · i ) ∈ ℝ ↔ 𝑅 = 0 ) ) |
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 ) ) |