![]() |
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 7589 | 1 ⊢ 1 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1448 ℝcr 7499 1c1 7501 |
This theorem was proved from axioms: ax-1re 7589 |
This theorem is referenced by: 0re 7638 1red 7653 0lt1 7760 peano2re 7769 peano2rem 7900 0reALT 7930 0le1 8110 1le1 8200 inelr 8212 1ap0 8218 eqneg 8353 ltp1 8460 ltm1 8462 recgt0 8466 mulgt1 8479 ltmulgt11 8480 lemulge11 8482 reclt1 8512 recgt1 8513 recgt1i 8514 recp1lt1 8515 recreclt 8516 sup3exmid 8573 cju 8577 peano5nni 8581 nnssre 8582 1nn 8589 nnge1 8601 nnle1eq1 8602 nngt0 8603 nnnlt1 8604 nn1gt1 8612 nngt1ne1 8613 nnrecre 8615 nnrecgt0 8616 nnsub 8617 2re 8648 3re 8652 4re 8655 5re 8657 6re 8659 7re 8661 8re 8663 9re 8665 0le2 8668 2pos 8669 3pos 8672 4pos 8675 5pos 8678 6pos 8679 7pos 8680 8pos 8681 9pos 8682 neg1rr 8684 neg1lt0 8686 1lt2 8741 1lt3 8743 1lt4 8746 1lt5 8750 1lt6 8755 1lt7 8761 1lt8 8768 1lt9 8776 1ne2 8778 1ap2 8779 1le2 8780 1le3 8783 halflt1 8789 iap0 8795 addltmul 8808 elnnnn0c 8874 nn0ge2m1nn 8889 elnnz1 8929 zltp1le 8960 zleltp1 8961 recnz 8996 gtndiv 8998 3halfnz 9000 1lt10 9172 eluzp1m1 9199 eluzp1p1 9201 eluz2b2 9247 1rp 9295 divlt1lt 9358 divle1le 9359 nnledivrp 9394 0elunit 9610 1elunit 9611 divelunit 9626 lincmb01cmp 9627 iccf1o 9628 unitssre 9629 fzpreddisj 9692 fznatpl1 9697 fztpval 9704 qbtwnxr 9876 flqbi2 9905 fldiv4p1lem1div2 9919 flqdiv 9935 reexpcl 10151 reexpclzap 10154 expge0 10170 expge1 10171 expgt1 10172 bernneq 10253 bernneq2 10254 expnbnd 10256 expnlbnd 10257 expnlbnd2 10258 facwordi 10327 faclbnd3 10330 faclbnd6 10331 facavg 10333 cjexp 10506 re1 10510 im1 10511 rei 10512 imi 10513 caucvgre 10593 sqrt1 10658 sqrt2gt1lt2 10661 abs1 10684 caubnd2 10729 mulcn2 10920 reccn2ap 10921 expcnvap0 11110 geo2sum 11122 cvgratnnlemrate 11138 ere 11174 ege2le3 11175 efgt1 11201 resin4p 11223 recos4p 11224 sinbnd 11257 cosbnd 11258 sinbnd2 11259 cosbnd2 11260 ef01bndlem 11261 sin01bnd 11262 cos01bnd 11263 cos1bnd 11264 cos2bnd 11265 sin01gt0 11266 cos01gt0 11267 sin02gt0 11268 sincos1sgn 11269 ene1 11286 eap1 11287 halfleoddlt 11386 flodddiv4 11426 isprm3 11592 sqnprm 11609 coprm 11615 phibndlem 11684 exmidunben 11731 basendxnmulrndx 11855 setsmsbasg 12407 tgioo 12465 ex-fl 12540 cvgcmp2nlemabs 12811 trilpolemclim 12813 trilpolemcl 12814 trilpolemisumle 12815 trilpolemeq1 12817 trilpolemlt1 12818 |
Copyright terms: Public domain | W3C validator |