Theorem nnred 12253

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 12242	. 2 ⊢ ℕ ⊆ ℝ
2		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3956	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11126  ℕcn 12238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7727  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rrecex 11199  ax-cnre 11200

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-ov 7406  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-nn 12239

This theorem is referenced by:  nnne0  12272  uzwo3  12957  modmulnn  13904  bernneq3  14247  expmulnbnd  14251  expnngt1b  14258  facwordi  14305  faclbnd  14306  faclbnd2  14307  faclbnd3  14308  faclbnd5  14314  faclbnd6  14315  facubnd  14316  facavg  14317  bcp1nk  14333  hashf1  14473  swrds2  14957  isercolllem1  15679  isercoll  15682  o1fsum  15827  climcndslem1  15863  climcndslem2  15864  climcnds  15865  eftabs  16089  efcllem  16091  ege2le3  16104  efcj  16106  eftlub  16125  eflegeo  16137  eirrlem  16220  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  16728  prmfac1  16737  prmndvdsfaclt  16742  divdenle  16766  qnumgt0  16767  zsqrtelqelz  16775  hashdvds  16792  eulerthlem2  16799  odzdvds  16813  vfermltl  16819  modprm0  16823  pythagtriplem11  16843  pythagtriplem13  16845  pythagtriplem19  16851  pclem  16856  pcpre1  16860  pcidlem  16890  dvdsprmpweqle  16904  pcadd  16907  pcmpt  16910  pcmpt2  16911  pcfaclem  16916  pcfac  16917  qexpz  16919  pockthlem  16923  pockthg  16924  prmreclem1  16934  prmreclem3  16936  prmreclem4  16937  prmreclem5  16938  1arithlem4  16944  1arith  16945  4sqlem5  16960  4sqlem6  16961  4sqlem10  16965  mul4sqlem  16971  4sqlem11  16973  4sqlem12  16974  4sqlem13  16975  4sqlem14  16976  4sqlem15  16977  4sqlem16  16978  4sqlem17  16979  vdwlem1  16999  vdwlem3  17001  vdwlem6  17004  vdwlem9  17007  vdwlem10  17008  vdwlem12  17010  vdwnnlem3  17015  ramub1lem1  17044  prmolefac  17064  prmgaplem4  17072  prmgaplem5  17073  prmgaplem6  17074  prmgaplem8  17076  2expltfac  17110  cshwshashnsame  17121  setsstruct2  17191  psgnunilem4  19476  mndodconglem  19520  oddvds  19526  sylow1lem1  19577  sylow1lem5  19581  fislw  19604  efgredlem  19726  gexexlem  19831  zringlpirlem3  21423  prmirredlem  21431  fvmptnn04if  22785  fvmptnn04ifb  22787  fvmptnn04ifc  22788  fvmptnn04ifd  22789  chfacfisf  22790  chfacfisfcpmat  22791  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  lebnumii  24914  lmnn  25213  ovolunlem1a  25447  ovoliunlem1  25453  ovolicc2lem3  25470  ovolicc2lem4  25471  iundisj  25499  voliunlem1  25501  uniioombllem3  25536  dyadf  25542  dyadovol  25544  dyaddisjlem  25546  dyadmaxlem  25548  opnmbllem  25552  vitalilem4  25562  mbfi1fseqlem1  25666  mbfi1fseqlem3  25668  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  mbfi1fseqlem6  25671  itg2gt0  25711  itg2cnlem2  25713  dgreq0  26221  dgrco  26231  elqaalem2  26278  aaliou3lem2  26301  aaliou3lem8  26303  aaliou3lem9  26308  rtprmirr  26720  leibpi  26902  log2tlbnd  26905  birthdaylem3  26913  amgm  26951  emcllem2  26957  harmonicbnd4  26971  lgamgulmlem1  26989  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamgulmlem4  26992  lgamgulmlem5  26993  lgamgulmlem6  26994  lgamucov  26998  lgamcvg2  27015  wilthlem1  27028  ftalem5  27037  basellem1  27041  basellem2  27042  basellem3  27043  basellem4  27044  basellem5  27045  basellem6  27046  basellem8  27048  chtge0  27072  chtwordi  27116  vma1  27126  dvdsflf1o  27147  dvdsflsumcom  27148  fsumfldivdiaglem  27149  sgmmul  27162  chtublem  27172  fsumvma2  27175  logfac2  27178  chpchtsum  27180  chpub  27181  logfaclbnd  27183  logexprlim  27186  mersenne  27188  perfectlem2  27191  dchrelbas4  27204  bposlem1  27245  bposlem2  27246  bposlem3  27247  bposlem4  27248  bposlem5  27249  bposlem6  27250  bposlem7  27251  bposlem9  27253  lgslem1  27258  lgsval2lem  27268  lgsdirprm  27292  lgsdir  27293  lgsne0  27296  lgsqrlem2  27308  gausslemma2dlem0h  27324  gausslemma2dlem0i  27325  gausslemma2dlem1a  27326  gausslemma2dlem2  27328  gausslemma2dlem7  27334  gausslemma2d  27335  lgseisenlem1  27336  lgseisenlem2  27337  lgseisenlem3  27338  lgseisenlem4  27339  lgseisen  27340  lgsquadlem1  27341  lgsquadlem2  27342  lgsquadlem3  27343  2sqlem3  27381  2sqlem8  27387  2sqblem  27392  2sqmod  27397  chebbnd1lem1  27430  chebbnd1lem3  27432  chtppilimlem1  27434  rplogsumlem1  27445  rplogsumlem2  27446  dchrisum0lem1a  27447  rpvmasumlem  27448  dchrisumlema  27449  dchrisumlem1  27450  dchrisumlem2  27451  dchrisumlem3  27452  dchrvmasumiflem1  27462  dchrisum0flblem2  27470  dchrisum0re  27474  dchrisum0lem1b  27476  dchrisum0lem1  27477  dirith2  27489  selbergb  27510  selberg2lem  27511  logdivbnd  27517  selberg3lem2  27519  selberg4lem1  27521  pntrsumo1  27526  pntrsumbnd2  27528  pntrlog2bndlem1  27538  pntrlog2bndlem2  27539  pntrlog2bndlem3  27540  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntpbnd1a  27546  pntpbnd1  27547  pntibndlem2a  27551  pntibndlem2  27552  pntlemg  27559  pntlemh  27560  pntlemj  27564  pntlemf  27566  ostth2lem1  27579  padicabvf  27592  padicabvcxp  27593  ostth2lem2  27595  ostth2lem3  27596  ostth2lem4  27597  ostth2  27598  ostth3  27599  numclwwlk5  30315  numclwwlk7  30318  nrt2irr  30400  ubthlem2  30798  minvecolem4  30807  iundisjf  32516  ssnnssfz  32710  iundisjfi  32719  nexple  32769  2exple2exp  32770  pfxlsw2ccat  32872  chnub  32938  pmtrto1cl  33056  psgnfzto1stlem  33057  fzto1st1  33059  fzto1st  33060  psgnfzto1st  33062  cycpmco2lem6  33088  cycpmco2lem7  33089  fldextrspundgdvdslem  33667  fldextrspundgdvds  33668  fldext2rspun  33669  smatrcl  33773  smattr  33776  smatbl  33777  smatbr  33778  1smat1  33781  submateqlem1  33784  submateqlem2  33785  submateq  33786  esumcst  34040  fiunelros  34151  oddpwdc  34332  eulerpartlems  34338  eulerpartlemgc  34340  fiblem  34376  dstfrvunirn  34453  dstfrvclim1  34456  ballotlemimin  34484  fsum2dsub  34585  reprinfz1  34600  hgt750lemd  34626  hgt750lemb  34634  hgt750leme  34636  tgoldbachgtde  34638  tgoldbachgt  34641  subfaclim  35156  subfacval3  35157  erdszelem7  35165  erdszelem8  35166  erdsze2lem2  35172  cvmliftlem2  35254  cvmliftlem6  35258  cvmliftlem7  35259  cvmliftlem8  35260  cvmliftlem9  35261  cvmliftlem10  35262  cvmliftlem13  35264  bcprod  35701  bccolsum  35702  faclimlem2  35707  faclim2  35711  nn0prpwlem  36286  knoppcnlem10  36466  knoppndvlem15  36490  knoppndvlem17  36492  knoppndvlem18  36493  knoppndvlem19  36494  knoppndvlem20  36495  knoppndvlem21  36496  poimirlem3  37593  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem9  37599  poimirlem10  37600  poimirlem11  37601  poimirlem12  37602  poimirlem13  37603  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem23  37613  poimirlem26  37616  poimirlem28  37618  opnmbllem0  37626  mblfinlem2  37628  incsequz  37718  nninfnub  37721  lcmineqlem4  41991  lcmineqlem10  41997  lcmineqlem11  41998  lcmineqlem15  42002  lcmineqlem18  42005  lcmineqlem19  42006  lcmineqlem20  42007  lcmineqlem21  42008  lcmineqlem22  42009  lcmineqlem23  42010  lcmineqlem  42011  3lexlogpow5ineq2  42014  3lexlogpow5ineq4  42015  3lexlogpow2ineq2  42018  3lexlogpow5ineq5  42019  aks4d1p1p3  42028  aks4d1p1p2  42029  aks4d1p1p4  42030  aks4d1p1p5  42034  aks4d1p1  42035  aks4d1p3  42037  aks4d1p4  42038  aks4d1p5  42039  aks4d1p6  42040  aks4d1p7  42042  aks4d1p8d2  42044  aks4d1p8  42046  aks4d1p9  42047  posbezout  42059  primrootlekpowne0  42064  primrootspoweq0  42065  aks6d1c1  42075  hashscontpow1  42080  aks6d1c3  42082  aks6d1c4  42083  aks6d1c2lem4  42086  aks6d1c2  42089  aks6d1c5lem1  42095  2ap1caineq  42104  sticksstones1  42105  sticksstones2  42106  sticksstones3  42107  sticksstones6  42110  sticksstones7  42111  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  aks6d1c6lem4  42132  bcled  42137  bcle2d  42138  aks6d1c7lem1  42139  aks6d1c7lem2  42140  unitscyglem1  42154  unitscyglem2  42155  unitscyglem4  42157  unitscyglem5  42158  aks5lem8  42160  metakunt1  42164  metakunt2  42165  metakunt6  42169  metakunt7  42170  metakunt9  42172  metakunt10  42173  metakunt11  42174  metakunt12  42175  metakunt16  42179  metakunt18  42181  metakunt20  42183  metakunt22  42185  metakunt24  42187  metakunt27  42190  metakunt28  42191  metakunt29  42192  metakunt30  42193  nnadddir  42267  oexpreposd  42318  fimgmcyclem  42503  fimgmcyc  42504  flt4lem5e  42626  flt4lem6  42628  flt4lem7  42629  fltltc  42631  fltnltalem  42632  fltnlta  42633  3cubeslem3r  42657  irrapxlem3  42794  irrapxlem4  42795  irrapxlem5  42796  pellexlem2  42800  pellexlem6  42804  pell14qrgt0  42829  pell14qrgapw  42846  pellfundgt1  42853  rmspecsqrtnq  42876  ltrmxnn0  42920  jm3.1lem1  42988  jm3.1lem3  42990  dgraa0p  43120  hashnzfz2  44293  rfcnnnub  45008  nnxrd  45250  fzisoeu  45277  fsumnncl  45549  sumnnodd  45607  limsup10exlem  45749  stoweidlem1  45978  stoweidlem3  45980  stoweidlem11  45988  stoweidlem17  45994  stoweidlem20  45997  stoweidlem25  46002  stoweidlem26  46003  stoweidlem34  46011  stoweidlem38  46015  stoweidlem42  46019  stoweidlem44  46021  stoweidlem51  46028  stoweidlem59  46036  stoweidlem60  46037  wallispi  46047  wallispi2  46050  stirlinglem3  46053  stirlinglem4  46054  stirlinglem8  46058  stirlinglem10  46060  stirlinglem12  46062  stirlinglem15  46065  dirkertrigeqlem2  46076  dirkertrigeqlem3  46077  dirkercncflem2  46081  fourierdlem11  46095  fourierdlem14  46098  fourierdlem15  46099  fourierdlem20  46104  fourierdlem31  46115  fourierdlem64  46147  fourierdlem93  46176  fourierdlem95  46178  fourierdlem103  46186  fourierdlem104  46187  fourierdlem112  46195  sqwvfourb  46206  etransclem3  46214  etransclem19  46230  etransclem23  46234  etransclem24  46235  etransclem25  46236  etransclem32  46243  etransclem35  46246  etransclem41  46252  etransclem48  46259  qndenserrnbllem  46271  hoiqssbllem1  46599  hoiqssbllem2  46600  ovolval5lem1  46629  ovolval5lem2  46630  iccpartlt  47386  iccpartgt  47389  odz2prm2pw  47525  fmtnoprmfac1lem  47526  2pwp1prm  47551  sfprmdvdsmersenne  47565  lighneallem2  47568  proththdlem  47575  perfectALTVlem2  47684  gbowge7  47725  ztprmneprm  48270  pgrple2abl  48288  logbpw2m1  48495  nnpw2pmod  48511  nnolog2flm1  48518  blennngt2o2  48520  itcovalt2lem2lem1  48601