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 4479. (Contributed by NM, 5-Jul-2005.) |
Ref | Expression |
---|---|
peano2re |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 7733 | . 2 | |
2 | readdcl 7714 | . 2 | |
3 | 1, 2 | mpan2 421 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1465 (class class class)co 5742 cr 7587 c1 7589 caddc 7591 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 ax-1re 7682 ax-addrcl 7685 |
This theorem is referenced by: lep1 8567 letrp1 8570 p1le 8571 ledivp1 8625 nnssre 8688 nn1suc 8703 nnge1 8707 div4p1lem1div2 8931 zltp1le 9066 suprzclex 9107 zeo 9114 peano2uz2 9116 uzind 9120 btwnapz 9139 numltc 9165 ge0p1rp 9428 fznatpl1 9811 ubmelm1fzo 9958 qbtwnxr 9990 flhalf 10030 fldiv4p1lem1div2 10033 seq3split 10207 seq3f1olemqsumk 10227 bernneq3 10369 facwordi 10441 faclbnd 10442 expcnvap0 11226 cvgratnnlemfm 11253 cvgratnnlemrate 11254 cvgratz 11256 mertenslemi1 11259 divalglemnqt 11529 infssuzex 11554 nonsq 11796 ennnfonelemkh 11836 tgioo 12626 suplociccreex 12682 |
Copyright terms: Public domain | W3C validator |