Metamath Proof Explorer

Theorem zre

Description: An integer is a real. (Contributed by NM, 8-Jan-2002)

Ref Expression
Assertion zre 
|- ( N e. ZZ -> N e. RR )

Proof

Step Hyp Ref Expression
1 elz 
 |-  ( N e. ZZ <-> ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) )
2 1 simplbi 
 |-  ( N e. ZZ -> N e. RR )