Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  rimul Unicode version

Theorem rimul 7650
 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.)
Assertion
Ref Expression
rimul

Proof of Theorem rimul
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 inelr 7649 . . 3
2 recexre 7643 . . . . . 6 #
32adantlr 454 . . . . 5 #
4 simplll 493 . . . . . . . . 9 #
54recnd 7113 . . . . . . . 8 #
6 simprl 491 . . . . . . . . 9 #
76recnd 7113 . . . . . . . 8 #
8 ax-icn 7037 . . . . . . . . 9
9 mulass 7070 . . . . . . . . 9
108, 9mp3an1 1230 . . . . . . . 8
115, 7, 10syl2anc 397 . . . . . . 7 #
12 oveq2 5548 . . . . . . . . 9
138mulid1i 7087 . . . . . . . . 9
1412, 13syl6eq 2104 . . . . . . . 8
1514ad2antll 468 . . . . . . 7 #
1611, 15eqtrd 2088 . . . . . 6 #
17 simpllr 494 . . . . . . 7 #
1817, 6remulcld 7115 . . . . . 6 #
1916, 18eqeltrrd 2131 . . . . 5 #
203, 19rexlimddv 2454 . . . 4 #
2120ex 112 . . 3 #
221, 21mtoi 600 . 2 #
23 0re 7085 . . . 4
24 reapti 7644 . . . 4 #
2523, 24mpan2 409 . . 3 #