Theorem nnre 11910

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 10801  ℕcn 11903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-i2m1 10870  ax-1ne0 10871  ax-rrecex 10874  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-nn 11904

This theorem is referenced by:  nnrei  11912  nnmulcl  11927  nn2ge  11930  nnge1  11931  nngt1ne1  11932  nnle1eq1  11933  nngt0  11934  nnnlt1  11935  nnnle0  11936  nndivre  11944  nnrecgt0  11946  nnsub  11947  nnunb  12159  arch  12160  nnrecl  12161  bndndx  12162  0mnnnnn0  12195  nnnegz  12252  elnnz  12259  elz2  12267  nnssz  12270  gtndiv  12327  prime  12331  btwnz  12352  indstr  12585  qre  12622  elpq  12644  elpqb  12645  rpnnen1lem2  12646  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem5  12650  nnrp  12670  nnledivrp  12771  qbtwnre  12862  elfzo0le  13359  fzonmapblen  13361  fzo1fzo0n0  13366  ubmelfzo  13380  fzonn0p1p1  13394  ubmelm1fzo  13411  subfzo0  13437  adddivflid  13466  flltdivnn0lt  13481  quoremz  13503  quoremnn0ALT  13505  intfracq  13507  fldiv  13508  modmulnn  13537  m1modnnsub1  13565  addmodid  13567  modifeq2int  13581  modaddmodup  13582  modaddmodlo  13583  modfzo0difsn  13591  modsumfzodifsn  13592  addmodlteq  13594  nnlesq  13850  digit2  13879  digit1  13880  expnngt1  13884  facdiv  13929  facndiv  13930  faclbnd  13932  faclbnd3  13934  faclbnd4lem4  13938  faclbnd5  13940  bcval5  13960  seqcoll  14106  ccatval21sw  14218  cshwidxmod  14444  cshwidxm1  14448  repswcshw  14453  isercolllem1  15304  harmonic  15499  efaddlem  15730  rpnnen2lem9  15859  rpnnen2lem12  15862  sqrt2irr  15886  nndivdvds  15900  dvdsle  15947  fzm1ndvds  15959  nno  16019  nnoddm1d2  16023  divalg2  16042  divalgmod  16043  ndvdsadd  16047  modgcd  16168  gcdmultipleOLD  16188  gcdmultiplezOLD  16189  gcdzeq  16190  sqgcd  16198  dvdssqlem  16199  lcmgcdlem  16239  lcmf  16266  coprmgcdb  16282  qredeq  16290  qredeu  16291  isprm3  16316  ge2nprmge4  16334  prmdvdsfz  16338  isprm5  16340  ncoprmlnprm  16360  divdenle  16381  phibndlem  16399  eulerthlem2  16411  hashgcdlem  16417  oddprm  16439  pythagtriplem10  16449  pythagtriplem12  16455  pythagtriplem14  16457  pythagtriplem16  16459  pythagtriplem19  16462  pclem  16467  pc2dvds  16508  pcmpt  16521  fldivp1  16526  pcbc  16529  infpnlem1  16539  infpn2  16542  prmreclem1  16545  prmreclem3  16547  vdwlem3  16612  ram0  16651  prmgaplem4  16683  prmgaplem7  16686  cshwshashlem1  16725  cshwshashlem2  16726  setsstruct2  16803  mulgnegnn  18629  mulgmodid  18657  odmodnn0  19063  gexdvds  19104  sylow3lem6  19152  prmirredlem  20606  znidomb  20681  chfacfisf  21911  chfacfisfcpmat  21912  chfacffsupp  21913  chfacfscmul0  21915  chfacfpmmul0  21919  ovolunlem1a  24565  ovoliunlem2  24572  ovolicc2lem3  24588  ovolicc2lem4  24589  iundisj2  24618  dyadss  24663  volsup2  24674  volivth  24676  vitali  24682  ismbf3d  24723  mbfi1fseqlem3  24787  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  itg2seq  24812  itg2gt0  24830  itg2cnlem1  24831  plyeq0lem  25276  dgreq0  25331  dgrcolem2  25340  elqaalem2  25385  elqaalem3  25386  logtayllem  25719  leibpi  25997  birthdaylem3  26008  zetacvg  26069  eldmgm  26076  basellem1  26135  basellem2  26136  basellem3  26137  basellem6  26140  basellem9  26143  prmorcht  26232  dvdsflsumcom  26242  muinv  26247  vmalelog  26258  chtublem  26264  logfac2  26270  logfaclbnd  26275  pcbcctr  26329  bcmono  26330  bposlem1  26337  bposlem5  26341  bposlem6  26342  bpos  26346  lgsval4a  26372  gausslemma2dlem0c  26411  gausslemma2dlem0d  26412  gausslemma2dlem1a  26418  gausslemma2dlem2  26420  gausslemma2dlem3  26421  gausslemma2dlem5  26424  lgsquadlem1  26433  lgsquadlem2  26434  2lgslem1a1  26442  2sqreunnlem1  26502  2sqreunnltlem  26503  dchrisum0re  26566  dchrisum0lem1  26569  logdivbnd  26609  ostth2lem1  26671  ostth2lem3  26688  pthdlem2lem  28036  crctcshwlkn0lem1  28076  crctcshwlkn0lem3  28078  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  crctcshwlkn0lem6  28081  crctcshwlkn0lem7  28082  crctcshwlkn0  28087  clwlkclwwlkf1lem2  28270  clwwisshclwwslem  28279  clwwlkel  28311  clwwlkf  28312  clwwlkf1  28314  wwlksext2clwwlk  28322  wwlksubclwwlk  28323  eucrctshift  28508  eucrct2eupth  28510  numclwlk2lem2f  28642  nmounbseqi  29040  nmounbseqiALT  29041  nmobndseqi  29042  nmobndseqiALT  29043  ubthlem1  29133  minvecolem3  29139  lnconi  30296  iundisj2f  30830  nnmulge  30975  xrsmulgzz  31189  esumpmono  31947  eulerpartlemb  32235  fibp1  32268  subfaclim  33050  subfacval3  33051  snmlff  33191  fz0n  33602  bcprod  33610  nn0prpwlem  34438  nn0prpw  34439  nndivsub  34573  nndivlub  34574  knoppcnlem2  34601  knoppcnlem4  34603  knoppcnlem10  34609  knoppndvlem11  34629  knoppndvlem12  34630  knoppndvlem14  34632  poimirlem13  35717  poimirlem14  35718  poimirlem31  35735  poimirlem32  35736  mblfinlem2  35742  fzmul  35826  incsequz  35833  nnubfi  35835  nninfnub  35836  2ap1caineq  40029  sticksstones1  40030  metakunt26  40078  metakunt29  40081  metakunt30  40082  factwoffsmonot  40091  nnadddir  40221  nnmul1com  40222  nn0rppwr  40254  nn0expgcd  40256  irrapxlem1  40560  irrapxlem2  40561  pellexlem1  40567  pellexlem5  40571  pellqrex  40617  monotoddzzfi  40680  jm2.24nn  40697  congabseq  40712  acongrep  40718  acongeq  40721  expdiophlem1  40759  idomrootle  40936  idomodle  40937  relexpmulnn  41206  prmunb2  41818  hashnzfzclim  41829  fmuldfeq  43014  sumnnodd  43061  stoweidlem14  43445  stoweidlem17  43448  stoweidlem20  43451  stoweidlem49  43480  stoweidlem60  43491  wallispilem3  43498  wallispilem4  43499  wallispilem5  43500  wallispi  43501  wallispi2lem1  43502  wallispi2lem2  43503  stirlinglem1  43505  stirlinglem3  43507  stirlinglem4  43508  stirlinglem6  43510  stirlinglem7  43511  stirlinglem10  43514  stirlinglem11  43515  stirlinglem12  43516  stirlinglem13  43517  stirlingr  43521  dirker2re  43523  dirkerval2  43525  dirkerre  43526  dirkertrigeqlem1  43529  fourierdlem66  43603  fourierdlem73  43610  fourierdlem83  43620  fourierdlem87  43624  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fouriersw  43662  etransclem24  43689  sge0rpcpnf  43849  hoicvr  43976  hoicvrrex  43984  vonioolem2  44109  vonicclem2  44112  subsubelfzo0  44706  fmtnodvds  44884  2pwp1prm  44929  lighneallem2  44946  nn0oALTV  45036  nneven  45038  nnsum4primes4  45129  nnsum4primesprm  45131  nnsum4primesgbe  45133  nnsum4primesle9  45135  bgoldbachlt  45153  tgoldbach  45157  altgsumbcALT  45577  modn0mul  45754  m1modmmod  45755  difmodm1lt  45756  nnlog2ge0lt1  45800  logbpw2m1  45801  blennn  45809  blennnelnn  45810  nnpw2pmod  45817  nnolog2flm1  45824  digvalnn0  45833  dignn0fr  45835  dignn0ldlem  45836  dignnld  45837  dig2nn1st  45839