Metamath Proof Explorer


Theorem cjmulge0i

Description: A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999)

Ref Expression
Hypothesis recl.1 A
Assertion cjmulge0i 0AA

Proof

Step Hyp Ref Expression
1 recl.1 A
2 cjmulge0 A0AA
3 1 2 ax-mp 0AA