Theorem nnre 12215

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℝcr 11105  ℕcn 12208

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-i2m1 11174  ax-1ne0 11175  ax-rrecex 11178  ax-cnre 11179

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-nn 12209

This theorem is referenced by:  nnrei  12217  nnmulcl  12232  nn2ge  12235  nnge1  12236  nngt1ne1  12237  nnle1eq1  12238  nngt0  12239  nnnlt1  12240  nnnle0  12241  nndivre  12249  nnrecgt0  12251  nnsub  12252  nnunb  12464  arch  12465  nnrecl  12466  bndndx  12467  0mnnnnn0  12500  nnnegz  12557  elnnz  12564  elz2  12572  nnz  12575  gtndiv  12635  prime  12639  btwnz  12661  indstr  12896  qre  12933  elpq  12955  elpqb  12956  rpnnen1lem2  12957  rpnnen1lem1  12958  rpnnen1lem3  12959  rpnnen1lem5  12961  nnrp  12981  nnledivrp  13082  qbtwnre  13174  elfzo0le  13672  fzonmapblen  13674  fzo1fzo0n0  13679  ubmelfzo  13693  fzonn0p1p1  13707  ubmelm1fzo  13724  subfzo0  13750  adddivflid  13779  flltdivnn0lt  13794  quoremz  13816  quoremnn0ALT  13818  intfracq  13820  fldiv  13821  modmulnn  13850  m1modnnsub1  13878  addmodid  13880  modifeq2int  13894  modaddmodup  13895  modaddmodlo  13896  modfzo0difsn  13904  modsumfzodifsn  13905  addmodlteq  13907  nnlesq  14165  digit2  14195  digit1  14196  expnngt1  14200  facdiv  14243  facndiv  14244  faclbnd  14246  faclbnd3  14248  faclbnd4lem4  14252  faclbnd5  14254  bcval5  14274  seqcoll  14421  ccatval21sw  14531  cshwidxmod  14749  cshwidxm1  14753  repswcshw  14758  isercolllem1  15607  harmonic  15801  efaddlem  16032  rpnnen2lem9  16161  rpnnen2lem12  16164  sqrt2irr  16188  nndivdvds  16202  dvdsle  16249  fzm1ndvds  16261  nno  16321  nnoddm1d2  16325  divalg2  16344  divalgmod  16345  ndvdsadd  16349  modgcd  16470  gcdzeq  16490  sqgcd  16498  dvdssqlem  16499  lcmgcdlem  16539  lcmf  16566  coprmgcdb  16582  qredeq  16590  qredeu  16591  isprm3  16616  ge2nprmge4  16634  prmdvdsfz  16638  isprm5  16640  ncoprmlnprm  16660  divdenle  16681  phibndlem  16699  eulerthlem2  16711  hashgcdlem  16717  oddprm  16739  pythagtriplem10  16749  pythagtriplem12  16755  pythagtriplem14  16757  pythagtriplem16  16759  pythagtriplem19  16762  pclem  16767  pc2dvds  16808  pcmpt  16821  fldivp1  16826  pcbc  16829  infpnlem1  16839  infpn2  16842  prmreclem1  16845  prmreclem3  16847  vdwlem3  16912  ram0  16951  prmgaplem4  16983  prmgaplem7  16986  cshwshashlem1  17025  cshwshashlem2  17026  setsstruct2  17103  mulgnegnn  18958  mulgmodid  18987  odmodnn0  19402  gexdvds  19446  sylow3lem6  19494  prmirredlem  21033  znidomb  21108  chfacfisf  22347  chfacfisfcpmat  22348  chfacffsupp  22349  chfacfscmul0  22351  chfacfpmmul0  22355  ovolunlem1a  25004  ovoliunlem2  25011  ovolicc2lem3  25027  ovolicc2lem4  25028  iundisj2  25057  dyadss  25102  volsup2  25113  volivth  25115  vitali  25121  ismbf3d  25162  mbfi1fseqlem3  25226  mbfi1fseqlem4  25227  mbfi1fseqlem5  25228  itg2seq  25251  itg2gt0  25269  itg2cnlem1  25270  plyeq0lem  25715  dgreq0  25770  dgrcolem2  25779  elqaalem2  25824  elqaalem3  25825  logtayllem  26158  leibpi  26436  birthdaylem3  26447  zetacvg  26508  eldmgm  26515  basellem1  26574  basellem2  26575  basellem3  26576  basellem6  26579  basellem9  26582  prmorcht  26671  dvdsflsumcom  26681  muinv  26686  vmalelog  26697  chtublem  26703  logfac2  26709  logfaclbnd  26714  pcbcctr  26768  bcmono  26769  bposlem1  26776  bposlem5  26780  bposlem6  26781  bpos  26785  lgsval4a  26811  gausslemma2dlem0c  26850  gausslemma2dlem0d  26851  gausslemma2dlem1a  26857  gausslemma2dlem2  26859  gausslemma2dlem3  26860  gausslemma2dlem5  26863  lgsquadlem1  26872  lgsquadlem2  26873  2lgslem1a1  26881  2sqreunnlem1  26941  2sqreunnltlem  26942  dchrisum0re  27005  dchrisum0lem1  27008  logdivbnd  27048  ostth2lem1  27110  ostth2lem3  27127  pthdlem2lem  29013  crctcshwlkn0lem1  29053  crctcshwlkn0lem3  29055  crctcshwlkn0lem4  29056  crctcshwlkn0lem5  29057  crctcshwlkn0lem6  29058  crctcshwlkn0lem7  29059  crctcshwlkn0  29064  clwlkclwwlkf1lem2  29247  clwwisshclwwslem  29256  clwwlkel  29288  clwwlkf  29289  clwwlkf1  29291  wwlksext2clwwlk  29299  wwlksubclwwlk  29300  eucrctshift  29485  eucrct2eupth  29487  numclwlk2lem2f  29619  nmounbseqi  30017  nmounbseqiALT  30018  nmobndseqi  30019  nmobndseqiALT  30020  ubthlem1  30110  minvecolem3  30116  lnconi  31273  iundisj2f  31808  nnmulge  31950  xrsmulgzz  32166  esumpmono  33065  eulerpartlemb  33355  fibp1  33388  subfaclim  34167  subfacval3  34168  snmlff  34308  fz0n  34688  bcprod  34696  nn0prpwlem  35195  nn0prpw  35196  nndivsub  35330  nndivlub  35331  knoppcnlem2  35358  knoppcnlem4  35360  knoppcnlem10  35366  knoppndvlem11  35386  knoppndvlem12  35387  knoppndvlem14  35389  poimirlem13  36489  poimirlem14  36490  poimirlem31  36507  poimirlem32  36508  mblfinlem2  36514  fzmul  36597  incsequz  36604  nnubfi  36606  nninfnub  36607  2ap1caineq  40949  sticksstones1  40950  metakunt26  40998  metakunt29  41001  metakunt30  41002  factwoffsmonot  41011  nnadddir  41181  nnmul1com  41182  nn0rppwr  41219  nn0expgcd  41221  sn-nnne0  41317  nn0addcom  41319  renegmulnnass  41322  nn0mulcom  41323  zmulcomlem  41324  irrapxlem1  41545  irrapxlem2  41546  pellexlem1  41552  pellexlem5  41556  pellqrex  41602  monotoddzzfi  41666  jm2.24nn  41683  congabseq  41698  acongrep  41704  acongeq  41707  expdiophlem1  41745  idomrootle  41922  idomodle  41923  relexpmulnn  42445  prmunb2  43055  hashnzfzclim  43066  fmuldfeq  44285  sumnnodd  44332  stoweidlem14  44716  stoweidlem17  44719  stoweidlem20  44722  stoweidlem49  44751  stoweidlem60  44762  wallispilem3  44769  wallispilem4  44770  wallispilem5  44771  wallispi  44772  wallispi2lem1  44773  wallispi2lem2  44774  stirlinglem1  44776  stirlinglem3  44778  stirlinglem4  44779  stirlinglem6  44781  stirlinglem7  44782  stirlinglem10  44785  stirlinglem11  44786  stirlinglem12  44787  stirlinglem13  44788  stirlingr  44792  dirker2re  44794  dirkerval2  44796  dirkerre  44797  dirkertrigeqlem1  44800  fourierdlem66  44874  fourierdlem73  44881  fourierdlem83  44891  fourierdlem87  44895  fourierdlem103  44911  fourierdlem104  44912  fourierdlem111  44919  fouriersw  44933  etransclem24  44960  sge0rpcpnf  45123  hoicvr  45250  hoicvrrex  45258  vonioolem2  45383  vonicclem2  45386  fsupdm  45544  finfdm  45548  smfinfdmmbllem  45550  subsubelfzo0  46020  fmtnodvds  46198  2pwp1prm  46243  lighneallem2  46260  nn0oALTV  46350  nneven  46352  nnsum4primes4  46443  nnsum4primesprm  46445  nnsum4primesgbe  46447  nnsum4primesle9  46449  bgoldbachlt  46467  tgoldbach  46471  altgsumbcALT  46982  modn0mul  47159  m1modmmod  47160  difmodm1lt  47161  nnlog2ge0lt1  47205  logbpw2m1  47206  blennn  47214  blennnelnn  47215  nnpw2pmod  47222  nnolog2flm1  47229  digvalnn0  47238  dignn0fr  47240  dignn0ldlem  47241  dignnld  47242  dig2nn1st  47244