![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 1re | Unicode version |
Description: ![]() |
Ref | Expression |
---|---|
1re |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1re 7968 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1re 7968 |
This theorem is referenced by: 0re 8021 1red 8036 1xr 8080 0lt1 8148 peano2re 8157 peano2rem 8288 0reALT 8318 0le1 8502 1le1 8593 inelr 8605 1ap0 8611 eqneg 8753 ltp1 8865 ltm1 8867 recgt0 8871 mulgt1 8884 ltmulgt11 8885 lemulge11 8887 reclt1 8917 recgt1 8918 recgt1i 8919 recp1lt1 8920 recreclt 8921 sup3exmid 8978 cju 8982 peano5nni 8987 nnssre 8988 1nn 8995 nnge1 9007 nnle1eq1 9008 nngt0 9009 nnnlt1 9010 nn1gt1 9018 nngt1ne1 9019 nnrecre 9021 nnrecgt0 9022 nnsub 9023 2re 9054 3re 9058 4re 9061 5re 9063 6re 9065 7re 9067 8re 9069 9re 9071 0le2 9074 2pos 9075 3pos 9078 4pos 9081 5pos 9084 6pos 9085 7pos 9086 8pos 9087 9pos 9088 neg1rr 9090 neg1lt0 9092 1lt2 9154 1lt3 9156 1lt4 9159 1lt5 9163 1lt6 9168 1lt7 9174 1lt8 9181 1lt9 9189 1ne2 9191 1ap2 9192 1le2 9193 1le3 9196 halflt1 9202 iap0 9208 addltmul 9222 elnnnn0c 9288 nn0ge2m1nn 9303 elnnz1 9343 zltp1le 9374 zleltp1 9375 recnz 9413 gtndiv 9415 3halfnz 9417 1lt10 9589 eluzp1m1 9619 eluzp1p1 9621 eluz2b2 9671 1rp 9726 divlt1lt 9793 divle1le 9794 nnledivrp 9835 0elunit 10055 1elunit 10056 divelunit 10071 lincmb01cmp 10072 iccf1o 10073 unitssre 10074 fzpreddisj 10140 fznatpl1 10145 fztpval 10152 qbtwnxr 10329 flqbi2 10363 fldiv4p1lem1div2 10377 flqdiv 10395 seqf1oglem1 10593 reexpcl 10630 reexpclzap 10633 expge0 10649 expge1 10650 expgt1 10651 bernneq 10734 bernneq2 10735 expnbnd 10737 expnlbnd 10738 expnlbnd2 10739 nn0ltexp2 10783 facwordi 10814 faclbnd3 10817 faclbnd6 10818 facavg 10820 cjexp 11040 re1 11044 im1 11045 rei 11046 imi 11047 caucvgre 11128 sqrt1 11193 sqrt2gt1lt2 11196 abs1 11219 caubnd2 11264 mulcn2 11458 reccn2ap 11459 expcnvap0 11648 geo2sum 11660 cvgratnnlemrate 11676 fprodge0 11783 fprodge1 11785 fprodle 11786 ere 11816 ege2le3 11817 efgt1 11843 resin4p 11864 recos4p 11865 sinbnd 11898 cosbnd 11899 sinbnd2 11900 cosbnd2 11901 ef01bndlem 11902 sin01bnd 11903 cos01bnd 11904 cos1bnd 11905 cos2bnd 11906 sinltxirr 11907 sin01gt0 11908 cos01gt0 11909 sin02gt0 11910 sincos1sgn 11911 cos12dec 11914 ene1 11931 eap1 11932 halfleoddlt 12038 flodddiv4 12078 isprm3 12259 sqnprm 12277 coprm 12285 phibndlem 12357 pythagtriplem3 12408 fldivp1 12489 pockthi 12499 exmidunben 12586 basendxnmulrndx 12754 starvndxnbasendx 12762 scandxnbasendx 12774 vscandxnbasendx 12779 ipndxnbasendx 12792 setsmsbasg 14658 tgioo 14733 dveflem 14905 reeff1olem 14947 reeff1o 14949 cosz12 14956 sinhalfpilem 14967 tangtx 15014 sincos4thpi 15016 pigt3 15020 coskpi 15024 cos0pilt1 15028 ioocosf1o 15030 loge 15043 logrpap0b 15052 logdivlti 15057 2logb9irrALT 15147 sqrt2cxp2logb9e3 15148 lgsdir 15192 lgsne0 15195 lgsabs1 15196 lgsdinn0 15205 gausslemma2dlem0i 15214 lgseisen 15231 2lgslem3 15258 ex-fl 15287 cvgcmp2nlemabs 15592 iooref1o 15594 trilpolemclim 15596 trilpolemcl 15597 trilpolemisumle 15598 trilpolemeq1 15600 trilpolemlt1 15601 apdiff 15608 nconstwlpolemgt0 15624 |
Copyright terms: Public domain | W3C validator |