Theorem nnre 12349

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 12346	. 2 ⊢ ℕ ⊆ ℝ
2	1	sseli 3905	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℝcr 11206  ℕcn 12342

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391  ax-un 7755  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-i2m1 11275  ax-1ne0 11276  ax-rrecex 11279  ax-cnre 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7427  df-om 7882  df-2nd 8006  df-frecs 8307  df-wrecs 8338  df-recs 8387  df-rdg 8426  df-nn 12343

This theorem is used by:  nnrei  12351  nnmulcl  12366  nn2ge  12372  nnge1  12373  nngt1ne1  12374  nnle1eq1  12375  nngt0  12376  nnnlt1  12377  nnnle0  12378  nndivre  12386  nnrecgt0  12388  nnsub  12389  nnadddir  12401  nnmul1com  12402  nnunb  12609  arch  12610  nnrecl  12611  bndndx  12612  0mnnnnn0  12645  nnnegz  12703  elnnz  12710  elz2  12718  nnz  12721  gtndiv  12783  prime  12787  btwnz  12809  indstr  13050  qre  13087  elpq  13110  elpqb  13111  rpnnen1lem2  13112  rpnnen1lem1  13113  rpnnen1lem3  13114  rpnnen1lem5  13116  nnrp  13139  nnledivrp  13241  qbtwnre  13336  elfzo0le  13845  fzonmapblen  13850  fzo1fzo0n0  13857  ubmelfzo  13872  fzonn0p1p1  13886  ubmelm1fzo  13905  subfzo0  13935  adddivflid  13965  flltdivnn0lt  13980  quoremz  14002  quoremnn0ALT  14004  intfracq  14006  fldiv  14007  modmulnn  14036  m1modnnsub1  14067  addmodid  14069  modifeq2int  14083  modaddmodup  14084  modaddmodlo  14085  modfzo0difsn  14093  modsumfzodifsn  14094  addmodlteq  14096  nnlesq  14356  digit2  14387  digit1  14388  expnngt1  14392  facdiv  14438  facndiv  14439  faclbnd  14441  faclbnd3  14443  faclbnd4lem4  14447  faclbnd5  14449  bcval5  14469  seqcoll  14616  ccatval21sw  14738  cshwidxmod  14962  cshwidxm1  14966  repswcshw  14971  isercolllem1  15841  harmonic  16037  efaddlem  16268  rpnnen2lem9  16399  rpnnen2lem12  16402  sqrt2irr  16426  nndivdvds  16440  dvdsle  16489  fzm1ndvds  16501  nno  16561  nnoddm1d2  16565  divalg2  16584  divalgmod  16585  ndvdsadd  16589  modgcd  16714  gcdzeq  16734  nn0rppwr  16744  sqgcd  16745  nn0expgcd  16747  lcmgcdlem  16790  lcmf  16817  coprmgcdb  16833  qredeq  16841  qredeu  16842  isprm3  16867  ge2nprmge4  16886  prmdvdsfz  16890  isprm5  16892  ncoprmlnprm  16913  divdenle  16934  phibndlem  16956  eulerthlem2  16968  hashgcdlem  16974  oddprm  16997  pythagtriplem10  17007  pythagtriplem12  17013  pythagtriplem14  17015  pythagtriplem16  17017  pythagtriplem19  17020  pclem  17025  pc2dvds  17066  pcmpt  17079  fldivp1  17084  pcbc  17087  infpnlem1  17097  infpn2  17100  prmreclem1  17103  prmreclem3  17105  vdwlem3  17170  ram0  17209  prmgaplem4  17241  prmgaplem7  17244  cshwshashlem1  17282  cshwshashlem2  17283  setsstruct2  17361  mulgnegnn  19303  mulgmodid  19332  odmodnn0  19763  gexdvds  19807  sylow3lem6  19855  prmirredlem  21787  znidomb  21876  chfacfisf  23181  chfacfisfcpmat  23182  chfacffsupp  23183  chfacfscmul0  23185  chfacfpmmul0  23189  ovolunlem1a  25826  ovoliunlem2  25833  ovolicc2lem3  25849  ovolicc2lem4  25850  iundisj2  25879  dyadss  25924  volsup2  25935  volivth  25937  vitali  25943  ismbf3d  25984  mbfi1fseqlem3  26047  mbfi1fseqlem4  26048  mbfi1fseqlem5  26049  itg2seq  26072  itg2gt0  26090  itg2cnlem1  26091  idomrootle  26500  plyeq0lem  26538  dgreq0  26593  dgrcolem2  26602  elqaalem2  26652  elqaalem3  26653  logtayllem  26996  leibpi  27279  birthdaylem3  27290  zetacvg  27351  eldmgm  27358  basellem1  27417  basellem2  27418  basellem3  27419  basellem6  27422  basellem9  27425  prmorcht  27514  dvdsflsumcom  27524  muinv  27529  vmalelog  27541  chtublem  27547  logfac2  27553  logfaclbnd  27558  pcbcctr  27612  bcmono  27613  bposlem1  27620  bposlem5  27624  bposlem6  27625  bpos  27629  lgsval4a  27655  gausslemma2dlem0c  27694  gausslemma2dlem0d  27695  gausslemma2dlem1a  27701  gausslemma2dlem2  27703  gausslemma2dlem3  27704  gausslemma2dlem5  27707  lgsquadlem1  27716  lgsquadlem2  27717  2lgslem1a1  27725  2sqreunnlem1  27785  2sqreunnltlem  27786  dchrisum0re  27849  dchrisum0lem1  27852  logdivbnd  27892  ostth2lem1  27954  ostth2lem3  27971  pthdlem2lem  30362  crctcshwlkn0lem1  30408  crctcshwlkn0lem3  30410  crctcshwlkn0lem4  30411  crctcshwlkn0lem5  30412  crctcshwlkn0lem6  30413  crctcshwlkn0lem7  30414  crctcshwlkn0  30419  clwlkclwwlkf1lem2  30605  clwwisshclwwslem  30614  clwwlkel  30646  clwwlkf  30647  clwwlkf1  30649  wwlksext2clwwlk  30657  wwlksubclwwlk  30658  eucrctshift  30853  eucrct2eupth  30855  numclwlk2lem2f  30987  nmounbseqi  31388  nmounbseqiALT  31389  nmobndseqi  31390  nmobndseqiALT  31391  ubthlem1  31481  minvecolem3  31487  lnconi  32644  iundisj2f  33235  nnmulge  33381  xrsmulgzz  33620  esumpmono  34761  eulerpartlemb  35050  fibp1  35083  subfaclim  36071  subfacval3  36072  snmlff  36212  fz0n  36620  bcprod  36627  nn0prpwlem  37234  nn0prpw  37235  nndivsub  37369  nndivlub  37370  knoppcnlem2  37484  knoppcnlem4  37486  knoppndvlem11  37512  knoppndvlem12  37513  knoppndvlem14  37515  poimirlem13  38688  poimirlem14  38689  poimirlem31  38706  poimirlem32  38707  mblfinlem2  38713  fzmul  38812  incsequz  38819  nnubfi  38821  nninfnub  38822  2ap1caineq  43332  sticksstones1  43333  unitscyglem5  43386  sn-nnne0  43661  nn0addcom  43663  renegmulnnass  43666  nn0mulcom  43667  zmulcomlem  43668  fimgmcyc  43735  irrapxlem1  43966  irrapxlem2  43967  pellexlem1  43973  pellexlem5  43977  pellqrex  44023  monotoddzzfi  44086  jm2.24nn  44103  congabseq  44118  acongrep  44124  acongeq  44127  expdiophlem1  44165  idomodle  44330  relexpmulnn  44846  prmunb2  45432  hashnzfzclim  45443  fmuldfeq  46731  sumnnodd  46778  stoweidlem14  47160  stoweidlem17  47163  stoweidlem20  47166  stoweidlem49  47195  stoweidlem60  47206  wallispilem3  47213  wallispilem4  47214  wallispilem5  47215  wallispi  47216  wallispi2lem1  47217  wallispi2lem2  47218  stirlinglem1  47220  stirlinglem3  47222  stirlinglem4  47223  stirlinglem6  47225  stirlinglem7  47226  stirlinglem10  47229  stirlinglem11  47230  stirlinglem12  47231  stirlinglem13  47232  stirlingr  47236  dirker2re  47238  dirkerval2  47240  dirkerre  47241  dirkertrigeqlem1  47244  fourierdlem66  47318  fourierdlem73  47325  fourierdlem83  47335  fourierdlem87  47339  fourierdlem103  47355  fourierdlem104  47356  fourierdlem111  47363  fouriersw  47377  etransclem24  47404  sge0rpcpnf  47567  hoicvr  47694  hoicvrrex  47702  vonioolem2  47827  vonicclem2  47830  fsupdm  47988  finfdm  47992  smfinfdmmbllem  47994  subsubelfzo0  48533  ceilhalfelfzo1  48540  2tceilhalfelfzo1  48542  ceilhalfnn  48546  addmodne  48556  submodlt  48562  modn0mul  48569  m1modmmod  48570  difmodm1lt  48571  modlt0b  48575  fmtnodvds  48765  2pwp1prm  48810  lighneallem2  48827  nn0oALTV  48930  nneven  48932  nnsum4primes4  49023  nnsum4primesprm  49025  nnsum4primesgbe  49027  nnsum4primesle9  49029  bgoldbachlt  49047  tgoldbach  49051  gpgusgralem  49290  gpgedgvtx0  49295  gpg3kgrtriexlem1  49317  gpg3kgrtriexlem2  49318  gpg3kgrtriexlem3  49319  gpg3kgrtriexlem4  49320  gpg3kgrtriexlem6  49322  altgsumbcALT  49601  nnlog2ge0lt1  49814  logbpw2m1  49815  blennn  49823  blennnelnn  49824  nnpw2pmod  49831  nnolog2flm1  49838  digvalnn0  49847  dignn0fr  49849  dignn0ldlem  49850  dignnld  49851  dig2nn1st  49853