Metamath Proof Explorer


Theorem peano2re

Description: A theorem for reals analogous the second Peano postulate peano2nn . (Contributed by NM, 5-Jul-2005)

Ref Expression
Assertion peano2re AA+1

Proof

Step Hyp Ref Expression
1 1re 1
2 readdcl A1A+1
3 1 2 mpan2 AA+1