Theorem nnre 12382

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℝcr 11238  ℕcn 12375

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-i2m1 11307  ax-1ne0 11308  ax-rrecex 11311  ax-cnre 11312

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-nn 12376

This theorem is used by:  nnrei  12384  nnmulcl  12399  nn2ge  12405  nnge1  12406  nngt1ne1  12407  nnle1eq1  12408  nngt0  12409  nnnlt1  12410  nnnle0  12411  nndivre  12419  nnrecgt0  12421  nnsub  12422  nnadddir  12434  nnmul1com  12435  nnunb  12642  arch  12643  nnrecl  12644  bndndx  12645  0mnnnnn0  12678  nnnegz  12736  elnnz  12743  elz2  12751  nnz  12754  gtndiv  12816  prime  12820  btwnz  12842  indstr  13083  qre  13120  elpq  13143  elpqb  13144  rpnnen1lem2  13145  rpnnen1lem1  13146  rpnnen1lem3  13147  rpnnen1lem5  13149  nnrp  13172  nnledivrp  13274  qbtwnre  13369  elfzo0le  13878  fzonmapblen  13883  fzo1fzo0n0  13890  ubmelfzo  13905  fzonn0p1p1  13919  ubmelm1fzo  13938  subfzo0  13968  adddivflid  13998  flltdivnn0lt  14013  quoremz  14035  quoremnn0ALT  14037  intfracq  14039  fldiv  14040  modmulnn  14069  m1modnnsub1  14100  addmodid  14102  modifeq2int  14116  modaddmodup  14117  modaddmodlo  14118  modfzo0difsn  14126  modsumfzodifsn  14127  addmodlteq  14129  nnlesq  14389  digit2  14421  digit1  14422  expnngt1  14426  facdiv  14472  facndiv  14473  faclbnd  14475  faclbnd3  14477  faclbnd4lem4  14481  faclbnd5  14483  bcval5  14503  seqcoll  14650  ccatval21sw  14772  cshwidxmod  14996  cshwidxm1  15000  repswcshw  15005  isercolllem1  15876  harmonic  16072  efaddlem  16303  rpnnen2lem9  16434  rpnnen2lem12  16437  sqrt2irr  16461  nndivdvds  16475  dvdsle  16524  fzm1ndvds  16536  nno  16596  nnoddm1d2  16600  divalg2  16619  divalgmod  16620  ndvdsadd  16624  modgcd  16749  gcdzeq  16769  nn0rppwr  16779  sqgcd  16780  nn0expgcd  16782  lcmgcdlem  16825  lcmf  16852  coprmgcdb  16868  qredeq  16876  qredeu  16877  isprm3  16902  ge2nprmge4  16921  prmdvdsfz  16925  isprm5  16927  ncoprmlnprm  16948  divdenle  16969  phibndlem  16991  eulerthlem2  17003  hashgcdlem  17009  oddprm  17032  pythagtriplem10  17042  pythagtriplem12  17048  pythagtriplem14  17050  pythagtriplem16  17052  pythagtriplem19  17055  pclem  17060  pc2dvds  17101  pcmpt  17114  fldivp1  17119  pcbc  17122  infpnlem1  17132  infpn2  17135  prmreclem1  17138  prmreclem3  17140  vdwlem3  17205  ram0  17244  prmgaplem4  17276  prmgaplem7  17279  cshwshashlem1  17317  cshwshashlem2  17318  setsstruct2  17396  mulgnegnn  19344  mulgmodid  19373  odmodnn0  19805  gexdvds  19849  sylow3lem6  19897  prmirredlem  21833  znidomb  21922  chfacfisf  23227  chfacfisfcpmat  23228  chfacffsupp  23229  chfacfscmul0  23231  chfacfpmmul0  23235  ovolunlem1a  25872  ovoliunlem2  25879  ovolicc2lem3  25895  ovolicc2lem4  25896  iundisj2  25925  dyadss  25970  volsup2  25981  volivth  25983  vitali  25989  ismbf3d  26030  mbfi1fseqlem3  26093  mbfi1fseqlem4  26094  mbfi1fseqlem5  26095  itg2seq  26118  itg2gt0  26136  itg2cnlem1  26137  idomrootle  26546  plyeq0lem  26584  dgreq0  26639  dgrcolem2  26648  elqaalem2  26700  elqaalem3  26701  logtayllem  27044  leibpi  27327  birthdaylem3  27338  zetacvg  27399  eldmgm  27406  basellem1  27465  basellem2  27466  basellem3  27467  basellem6  27470  basellem9  27473  prmorcht  27562  dvdsflsumcom  27572  muinv  27577  vmalelog  27589  chtublem  27595  logfac2  27601  logfaclbnd  27606  pcbcctr  27660  bcmono  27661  bposlem1  27668  bposlem5  27672  bposlem6  27673  bpos  27677  lgsval4a  27703  gausslemma2dlem0c  27742  gausslemma2dlem0d  27743  gausslemma2dlem1a  27749  gausslemma2dlem2  27751  gausslemma2dlem3  27752  gausslemma2dlem5  27755  lgsquadlem1  27764  lgsquadlem2  27765  2lgslem1a1  27773  2sqreunnlem1  27833  2sqreunnltlem  27834  dchrisum0re  27897  dchrisum0lem1  27900  logdivbnd  27940  ostth2lem1  28002  ostth2lem3  28019  pthdlem2lem  30410  crctcshwlkn0lem1  30456  crctcshwlkn0lem3  30458  crctcshwlkn0lem4  30459  crctcshwlkn0lem5  30460  crctcshwlkn0lem6  30461  crctcshwlkn0lem7  30462  crctcshwlkn0  30467  clwlkclwwlkf1lem2  30653  clwwisshclwwslem  30662  clwwlkel  30694  clwwlkf  30695  clwwlkf1  30697  wwlksext2clwwlk  30705  wwlksubclwwlk  30706  eucrctshift  30901  eucrct2eupth  30903  numclwlk2lem2f  31035  nmounbseqi  31436  nmounbseqiALT  31437  nmobndseqi  31438  nmobndseqiALT  31439  ubthlem1  31529  minvecolem3  31535  lnconi  32692  iundisj2f  33282  nnmulge  33427  xrsmulgzz  33669  esumpmono  34822  eulerpartlemb  35111  fibp1  35144  subfaclim  36161  subfacval3  36162  snmlff  36302  fz0n  36711  bcprod  36718  nn0prpwlem  37325  nn0prpw  37326  nndivsub  37460  nndivlub  37461  knoppcnlem2  37575  knoppcnlem4  37577  knoppndvlem11  37603  knoppndvlem12  37604  knoppndvlem14  37606  poimirlem13  38819  poimirlem14  38820  poimirlem31  38837  poimirlem32  38838  mblfinlem2  38844  fzmul  38941  incsequz  38948  nnubfi  38950  nninfnub  38951  2ap1caineq  43461  sticksstones1  43462  unitscyglem5  43515  sn-nnne0  43790  nn0addcom  43792  renegmulnnass  43795  nn0mulcom  43796  zmulcomlem  43797  fimgmcyc  43864  irrapxlem1  44095  irrapxlem2  44096  pellexlem1  44102  pellexlem5  44106  pellqrex  44152  monotoddzzfi  44215  jm2.24nn  44232  congabseq  44247  acongrep  44253  acongeq  44256  expdiophlem1  44294  idomodle  44454  relexpmulnn  44970  prmunb2  45556  hashnzfzclim  45567  fmuldfeq  46868  sumnnodd  46915  stoweidlem14  47297  stoweidlem17  47300  stoweidlem20  47303  stoweidlem49  47332  stoweidlem60  47343  wallispilem3  47350  wallispilem4  47351  wallispilem5  47352  wallispi  47353  wallispi2lem1  47354  wallispi2lem2  47355  stirlinglem1  47357  stirlinglem3  47359  stirlinglem4  47360  stirlinglem6  47362  stirlinglem7  47363  stirlinglem10  47366  stirlinglem11  47367  stirlinglem12  47368  stirlinglem13  47369  stirlingr  47373  dirker2re  47375  dirkerval2  47377  dirkerre  47378  dirkertrigeqlem1  47381  fourierdlem66  47455  fourierdlem73  47462  fourierdlem83  47472  fourierdlem87  47476  fourierdlem103  47492  fourierdlem104  47493  fourierdlem111  47500  fouriersw  47514  etransclem24  47541  sge0rpcpnf  47704  hoicvr  47831  hoicvrrex  47839  vonioolem2  47964  vonicclem2  47967  fsupdm  48125  finfdm  48129  smfinfdmmbllem  48131  subsubelfzo0  48670  ceilhalfelfzo1  48677  2tceilhalfelfzo1  48679  ceilhalfnn  48683  addmodne  48693  submodlt  48699  modn0mul  48706  m1modmmod  48707  difmodm1lt  48708  modlt0b  48712  fmtnodvds  48902  2pwp1prm  48947  lighneallem2  48964  nn0oALTV  49067  nneven  49069  nnsum4primes4  49160  nnsum4primesprm  49162  nnsum4primesgbe  49164  nnsum4primesle9  49166  bgoldbachlt  49184  tgoldbach  49188  gpgusgralem  49427  gpgedgvtx0  49432  gpg3kgrtriexlem1  49454  gpg3kgrtriexlem2  49455  gpg3kgrtriexlem3  49456  gpg3kgrtriexlem4  49457  gpg3kgrtriexlem6  49459  altgsumbcALT  49796  nnlog2ge0lt1  50009  logbpw2m1  50010  blennn  50018  blennnelnn  50019  nnpw2pmod  50026  nnolog2flm1  50033  digvalnn0  50042  dignn0fr  50044  dignn0ldlem  50045  dignnld  50046  dig2nn1st  50048