Theorem nnre 11639

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

Syntax hints:   → wi 4   ∈ wcel 2110  ℝcr 10530  ℕcn 11632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-i2m1 10599  ax-1ne0 10600  ax-rrecex 10603  ax-cnre 10604

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7153  df-om 7575  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-nn 11633

This theorem is referenced by:  nnrei  11641  nnmulcl  11655  nn2ge  11658  nnge1  11659  nngt1ne1  11660  nnle1eq1  11661  nngt0  11662  nnnlt1  11663  nnnle0  11664  nndivre  11672  nnrecgt0  11674  nnsub  11675  nnunb  11887  arch  11888  nnrecl  11889  bndndx  11890  0mnnnnn0  11923  nnnegz  11978  elnnz  11985  elz2  11993  nnssz  11996  gtndiv  12053  prime  12057  btwnz  12078  indstr  12310  qre  12347  elpq  12368  elpqb  12369  rpnnen1lem2  12370  rpnnen1lem1  12371  rpnnen1lem3  12372  rpnnen1lem5  12374  nnrp  12394  nnledivrp  12495  qbtwnre  12586  elfzo0le  13075  fzonmapblen  13077  fzo1fzo0n0  13082  ubmelfzo  13096  fzonn0p1p1  13110  ubmelm1fzo  13127  subfzo0  13153  adddivflid  13182  flltdivnn0lt  13197  quoremz  13217  quoremnn0ALT  13219  intfracq  13221  fldiv  13222  modmulnn  13251  m1modnnsub1  13279  addmodid  13281  modifeq2int  13295  modaddmodup  13296  modaddmodlo  13297  modfzo0difsn  13305  modsumfzodifsn  13306  addmodlteq  13308  nnlesq  13562  digit2  13591  digit1  13592  expnngt1  13596  facdiv  13641  facndiv  13642  faclbnd  13644  faclbnd3  13646  faclbnd4lem4  13650  faclbnd5  13652  bcval5  13672  seqcoll  13816  ccatval21sw  13933  cshwidxmod  14159  cshwidxm1  14163  repswcshw  14168  isercolllem1  15015  harmonic  15208  efaddlem  15440  rpnnen2lem9  15569  rpnnen2lem12  15572  sqrt2irr  15596  nndivdvds  15610  dvdsle  15654  fzm1ndvds  15666  nno  15727  nnoddm1d2  15731  divalg2  15750  divalgmod  15751  ndvdsadd  15755  modgcd  15874  gcdmultipleOLD  15894  gcdmultiplezOLD  15895  gcdzeq  15896  sqgcd  15903  dvdssqlem  15904  lcmgcdlem  15944  lcmf  15971  coprmgcdb  15987  qredeq  15995  qredeu  15996  isprm3  16021  ge2nprmge4  16039  prmdvdsfz  16043  isprm5  16045  ncoprmlnprm  16062  divdenle  16083  phibndlem  16101  eulerthlem2  16113  hashgcdlem  16119  oddprm  16141  pythagtriplem10  16151  pythagtriplem12  16157  pythagtriplem14  16159  pythagtriplem16  16161  pythagtriplem19  16164  pclem  16169  pc2dvds  16209  pcmpt  16222  fldivp1  16227  pcbc  16230  infpnlem1  16240  infpn2  16243  prmreclem1  16246  prmreclem3  16248  vdwlem3  16313  ram0  16352  prmgaplem4  16384  prmgaplem7  16387  cshwshashlem1  16423  cshwshashlem2  16424  setsstruct2  16515  mulgnegnn  18232  mulgmodid  18260  odmodnn0  18662  gexdvds  18703  sylow3lem6  18751  prmirredlem  20634  znidomb  20702  chfacfisf  21456  chfacfisfcpmat  21457  chfacffsupp  21458  chfacfscmul0  21460  chfacfpmmul0  21464  ovolunlem1a  24091  ovoliunlem2  24098  ovolicc2lem3  24114  ovolicc2lem4  24115  iundisj2  24144  dyadss  24189  volsup2  24200  volivth  24202  vitali  24208  ismbf3d  24249  mbfi1fseqlem3  24312  mbfi1fseqlem4  24313  mbfi1fseqlem5  24314  itg2seq  24337  itg2gt0  24355  itg2cnlem1  24356  plyeq0lem  24794  dgreq0  24849  dgrcolem2  24858  elqaalem2  24903  elqaalem3  24904  logtayllem  25236  leibpi  25514  birthdaylem3  25525  zetacvg  25586  eldmgm  25593  basellem1  25652  basellem2  25653  basellem3  25654  basellem6  25657  basellem9  25660  prmorcht  25749  dvdsflsumcom  25759  muinv  25764  vmalelog  25775  chtublem  25781  logfac2  25787  logfaclbnd  25792  pcbcctr  25846  bcmono  25847  bposlem1  25854  bposlem5  25858  bposlem6  25859  bpos  25863  lgsval4a  25889  gausslemma2dlem0c  25928  gausslemma2dlem0d  25929  gausslemma2dlem1a  25935  gausslemma2dlem2  25937  gausslemma2dlem3  25938  gausslemma2dlem5  25941  lgsquadlem1  25950  lgsquadlem2  25951  2lgslem1a1  25959  2sqreunnlem1  26019  2sqreunnltlem  26020  dchrisum0re  26083  dchrisum0lem1  26086  logdivbnd  26126  ostth2lem1  26188  ostth2lem3  26205  pthdlem2lem  27542  crctcshwlkn0lem1  27582  crctcshwlkn0lem3  27584  crctcshwlkn0lem4  27585  crctcshwlkn0lem5  27586  crctcshwlkn0lem6  27587  crctcshwlkn0lem7  27588  crctcshwlkn0  27593  clwlkclwwlkf1lem2  27777  clwwisshclwwslem  27786  clwwlkel  27819  clwwlkf  27820  clwwlkf1  27822  wwlksext2clwwlk  27830  wwlksubclwwlk  27831  eucrctshift  28016  eucrct2eupth  28018  numclwlk2lem2f  28150  nmounbseqi  28548  nmounbseqiALT  28549  nmobndseqi  28550  nmobndseqiALT  28551  ubthlem1  28641  minvecolem3  28647  lnconi  29804  iundisj2f  30334  nnmulge  30468  xrsmulgzz  30660  esumpmono  31333  eulerpartlemb  31621  fibp1  31654  subfaclim  32430  subfacval3  32431  snmlff  32571  fz0n  32957  bcprod  32965  nn0prpwlem  33665  nn0prpw  33666  nndivsub  33800  nndivlub  33801  knoppcnlem2  33828  knoppcnlem4  33830  knoppcnlem10  33836  knoppndvlem11  33856  knoppndvlem12  33857  knoppndvlem14  33859  poimirlem13  34899  poimirlem14  34900  poimirlem31  34917  poimirlem32  34918  mblfinlem2  34924  fzmul  35010  incsequz  35017  nnubfi  35019  nninfnub  35020  nnadddir  39156  nnmul1com  39157  nn0rppwr  39175  nn0expgcd  39177  irrapxlem1  39412  irrapxlem2  39413  pellexlem1  39419  pellexlem5  39423  pellqrex  39469  monotoddzzfi  39532  jm2.24nn  39549  congabseq  39564  acongrep  39570  acongeq  39573  expdiophlem1  39611  idomrootle  39788  idomodle  39789  relexpmulnn  40047  prmunb2  40636  hashnzfzclim  40647  fmuldfeq  41857  sumnnodd  41904  stoweidlem14  42293  stoweidlem17  42296  stoweidlem20  42299  stoweidlem49  42328  stoweidlem60  42339  wallispilem3  42346  wallispilem4  42347  wallispilem5  42348  wallispi  42349  wallispi2lem1  42350  wallispi2lem2  42351  stirlinglem1  42353  stirlinglem3  42355  stirlinglem4  42356  stirlinglem6  42358  stirlinglem7  42359  stirlinglem10  42362  stirlinglem11  42363  stirlinglem12  42364  stirlinglem13  42365  stirlingr  42369  dirker2re  42371  dirkerval2  42373  dirkerre  42374  dirkertrigeqlem1  42377  fourierdlem66  42451  fourierdlem73  42458  fourierdlem83  42468  fourierdlem87  42472  fourierdlem103  42488  fourierdlem104  42489  fourierdlem111  42496  fouriersw  42510  etransclem24  42537  sge0rpcpnf  42697  hoicvr  42824  hoicvrrex  42832  vonioolem2  42957  vonicclem2  42960  subsubelfzo0  43520  fmtnodvds  43700  2pwp1prm  43745  lighneallem2  43765  nn0oALTV  43855  nneven  43857  nnsum4primes4  43948  nnsum4primesprm  43950  nnsum4primesgbe  43952  nnsum4primesle9  43954  bgoldbachlt  43972  tgoldbach  43976  altgsumbcALT  44395  modn0mul  44574  m1modmmod  44575  difmodm1lt  44576  nnlog2ge0lt1  44620  logbpw2m1  44621  blennn  44629  blennnelnn  44630  nnpw2pmod  44637  nnolog2flm1  44644  digvalnn0  44653  dignn0fr  44655  dignn0ldlem  44656  dignnld  44657  dig2nn1st  44659