Metamath Proof Explorer


Theorem reim0d

Description: The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypothesis crred.1 φ A
Assertion reim0d φ A = 0

Proof

Step Hyp Ref Expression
1 crred.1 φ A
2 reim0 A A = 0
3 1 2 syl φ A = 0