![]() |
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 7940 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1re 7940 |
This theorem is referenced by: 0re 7992 1red 8007 1xr 8051 0lt1 8119 peano2re 8128 peano2rem 8259 0reALT 8289 0le1 8473 1le1 8564 inelr 8576 1ap0 8582 eqneg 8724 ltp1 8836 ltm1 8838 recgt0 8842 mulgt1 8855 ltmulgt11 8856 lemulge11 8858 reclt1 8888 recgt1 8889 recgt1i 8890 recp1lt1 8891 recreclt 8892 sup3exmid 8949 cju 8953 peano5nni 8957 nnssre 8958 1nn 8965 nnge1 8977 nnle1eq1 8978 nngt0 8979 nnnlt1 8980 nn1gt1 8988 nngt1ne1 8989 nnrecre 8991 nnrecgt0 8992 nnsub 8993 2re 9024 3re 9028 4re 9031 5re 9033 6re 9035 7re 9037 8re 9039 9re 9041 0le2 9044 2pos 9045 3pos 9048 4pos 9051 5pos 9054 6pos 9055 7pos 9056 8pos 9057 9pos 9058 neg1rr 9060 neg1lt0 9062 1lt2 9123 1lt3 9125 1lt4 9128 1lt5 9132 1lt6 9137 1lt7 9143 1lt8 9150 1lt9 9158 1ne2 9160 1ap2 9161 1le2 9162 1le3 9165 halflt1 9171 iap0 9177 addltmul 9190 elnnnn0c 9256 nn0ge2m1nn 9271 elnnz1 9311 zltp1le 9342 zleltp1 9343 recnz 9381 gtndiv 9383 3halfnz 9385 1lt10 9557 eluzp1m1 9587 eluzp1p1 9589 eluz2b2 9639 1rp 9693 divlt1lt 9760 divle1le 9761 nnledivrp 9802 0elunit 10022 1elunit 10023 divelunit 10038 lincmb01cmp 10039 iccf1o 10040 unitssre 10041 fzpreddisj 10107 fznatpl1 10112 fztpval 10119 qbtwnxr 10294 flqbi2 10328 fldiv4p1lem1div2 10342 flqdiv 10358 reexpcl 10577 reexpclzap 10580 expge0 10596 expge1 10597 expgt1 10598 bernneq 10681 bernneq2 10682 expnbnd 10684 expnlbnd 10685 expnlbnd2 10686 nn0ltexp2 10730 facwordi 10761 faclbnd3 10764 faclbnd6 10765 facavg 10767 cjexp 10943 re1 10947 im1 10948 rei 10949 imi 10950 caucvgre 11031 sqrt1 11096 sqrt2gt1lt2 11099 abs1 11122 caubnd2 11167 mulcn2 11361 reccn2ap 11362 expcnvap0 11551 geo2sum 11563 cvgratnnlemrate 11579 fprodge0 11686 fprodge1 11688 fprodle 11689 ere 11719 ege2le3 11720 efgt1 11746 resin4p 11767 recos4p 11768 sinbnd 11801 cosbnd 11802 sinbnd2 11803 cosbnd2 11804 ef01bndlem 11805 sin01bnd 11806 cos01bnd 11807 cos1bnd 11808 cos2bnd 11809 sin01gt0 11810 cos01gt0 11811 sin02gt0 11812 sincos1sgn 11813 cos12dec 11816 ene1 11833 eap1 11834 halfleoddlt 11940 flodddiv4 11980 isprm3 12161 sqnprm 12179 coprm 12187 phibndlem 12259 pythagtriplem3 12310 fldivp1 12391 pockthi 12401 exmidunben 12488 basendxnmulrndx 12656 starvndxnbasendx 12664 scandxnbasendx 12676 vscandxnbasendx 12681 ipndxnbasendx 12694 setsmsbasg 14464 tgioo 14531 dveflem 14672 reeff1olem 14677 reeff1o 14679 cosz12 14686 sinhalfpilem 14697 tangtx 14744 sincos4thpi 14746 pigt3 14750 coskpi 14754 cos0pilt1 14758 ioocosf1o 14760 loge 14773 logrpap0b 14782 logdivlti 14787 2logb9irrALT 14877 sqrt2cxp2logb9e3 14878 lgsdir 14922 lgsne0 14925 lgsabs1 14926 lgsdinn0 14935 ex-fl 14963 cvgcmp2nlemabs 15268 iooref1o 15270 trilpolemclim 15272 trilpolemcl 15273 trilpolemisumle 15274 trilpolemeq1 15276 trilpolemlt1 15277 apdiff 15284 nconstwlpolemgt0 15300 |
Copyright terms: Public domain | W3C validator |