Theorem nnre 12257

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℝcr 11116  ℕcn 12250

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7742  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-i2m1 11185  ax-1ne0 11186  ax-rrecex 11189  ax-cnre 11190

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 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7422  df-om 7869  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-nn 12251

This theorem is used by:  nnrei  12259  nnmulcl  12274  nn2ge  12280  nnge1  12281  nngt1ne1  12282  nnle1eq1  12283  nngt0  12284  nnnlt1  12285  nnnle0  12286  nndivre  12294  nnrecgt0  12296  nnsub  12297  nnadddir  12309  nnmul1com  12310  nnunb  12517  arch  12518  nnrecl  12519  bndndx  12520  0mnnnnn0  12553  nnnegz  12611  elnnz  12618  elz2  12626  nnz  12629  gtndiv  12691  prime  12695  btwnz  12717  indstr  12958  qre  12995  elpq  13017  elpqb  13018  rpnnen1lem2  13019  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  nnrp  13046  nnledivrp  13148  qbtwnre  13243  elfzo0le  13751  fzonmapblen  13756  fzo1fzo0n0  13763  ubmelfzo  13778  fzonn0p1p1  13792  ubmelm1fzo  13811  subfzo0  13841  adddivflid  13871  flltdivnn0lt  13886  quoremz  13908  quoremnn0ALT  13910  intfracq  13912  fldiv  13913  modmulnn  13942  m1modnnsub1  13973  addmodid  13975  modifeq2int  13989  modaddmodup  13990  modaddmodlo  13991  modfzo0difsn  13999  modsumfzodifsn  14000  addmodlteq  14002  nnlesq  14261  digit2  14292  digit1  14293  expnngt1  14297  facdiv  14343  facndiv  14344  faclbnd  14346  faclbnd3  14348  faclbnd4lem4  14352  faclbnd5  14354  bcval5  14374  seqcoll  14521  ccatval21sw  14643  cshwidxmod  14866  cshwidxm1  14870  repswcshw  14875  isercolllem1  15742  harmonic  15938  efaddlem  16171  rpnnen2lem9  16302  rpnnen2lem12  16305  sqrt2irr  16329  nndivdvds  16343  dvdsle  16392  fzm1ndvds  16404  nno  16464  nnoddm1d2  16468  divalg2  16487  divalgmod  16488  ndvdsadd  16492  modgcd  16614  gcdzeq  16634  nn0rppwr  16643  sqgcd  16644  nn0expgcd  16646  dvdssqlem  16648  lcmgcdlem  16688  lcmf  16715  coprmgcdb  16731  qredeq  16739  qredeu  16740  isprm3  16765  ge2nprmge4  16784  prmdvdsfz  16788  isprm5  16790  ncoprmlnprm  16811  divdenle  16832  phibndlem  16853  eulerthlem2  16865  hashgcdlem  16871  oddprm  16894  pythagtriplem10  16904  pythagtriplem12  16910  pythagtriplem14  16912  pythagtriplem16  16914  pythagtriplem19  16917  pclem  16922  pc2dvds  16963  pcmpt  16976  fldivp1  16981  pcbc  16984  infpnlem1  16994  infpn2  16997  prmreclem1  17000  prmreclem3  17002  vdwlem3  17067  ram0  17106  prmgaplem4  17138  prmgaplem7  17141  cshwshashlem1  17179  cshwshashlem2  17180  setsstruct2  17258  mulgnegnn  19196  mulgmodid  19225  odmodnn0  19656  gexdvds  19700  sylow3lem6  19748  prmirredlem  21674  znidomb  21763  chfacfisf  23063  chfacfisfcpmat  23064  chfacffsupp  23065  chfacfscmul0  23067  chfacfpmmul0  23071  ovolunlem1a  25708  ovoliunlem2  25715  ovolicc2lem3  25731  ovolicc2lem4  25732  iundisj2  25761  dyadss  25806  volsup2  25817  volivth  25819  vitali  25825  ismbf3d  25866  mbfi1fseqlem3  25929  mbfi1fseqlem4  25930  mbfi1fseqlem5  25931  itg2seq  25954  itg2gt0  25972  itg2cnlem1  25973  idomrootle  26383  plyeq0lem  26420  dgreq0  26475  dgrcolem2  26484  elqaalem2  26534  elqaalem3  26535  logtayllem  26877  leibpi  27160  birthdaylem3  27171  zetacvg  27232  eldmgm  27239  basellem1  27298  basellem2  27299  basellem3  27300  basellem6  27303  basellem9  27306  prmorcht  27395  dvdsflsumcom  27405  muinv  27410  vmalelog  27422  chtublem  27428  logfac2  27434  logfaclbnd  27439  pcbcctr  27493  bcmono  27494  bposlem1  27501  bposlem5  27505  bposlem6  27506  bpos  27510  lgsval4a  27536  gausslemma2dlem0c  27575  gausslemma2dlem0d  27576  gausslemma2dlem1a  27582  gausslemma2dlem2  27584  gausslemma2dlem3  27585  gausslemma2dlem5  27588  lgsquadlem1  27597  lgsquadlem2  27598  2lgslem1a1  27606  2sqreunnlem1  27666  2sqreunnltlem  27667  dchrisum0re  27730  dchrisum0lem1  27733  logdivbnd  27773  ostth2lem1  27835  ostth2lem3  27852  pthdlem2lem  30182  crctcshwlkn0lem1  30228  crctcshwlkn0lem3  30230  crctcshwlkn0lem4  30231  crctcshwlkn0lem5  30232  crctcshwlkn0lem6  30233  crctcshwlkn0lem7  30234  crctcshwlkn0  30239  clwlkclwwlkf1lem2  30425  clwwisshclwwslem  30434  clwwlkel  30466  clwwlkf  30467  clwwlkf1  30469  wwlksext2clwwlk  30477  wwlksubclwwlk  30478  eucrctshift  30667  eucrct2eupth  30669  numclwlk2lem2f  30801  nmounbseqi  31202  nmounbseqiALT  31203  nmobndseqi  31204  nmobndseqiALT  31205  ubthlem1  31295  minvecolem3  31301  lnconi  32458  iundisj2f  33008  nnmulge  33156  xrsmulgzz  33395  esumpmono  34535  eulerpartlemb  34825  fibp1  34858  subfaclim  35719  subfacval3  35720  snmlff  35860  fz0n  36262  bcprod  36269  nn0prpwlem  36892  nn0prpw  36893  nndivsub  37027  nndivlub  37028  knoppcnlem2  37142  knoppcnlem4  37144  knoppndvlem11  37170  knoppndvlem12  37171  knoppndvlem14  37173  poimirlem13  38343  poimirlem14  38344  poimirlem31  38361  poimirlem32  38362  mblfinlem2  38368  fzmul  38452  incsequz  38459  nnubfi  38461  nninfnub  38462  2ap1caineq  42972  sticksstones1  42973  unitscyglem5  43026  sn-nnne0  43294  nn0addcom  43296  renegmulnnass  43299  nn0mulcom  43300  zmulcomlem  43301  fimgmcyc  43362  irrapxlem1  43609  irrapxlem2  43610  pellexlem1  43616  pellexlem5  43620  pellqrex  43666  monotoddzzfi  43729  jm2.24nn  43746  congabseq  43761  acongrep  43767  acongeq  43770  expdiophlem1  43808  idomodle  43978  relexpmulnn  44495  prmunb2  45081  hashnzfzclim  45092  fmuldfeq  46359  sumnnodd  46406  stoweidlem14  46788  stoweidlem17  46791  stoweidlem20  46794  stoweidlem49  46823  stoweidlem60  46834  wallispilem3  46841  wallispilem4  46842  wallispilem5  46843  wallispi  46844  wallispi2lem1  46845  wallispi2lem2  46846  stirlinglem1  46848  stirlinglem3  46850  stirlinglem4  46851  stirlinglem6  46853  stirlinglem7  46854  stirlinglem10  46857  stirlinglem11  46858  stirlinglem12  46859  stirlinglem13  46860  stirlingr  46864  dirker2re  46866  dirkerval2  46868  dirkerre  46869  dirkertrigeqlem1  46872  fourierdlem66  46946  fourierdlem73  46953  fourierdlem83  46963  fourierdlem87  46967  fourierdlem103  46983  fourierdlem104  46984  fourierdlem111  46991  fouriersw  47005  etransclem24  47032  sge0rpcpnf  47195  hoicvr  47322  hoicvrrex  47330  vonioolem2  47455  vonicclem2  47458  fsupdm  47616  finfdm  47620  smfinfdmmbllem  47622  subsubelfzo0  48124  ceilhalfelfzo1  48131  2tceilhalfelfzo1  48133  ceilhalfnn  48137  addmodne  48147  submodlt  48153  modn0mul  48160  m1modmmod  48161  difmodm1lt  48162  modlt0b  48166  fmtnodvds  48356  2pwp1prm  48401  lighneallem2  48418  nn0oALTV  48521  nneven  48523  nnsum4primes4  48614  nnsum4primesprm  48616  nnsum4primesgbe  48618  nnsum4primesle9  48620  bgoldbachlt  48638  tgoldbach  48642  gpgusgralem  48881  gpgedgvtx0  48886  gpg3kgrtriexlem1  48908  gpg3kgrtriexlem2  48909  gpg3kgrtriexlem3  48910  gpg3kgrtriexlem4  48911  gpg3kgrtriexlem6  48913  altgsumbcALT  49192  nnlog2ge0lt1  49405  logbpw2m1  49406  blennn  49414  blennnelnn  49415  nnpw2pmod  49422  nnolog2flm1  49429  digvalnn0  49438  dignn0fr  49440  dignn0ldlem  49441  dignnld  49442  dig2nn1st  49444