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 7838 | 1 ⊢ 1 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2135 ℝcr 7743 1c1 7745 |
This theorem was proved from axioms: ax-1re 7838 |
This theorem is referenced by: 0re 7890 1red 7905 1xr 7948 0lt1 8016 peano2re 8025 peano2rem 8156 0reALT 8186 0le1 8370 1le1 8461 inelr 8473 1ap0 8479 eqneg 8619 ltp1 8730 ltm1 8732 recgt0 8736 mulgt1 8749 ltmulgt11 8750 lemulge11 8752 reclt1 8782 recgt1 8783 recgt1i 8784 recp1lt1 8785 recreclt 8786 sup3exmid 8843 cju 8847 peano5nni 8851 nnssre 8852 1nn 8859 nnge1 8871 nnle1eq1 8872 nngt0 8873 nnnlt1 8874 nn1gt1 8882 nngt1ne1 8883 nnrecre 8885 nnrecgt0 8886 nnsub 8887 2re 8918 3re 8922 4re 8925 5re 8927 6re 8929 7re 8931 8re 8933 9re 8935 0le2 8938 2pos 8939 3pos 8942 4pos 8945 5pos 8948 6pos 8949 7pos 8950 8pos 8951 9pos 8952 neg1rr 8954 neg1lt0 8956 1lt2 9017 1lt3 9019 1lt4 9022 1lt5 9026 1lt6 9031 1lt7 9037 1lt8 9044 1lt9 9052 1ne2 9054 1ap2 9055 1le2 9056 1le3 9059 halflt1 9065 iap0 9071 addltmul 9084 elnnnn0c 9150 nn0ge2m1nn 9165 elnnz1 9205 zltp1le 9236 zleltp1 9237 recnz 9275 gtndiv 9277 3halfnz 9279 1lt10 9451 eluzp1m1 9480 eluzp1p1 9482 eluz2b2 9532 1rp 9584 divlt1lt 9651 divle1le 9652 nnledivrp 9693 0elunit 9913 1elunit 9914 divelunit 9929 lincmb01cmp 9930 iccf1o 9931 unitssre 9932 fzpreddisj 9996 fznatpl1 10001 fztpval 10008 qbtwnxr 10183 flqbi2 10216 fldiv4p1lem1div2 10230 flqdiv 10246 reexpcl 10462 reexpclzap 10465 expge0 10481 expge1 10482 expgt1 10483 bernneq 10564 bernneq2 10565 expnbnd 10567 expnlbnd 10568 expnlbnd2 10569 nn0ltexp2 10612 facwordi 10642 faclbnd3 10645 faclbnd6 10646 facavg 10648 cjexp 10821 re1 10825 im1 10826 rei 10827 imi 10828 caucvgre 10909 sqrt1 10974 sqrt2gt1lt2 10977 abs1 11000 caubnd2 11045 mulcn2 11239 reccn2ap 11240 expcnvap0 11429 geo2sum 11441 cvgratnnlemrate 11457 fprodge0 11564 fprodge1 11566 fprodle 11567 ere 11597 ege2le3 11598 efgt1 11624 resin4p 11645 recos4p 11646 sinbnd 11679 cosbnd 11680 sinbnd2 11681 cosbnd2 11682 ef01bndlem 11683 sin01bnd 11684 cos01bnd 11685 cos1bnd 11686 cos2bnd 11687 sin01gt0 11688 cos01gt0 11689 sin02gt0 11690 sincos1sgn 11691 cos12dec 11694 ene1 11711 eap1 11712 halfleoddlt 11816 flodddiv4 11856 isprm3 12029 sqnprm 12047 coprm 12055 phibndlem 12127 pythagtriplem3 12178 fldivp1 12257 pockthi 12267 exmidunben 12302 basendxnmulrndx 12451 setsmsbasg 13026 tgioo 13093 dveflem 13234 reeff1olem 13239 reeff1o 13241 cosz12 13248 sinhalfpilem 13259 tangtx 13306 sincos4thpi 13308 pigt3 13312 coskpi 13316 cos0pilt1 13320 ioocosf1o 13322 loge 13335 logrpap0b 13344 logdivlti 13349 2logb9irrALT 13439 sqrt2cxp2logb9e3 13440 ex-fl 13449 cvgcmp2nlemabs 13752 iooref1o 13754 trilpolemclim 13756 trilpolemcl 13757 trilpolemisumle 13758 trilpolemeq1 13760 trilpolemlt1 13761 apdiff 13768 nconstwlpolemgt0 13783 |
Copyright terms: Public domain | W3C validator |