Theorem nnre 12300

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11183  ℕcn 12293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-nn 12294

This theorem is referenced by:  nnrei  12302  nnmulcl  12317  nn2ge  12320  nnge1  12321  nngt1ne1  12322  nnle1eq1  12323  nngt0  12324  nnnlt1  12325  nnnle0  12326  nndivre  12334  nnrecgt0  12336  nnsub  12337  nnunb  12549  arch  12550  nnrecl  12551  bndndx  12552  0mnnnnn0  12585  nnnegz  12642  elnnz  12649  elz2  12657  nnz  12660  gtndiv  12720  prime  12724  btwnz  12746  indstr  12981  qre  13018  elpq  13040  elpqb  13041  rpnnen1lem2  13042  rpnnen1lem1  13043  rpnnen1lem3  13044  rpnnen1lem5  13046  nnrp  13068  nnledivrp  13169  qbtwnre  13261  elfzo0le  13760  fzonmapblen  13762  fzo1fzo0n0  13767  ubmelfzo  13781  fzonn0p1p1  13795  ubmelm1fzo  13813  subfzo0  13839  adddivflid  13869  flltdivnn0lt  13884  quoremz  13906  quoremnn0ALT  13908  intfracq  13910  fldiv  13911  modmulnn  13940  m1modnnsub1  13968  addmodid  13970  modifeq2int  13984  modaddmodup  13985  modaddmodlo  13986  modfzo0difsn  13994  modsumfzodifsn  13995  addmodlteq  13997  nnlesq  14254  digit2  14285  digit1  14286  expnngt1  14290  facdiv  14336  facndiv  14337  faclbnd  14339  faclbnd3  14341  faclbnd4lem4  14345  faclbnd5  14347  bcval5  14367  seqcoll  14513  ccatval21sw  14633  cshwidxmod  14851  cshwidxm1  14855  repswcshw  14860  isercolllem1  15713  harmonic  15907  efaddlem  16141  rpnnen2lem9  16270  rpnnen2lem12  16273  sqrt2irr  16297  nndivdvds  16311  dvdsle  16358  fzm1ndvds  16370  nno  16430  nnoddm1d2  16434  divalg2  16453  divalgmod  16454  ndvdsadd  16458  modgcd  16579  gcdzeq  16599  nn0rppwr  16608  sqgcd  16609  nn0expgcd  16611  dvdssqlem  16613  lcmgcdlem  16653  lcmf  16680  coprmgcdb  16696  qredeq  16704  qredeu  16705  isprm3  16730  ge2nprmge4  16748  prmdvdsfz  16752  isprm5  16754  ncoprmlnprm  16775  divdenle  16796  phibndlem  16817  eulerthlem2  16829  hashgcdlem  16835  oddprm  16857  pythagtriplem10  16867  pythagtriplem12  16873  pythagtriplem14  16875  pythagtriplem16  16877  pythagtriplem19  16880  pclem  16885  pc2dvds  16926  pcmpt  16939  fldivp1  16944  pcbc  16947  infpnlem1  16957  infpn2  16960  prmreclem1  16963  prmreclem3  16965  vdwlem3  17030  ram0  17069  prmgaplem4  17101  prmgaplem7  17104  cshwshashlem1  17143  cshwshashlem2  17144  setsstruct2  17221  mulgnegnn  19124  mulgmodid  19153  odmodnn0  19582  gexdvds  19626  sylow3lem6  19674  prmirredlem  21506  znidomb  21603  chfacfisf  22881  chfacfisfcpmat  22882  chfacffsupp  22883  chfacfscmul0  22885  chfacfpmmul0  22889  ovolunlem1a  25550  ovoliunlem2  25557  ovolicc2lem3  25573  ovolicc2lem4  25574  iundisj2  25603  dyadss  25648  volsup2  25659  volivth  25661  vitali  25667  ismbf3d  25708  mbfi1fseqlem3  25772  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  itg2seq  25797  itg2gt0  25815  itg2cnlem1  25816  idomrootle  26232  plyeq0lem  26269  dgreq0  26325  dgrcolem2  26334  elqaalem2  26380  elqaalem3  26381  logtayllem  26719  leibpi  27003  birthdaylem3  27014  zetacvg  27076  eldmgm  27083  basellem1  27142  basellem2  27143  basellem3  27144  basellem6  27147  basellem9  27150  prmorcht  27239  dvdsflsumcom  27249  muinv  27254  vmalelog  27267  chtublem  27273  logfac2  27279  logfaclbnd  27284  pcbcctr  27338  bcmono  27339  bposlem1  27346  bposlem5  27350  bposlem6  27351  bpos  27355  lgsval4a  27381  gausslemma2dlem0c  27420  gausslemma2dlem0d  27421  gausslemma2dlem1a  27427  gausslemma2dlem2  27429  gausslemma2dlem3  27430  gausslemma2dlem5  27433  lgsquadlem1  27442  lgsquadlem2  27443  2lgslem1a1  27451  2sqreunnlem1  27511  2sqreunnltlem  27512  dchrisum0re  27575  dchrisum0lem1  27578  logdivbnd  27618  ostth2lem1  27680  ostth2lem3  27697  pthdlem2lem  29803  crctcshwlkn0lem1  29843  crctcshwlkn0lem3  29845  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  crctcshwlkn0lem6  29848  crctcshwlkn0lem7  29849  crctcshwlkn0  29854  clwlkclwwlkf1lem2  30037  clwwisshclwwslem  30046  clwwlkel  30078  clwwlkf  30079  clwwlkf1  30081  wwlksext2clwwlk  30089  wwlksubclwwlk  30090  eucrctshift  30275  eucrct2eupth  30277  numclwlk2lem2f  30409  nmounbseqi  30809  nmounbseqiALT  30810  nmobndseqi  30811  nmobndseqiALT  30812  ubthlem1  30902  minvecolem3  30908  lnconi  32065  iundisj2f  32612  nnmulge  32752  xrsmulgzz  32992  esumpmono  34043  eulerpartlemb  34333  fibp1  34366  subfaclim  35156  subfacval3  35157  snmlff  35297  fz0n  35693  bcprod  35700  nn0prpwlem  36288  nn0prpw  36289  nndivsub  36423  nndivlub  36424  knoppcnlem2  36460  knoppcnlem4  36462  knoppndvlem11  36488  knoppndvlem12  36489  knoppndvlem14  36491  poimirlem13  37593  poimirlem14  37594  poimirlem31  37611  poimirlem32  37612  mblfinlem2  37618  fzmul  37701  incsequz  37708  nnubfi  37710  nninfnub  37711  2ap1caineq  42102  sticksstones1  42103  unitscyglem5  42156  metakunt26  42187  metakunt29  42190  metakunt30  42191  factwoffsmonot  42199  nnadddir  42259  nnmul1com  42260  sn-nnne0  42424  nn0addcom  42426  renegmulnnass  42429  nn0mulcom  42430  zmulcomlem  42431  fimgmcyc  42489  irrapxlem1  42778  irrapxlem2  42779  pellexlem1  42785  pellexlem5  42789  pellqrex  42835  monotoddzzfi  42899  jm2.24nn  42916  congabseq  42931  acongrep  42937  acongeq  42940  expdiophlem1  42978  idomodle  43152  relexpmulnn  43671  prmunb2  44280  hashnzfzclim  44291  fmuldfeq  45504  sumnnodd  45551  stoweidlem14  45935  stoweidlem17  45938  stoweidlem20  45941  stoweidlem49  45970  stoweidlem60  45981  wallispilem3  45988  wallispilem4  45989  wallispilem5  45990  wallispi  45991  wallispi2lem1  45992  wallispi2lem2  45993  stirlinglem1  45995  stirlinglem3  45997  stirlinglem4  45998  stirlinglem6  46000  stirlinglem7  46001  stirlinglem10  46004  stirlinglem11  46005  stirlinglem12  46006  stirlinglem13  46007  stirlingr  46011  dirker2re  46013  dirkerval2  46015  dirkerre  46016  dirkertrigeqlem1  46019  fourierdlem66  46093  fourierdlem73  46100  fourierdlem83  46110  fourierdlem87  46114  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fouriersw  46152  etransclem24  46179  sge0rpcpnf  46342  hoicvr  46469  hoicvrrex  46477  vonioolem2  46602  vonicclem2  46605  fsupdm  46763  finfdm  46767  smfinfdmmbllem  46769  subsubelfzo0  47241  fmtnodvds  47418  2pwp1prm  47463  lighneallem2  47480  nn0oALTV  47570  nneven  47572  nnsum4primes4  47663  nnsum4primesprm  47665  nnsum4primesgbe  47667  nnsum4primesle9  47669  bgoldbachlt  47687  tgoldbach  47691  altgsumbcALT  48078  modn0mul  48254  m1modmmod  48255  difmodm1lt  48256  nnlog2ge0lt1  48300  logbpw2m1  48301  blennn  48309  blennnelnn  48310  nnpw2pmod  48317  nnolog2flm1  48324  digvalnn0  48333  dignn0fr  48335  dignn0ldlem  48336  dignnld  48337  dig2nn1st  48339