Theorem nnre 12219

Description: A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)

Assertion

Ref	Expression
nnre	⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)

Proof of Theorem nnre

Step	Hyp	Ref	Expression
1		nnssre 12216	. 2 ⊢ ℕ ⊆ ℝ
2	1	sseli 3979	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11109  ℕcn 12212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-i2m1 11178  ax-1ne0 11179  ax-rrecex 11182  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-nn 12213

This theorem is referenced by:  nnrei  12221  nnmulcl  12236  nn2ge  12239  nnge1  12240  nngt1ne1  12241  nnle1eq1  12242  nngt0  12243  nnnlt1  12244  nnnle0  12245  nndivre  12253  nnrecgt0  12255  nnsub  12256  nnunb  12468  arch  12469  nnrecl  12470  bndndx  12471  0mnnnnn0  12504  nnnegz  12561  elnnz  12568  elz2  12576  nnz  12579  gtndiv  12639  prime  12643  btwnz  12665  indstr  12900  qre  12937  elpq  12959  elpqb  12960  rpnnen1lem2  12961  rpnnen1lem1  12962  rpnnen1lem3  12963  rpnnen1lem5  12965  nnrp  12985  nnledivrp  13086  qbtwnre  13178  elfzo0le  13676  fzonmapblen  13678  fzo1fzo0n0  13683  ubmelfzo  13697  fzonn0p1p1  13711  ubmelm1fzo  13728  subfzo0  13754  adddivflid  13783  flltdivnn0lt  13798  quoremz  13820  quoremnn0ALT  13822  intfracq  13824  fldiv  13825  modmulnn  13854  m1modnnsub1  13882  addmodid  13884  modifeq2int  13898  modaddmodup  13899  modaddmodlo  13900  modfzo0difsn  13908  modsumfzodifsn  13909  addmodlteq  13911  nnlesq  14169  digit2  14199  digit1  14200  expnngt1  14204  facdiv  14247  facndiv  14248  faclbnd  14250  faclbnd3  14252  faclbnd4lem4  14256  faclbnd5  14258  bcval5  14278  seqcoll  14425  ccatval21sw  14535  cshwidxmod  14753  cshwidxm1  14757  repswcshw  14762  isercolllem1  15611  harmonic  15805  efaddlem  16036  rpnnen2lem9  16165  rpnnen2lem12  16168  sqrt2irr  16192  nndivdvds  16206  dvdsle  16253  fzm1ndvds  16265  nno  16325  nnoddm1d2  16329  divalg2  16348  divalgmod  16349  ndvdsadd  16353  modgcd  16474  gcdzeq  16494  sqgcd  16502  dvdssqlem  16503  lcmgcdlem  16543  lcmf  16570  coprmgcdb  16586  qredeq  16594  qredeu  16595  isprm3  16620  ge2nprmge4  16638  prmdvdsfz  16642  isprm5  16644  ncoprmlnprm  16664  divdenle  16685  phibndlem  16703  eulerthlem2  16715  hashgcdlem  16721  oddprm  16743  pythagtriplem10  16753  pythagtriplem12  16759  pythagtriplem14  16761  pythagtriplem16  16763  pythagtriplem19  16766  pclem  16771  pc2dvds  16812  pcmpt  16825  fldivp1  16830  pcbc  16833  infpnlem1  16843  infpn2  16846  prmreclem1  16849  prmreclem3  16851  vdwlem3  16916  ram0  16955  prmgaplem4  16987  prmgaplem7  16990  cshwshashlem1  17029  cshwshashlem2  17030  setsstruct2  17107  mulgnegnn  18964  mulgmodid  18993  odmodnn0  19408  gexdvds  19452  sylow3lem6  19500  prmirredlem  21042  znidomb  21117  chfacfisf  22356  chfacfisfcpmat  22357  chfacffsupp  22358  chfacfscmul0  22360  chfacfpmmul0  22364  ovolunlem1a  25013  ovoliunlem2  25020  ovolicc2lem3  25036  ovolicc2lem4  25037  iundisj2  25066  dyadss  25111  volsup2  25122  volivth  25124  vitali  25130  ismbf3d  25171  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  itg2seq  25260  itg2gt0  25278  itg2cnlem1  25279  plyeq0lem  25724  dgreq0  25779  dgrcolem2  25788  elqaalem2  25833  elqaalem3  25834  logtayllem  26167  leibpi  26447  birthdaylem3  26458  zetacvg  26519  eldmgm  26526  basellem1  26585  basellem2  26586  basellem3  26587  basellem6  26590  basellem9  26593  prmorcht  26682  dvdsflsumcom  26692  muinv  26697  vmalelog  26708  chtublem  26714  logfac2  26720  logfaclbnd  26725  pcbcctr  26779  bcmono  26780  bposlem1  26787  bposlem5  26791  bposlem6  26792  bpos  26796  lgsval4a  26822  gausslemma2dlem0c  26861  gausslemma2dlem0d  26862  gausslemma2dlem1a  26868  gausslemma2dlem2  26870  gausslemma2dlem3  26871  gausslemma2dlem5  26874  lgsquadlem1  26883  lgsquadlem2  26884  2lgslem1a1  26892  2sqreunnlem1  26952  2sqreunnltlem  26953  dchrisum0re  27016  dchrisum0lem1  27019  logdivbnd  27059  ostth2lem1  27121  ostth2lem3  27138  pthdlem2lem  29024  crctcshwlkn0lem1  29064  crctcshwlkn0lem3  29066  crctcshwlkn0lem4  29067  crctcshwlkn0lem5  29068  crctcshwlkn0lem6  29069  crctcshwlkn0lem7  29070  crctcshwlkn0  29075  clwlkclwwlkf1lem2  29258  clwwisshclwwslem  29267  clwwlkel  29299  clwwlkf  29300  clwwlkf1  29302  wwlksext2clwwlk  29310  wwlksubclwwlk  29311  eucrctshift  29496  eucrct2eupth  29498  numclwlk2lem2f  29630  nmounbseqi  30030  nmounbseqiALT  30031  nmobndseqi  30032  nmobndseqiALT  30033  ubthlem1  30123  minvecolem3  30129  lnconi  31286  iundisj2f  31821  nnmulge  31963  xrsmulgzz  32179  esumpmono  33077  eulerpartlemb  33367  fibp1  33400  subfaclim  34179  subfacval3  34180  snmlff  34320  fz0n  34700  bcprod  34708  nn0prpwlem  35207  nn0prpw  35208  nndivsub  35342  nndivlub  35343  knoppcnlem2  35370  knoppcnlem4  35372  knoppcnlem10  35378  knoppndvlem11  35398  knoppndvlem12  35399  knoppndvlem14  35401  poimirlem13  36501  poimirlem14  36502  poimirlem31  36519  poimirlem32  36520  mblfinlem2  36526  fzmul  36609  incsequz  36616  nnubfi  36618  nninfnub  36619  2ap1caineq  40961  sticksstones1  40962  metakunt26  41010  metakunt29  41013  metakunt30  41014  factwoffsmonot  41023  nnadddir  41184  nnmul1com  41185  nn0rppwr  41224  nn0expgcd  41226  sn-nnne0  41321  nn0addcom  41323  renegmulnnass  41326  nn0mulcom  41327  zmulcomlem  41328  irrapxlem1  41560  irrapxlem2  41561  pellexlem1  41567  pellexlem5  41571  pellqrex  41617  monotoddzzfi  41681  jm2.24nn  41698  congabseq  41713  acongrep  41719  acongeq  41722  expdiophlem1  41760  idomrootle  41937  idomodle  41938  relexpmulnn  42460  prmunb2  43070  hashnzfzclim  43081  fmuldfeq  44299  sumnnodd  44346  stoweidlem14  44730  stoweidlem17  44733  stoweidlem20  44736  stoweidlem49  44765  stoweidlem60  44776  wallispilem3  44783  wallispilem4  44784  wallispilem5  44785  wallispi  44786  wallispi2lem1  44787  wallispi2lem2  44788  stirlinglem1  44790  stirlinglem3  44792  stirlinglem4  44793  stirlinglem6  44795  stirlinglem7  44796  stirlinglem10  44799  stirlinglem11  44800  stirlinglem12  44801  stirlinglem13  44802  stirlingr  44806  dirker2re  44808  dirkerval2  44810  dirkerre  44811  dirkertrigeqlem1  44814  fourierdlem66  44888  fourierdlem73  44895  fourierdlem83  44905  fourierdlem87  44909  fourierdlem103  44925  fourierdlem104  44926  fourierdlem111  44933  fouriersw  44947  etransclem24  44974  sge0rpcpnf  45137  hoicvr  45264  hoicvrrex  45272  vonioolem2  45397  vonicclem2  45400  fsupdm  45558  finfdm  45562  smfinfdmmbllem  45564  subsubelfzo0  46034  fmtnodvds  46212  2pwp1prm  46257  lighneallem2  46274  nn0oALTV  46364  nneven  46366  nnsum4primes4  46457  nnsum4primesprm  46459  nnsum4primesgbe  46461  nnsum4primesle9  46463  bgoldbachlt  46481  tgoldbach  46485  altgsumbcALT  47029  modn0mul  47206  m1modmmod  47207  difmodm1lt  47208  nnlog2ge0lt1  47252  logbpw2m1  47253  blennn  47261  blennnelnn  47262  nnpw2pmod  47269  nnolog2flm1  47276  digvalnn0  47285  dignn0fr  47287  dignn0ldlem  47288  dignnld  47289  dig2nn1st  47291