Theorem nnre 12175

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11031  ℕcn 12168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-un 7683  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-i2m1 11100  ax-1ne0 11101  ax-rrecex 11104  ax-cnre 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7364  df-om 7812  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-nn 12169

This theorem is referenced by:  nnrei  12177  nnmulcl  12192  nn2ge  12198  nnge1  12199  nngt1ne1  12200  nnle1eq1  12201  nngt0  12202  nnnlt1  12203  nnnle0  12204  nndivre  12212  nnrecgt0  12214  nnsub  12215  nnadddir  12227  nnmul1com  12228  nnunb  12427  arch  12428  nnrecl  12429  bndndx  12430  0mnnnnn0  12463  nnnegz  12521  elnnz  12528  elz2  12536  nnz  12539  gtndiv  12600  prime  12604  btwnz  12626  indstr  12860  qre  12897  elpq  12919  elpqb  12920  rpnnen1lem2  12921  rpnnen1lem1  12922  rpnnen1lem3  12923  rpnnen1lem5  12925  nnrp  12948  nnledivrp  13050  qbtwnre  13145  elfzo0le  13652  fzonmapblen  13657  fzo1fzo0n0  13664  ubmelfzo  13679  fzonn0p1p1  13693  ubmelm1fzo  13712  subfzo0  13741  adddivflid  13771  flltdivnn0lt  13786  quoremz  13808  quoremnn0ALT  13810  intfracq  13812  fldiv  13813  modmulnn  13842  m1modnnsub1  13873  addmodid  13875  modifeq2int  13889  modaddmodup  13890  modaddmodlo  13891  modfzo0difsn  13899  modsumfzodifsn  13900  addmodlteq  13902  nnlesq  14161  digit2  14192  digit1  14193  expnngt1  14197  facdiv  14243  facndiv  14244  faclbnd  14246  faclbnd3  14248  faclbnd4lem4  14252  faclbnd5  14254  bcval5  14274  seqcoll  14420  ccatval21sw  14542  cshwidxmod  14759  cshwidxm1  14763  repswcshw  14768  isercolllem1  15621  harmonic  15818  efaddlem  16052  rpnnen2lem9  16183  rpnnen2lem12  16186  sqrt2irr  16210  nndivdvds  16224  dvdsle  16273  fzm1ndvds  16285  nno  16345  nnoddm1d2  16349  divalg2  16368  divalgmod  16369  ndvdsadd  16373  modgcd  16495  gcdzeq  16515  nn0rppwr  16524  sqgcd  16525  nn0expgcd  16527  dvdssqlem  16529  lcmgcdlem  16569  lcmf  16596  coprmgcdb  16612  qredeq  16620  qredeu  16621  isprm3  16646  ge2nprmge4  16665  prmdvdsfz  16669  isprm5  16671  ncoprmlnprm  16692  divdenle  16713  phibndlem  16734  eulerthlem2  16746  hashgcdlem  16752  oddprm  16775  pythagtriplem10  16785  pythagtriplem12  16791  pythagtriplem14  16793  pythagtriplem16  16795  pythagtriplem19  16798  pclem  16803  pc2dvds  16844  pcmpt  16857  fldivp1  16862  pcbc  16865  infpnlem1  16875  infpn2  16878  prmreclem1  16881  prmreclem3  16883  vdwlem3  16948  ram0  16987  prmgaplem4  17019  prmgaplem7  17022  cshwshashlem1  17060  cshwshashlem2  17061  setsstruct2  17138  mulgnegnn  19054  mulgmodid  19083  odmodnn0  19509  gexdvds  19553  sylow3lem6  19601  prmirredlem  21465  znidomb  21554  chfacfisf  22832  chfacfisfcpmat  22833  chfacffsupp  22834  chfacfscmul0  22836  chfacfpmmul0  22840  ovolunlem1a  25476  ovoliunlem2  25483  ovolicc2lem3  25499  ovolicc2lem4  25500  iundisj2  25529  dyadss  25574  volsup2  25585  volivth  25587  vitali  25593  ismbf3d  25634  mbfi1fseqlem3  25697  mbfi1fseqlem4  25698  mbfi1fseqlem5  25699  itg2seq  25722  itg2gt0  25740  itg2cnlem1  25741  idomrootle  26151  plyeq0lem  26188  dgreq0  26243  dgrcolem2  26252  elqaalem2  26300  elqaalem3  26301  logtayllem  26639  leibpi  26922  birthdaylem3  26933  zetacvg  26995  eldmgm  27002  basellem1  27061  basellem2  27062  basellem3  27063  basellem6  27066  basellem9  27069  prmorcht  27158  dvdsflsumcom  27168  muinv  27173  vmalelog  27185  chtublem  27191  logfac2  27197  logfaclbnd  27202  pcbcctr  27256  bcmono  27257  bposlem1  27264  bposlem5  27268  bposlem6  27269  bpos  27273  lgsval4a  27299  gausslemma2dlem0c  27338  gausslemma2dlem0d  27339  gausslemma2dlem1a  27345  gausslemma2dlem2  27347  gausslemma2dlem3  27348  gausslemma2dlem5  27351  lgsquadlem1  27360  lgsquadlem2  27361  2lgslem1a1  27369  2sqreunnlem1  27429  2sqreunnltlem  27430  dchrisum0re  27493  dchrisum0lem1  27496  logdivbnd  27536  ostth2lem1  27598  ostth2lem3  27615  pthdlem2lem  29853  crctcshwlkn0lem1  29896  crctcshwlkn0lem3  29898  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  crctcshwlkn0lem6  29901  crctcshwlkn0lem7  29902  crctcshwlkn0  29907  clwlkclwwlkf1lem2  30093  clwwisshclwwslem  30102  clwwlkel  30134  clwwlkf  30135  clwwlkf1  30137  wwlksext2clwwlk  30145  wwlksubclwwlk  30146  eucrctshift  30331  eucrct2eupth  30333  numclwlk2lem2f  30465  nmounbseqi  30866  nmounbseqiALT  30867  nmobndseqi  30868  nmobndseqiALT  30869  ubthlem1  30959  minvecolem3  30965  lnconi  32122  iundisj2f  32678  nnmulge  32830  xrsmulgzz  33087  esumpmono  34242  eulerpartlemb  34531  fibp1  34564  subfaclim  35389  subfacval3  35390  snmlff  35530  fz0n  35932  bcprod  35939  nn0prpwlem  36523  nn0prpw  36524  nndivsub  36658  nndivlub  36659  knoppcnlem2  36773  knoppcnlem4  36775  knoppndvlem11  36801  knoppndvlem12  36802  knoppndvlem14  36804  poimirlem13  37971  poimirlem14  37972  poimirlem31  37989  poimirlem32  37990  mblfinlem2  37996  fzmul  38079  incsequz  38086  nnubfi  38088  nninfnub  38089  2ap1caineq  42601  sticksstones1  42602  unitscyglem5  42655  sn-nnne0  42922  nn0addcom  42924  renegmulnnass  42927  nn0mulcom  42928  zmulcomlem  42929  fimgmcyc  42996  irrapxlem1  43271  irrapxlem2  43272  pellexlem1  43278  pellexlem5  43282  pellqrex  43328  monotoddzzfi  43391  jm2.24nn  43408  congabseq  43423  acongrep  43429  acongeq  43432  expdiophlem1  43470  idomodle  43640  relexpmulnn  44157  prmunb2  44759  hashnzfzclim  44770  fmuldfeq  46034  sumnnodd  46081  stoweidlem14  46463  stoweidlem17  46466  stoweidlem20  46469  stoweidlem49  46498  stoweidlem60  46509  wallispilem3  46516  wallispilem4  46517  wallispilem5  46518  wallispi  46519  wallispi2lem1  46520  wallispi2lem2  46521  stirlinglem1  46523  stirlinglem3  46525  stirlinglem4  46526  stirlinglem6  46528  stirlinglem7  46529  stirlinglem10  46532  stirlinglem11  46533  stirlinglem12  46534  stirlinglem13  46535  stirlingr  46539  dirker2re  46541  dirkerval2  46543  dirkerre  46544  dirkertrigeqlem1  46547  fourierdlem66  46621  fourierdlem73  46628  fourierdlem83  46638  fourierdlem87  46642  fourierdlem103  46658  fourierdlem104  46659  fourierdlem111  46666  fouriersw  46680  etransclem24  46707  sge0rpcpnf  46870  hoicvr  46997  hoicvrrex  47005  vonioolem2  47130  vonicclem2  47133  fsupdm  47291  finfdm  47295  smfinfdmmbllem  47297  subsubelfzo0  47790  ceilhalfelfzo1  47797  2tceilhalfelfzo1  47799  ceilhalfnn  47803  addmodne  47813  submodlt  47819  modn0mul  47826  m1modmmod  47827  difmodm1lt  47828  modlt0b  47832  fmtnodvds  48022  2pwp1prm  48067  lighneallem2  48084  nn0oALTV  48187  nneven  48189  nnsum4primes4  48280  nnsum4primesprm  48282  nnsum4primesgbe  48284  nnsum4primesle9  48286  bgoldbachlt  48304  tgoldbach  48308  gpgusgralem  48547  gpgedgvtx0  48552  gpg3kgrtriexlem1  48574  gpg3kgrtriexlem2  48575  gpg3kgrtriexlem3  48576  gpg3kgrtriexlem4  48577  gpg3kgrtriexlem6  48579  altgsumbcALT  48844  nnlog2ge0lt1  49057  logbpw2m1  49058  blennn  49066  blennnelnn  49067  nnpw2pmod  49074  nnolog2flm1  49081  digvalnn0  49090  dignn0fr  49092  dignn0ldlem  49093  dignnld  49094  dig2nn1st  49096