Theorem nnred 12222

Description: A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnred.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnred	⊢ (𝜑 → 𝐴 ∈ ℝ)

Proof of Theorem nnred

Step	Hyp	Ref	Expression
1		nnssre 12211	. 2 ⊢ ℕ ⊆ ℝ
2		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3934	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2141  ℝcr 11069  ℕcn 12207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389  ax-un 7714  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-addrcl 11131  ax-mulcl 11132  ax-mulrcl 11133  ax-i2m1 11138  ax-1ne0 11139  ax-rrecex 11142  ax-cnre 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5540  df-eprel 5545  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-pred 6284  df-ord 6345  df-on 6346  df-lim 6347  df-suc 6348  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-ov 7395  df-om 7843  df-2nd 7967  df-frecs 8257  df-wrecs 8288  df-recs 8337  df-rdg 8376  df-nn 12208

This theorem is referenced by:  nnne0  12244  nnadddir  12266  uzwo3  12941  modmulnn  13896  bernneq3  14241  expmulnbnd  14245  expnngt1b  14252  facwordi  14299  faclbnd  14300  faclbnd2  14301  faclbnd3  14302  faclbnd5  14308  faclbnd6  14309  facubnd  14310  facavg  14311  bcp1nk  14327  hashf1  14467  swrds2  14950  isercolllem1  15675  isercoll  15678  o1fsum  15824  climcndslem1  15862  climcndslem2  15863  climcnds  15864  eftabs  16088  efcllem  16090  ege2le3  16103  efcj  16105  eftlub  16124  eflegeo  16136  eirrlem  16219  fzm1ndvds  16339  nno  16399  nnoddm1d2  16403  bitsfzolem  16451  bitsfzo  16452  bitsinv1lem  16458  sadcaddlem  16474  smueqlem  16507  bezoutlem3  16558  bezoutlem4  16559  sqgcd  16579  nn0expgcd  16581  lcmgcdlem  16623  lcmf  16650  prmind2  16702  coprm  16729  prmfac1  16738  prmndvdsfaclt  16743  divdenle  16767  qnumgt0  16768  zsqrtelqelz  16776  hashdvds  16793  eulerthlem2  16800  odzdvds  16814  vfermltl  16820  modprm0  16824  pythagtriplem11  16844  pythagtriplem13  16846  pythagtriplem19  16852  pclem  16857  pcpre1  16861  pcidlem  16891  dvdsprmpweqle  16905  pcadd  16908  pcmpt  16911  pcmpt2  16912  pcfaclem  16917  pcfac  16918  qexpz  16920  pockthlem  16924  pockthg  16925  prmreclem1  16935  prmreclem3  16937  prmreclem4  16938  prmreclem5  16939  1arithlem4  16945  1arith  16946  4sqlem5  16961  4sqlem6  16962  4sqlem10  16966  mul4sqlem  16972  4sqlem11  16974  4sqlem12  16975  4sqlem13  16976  4sqlem14  16977  4sqlem15  16978  4sqlem16  16979  4sqlem17  16980  vdwlem1  17000  vdwlem3  17002  vdwlem6  17005  vdwlem9  17008  vdwlem10  17009  vdwlem12  17011  vdwnnlem3  17016  ramub1lem1  17045  prmolefac  17065  prmgaplem4  17073  prmgaplem5  17074  prmgaplem6  17075  prmgaplem8  17077  2expltfac  17111  cshwshashnsame  17122  setsstruct2  17193  chnub  18637  psgnunilem4  19520  mndodconglem  19564  oddvds  19570  sylow1lem1  19621  sylow1lem5  19625  fislw  19648  efgredlem  19770  gexexlem  19875  zringlpirlem3  21496  prmirredlem  21504  fvmptnn04if  22889  fvmptnn04ifb  22891  fvmptnn04ifc  22892  fvmptnn04ifd  22893  chfacfisf  22894  chfacfisfcpmat  22895  chfacfscmulgsum  22900  chfacfpmmulgsum  22904  lebnumii  25008  lmnn  25305  ovolunlem1a  25538  ovoliunlem1  25544  ovolicc2lem3  25561  ovolicc2lem4  25562  iundisj  25590  voliunlem1  25592  uniioombllem3  25627  dyadf  25633  dyadovol  25635  dyaddisjlem  25637  dyadmaxlem  25639  opnmbllem  25643  vitalilem4  25653  mbfi1fseqlem1  25757  mbfi1fseqlem3  25759  mbfi1fseqlem4  25760  mbfi1fseqlem5  25761  mbfi1fseqlem6  25762  itg2gt0  25802  itg2cnlem2  25804  dgreq0  26305  dgrco  26315  elqaalem2  26361  aaliou3lem2  26384  aaliou3lem8  26386  aaliou3lem9  26391  rtprmirr  26802  leibpi  26984  log2tlbnd  26987  birthdaylem3  26995  amgm  27032  emcllem2  27038  harmonicbnd4  27052  lgamgulmlem1  27070  lgamgulmlem2  27071  lgamgulmlem3  27072  lgamgulmlem4  27073  lgamgulmlem5  27074  lgamgulmlem6  27075  lgamucov  27079  lgamcvg2  27096  wilthlem1  27109  ftalem5  27118  basellem1  27122  basellem2  27123  basellem3  27124  basellem4  27125  basellem5  27126  basellem6  27127  basellem8  27129  chtge0  27153  chtwordi  27197  vma1  27207  dvdsflf1o  27228  dvdsflsumcom  27229  fsumfldivdiaglem  27230  sgmmul  27242  chtublem  27252  fsumvma2  27255  logfac2  27258  chpchtsum  27260  chpub  27261  logfaclbnd  27263  logexprlim  27266  mersenne  27268  perfectlem2  27271  dchrelbas4  27284  bposlem1  27325  bposlem2  27326  bposlem3  27327  bposlem4  27328  bposlem5  27329  bposlem6  27330  bposlem7  27331  bposlem9  27333  lgslem1  27338  lgsval2lem  27348  lgsdirprm  27372  lgsdir  27373  lgsne0  27376  lgsqrlem2  27388  gausslemma2dlem0h  27404  gausslemma2dlem0i  27405  gausslemma2dlem1a  27406  gausslemma2dlem2  27408  gausslemma2dlem7  27414  gausslemma2d  27415  lgseisenlem1  27416  lgseisenlem2  27417  lgseisenlem3  27418  lgseisenlem4  27419  lgseisen  27420  lgsquadlem1  27421  lgsquadlem2  27422  lgsquadlem3  27423  2sqlem3  27461  2sqlem8  27467  2sqblem  27472  2sqmod  27477  chebbnd1lem1  27510  chebbnd1lem3  27512  chtppilimlem1  27514  rplogsumlem1  27525  rplogsumlem2  27526  dchrisum0lem1a  27527  rpvmasumlem  27528  dchrisumlema  27529  dchrisumlem1  27530  dchrisumlem2  27531  dchrisumlem3  27532  dchrvmasumiflem1  27542  dchrisum0flblem2  27550  dchrisum0re  27554  dchrisum0lem1b  27556  dchrisum0lem1  27557  dirith2  27569  selbergb  27590  selberg2lem  27591  logdivbnd  27597  selberg3lem2  27599  selberg4lem1  27601  pntrsumo1  27606  pntrsumbnd2  27608  pntrlog2bndlem1  27618  pntrlog2bndlem2  27619  pntrlog2bndlem3  27620  pntrlog2bndlem4  27621  pntrlog2bndlem5  27622  pntpbnd1a  27626  pntpbnd1  27627  pntibndlem2a  27631  pntibndlem2  27632  pntlemg  27639  pntlemh  27640  pntlemj  27644  pntlemf  27646  ostth2lem1  27659  padicabvf  27672  padicabvcxp  27673  ostth2lem2  27675  ostth2lem3  27676  ostth2lem4  27677  ostth2  27678  ostth3  27679  numclwwlk5  30536  numclwwlk7  30539  nrt2irr  30621  ubthlem2  31020  minvecolem4  31029  iundisjf  32738  ssnnssfz  32939  iundisjfi  32948  nexple  32996  2exple2exp  32997  pfxlsw2ccat  33089  pmtrto1cl  33240  psgnfzto1stlem  33241  fzto1st1  33243  fzto1st  33244  psgnfzto1st  33246  cycpmco2lem6  33272  cycpmco2lem7  33273  fldextrspundgdvdslem  33938  fldextrspundgdvds  33939  fldext2rspun  33940  smatrcl  34054  smattr  34057  smatbl  34058  smatbr  34059  1smat1  34062  submateqlem1  34065  submateqlem2  34066  submateq  34067  esumcst  34321  fiunelros  34432  oddpwdc  34612  eulerpartlems  34618  eulerpartlemgc  34620  fiblem  34656  dstfrvunirn  34733  dstfrvclim1  34736  ballotlemimin  34764  fsum2dsub  34865  reprinfz1  34880  hgt750lemd  34906  hgt750lemb  34914  hgt750leme  34916  tgoldbachgtde  34918  tgoldbachgt  34921  subfaclim  35502  subfacval3  35503  erdszelem7  35511  erdszelem8  35512  erdsze2lem2  35518  cvmliftlem2  35600  cvmliftlem6  35604  cvmliftlem7  35605  cvmliftlem8  35606  cvmliftlem9  35607  cvmliftlem10  35608  cvmliftlem13  35610  bcprod  36052  bccolsum  36053  faclimlem2  36058  faclim2  36062  nn0prpwlem  36646  knoppcnlem10  36904  knoppndvlem15  36928  knoppndvlem17  36930  knoppndvlem18  36931  knoppndvlem19  36932  knoppndvlem20  36933  knoppndvlem21  36934  poimirlem3  38086  poimirlem6  38089  poimirlem7  38090  poimirlem8  38091  poimirlem9  38092  poimirlem10  38093  poimirlem11  38094  poimirlem12  38095  poimirlem13  38096  poimirlem15  38098  poimirlem16  38099  poimirlem17  38100  poimirlem19  38102  poimirlem20  38103  poimirlem21  38104  poimirlem22  38105  poimirlem23  38106  poimirlem26  38109  poimirlem28  38111  opnmbllem0  38119  mblfinlem2  38121  incsequz  38211  nninfnub  38214  lcmineqlem4  42613  lcmineqlem10  42619  lcmineqlem11  42620  lcmineqlem15  42624  lcmineqlem18  42627  lcmineqlem19  42628  lcmineqlem20  42629  lcmineqlem21  42630  lcmineqlem22  42631  lcmineqlem23  42632  lcmineqlem  42633  3lexlogpow5ineq2  42636  3lexlogpow5ineq4  42637  3lexlogpow2ineq2  42640  3lexlogpow5ineq5  42641  aks4d1p1p3  42650  aks4d1p1p2  42651  aks4d1p1p4  42652  aks4d1p1p5  42656  aks4d1p1  42657  aks4d1p3  42659  aks4d1p4  42660  aks4d1p5  42661  aks4d1p6  42662  aks4d1p7  42664  aks4d1p8d2  42666  aks4d1p8  42668  aks4d1p9  42669  posbezout  42681  primrootlekpowne0  42686  primrootspoweq0  42687  aks6d1c1  42697  hashscontpow1  42702  aks6d1c3  42704  aks6d1c4  42705  aks6d1c2lem4  42708  aks6d1c2  42711  aks6d1c5lem1  42717  2ap1caineq  42726  sticksstones1  42727  sticksstones2  42728  sticksstones3  42729  sticksstones6  42732  sticksstones7  42733  sticksstones10  42736  sticksstones12a  42738  sticksstones12  42739  aks6d1c6lem4  42754  bcled  42759  bcle2d  42760  aks6d1c7lem1  42761  aks6d1c7lem2  42762  unitscyglem1  42776  unitscyglem2  42777  unitscyglem4  42779  unitscyglem5  42780  aks5lem8  42782  oexpreposd  42895  fimgmcyclem  43115  fimgmcyc  43116  flt4lem5e  43202  flt4lem6  43204  flt4lem7  43205  fltltc  43207  fltnltalem  43208  fltnlta  43209  3cubeslem3r  43232  irrapxlem3  43365  irrapxlem4  43366  irrapxlem5  43367  pellexlem2  43371  pellexlem6  43375  pell14qrgt0  43400  pell14qrgapw  43417  pellfundgt1  43424  rmspecsqrtnq  43447  ltrmxnn0  43490  jm3.1lem1  43558  jm3.1lem3  43560  dgraa0p  43690  hashnzfz2  44861  rfcnnnub  45580  nnxrd  45817  fzisoeu  45843  fsumnncl  46112  sumnnodd  46170  limsup10exlem  46310  stoweidlem1  46539  stoweidlem3  46541  stoweidlem11  46549  stoweidlem17  46555  stoweidlem20  46558  stoweidlem25  46563  stoweidlem26  46564  stoweidlem34  46572  stoweidlem38  46576  stoweidlem42  46580  stoweidlem44  46582  stoweidlem51  46589  stoweidlem59  46597  stoweidlem60  46598  wallispi  46608  wallispi2  46611  stirlinglem3  46614  stirlinglem4  46615  stirlinglem8  46619  stirlinglem10  46621  stirlinglem12  46623  stirlinglem15  46626  dirkertrigeqlem2  46637  dirkertrigeqlem3  46638  dirkercncflem2  46642  fourierdlem11  46656  fourierdlem14  46659  fourierdlem15  46660  fourierdlem20  46665  fourierdlem31  46676  fourierdlem64  46708  fourierdlem93  46737  fourierdlem95  46739  fourierdlem103  46747  fourierdlem104  46748  fourierdlem112  46756  sqwvfourb  46767  etransclem3  46775  etransclem19  46791  etransclem23  46795  etransclem24  46796  etransclem25  46797  etransclem32  46804  etransclem35  46807  etransclem41  46813  etransclem48  46820  qndenserrnbllem  46832  hoiqssbllem1  47160  hoiqssbllem2  47161  ovolval5lem1  47190  ovolval5lem2  47191  iccpartlt  47994  iccpartgt  47997  odz2prm2pw  48136  fmtnoprmfac1lem  48137  2pwp1prm  48162  sfprmdvdsmersenne  48176  lighneallem2  48179  proththdlem  48186  perfectALTVlem2  48308  gbowge7  48349  ztprmneprm  48933  pgrple2abl  48951  logbpw2m1  49153  nnpw2pmod  49169  nnolog2flm1  49176  blennngt2o2  49178  itcovalt2lem2lem1  49259