![]() |
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 4467. (Contributed by NM, 5-Jul-2005.) |
Ref | Expression |
---|---|
peano2re |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 7683 |
. 2
![]() ![]() ![]() ![]() | |
2 | readdcl 7664 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpan2 419 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 107 ax-1re 7633 ax-addrcl 7636 |
This theorem is referenced by: lep1 8507 letrp1 8510 p1le 8511 ledivp1 8565 nnssre 8628 nn1suc 8643 nnge1 8647 div4p1lem1div2 8871 zltp1le 9006 suprzclex 9047 zeo 9054 peano2uz2 9056 uzind 9060 btwnapz 9079 numltc 9105 ge0p1rp 9368 fznatpl1 9743 ubmelm1fzo 9890 qbtwnxr 9922 flhalf 9962 fldiv4p1lem1div2 9965 seq3split 10139 seq3f1olemqsumk 10159 bernneq3 10301 facwordi 10373 faclbnd 10374 expcnvap0 11157 cvgratnnlemfm 11184 cvgratnnlemrate 11185 cvgratz 11187 mertenslemi1 11190 divalglemnqt 11459 infssuzex 11484 nonsq 11724 ennnfonelemkh 11764 tgioo 12526 |
Copyright terms: Public domain | W3C validator |