Metamath Proof Explorer


Theorem re1

Description: The real part of one. (Contributed by Scott Fenton, 9-Jun-2006)

Ref Expression
Assertion re1 1 = 1

Proof

Step Hyp Ref Expression
1 1re 1
2 rere 1 1 = 1
3 1 2 ax-mp 1 = 1