Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 1re | GIF version |
Description: 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.) |
Ref | Expression |
---|---|
1re | ⊢ 1 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1re 7857 | 1 ⊢ 1 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2141 ℝcr 7762 1c1 7764 |
This theorem was proved from axioms: ax-1re 7857 |
This theorem is referenced by: 0re 7909 1red 7924 1xr 7967 0lt1 8035 peano2re 8044 peano2rem 8175 0reALT 8205 0le1 8389 1le1 8480 inelr 8492 1ap0 8498 eqneg 8638 ltp1 8749 ltm1 8751 recgt0 8755 mulgt1 8768 ltmulgt11 8769 lemulge11 8771 reclt1 8801 recgt1 8802 recgt1i 8803 recp1lt1 8804 recreclt 8805 sup3exmid 8862 cju 8866 peano5nni 8870 nnssre 8871 1nn 8878 nnge1 8890 nnle1eq1 8891 nngt0 8892 nnnlt1 8893 nn1gt1 8901 nngt1ne1 8902 nnrecre 8904 nnrecgt0 8905 nnsub 8906 2re 8937 3re 8941 4re 8944 5re 8946 6re 8948 7re 8950 8re 8952 9re 8954 0le2 8957 2pos 8958 3pos 8961 4pos 8964 5pos 8967 6pos 8968 7pos 8969 8pos 8970 9pos 8971 neg1rr 8973 neg1lt0 8975 1lt2 9036 1lt3 9038 1lt4 9041 1lt5 9045 1lt6 9050 1lt7 9056 1lt8 9063 1lt9 9071 1ne2 9073 1ap2 9074 1le2 9075 1le3 9078 halflt1 9084 iap0 9090 addltmul 9103 elnnnn0c 9169 nn0ge2m1nn 9184 elnnz1 9224 zltp1le 9255 zleltp1 9256 recnz 9294 gtndiv 9296 3halfnz 9298 1lt10 9470 eluzp1m1 9499 eluzp1p1 9501 eluz2b2 9551 1rp 9603 divlt1lt 9670 divle1le 9671 nnledivrp 9712 0elunit 9932 1elunit 9933 divelunit 9948 lincmb01cmp 9949 iccf1o 9950 unitssre 9951 fzpreddisj 10016 fznatpl1 10021 fztpval 10028 qbtwnxr 10203 flqbi2 10236 fldiv4p1lem1div2 10250 flqdiv 10266 reexpcl 10482 reexpclzap 10485 expge0 10501 expge1 10502 expgt1 10503 bernneq 10585 bernneq2 10586 expnbnd 10588 expnlbnd 10589 expnlbnd2 10590 nn0ltexp2 10633 facwordi 10663 faclbnd3 10666 faclbnd6 10667 facavg 10669 cjexp 10846 re1 10850 im1 10851 rei 10852 imi 10853 caucvgre 10934 sqrt1 10999 sqrt2gt1lt2 11002 abs1 11025 caubnd2 11070 mulcn2 11264 reccn2ap 11265 expcnvap0 11454 geo2sum 11466 cvgratnnlemrate 11482 fprodge0 11589 fprodge1 11591 fprodle 11592 ere 11622 ege2le3 11623 efgt1 11649 resin4p 11670 recos4p 11671 sinbnd 11704 cosbnd 11705 sinbnd2 11706 cosbnd2 11707 ef01bndlem 11708 sin01bnd 11709 cos01bnd 11710 cos1bnd 11711 cos2bnd 11712 sin01gt0 11713 cos01gt0 11714 sin02gt0 11715 sincos1sgn 11716 cos12dec 11719 ene1 11736 eap1 11737 halfleoddlt 11842 flodddiv4 11882 isprm3 12061 sqnprm 12079 coprm 12087 phibndlem 12159 pythagtriplem3 12210 fldivp1 12289 pockthi 12299 exmidunben 12370 basendxnmulrndx 12521 setsmsbasg 13234 tgioo 13301 dveflem 13442 reeff1olem 13447 reeff1o 13449 cosz12 13456 sinhalfpilem 13467 tangtx 13514 sincos4thpi 13516 pigt3 13520 coskpi 13524 cos0pilt1 13528 ioocosf1o 13530 loge 13543 logrpap0b 13552 logdivlti 13557 2logb9irrALT 13647 sqrt2cxp2logb9e3 13648 lgsdir 13691 lgsne0 13694 lgsabs1 13695 lgsdinn0 13704 ex-fl 13721 cvgcmp2nlemabs 14026 iooref1o 14028 trilpolemclim 14030 trilpolemcl 14031 trilpolemisumle 14032 trilpolemeq1 14034 trilpolemlt1 14035 apdiff 14042 nconstwlpolemgt0 14057 |
Copyright terms: Public domain | W3C validator |