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	$⊢ (A \in ℝ \land i A \in ℝ) \to A = 0$

Proof

Step	Hyp	Ref	Expression
1		inelr	$⊢ \neg i \in ℝ$
2		ax-icn	$⊢ i \in ℂ$
3	2	a1i	$⊢ ((A \in ℝ \land i A \in ℝ) \land A \neq 0) \to i \in ℂ$
4		simpll	$⊢ ((A \in ℝ \land i A \in ℝ) \land A \neq 0) \to A \in ℝ$
5	4	recnd	$⊢ ((A \in ℝ \land i A \in ℝ) \land A \neq 0) \to A \in ℂ$
6		simpr	$⊢ ((A \in ℝ \land i A \in ℝ) \land A \neq 0) \to A \neq 0$
7	3 5 6	divcan4d	$⊢ ((A \in ℝ \land i A \in ℝ) \land A \neq 0) \to \frac{i A}{A} = i$
8		simplr	$⊢ ((A \in ℝ \land i A \in ℝ) \land A \neq 0) \to i A \in ℝ$
9	8 4 6	redivcld	$⊢ ((A \in ℝ \land i A \in ℝ) \land A \neq 0) \to \frac{i A}{A} \in ℝ$
10	7 9	eqeltrrd	$⊢ ((A \in ℝ \land i A \in ℝ) \land A \neq 0) \to i \in ℝ$
11	10	ex	$⊢ (A \in ℝ \land i A \in ℝ) \to (A \neq 0 \to i \in ℝ)$
12	11	necon1bd	$⊢ (A \in ℝ \land i A \in ℝ) \to (\neg i \in ℝ \to A = 0)$
13	1 12	mpi	$⊢ (A \in ℝ \land i A \in ℝ) \to A = 0$