Theorem nnre 12239

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

Syntax hints:   → wi 4   ∈ wcel 2149  ℝcr 11098  ℕcn 12232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-i2m1 11167  ax-1ne0 11168  ax-rrecex 11171  ax-cnre 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-om 7862  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-nn 12233

This theorem is referenced by:  nnrei  12241  nnmulcl  12256  nn2ge  12262  nnge1  12263  nngt1ne1  12264  nnle1eq1  12265  nngt0  12266  nnnlt1  12267  nnnle0  12268  nndivre  12276  nnrecgt0  12278  nnsub  12279  nnadddir  12291  nnmul1com  12292  nnunb  12499  arch  12500  nnrecl  12501  bndndx  12502  0mnnnnn0  12535  nnnegz  12593  elnnz  12600  elz2  12608  nnz  12611  gtndiv  12672  prime  12676  btwnz  12698  indstr  12939  qre  12976  elpq  12998  elpqb  12999  rpnnen1lem2  13000  rpnnen1lem1  13001  rpnnen1lem3  13002  rpnnen1lem5  13004  nnrp  13027  nnledivrp  13129  qbtwnre  13224  elfzo0le  13731  fzonmapblen  13736  fzo1fzo0n0  13743  ubmelfzo  13758  fzonn0p1p1  13772  ubmelm1fzo  13791  subfzo0  13820  adddivflid  13850  flltdivnn0lt  13865  quoremz  13887  quoremnn0ALT  13889  intfracq  13891  fldiv  13892  modmulnn  13921  m1modnnsub1  13952  addmodid  13954  modifeq2int  13968  modaddmodup  13969  modaddmodlo  13970  modfzo0difsn  13978  modsumfzodifsn  13979  addmodlteq  13981  nnlesq  14240  digit2  14271  digit1  14272  expnngt1  14276  facdiv  14322  facndiv  14323  faclbnd  14325  faclbnd3  14327  faclbnd4lem4  14331  faclbnd5  14333  bcval5  14353  seqcoll  14500  ccatval21sw  14622  cshwidxmod  14839  cshwidxm1  14843  repswcshw  14848  isercolllem1  15715  harmonic  15912  efaddlem  16146  rpnnen2lem9  16277  rpnnen2lem12  16280  sqrt2irr  16304  nndivdvds  16318  dvdsle  16367  fzm1ndvds  16379  nno  16439  nnoddm1d2  16443  divalg2  16462  divalgmod  16463  ndvdsadd  16467  modgcd  16589  gcdzeq  16609  nn0rppwr  16618  sqgcd  16619  nn0expgcd  16621  dvdssqlem  16623  lcmgcdlem  16663  lcmf  16690  coprmgcdb  16706  qredeq  16714  qredeu  16715  isprm3  16740  ge2nprmge4  16759  prmdvdsfz  16763  isprm5  16765  ncoprmlnprm  16786  divdenle  16807  phibndlem  16828  eulerthlem2  16840  hashgcdlem  16846  oddprm  16869  pythagtriplem10  16879  pythagtriplem12  16885  pythagtriplem14  16887  pythagtriplem16  16889  pythagtriplem19  16892  pclem  16897  pc2dvds  16938  pcmpt  16951  fldivp1  16956  pcbc  16959  infpnlem1  16969  infpn2  16972  prmreclem1  16975  prmreclem3  16977  vdwlem3  17042  ram0  17081  prmgaplem4  17113  prmgaplem7  17116  cshwshashlem1  17154  cshwshashlem2  17155  setsstruct2  17233  mulgnegnn  19149  mulgmodid  19178  odmodnn0  19609  gexdvds  19653  sylow3lem6  19701  prmirredlem  21590  znidomb  21679  chfacfisf  22979  chfacfisfcpmat  22980  chfacffsupp  22981  chfacfscmul0  22983  chfacfpmmul0  22987  ovolunlem1a  25623  ovoliunlem2  25630  ovolicc2lem3  25646  ovolicc2lem4  25647  iundisj2  25676  dyadss  25721  volsup2  25732  volivth  25734  vitali  25740  ismbf3d  25781  mbfi1fseqlem3  25844  mbfi1fseqlem4  25845  mbfi1fseqlem5  25846  itg2seq  25869  itg2gt0  25887  itg2cnlem1  25888  idomrootle  26298  plyeq0lem  26335  dgreq0  26390  dgrcolem2  26399  elqaalem2  26449  elqaalem3  26450  logtayllem  26789  leibpi  27072  birthdaylem3  27083  zetacvg  27144  eldmgm  27151  basellem1  27210  basellem2  27211  basellem3  27212  basellem6  27215  basellem9  27218  prmorcht  27307  dvdsflsumcom  27317  muinv  27322  vmalelog  27334  chtublem  27340  logfac2  27346  logfaclbnd  27351  pcbcctr  27405  bcmono  27406  bposlem1  27413  bposlem5  27417  bposlem6  27418  bpos  27422  lgsval4a  27448  gausslemma2dlem0c  27487  gausslemma2dlem0d  27488  gausslemma2dlem1a  27494  gausslemma2dlem2  27496  gausslemma2dlem3  27497  gausslemma2dlem5  27500  lgsquadlem1  27509  lgsquadlem2  27510  2lgslem1a1  27518  2sqreunnlem1  27578  2sqreunnltlem  27579  dchrisum0re  27642  dchrisum0lem1  27645  logdivbnd  27685  ostth2lem1  27747  ostth2lem3  27764  pthdlem2lem  30056  crctcshwlkn0lem1  30099  crctcshwlkn0lem3  30101  crctcshwlkn0lem4  30102  crctcshwlkn0lem5  30103  crctcshwlkn0lem6  30104  crctcshwlkn0lem7  30105  crctcshwlkn0  30110  clwlkclwwlkf1lem2  30296  clwwisshclwwslem  30305  clwwlkel  30337  clwwlkf  30338  clwwlkf1  30340  wwlksext2clwwlk  30348  wwlksubclwwlk  30349  eucrctshift  30534  eucrct2eupth  30536  numclwlk2lem2f  30668  nmounbseqi  31069  nmounbseqiALT  31070  nmobndseqi  31071  nmobndseqiALT  31072  ubthlem1  31162  minvecolem3  31168  lnconi  32325  iundisj2f  32875  nnmulge  33024  xrsmulgzz  33269  esumpmono  34413  eulerpartlemb  34702  fibp1  34735  subfaclim  35578  subfacval3  35579  snmlff  35719  fz0n  36121  bcprod  36128  nn0prpwlem  36721  nn0prpw  36722  nndivsub  36856  nndivlub  36857  knoppcnlem2  36971  knoppcnlem4  36973  knoppndvlem11  36999  knoppndvlem12  37000  knoppndvlem14  37002  poimirlem13  38171  poimirlem14  38172  poimirlem31  38189  poimirlem32  38190  mblfinlem2  38196  fzmul  38279  incsequz  38286  nnubfi  38288  nninfnub  38289  2ap1caineq  42801  sticksstones1  42802  unitscyglem5  42855  sn-nnne0  43123  nn0addcom  43125  renegmulnnass  43128  nn0mulcom  43129  zmulcomlem  43130  fimgmcyc  43193  irrapxlem1  43440  irrapxlem2  43441  pellexlem1  43447  pellexlem5  43451  pellqrex  43497  monotoddzzfi  43560  jm2.24nn  43577  congabseq  43592  acongrep  43598  acongeq  43601  expdiophlem1  43639  idomodle  43809  relexpmulnn  44326  prmunb2  44912  hashnzfzclim  44923  fmuldfeq  46190  sumnnodd  46237  stoweidlem14  46619  stoweidlem17  46622  stoweidlem20  46625  stoweidlem49  46654  stoweidlem60  46665  wallispilem3  46672  wallispilem4  46673  wallispilem5  46674  wallispi  46675  wallispi2lem1  46676  wallispi2lem2  46677  stirlinglem1  46679  stirlinglem3  46681  stirlinglem4  46682  stirlinglem6  46684  stirlinglem7  46685  stirlinglem10  46688  stirlinglem11  46689  stirlinglem12  46690  stirlinglem13  46691  stirlingr  46695  dirker2re  46697  dirkerval2  46699  dirkerre  46700  dirkertrigeqlem1  46703  fourierdlem66  46777  fourierdlem73  46784  fourierdlem83  46794  fourierdlem87  46798  fourierdlem103  46814  fourierdlem104  46815  fourierdlem111  46822  fouriersw  46836  etransclem24  46863  sge0rpcpnf  47026  hoicvr  47153  hoicvrrex  47161  vonioolem2  47286  vonicclem2  47289  fsupdm  47447  finfdm  47451  smfinfdmmbllem  47453  subsubelfzo0  47952  ceilhalfelfzo1  47959  2tceilhalfelfzo1  47961  ceilhalfnn  47965  addmodne  47975  submodlt  47981  modn0mul  47988  m1modmmod  47989  difmodm1lt  47990  modlt0b  47994  fmtnodvds  48184  2pwp1prm  48229  lighneallem2  48246  nn0oALTV  48349  nneven  48351  nnsum4primes4  48442  nnsum4primesprm  48444  nnsum4primesgbe  48446  nnsum4primesle9  48448  bgoldbachlt  48466  tgoldbach  48470  gpgusgralem  48709  gpgedgvtx0  48714  gpg3kgrtriexlem1  48736  gpg3kgrtriexlem2  48737  gpg3kgrtriexlem3  48738  gpg3kgrtriexlem4  48739  gpg3kgrtriexlem6  48741  altgsumbcALT  49017  nnlog2ge0lt1  49230  logbpw2m1  49231  blennn  49239  blennnelnn  49240  nnpw2pmod  49247  nnolog2flm1  49254  digvalnn0  49263  dignn0fr  49265  dignn0ldlem  49266  dignnld  49267  dig2nn1st  49269