Theorem nnre 12235

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

Syntax hints:   → wi 4   ∈ wcel 2099  ℝcr 11123  ℕcn 12228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7732  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-i2m1 11192  ax-1ne0 11193  ax-rrecex 11196  ax-cnre 11197

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-om 7863  df-2nd 7986  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-nn 12229

This theorem is referenced by:  nnrei  12237  nnmulcl  12252  nn2ge  12255  nnge1  12256  nngt1ne1  12257  nnle1eq1  12258  nngt0  12259  nnnlt1  12260  nnnle0  12261  nndivre  12269  nnrecgt0  12271  nnsub  12272  nnunb  12484  arch  12485  nnrecl  12486  bndndx  12487  0mnnnnn0  12520  nnnegz  12577  elnnz  12584  elz2  12592  nnz  12595  gtndiv  12655  prime  12659  btwnz  12681  indstr  12916  qre  12953  elpq  12975  elpqb  12976  rpnnen1lem2  12977  rpnnen1lem1  12978  rpnnen1lem3  12979  rpnnen1lem5  12981  nnrp  13003  nnledivrp  13104  qbtwnre  13196  elfzo0le  13694  fzonmapblen  13696  fzo1fzo0n0  13701  ubmelfzo  13715  fzonn0p1p1  13729  ubmelm1fzo  13746  subfzo0  13772  adddivflid  13801  flltdivnn0lt  13816  quoremz  13838  quoremnn0ALT  13840  intfracq  13842  fldiv  13843  modmulnn  13872  m1modnnsub1  13900  addmodid  13902  modifeq2int  13916  modaddmodup  13917  modaddmodlo  13918  modfzo0difsn  13926  modsumfzodifsn  13927  addmodlteq  13929  nnlesq  14186  digit2  14216  digit1  14217  expnngt1  14221  facdiv  14264  facndiv  14265  faclbnd  14267  faclbnd3  14269  faclbnd4lem4  14273  faclbnd5  14275  bcval5  14295  seqcoll  14443  ccatval21sw  14553  cshwidxmod  14771  cshwidxm1  14775  repswcshw  14780  isercolllem1  15629  harmonic  15823  efaddlem  16055  rpnnen2lem9  16184  rpnnen2lem12  16187  sqrt2irr  16211  nndivdvds  16225  dvdsle  16272  fzm1ndvds  16284  nno  16344  nnoddm1d2  16348  divalg2  16367  divalgmod  16368  ndvdsadd  16372  modgcd  16493  gcdzeq  16513  sqgcd  16521  dvdssqlem  16522  lcmgcdlem  16562  lcmf  16589  coprmgcdb  16605  qredeq  16613  qredeu  16614  isprm3  16639  ge2nprmge4  16657  prmdvdsfz  16661  isprm5  16663  ncoprmlnprm  16685  divdenle  16706  phibndlem  16724  eulerthlem2  16736  hashgcdlem  16742  oddprm  16764  pythagtriplem10  16774  pythagtriplem12  16780  pythagtriplem14  16782  pythagtriplem16  16784  pythagtriplem19  16787  pclem  16792  pc2dvds  16833  pcmpt  16846  fldivp1  16851  pcbc  16854  infpnlem1  16864  infpn2  16867  prmreclem1  16870  prmreclem3  16872  vdwlem3  16937  ram0  16976  prmgaplem4  17008  prmgaplem7  17011  cshwshashlem1  17050  cshwshashlem2  17051  setsstruct2  17128  mulgnegnn  19023  mulgmodid  19052  odmodnn0  19479  gexdvds  19523  sylow3lem6  19571  prmirredlem  21378  znidomb  21475  chfacfisf  22730  chfacfisfcpmat  22731  chfacffsupp  22732  chfacfscmul0  22734  chfacfpmmul0  22738  ovolunlem1a  25399  ovoliunlem2  25406  ovolicc2lem3  25422  ovolicc2lem4  25423  iundisj2  25452  dyadss  25497  volsup2  25508  volivth  25510  vitali  25516  ismbf3d  25557  mbfi1fseqlem3  25621  mbfi1fseqlem4  25622  mbfi1fseqlem5  25623  itg2seq  25646  itg2gt0  25664  itg2cnlem1  25665  idomrootle  26081  plyeq0lem  26118  dgreq0  26174  dgrcolem2  26183  elqaalem2  26229  elqaalem3  26230  logtayllem  26567  leibpi  26848  birthdaylem3  26859  zetacvg  26921  eldmgm  26928  basellem1  26987  basellem2  26988  basellem3  26989  basellem6  26992  basellem9  26995  prmorcht  27084  dvdsflsumcom  27094  muinv  27099  vmalelog  27112  chtublem  27118  logfac2  27124  logfaclbnd  27129  pcbcctr  27183  bcmono  27184  bposlem1  27191  bposlem5  27195  bposlem6  27196  bpos  27200  lgsval4a  27226  gausslemma2dlem0c  27265  gausslemma2dlem0d  27266  gausslemma2dlem1a  27272  gausslemma2dlem2  27274  gausslemma2dlem3  27275  gausslemma2dlem5  27278  lgsquadlem1  27287  lgsquadlem2  27288  2lgslem1a1  27296  2sqreunnlem1  27356  2sqreunnltlem  27357  dchrisum0re  27420  dchrisum0lem1  27423  logdivbnd  27463  ostth2lem1  27525  ostth2lem3  27542  pthdlem2lem  29555  crctcshwlkn0lem1  29595  crctcshwlkn0lem3  29597  crctcshwlkn0lem4  29598  crctcshwlkn0lem5  29599  crctcshwlkn0lem6  29600  crctcshwlkn0lem7  29601  crctcshwlkn0  29606  clwlkclwwlkf1lem2  29789  clwwisshclwwslem  29798  clwwlkel  29830  clwwlkf  29831  clwwlkf1  29833  wwlksext2clwwlk  29841  wwlksubclwwlk  29842  eucrctshift  30027  eucrct2eupth  30029  numclwlk2lem2f  30161  nmounbseqi  30561  nmounbseqiALT  30562  nmobndseqi  30563  nmobndseqiALT  30564  ubthlem1  30654  minvecolem3  30660  lnconi  31817  iundisj2f  32352  nnmulge  32491  xrsmulgzz  32705  esumpmono  33621  eulerpartlemb  33911  fibp1  33944  subfaclim  34721  subfacval3  34722  snmlff  34862  fz0n  35248  bcprod  35255  nn0prpwlem  35729  nn0prpw  35730  nndivsub  35864  nndivlub  35865  knoppcnlem2  35892  knoppcnlem4  35894  knoppndvlem11  35920  knoppndvlem12  35921  knoppndvlem14  35923  poimirlem13  37028  poimirlem14  37029  poimirlem31  37046  poimirlem32  37047  mblfinlem2  37053  fzmul  37136  incsequz  37143  nnubfi  37145  nninfnub  37146  2ap1caineq  41536  sticksstones1  41537  metakunt26  41589  metakunt29  41592  metakunt30  41593  factwoffsmonot  41601  nnadddir  41757  nnmul1com  41758  nn0rppwr  41805  nn0expgcd  41807  sn-nnne0  41915  nn0addcom  41917  renegmulnnass  41920  nn0mulcom  41921  zmulcomlem  41922  irrapxlem1  42154  irrapxlem2  42155  pellexlem1  42161  pellexlem5  42165  pellqrex  42211  monotoddzzfi  42275  jm2.24nn  42292  congabseq  42307  acongrep  42313  acongeq  42316  expdiophlem1  42354  idomodle  42531  relexpmulnn  43052  prmunb2  43661  hashnzfzclim  43672  fmuldfeq  44884  sumnnodd  44931  stoweidlem14  45315  stoweidlem17  45318  stoweidlem20  45321  stoweidlem49  45350  stoweidlem60  45361  wallispilem3  45368  wallispilem4  45369  wallispilem5  45370  wallispi  45371  wallispi2lem1  45372  wallispi2lem2  45373  stirlinglem1  45375  stirlinglem3  45377  stirlinglem4  45378  stirlinglem6  45380  stirlinglem7  45381  stirlinglem10  45384  stirlinglem11  45385  stirlinglem12  45386  stirlinglem13  45387  stirlingr  45391  dirker2re  45393  dirkerval2  45395  dirkerre  45396  dirkertrigeqlem1  45399  fourierdlem66  45473  fourierdlem73  45480  fourierdlem83  45490  fourierdlem87  45494  fourierdlem103  45510  fourierdlem104  45511  fourierdlem111  45518  fouriersw  45532  etransclem24  45559  sge0rpcpnf  45722  hoicvr  45849  hoicvrrex  45857  vonioolem2  45982  vonicclem2  45985  fsupdm  46143  finfdm  46147  smfinfdmmbllem  46149  subsubelfzo0  46619  fmtnodvds  46797  2pwp1prm  46842  lighneallem2  46859  nn0oALTV  46949  nneven  46951  nnsum4primes4  47042  nnsum4primesprm  47044  nnsum4primesgbe  47046  nnsum4primesle9  47048  bgoldbachlt  47066  tgoldbach  47070  altgsumbcALT  47330  modn0mul  47506  m1modmmod  47507  difmodm1lt  47508  nnlog2ge0lt1  47552  logbpw2m1  47553  blennn  47561  blennnelnn  47562  nnpw2pmod  47569  nnolog2flm1  47576  digvalnn0  47585  dignn0fr  47587  dignn0ldlem  47588  dignnld  47589  dig2nn1st  47591