Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 1re | Unicode version |
Description: is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.) |
Ref | Expression |
---|---|
1re |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1re 7707 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 1480 cr 7612 c1 7614 |
This theorem was proved from axioms: ax-1re 7707 |
This theorem is referenced by: 0re 7759 1red 7774 0lt1 7882 peano2re 7891 peano2rem 8022 0reALT 8052 0le1 8236 1le1 8327 inelr 8339 1ap0 8345 eqneg 8485 ltp1 8595 ltm1 8597 recgt0 8601 mulgt1 8614 ltmulgt11 8615 lemulge11 8617 reclt1 8647 recgt1 8648 recgt1i 8649 recp1lt1 8650 recreclt 8651 sup3exmid 8708 cju 8712 peano5nni 8716 nnssre 8717 1nn 8724 nnge1 8736 nnle1eq1 8737 nngt0 8738 nnnlt1 8739 nn1gt1 8747 nngt1ne1 8748 nnrecre 8750 nnrecgt0 8751 nnsub 8752 2re 8783 3re 8787 4re 8790 5re 8792 6re 8794 7re 8796 8re 8798 9re 8800 0le2 8803 2pos 8804 3pos 8807 4pos 8810 5pos 8813 6pos 8814 7pos 8815 8pos 8816 9pos 8817 neg1rr 8819 neg1lt0 8821 1lt2 8882 1lt3 8884 1lt4 8887 1lt5 8891 1lt6 8896 1lt7 8902 1lt8 8909 1lt9 8917 1ne2 8919 1ap2 8920 1le2 8921 1le3 8924 halflt1 8930 iap0 8936 addltmul 8949 elnnnn0c 9015 nn0ge2m1nn 9030 elnnz1 9070 zltp1le 9101 zleltp1 9102 recnz 9137 gtndiv 9139 3halfnz 9141 1lt10 9313 eluzp1m1 9342 eluzp1p1 9344 eluz2b2 9390 1rp 9438 divlt1lt 9504 divle1le 9505 nnledivrp 9546 0elunit 9762 1elunit 9763 divelunit 9778 lincmb01cmp 9779 iccf1o 9780 unitssre 9781 fzpreddisj 9844 fznatpl1 9849 fztpval 9856 qbtwnxr 10028 flqbi2 10057 fldiv4p1lem1div2 10071 flqdiv 10087 reexpcl 10303 reexpclzap 10306 expge0 10322 expge1 10323 expgt1 10324 bernneq 10405 bernneq2 10406 expnbnd 10408 expnlbnd 10409 expnlbnd2 10410 facwordi 10479 faclbnd3 10482 faclbnd6 10483 facavg 10485 cjexp 10658 re1 10662 im1 10663 rei 10664 imi 10665 caucvgre 10746 sqrt1 10811 sqrt2gt1lt2 10814 abs1 10837 caubnd2 10882 mulcn2 11074 reccn2ap 11075 expcnvap0 11264 geo2sum 11276 cvgratnnlemrate 11292 ere 11365 ege2le3 11366 efgt1 11392 resin4p 11414 recos4p 11415 sinbnd 11448 cosbnd 11449 sinbnd2 11450 cosbnd2 11451 ef01bndlem 11452 sin01bnd 11453 cos01bnd 11454 cos1bnd 11455 cos2bnd 11456 sin01gt0 11457 cos01gt0 11458 sin02gt0 11459 sincos1sgn 11460 cos12dec 11463 ene1 11480 eap1 11481 halfleoddlt 11580 flodddiv4 11620 isprm3 11788 sqnprm 11805 coprm 11811 phibndlem 11881 exmidunben 11928 basendxnmulrndx 12062 setsmsbasg 12637 tgioo 12704 dveflem 12844 cosz12 12850 sinhalfpilem 12861 tangtx 12908 sincos4thpi 12910 pigt3 12914 coskpi 12918 ex-fl 12926 cvgcmp2nlemabs 13216 trilpolemclim 13218 trilpolemcl 13219 trilpolemisumle 13220 trilpolemeq1 13222 trilpolemlt1 13223 |
Copyright terms: Public domain | W3C validator |