ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nnred Unicode version

Theorem nnred 8908
Description: A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nnred.1  |-  ( ph  ->  A  e.  NN )
Assertion
Ref Expression
nnred  |-  ( ph  ->  A  e.  RR )

Proof of Theorem nnred
StepHypRef Expression
1 nnssre 8899 . 2  |-  NN  C_  RR
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sselid 3153 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 2148   RRcr 7788   NNcn 8895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4118  ax-cnex 7880  ax-resscn 7881  ax-1re 7883  ax-addrcl 7886
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2739  df-in 3135  df-ss 3142  df-int 3843  df-inn 8896
This theorem is referenced by:  exbtwnzlemstep  10221  qbtwnrelemcalc  10229  qbtwnre  10230  flqdiv  10294  modqmulnn  10315  modifeq2int  10359  modaddmodup  10360  modaddmodlo  10361  modsumfzodifsn  10369  addmodlteq  10371  bernneq3  10615  expnbnd  10616  facwordi  10691  faclbnd  10692  faclbnd2  10693  faclbnd3  10694  faclbnd6  10695  facubnd  10696  facavg  10697  bcp1nk  10713  bcval5  10714  caucvgrelemcau  10960  caucvgre  10961  cvg1nlemcxze  10962  cvg1nlemcau  10964  cvg1nlemres  10965  resqrexlemdecn  10992  resqrexlemga  11003  fsum3cvg3  11375  divcnv  11476  cvgratnnlembern  11502  cvgratnnlemseq  11505  cvgratnnlemabsle  11506  cvgratnnlemsumlt  11507  cvgratnnlemrate  11509  cvgratz  11511  eftabs  11635  efcllemp  11637  ege2le3  11650  efcj  11652  eftlub  11669  eflegeo  11680  eirraplem  11755  dvdslelemd  11819  nno  11881  nnoddm1d2  11885  divalglemnqt  11895  divalglemeunn  11896  dvdsbnd  11927  sqgcd  12000  uzwodc  12008  lcmgcdlem  12047  ncoprmgcdne1b  12059  prmind2  12090  isprm5lem  12111  coprm  12114  prmfac1  12122  sqrt2irraplemnn  12149  divdenle  12167  qnumgt0  12168  nn0sqrtelqelz  12176  hashdvds  12191  eulerthlemrprm  12199  eulerthlema  12200  odzdvds  12215  pythagtriplem11  12244  pythagtriplem12  12245  pythagtriplem13  12246  pythagtriplem14  12247  pythagtriplem19  12252  pclemub  12257  pcpre1  12262  pcidlem  12292  dvdsprmpweqle  12306  pcadd  12309  pcmpt  12311  pcmpt2  12312  pcfaclem  12317  pcfac  12318  qexpz  12320  pockthlem  12324  pockthg  12325  1arith  12335  4sqlem5  12350  4sqlem6  12351  4sqlem10  12355  mul4sqlem  12361  znnen  12369  exmidunben  12397  nninfdclemp1  12421  nninfdclemlt  12422  nninfdclemf1  12423  strleund  12531  logbgcd1irraplemexp  14019  logbgcd1irraplemap  14020  lgslem1  14034  lgsval2lem  14044  lgsdirprm  14068  lgsdir  14069  2sqlem3  14086  2sqlem8  14092  cvgcmp2nlemabs  14403
  Copyright terms: Public domain W3C validator