![]() |
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 7934 | 1 ⊢ 1 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2160 ℝcr 7839 1c1 7841 |
This theorem was proved from axioms: ax-1re 7934 |
This theorem is referenced by: 0re 7986 1red 8001 1xr 8045 0lt1 8113 peano2re 8122 peano2rem 8253 0reALT 8283 0le1 8467 1le1 8558 inelr 8570 1ap0 8576 eqneg 8718 ltp1 8830 ltm1 8832 recgt0 8836 mulgt1 8849 ltmulgt11 8850 lemulge11 8852 reclt1 8882 recgt1 8883 recgt1i 8884 recp1lt1 8885 recreclt 8886 sup3exmid 8943 cju 8947 peano5nni 8951 nnssre 8952 1nn 8959 nnge1 8971 nnle1eq1 8972 nngt0 8973 nnnlt1 8974 nn1gt1 8982 nngt1ne1 8983 nnrecre 8985 nnrecgt0 8986 nnsub 8987 2re 9018 3re 9022 4re 9025 5re 9027 6re 9029 7re 9031 8re 9033 9re 9035 0le2 9038 2pos 9039 3pos 9042 4pos 9045 5pos 9048 6pos 9049 7pos 9050 8pos 9051 9pos 9052 neg1rr 9054 neg1lt0 9056 1lt2 9117 1lt3 9119 1lt4 9122 1lt5 9126 1lt6 9131 1lt7 9137 1lt8 9144 1lt9 9152 1ne2 9154 1ap2 9155 1le2 9156 1le3 9159 halflt1 9165 iap0 9171 addltmul 9184 elnnnn0c 9250 nn0ge2m1nn 9265 elnnz1 9305 zltp1le 9336 zleltp1 9337 recnz 9375 gtndiv 9377 3halfnz 9379 1lt10 9551 eluzp1m1 9580 eluzp1p1 9582 eluz2b2 9632 1rp 9686 divlt1lt 9753 divle1le 9754 nnledivrp 9795 0elunit 10015 1elunit 10016 divelunit 10031 lincmb01cmp 10032 iccf1o 10033 unitssre 10034 fzpreddisj 10100 fznatpl1 10105 fztpval 10112 qbtwnxr 10287 flqbi2 10321 fldiv4p1lem1div2 10335 flqdiv 10351 reexpcl 10567 reexpclzap 10570 expge0 10586 expge1 10587 expgt1 10588 bernneq 10671 bernneq2 10672 expnbnd 10674 expnlbnd 10675 expnlbnd2 10676 nn0ltexp2 10720 facwordi 10751 faclbnd3 10754 faclbnd6 10755 facavg 10757 cjexp 10933 re1 10937 im1 10938 rei 10939 imi 10940 caucvgre 11021 sqrt1 11086 sqrt2gt1lt2 11089 abs1 11112 caubnd2 11157 mulcn2 11351 reccn2ap 11352 expcnvap0 11541 geo2sum 11553 cvgratnnlemrate 11569 fprodge0 11676 fprodge1 11678 fprodle 11679 ere 11709 ege2le3 11710 efgt1 11736 resin4p 11757 recos4p 11758 sinbnd 11791 cosbnd 11792 sinbnd2 11793 cosbnd2 11794 ef01bndlem 11795 sin01bnd 11796 cos01bnd 11797 cos1bnd 11798 cos2bnd 11799 sin01gt0 11800 cos01gt0 11801 sin02gt0 11802 sincos1sgn 11803 cos12dec 11806 ene1 11823 eap1 11824 halfleoddlt 11930 flodddiv4 11970 isprm3 12149 sqnprm 12167 coprm 12175 phibndlem 12247 pythagtriplem3 12298 fldivp1 12379 pockthi 12389 exmidunben 12476 basendxnmulrndx 12642 starvndxnbasendx 12650 scandxnbasendx 12662 vscandxnbasendx 12667 ipndxnbasendx 12680 setsmsbasg 14431 tgioo 14498 dveflem 14639 reeff1olem 14644 reeff1o 14646 cosz12 14653 sinhalfpilem 14664 tangtx 14711 sincos4thpi 14713 pigt3 14717 coskpi 14721 cos0pilt1 14725 ioocosf1o 14727 loge 14740 logrpap0b 14749 logdivlti 14754 2logb9irrALT 14844 sqrt2cxp2logb9e3 14845 lgsdir 14889 lgsne0 14892 lgsabs1 14893 lgsdinn0 14902 ex-fl 14930 cvgcmp2nlemabs 15234 iooref1o 15236 trilpolemclim 15238 trilpolemcl 15239 trilpolemisumle 15240 trilpolemeq1 15242 trilpolemlt1 15243 apdiff 15250 nconstwlpolemgt0 15266 |
Copyright terms: Public domain | W3C validator |