Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > peano2re | Unicode version |
Description: A theorem for reals analogous the second Peano postulate peano2 4504. (Contributed by NM, 5-Jul-2005.) |
Ref | Expression |
---|---|
peano2re |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 7758 | . 2 | |
2 | readdcl 7739 | . 2 | |
3 | 1, 2 | mpan2 421 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1480 (class class class)co 5767 cr 7612 c1 7614 caddc 7616 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 ax-1re 7707 ax-addrcl 7710 |
This theorem is referenced by: lep1 8596 letrp1 8599 p1le 8600 ledivp1 8654 nnssre 8717 nn1suc 8732 nnge1 8736 div4p1lem1div2 8966 zltp1le 9101 suprzclex 9142 zeo 9149 peano2uz2 9151 uzind 9155 btwnapz 9174 numltc 9200 ge0p1rp 9466 fznatpl1 9849 ubmelm1fzo 9996 qbtwnxr 10028 flhalf 10068 fldiv4p1lem1div2 10071 seq3split 10245 seq3f1olemqsumk 10265 bernneq3 10407 facwordi 10479 faclbnd 10480 expcnvap0 11264 cvgratnnlemfm 11291 cvgratnnlemrate 11292 cvgratz 11294 mertenslemi1 11297 divalglemnqt 11606 infssuzex 11631 nonsq 11874 ennnfonelemkh 11914 tgioo 12704 suplociccreex 12760 |
Copyright terms: Public domain | W3C validator |