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 i A A = 0

Proof

Step Hyp Ref Expression
1 inelr ¬ i
2 ax-icn i
3 2 a1i A i A A 0 i
4 simpll A i A A 0 A
5 4 recnd A i A A 0 A
6 simpr A i A A 0 A 0
7 3 5 6 divcan4d A i A A 0 i A A = i
8 simplr A i A A 0 i A
9 8 4 6 redivcld A i A A 0 i A A
10 7 9 eqeltrrd A i A A 0 i
11 10 ex A i A A 0 i
12 11 necon1bd A i A ¬ i A = 0
13 1 12 mpi A i A A = 0