![]() |
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 4596. (Contributed by NM, 5-Jul-2005.) |
Ref | Expression |
---|---|
peano2re |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 7958 |
. 2
![]() ![]() ![]() ![]() | |
2 | readdcl 7939 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpan2 425 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 ax-1re 7907 ax-addrcl 7910 |
This theorem is referenced by: lep1 8804 letrp1 8807 p1le 8808 ledivp1 8862 nnssre 8925 nn1suc 8940 nnge1 8944 div4p1lem1div2 9174 zltp1le 9309 suprzclex 9353 zeo 9360 peano2uz2 9362 uzind 9366 btwnapz 9385 numltc 9411 ge0p1rp 9687 fznatpl1 10078 ubmelm1fzo 10228 qbtwnxr 10260 flhalf 10304 fldiv4p1lem1div2 10307 seq3split 10481 seq3f1olemqsumk 10501 bernneq3 10645 facwordi 10722 faclbnd 10723 expcnvap0 11512 cvgratnnlemfm 11539 cvgratnnlemrate 11540 cvgratz 11542 mertenslemi1 11545 fprodntrivap 11594 divalglemnqt 11927 infssuzex 11952 nonsq 12209 eulerthlema 12232 pcfac 12350 1arith 12367 ennnfonelemkh 12415 tgioo 14085 suplociccreex 14141 reeff1olem 14231 lgsvalmod 14459 |
Copyright terms: Public domain | W3C validator |