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 4554. (Contributed by NM, 5-Jul-2005.) |
Ref | Expression |
---|---|
peano2re |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 7877 | . 2 | |
2 | readdcl 7858 | . 2 | |
3 | 1, 2 | mpan2 422 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 2128 (class class class)co 5824 cr 7731 c1 7733 caddc 7735 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 ax-1re 7826 ax-addrcl 7829 |
This theorem is referenced by: lep1 8716 letrp1 8719 p1le 8720 ledivp1 8774 nnssre 8837 nn1suc 8852 nnge1 8856 div4p1lem1div2 9086 zltp1le 9221 suprzclex 9262 zeo 9269 peano2uz2 9271 uzind 9275 btwnapz 9294 numltc 9320 ge0p1rp 9592 fznatpl1 9978 ubmelm1fzo 10125 qbtwnxr 10157 flhalf 10201 fldiv4p1lem1div2 10204 seq3split 10378 seq3f1olemqsumk 10398 bernneq3 10540 facwordi 10614 faclbnd 10615 expcnvap0 11399 cvgratnnlemfm 11426 cvgratnnlemrate 11427 cvgratz 11429 mertenslemi1 11432 fprodntrivap 11481 divalglemnqt 11810 infssuzex 11835 nonsq 12081 eulerthlema 12104 ennnfonelemkh 12141 tgioo 12946 suplociccreex 13002 reeff1olem 13092 |
Copyright terms: Public domain | W3C validator |