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 )