Theorem nnre 12217

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

Syntax hints:   → wi 4   ∈ wcel 2142  ℝcr 11072  ℕcn 12210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-un 7718  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-i2m1 11141  ax-1ne0 11142  ax-rrecex 11145  ax-cnre 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-om 7847  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-nn 12211

This theorem is referenced by:  nnrei  12219  nnmulcl  12234  nn2ge  12240  nnge1  12241  nngt1ne1  12242  nnle1eq1  12243  nngt0  12244  nnnlt1  12245  nnnle0  12246  nndivre  12254  nnrecgt0  12256  nnsub  12257  nnadddir  12269  nnmul1com  12270  nnunb  12477  arch  12478  nnrecl  12479  bndndx  12480  0mnnnnn0  12513  nnnegz  12571  elnnz  12578  elz2  12586  nnz  12589  gtndiv  12650  prime  12654  btwnz  12676  indstr  12917  qre  12954  elpq  12976  elpqb  12977  rpnnen1lem2  12978  rpnnen1lem1  12979  rpnnen1lem3  12980  rpnnen1lem5  12982  nnrp  13005  nnledivrp  13107  qbtwnre  13202  elfzo0le  13709  fzonmapblen  13714  fzo1fzo0n0  13721  ubmelfzo  13736  fzonn0p1p1  13750  ubmelm1fzo  13769  subfzo0  13798  adddivflid  13828  flltdivnn0lt  13843  quoremz  13865  quoremnn0ALT  13867  intfracq  13869  fldiv  13870  modmulnn  13899  m1modnnsub1  13930  addmodid  13932  modifeq2int  13946  modaddmodup  13947  modaddmodlo  13948  modfzo0difsn  13956  modsumfzodifsn  13957  addmodlteq  13959  nnlesq  14218  digit2  14249  digit1  14250  expnngt1  14254  facdiv  14300  facndiv  14301  faclbnd  14303  faclbnd3  14305  faclbnd4lem4  14309  faclbnd5  14311  bcval5  14331  seqcoll  14477  ccatval21sw  14599  cshwidxmod  14816  cshwidxm1  14820  repswcshw  14825  isercolllem1  15692  harmonic  15889  efaddlem  16123  rpnnen2lem9  16254  rpnnen2lem12  16257  sqrt2irr  16281  nndivdvds  16295  dvdsle  16344  fzm1ndvds  16356  nno  16416  nnoddm1d2  16420  divalg2  16439  divalgmod  16440  ndvdsadd  16444  modgcd  16566  gcdzeq  16586  nn0rppwr  16595  sqgcd  16596  nn0expgcd  16598  dvdssqlem  16600  lcmgcdlem  16640  lcmf  16667  coprmgcdb  16683  qredeq  16691  qredeu  16692  isprm3  16717  ge2nprmge4  16736  prmdvdsfz  16740  isprm5  16742  ncoprmlnprm  16763  divdenle  16784  phibndlem  16805  eulerthlem2  16817  hashgcdlem  16823  oddprm  16846  pythagtriplem10  16856  pythagtriplem12  16862  pythagtriplem14  16864  pythagtriplem16  16866  pythagtriplem19  16869  pclem  16874  pc2dvds  16915  pcmpt  16928  fldivp1  16933  pcbc  16936  infpnlem1  16946  infpn2  16949  prmreclem1  16952  prmreclem3  16954  vdwlem3  17019  ram0  17058  prmgaplem4  17090  prmgaplem7  17093  cshwshashlem1  17131  cshwshashlem2  17132  setsstruct2  17210  mulgnegnn  19126  mulgmodid  19155  odmodnn0  19580  gexdvds  19624  sylow3lem6  19672  prmirredlem  21524  znidomb  21613  chfacfisf  22914  chfacfisfcpmat  22915  chfacffsupp  22916  chfacfscmul0  22918  chfacfpmmul0  22922  ovolunlem1a  25558  ovoliunlem2  25565  ovolicc2lem3  25581  ovolicc2lem4  25582  iundisj2  25611  dyadss  25656  volsup2  25667  volivth  25669  vitali  25675  ismbf3d  25716  mbfi1fseqlem3  25779  mbfi1fseqlem4  25780  mbfi1fseqlem5  25781  itg2seq  25804  itg2gt0  25822  itg2cnlem1  25823  idomrootle  26233  plyeq0lem  26270  dgreq0  26325  dgrcolem2  26334  elqaalem2  26384  elqaalem3  26385  logtayllem  26724  leibpi  27007  birthdaylem3  27018  zetacvg  27079  eldmgm  27086  basellem1  27145  basellem2  27146  basellem3  27147  basellem6  27150  basellem9  27153  prmorcht  27242  dvdsflsumcom  27252  muinv  27257  vmalelog  27269  chtublem  27275  logfac2  27281  logfaclbnd  27286  pcbcctr  27340  bcmono  27341  bposlem1  27348  bposlem5  27352  bposlem6  27353  bpos  27357  lgsval4a  27383  gausslemma2dlem0c  27422  gausslemma2dlem0d  27423  gausslemma2dlem1a  27429  gausslemma2dlem2  27431  gausslemma2dlem3  27432  gausslemma2dlem5  27435  lgsquadlem1  27444  lgsquadlem2  27445  2lgslem1a1  27453  2sqreunnlem1  27513  2sqreunnltlem  27514  dchrisum0re  27577  dchrisum0lem1  27580  logdivbnd  27620  ostth2lem1  27682  ostth2lem3  27699  pthdlem2lem  29967  crctcshwlkn0lem1  30010  crctcshwlkn0lem3  30012  crctcshwlkn0lem4  30013  crctcshwlkn0lem5  30014  crctcshwlkn0lem6  30015  crctcshwlkn0lem7  30016  crctcshwlkn0  30021  clwlkclwwlkf1lem2  30207  clwwisshclwwslem  30216  clwwlkel  30248  clwwlkf  30249  clwwlkf1  30251  wwlksext2clwwlk  30259  wwlksubclwwlk  30260  eucrctshift  30445  eucrct2eupth  30447  numclwlk2lem2f  30579  nmounbseqi  30980  nmounbseqiALT  30981  nmobndseqi  30982  nmobndseqiALT  30983  ubthlem1  31073  minvecolem3  31079  lnconi  32236  iundisj2f  32790  nnmulge  32941  xrsmulgzz  33187  esumpmono  34376  eulerpartlemb  34665  fibp1  34698  subfaclim  35538  subfacval3  35539  snmlff  35679  fz0n  36081  bcprod  36088  nn0prpwlem  36682  nn0prpw  36683  nndivsub  36817  nndivlub  36818  knoppcnlem2  36932  knoppcnlem4  36934  knoppndvlem11  36960  knoppndvlem12  36961  knoppndvlem14  36963  poimirlem13  38132  poimirlem14  38133  poimirlem31  38150  poimirlem32  38151  mblfinlem2  38157  fzmul  38240  incsequz  38247  nnubfi  38249  nninfnub  38250  2ap1caineq  42762  sticksstones1  42763  unitscyglem5  42816  sn-nnne0  43082  nn0addcom  43084  renegmulnnass  43087  nn0mulcom  43088  zmulcomlem  43089  fimgmcyc  43152  irrapxlem1  43399  irrapxlem2  43400  pellexlem1  43406  pellexlem5  43410  pellqrex  43456  monotoddzzfi  43519  jm2.24nn  43536  congabseq  43551  acongrep  43557  acongeq  43560  expdiophlem1  43598  idomodle  43768  relexpmulnn  44285  prmunb2  44887  hashnzfzclim  44898  fmuldfeq  46159  sumnnodd  46206  stoweidlem14  46588  stoweidlem17  46591  stoweidlem20  46594  stoweidlem49  46623  stoweidlem60  46634  wallispilem3  46641  wallispilem4  46642  wallispilem5  46643  wallispi  46644  wallispi2lem1  46645  wallispi2lem2  46646  stirlinglem1  46648  stirlinglem3  46650  stirlinglem4  46651  stirlinglem6  46653  stirlinglem7  46654  stirlinglem10  46657  stirlinglem11  46658  stirlinglem12  46659  stirlinglem13  46660  stirlingr  46664  dirker2re  46666  dirkerval2  46668  dirkerre  46669  dirkertrigeqlem1  46672  fourierdlem66  46746  fourierdlem73  46753  fourierdlem83  46763  fourierdlem87  46767  fourierdlem103  46783  fourierdlem104  46784  fourierdlem111  46791  fouriersw  46805  etransclem24  46832  sge0rpcpnf  46995  hoicvr  47122  hoicvrrex  47130  vonioolem2  47255  vonicclem2  47258  fsupdm  47416  finfdm  47420  smfinfdmmbllem  47422  subsubelfzo0  47921  ceilhalfelfzo1  47928  2tceilhalfelfzo1  47930  ceilhalfnn  47934  addmodne  47944  submodlt  47950  modn0mul  47957  m1modmmod  47958  difmodm1lt  47959  modlt0b  47963  fmtnodvds  48153  2pwp1prm  48198  lighneallem2  48215  nn0oALTV  48318  nneven  48320  nnsum4primes4  48411  nnsum4primesprm  48413  nnsum4primesgbe  48415  nnsum4primesle9  48417  bgoldbachlt  48435  tgoldbach  48439  gpgusgralem  48678  gpgedgvtx0  48683  gpg3kgrtriexlem1  48705  gpg3kgrtriexlem2  48706  gpg3kgrtriexlem3  48707  gpg3kgrtriexlem4  48708  gpg3kgrtriexlem6  48710  altgsumbcALT  48975  nnlog2ge0lt1  49188  logbpw2m1  49189  blennn  49197  blennnelnn  49198  nnpw2pmod  49205  nnolog2flm1  49212  digvalnn0  49221  dignn0fr  49223  dignn0ldlem  49224  dignnld  49225  dig2nn1st  49227