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

Metamath Proof Explorer

Theorem rimul

Description: A real number times the imaginary unit is real only if the number is 0. (Contributed by NM, 28-May-1999) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion rimul ( ( 𝐴 ∈ ℝ ∧ ( i · 𝐴 ) ∈ ℝ ) → 𝐴 = 0 )

Proof

Step Hyp Ref Expression
1 inelr ⊢ ¬ i ∈ ℝ
2 ax-icn ⊢ i ∈ ℂ
3 2 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( i · 𝐴 ) ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → i ∈ ℂ )
4 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( i · 𝐴 ) ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℝ )
5 4 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( i · 𝐴 ) ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
6 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( i · 𝐴 ) ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → 𝐴 ≠ 0 )
7 3 5 6 divcan4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( i · 𝐴 ) ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( ( i · 𝐴 ) / 𝐴 ) = i )
8 simplr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( i · 𝐴 ) ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( i · 𝐴 ) ∈ ℝ )
9 8 4 6 redivcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( i · 𝐴 ) ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( ( i · 𝐴 ) / 𝐴 ) ∈ ℝ )
10 7 9 eqeltrrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( i · 𝐴 ) ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → i ∈ ℝ )
11 10 ex ⊢ ( ( 𝐴 ∈ ℝ ∧ ( i · 𝐴 ) ∈ ℝ ) → ( 𝐴 ≠ 0 → i ∈ ℝ ) )
12 11 necon1bd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( i · 𝐴 ) ∈ ℝ ) → ( ¬ i ∈ ℝ → 𝐴 = 0 ) )
13 1 12 mpi ⊢ ( ( 𝐴 ∈ ℝ ∧ ( i · 𝐴 ) ∈ ℝ ) → 𝐴 = 0 )