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 7070 | 1 ⊢ 1 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1433 ℝcr 6980 1c1 6982 |
This theorem was proved from axioms: ax-1re 7070 |
This theorem is referenced by: 0re 7119 1red 7134 0lt1 7236 peano2re 7244 peano2rem 7375 0reALT 7405 0le1 7585 1le1 7672 inelr 7684 1ap0 7690 eqneg 7820 ltp1 7922 ltm1 7924 recgt0 7928 mulgt1 7941 ltmulgt11 7942 lemulge11 7944 reclt1 7974 recgt1 7975 recgt1i 7976 recp1lt1 7977 recreclt 7978 cju 8038 peano5nni 8042 nnssre 8043 1nn 8050 nnge1 8062 nnle1eq1 8063 nngt0 8064 nnnlt1 8065 nn1gt1 8072 nngt1ne1 8073 nnrecre 8075 nnrecgt0 8076 nnsub 8077 2re 8109 3re 8113 4re 8116 5re 8118 6re 8120 7re 8122 8re 8124 9re 8126 0le2 8129 2pos 8130 3pos 8133 4pos 8136 5pos 8139 6pos 8140 7pos 8141 8pos 8142 9pos 8143 neg1rr 8145 neg1lt0 8147 1lt2 8201 1lt3 8203 1lt4 8206 1lt5 8210 1lt6 8215 1lt7 8221 1lt8 8228 1lt9 8236 1ne2 8238 1le2 8239 1le3 8242 halflt1 8248 iap0 8254 addltmul 8267 elnnnn0c 8333 nn0ge2m1nn 8348 elnnz1 8374 zltp1le 8405 zleltp1 8406 recnz 8440 gtndiv 8442 3halfnz 8444 1lt10 8615 eluzp1m1 8642 eluzp1p1 8644 eluz2b2 8690 1rp 8738 divlt1lt 8801 divle1le 8802 nnledivrp 8837 0elunit 9008 1elunit 9009 divelunit 9024 lincmb01cmp 9025 iccf1o 9026 unitssre 9027 fzpreddisj 9088 fznatpl1 9093 fztpval 9100 qbtwnxr 9266 flqbi2 9293 fldiv4p1lem1div2 9307 flqdiv 9323 reexpcl 9493 reexpclzap 9496 expge0 9512 expge1 9513 expgt1 9514 bernneq 9593 bernneq2 9594 expnbnd 9596 expnlbnd 9597 expnlbnd2 9598 facwordi 9667 faclbnd3 9670 faclbnd6 9671 facavg 9673 cjexp 9780 re1 9784 im1 9785 rei 9786 imi 9787 caucvgre 9867 sqrt1 9932 sqrt2gt1lt2 9935 abs1 9958 caubnd2 10003 mulcn2 10151 halfleoddlt 10294 flodddiv4 10334 isprm3 10500 sqnprm 10517 coprm 10523 ex-fl 10563 |
Copyright terms: Public domain | W3C validator |