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 7714 | 1 ⊢ 1 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1480 ℝcr 7619 1c1 7621 |
This theorem was proved from axioms: ax-1re 7714 |
This theorem is referenced by: 0re 7766 1red 7781 0lt1 7889 peano2re 7898 peano2rem 8029 0reALT 8059 0le1 8243 1le1 8334 inelr 8346 1ap0 8352 eqneg 8492 ltp1 8602 ltm1 8604 recgt0 8608 mulgt1 8621 ltmulgt11 8622 lemulge11 8624 reclt1 8654 recgt1 8655 recgt1i 8656 recp1lt1 8657 recreclt 8658 sup3exmid 8715 cju 8719 peano5nni 8723 nnssre 8724 1nn 8731 nnge1 8743 nnle1eq1 8744 nngt0 8745 nnnlt1 8746 nn1gt1 8754 nngt1ne1 8755 nnrecre 8757 nnrecgt0 8758 nnsub 8759 2re 8790 3re 8794 4re 8797 5re 8799 6re 8801 7re 8803 8re 8805 9re 8807 0le2 8810 2pos 8811 3pos 8814 4pos 8817 5pos 8820 6pos 8821 7pos 8822 8pos 8823 9pos 8824 neg1rr 8826 neg1lt0 8828 1lt2 8889 1lt3 8891 1lt4 8894 1lt5 8898 1lt6 8903 1lt7 8909 1lt8 8916 1lt9 8924 1ne2 8926 1ap2 8927 1le2 8928 1le3 8931 halflt1 8937 iap0 8943 addltmul 8956 elnnnn0c 9022 nn0ge2m1nn 9037 elnnz1 9077 zltp1le 9108 zleltp1 9109 recnz 9144 gtndiv 9146 3halfnz 9148 1lt10 9320 eluzp1m1 9349 eluzp1p1 9351 eluz2b2 9397 1rp 9445 divlt1lt 9511 divle1le 9512 nnledivrp 9553 0elunit 9769 1elunit 9770 divelunit 9785 lincmb01cmp 9786 iccf1o 9787 unitssre 9788 fzpreddisj 9851 fznatpl1 9856 fztpval 9863 qbtwnxr 10035 flqbi2 10064 fldiv4p1lem1div2 10078 flqdiv 10094 reexpcl 10310 reexpclzap 10313 expge0 10329 expge1 10330 expgt1 10331 bernneq 10412 bernneq2 10413 expnbnd 10415 expnlbnd 10416 expnlbnd2 10417 facwordi 10486 faclbnd3 10489 faclbnd6 10490 facavg 10492 cjexp 10665 re1 10669 im1 10670 rei 10671 imi 10672 caucvgre 10753 sqrt1 10818 sqrt2gt1lt2 10821 abs1 10844 caubnd2 10889 mulcn2 11081 reccn2ap 11082 expcnvap0 11271 geo2sum 11283 cvgratnnlemrate 11299 ere 11376 ege2le3 11377 efgt1 11403 resin4p 11425 recos4p 11426 sinbnd 11459 cosbnd 11460 sinbnd2 11461 cosbnd2 11462 ef01bndlem 11463 sin01bnd 11464 cos01bnd 11465 cos1bnd 11466 cos2bnd 11467 sin01gt0 11468 cos01gt0 11469 sin02gt0 11470 sincos1sgn 11471 cos12dec 11474 ene1 11491 eap1 11492 halfleoddlt 11591 flodddiv4 11631 isprm3 11799 sqnprm 11816 coprm 11822 phibndlem 11892 exmidunben 11939 basendxnmulrndx 12073 setsmsbasg 12648 tgioo 12715 dveflem 12855 cosz12 12861 sinhalfpilem 12872 tangtx 12919 sincos4thpi 12921 pigt3 12925 coskpi 12929 ex-fl 12937 cvgcmp2nlemabs 13227 trilpolemclim 13229 trilpolemcl 13230 trilpolemisumle 13231 trilpolemeq1 13233 trilpolemlt1 13234 |
Copyright terms: Public domain | W3C validator |