Theorem nnre 12265

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11124  ℕcn 12258

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7737  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-i2m1 11193  ax-1ne0 11194  ax-rrecex 11197  ax-cnre 11198

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7417  df-om 7864  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-nn 12259

This theorem is used by:  nnrei  12267  nnmulcl  12282  nn2ge  12288  nnge1  12289  nngt1ne1  12290  nnle1eq1  12291  nngt0  12292  nnnlt1  12293  nnnle0  12294  nndivre  12302  nnrecgt0  12304  nnsub  12305  nnadddir  12317  nnmul1com  12318  nnunb  12525  arch  12526  nnrecl  12527  bndndx  12528  0mnnnnn0  12561  nnnegz  12619  elnnz  12626  elz2  12634  nnz  12637  gtndiv  12699  prime  12703  btwnz  12725  indstr  12966  qre  13003  elpq  13026  elpqb  13027  rpnnen1lem2  13028  rpnnen1lem1  13029  rpnnen1lem3  13030  rpnnen1lem5  13032  nnrp  13055  nnledivrp  13157  qbtwnre  13252  elfzo0le  13760  fzonmapblen  13765  fzo1fzo0n0  13772  ubmelfzo  13787  fzonn0p1p1  13801  ubmelm1fzo  13820  subfzo0  13850  adddivflid  13880  flltdivnn0lt  13895  quoremz  13917  quoremnn0ALT  13919  intfracq  13921  fldiv  13922  modmulnn  13951  m1modnnsub1  13982  addmodid  13984  modifeq2int  13998  modaddmodup  13999  modaddmodlo  14000  modfzo0difsn  14008  modsumfzodifsn  14009  addmodlteq  14011  nnlesq  14270  digit2  14301  digit1  14302  expnngt1  14306  facdiv  14352  facndiv  14353  faclbnd  14355  faclbnd3  14357  faclbnd4lem4  14361  faclbnd5  14363  bcval5  14383  seqcoll  14530  ccatval21sw  14652  cshwidxmod  14875  cshwidxm1  14879  repswcshw  14884  isercolllem1  15753  harmonic  15949  efaddlem  16180  rpnnen2lem9  16311  rpnnen2lem12  16314  sqrt2irr  16338  nndivdvds  16352  dvdsle  16401  fzm1ndvds  16413  nno  16473  nnoddm1d2  16477  divalg2  16496  divalgmod  16497  ndvdsadd  16501  modgcd  16623  gcdzeq  16643  nn0rppwr  16652  sqgcd  16653  nn0expgcd  16655  dvdssqlem  16657  lcmgcdlem  16697  lcmf  16724  coprmgcdb  16740  qredeq  16748  qredeu  16749  isprm3  16774  ge2nprmge4  16793  prmdvdsfz  16797  isprm5  16799  ncoprmlnprm  16820  divdenle  16841  phibndlem  16862  eulerthlem2  16874  hashgcdlem  16880  oddprm  16903  pythagtriplem10  16913  pythagtriplem12  16919  pythagtriplem14  16921  pythagtriplem16  16923  pythagtriplem19  16926  pclem  16931  pc2dvds  16972  pcmpt  16985  fldivp1  16990  pcbc  16993  infpnlem1  17003  infpn2  17006  prmreclem1  17009  prmreclem3  17011  vdwlem3  17076  ram0  17115  prmgaplem4  17147  prmgaplem7  17150  cshwshashlem1  17188  cshwshashlem2  17189  setsstruct2  17267  mulgnegnn  19208  mulgmodid  19237  odmodnn0  19668  gexdvds  19712  sylow3lem6  19760  prmirredlem  21686  znidomb  21775  chfacfisf  23080  chfacfisfcpmat  23081  chfacffsupp  23082  chfacfscmul0  23084  chfacfpmmul0  23088  ovolunlem1a  25725  ovoliunlem2  25732  ovolicc2lem3  25748  ovolicc2lem4  25749  iundisj2  25778  dyadss  25823  volsup2  25834  volivth  25836  vitali  25842  ismbf3d  25883  mbfi1fseqlem3  25946  mbfi1fseqlem4  25947  mbfi1fseqlem5  25948  itg2seq  25971  itg2gt0  25989  itg2cnlem1  25990  idomrootle  26399  plyeq0lem  26437  dgreq0  26492  dgrcolem2  26501  elqaalem2  26553  elqaalem3  26554  logtayllem  26897  leibpi  27180  birthdaylem3  27191  zetacvg  27252  eldmgm  27259  basellem1  27318  basellem2  27319  basellem3  27320  basellem6  27323  basellem9  27326  prmorcht  27415  dvdsflsumcom  27425  muinv  27430  vmalelog  27442  chtublem  27448  logfac2  27454  logfaclbnd  27459  pcbcctr  27513  bcmono  27514  bposlem1  27521  bposlem5  27525  bposlem6  27526  bpos  27530  lgsval4a  27556  gausslemma2dlem0c  27595  gausslemma2dlem0d  27596  gausslemma2dlem1a  27602  gausslemma2dlem2  27604  gausslemma2dlem3  27605  gausslemma2dlem5  27608  lgsquadlem1  27617  lgsquadlem2  27618  2lgslem1a1  27626  2sqreunnlem1  27686  2sqreunnltlem  27687  dchrisum0re  27750  dchrisum0lem1  27753  logdivbnd  27793  ostth2lem1  27855  ostth2lem3  27872  pthdlem2lem  30233  crctcshwlkn0lem1  30279  crctcshwlkn0lem3  30281  crctcshwlkn0lem4  30282  crctcshwlkn0lem5  30283  crctcshwlkn0lem6  30284  crctcshwlkn0lem7  30285  crctcshwlkn0  30290  clwlkclwwlkf1lem2  30476  clwwisshclwwslem  30485  clwwlkel  30517  clwwlkf  30518  clwwlkf1  30520  wwlksext2clwwlk  30528  wwlksubclwwlk  30529  eucrctshift  30724  eucrct2eupth  30726  numclwlk2lem2f  30858  nmounbseqi  31259  nmounbseqiALT  31260  nmobndseqi  31261  nmobndseqiALT  31262  ubthlem1  31352  minvecolem3  31358  lnconi  32515  iundisj2f  33064  nnmulge  33211  xrsmulgzz  33450  esumpmono  34590  eulerpartlemb  34880  fibp1  34913  subfaclim  35768  subfacval3  35769  snmlff  35909  fz0n  36311  bcprod  36318  nn0prpwlem  36942  nn0prpw  36943  nndivsub  37077  nndivlub  37078  knoppcnlem2  37192  knoppcnlem4  37194  knoppndvlem11  37220  knoppndvlem12  37221  knoppndvlem14  37223  poimirlem13  38383  poimirlem14  38384  poimirlem31  38401  poimirlem32  38402  mblfinlem2  38408  fzmul  38492  incsequz  38499  nnubfi  38501  nninfnub  38502  2ap1caineq  43012  sticksstones1  43013  unitscyglem5  43066  sn-nnne0  43349  nn0addcom  43351  renegmulnnass  43354  nn0mulcom  43355  zmulcomlem  43356  fimgmcyc  43417  irrapxlem1  43664  irrapxlem2  43665  pellexlem1  43671  pellexlem5  43675  pellqrex  43721  monotoddzzfi  43784  jm2.24nn  43801  congabseq  43816  acongrep  43822  acongeq  43825  expdiophlem1  43863  idomodle  44033  relexpmulnn  44550  prmunb2  45136  hashnzfzclim  45147  fmuldfeq  46414  sumnnodd  46461  stoweidlem14  46843  stoweidlem17  46846  stoweidlem20  46849  stoweidlem49  46878  stoweidlem60  46889  wallispilem3  46896  wallispilem4  46897  wallispilem5  46898  wallispi  46899  wallispi2lem1  46900  wallispi2lem2  46901  stirlinglem1  46903  stirlinglem3  46905  stirlinglem4  46906  stirlinglem6  46908  stirlinglem7  46909  stirlinglem10  46912  stirlinglem11  46913  stirlinglem12  46914  stirlinglem13  46915  stirlingr  46919  dirker2re  46921  dirkerval2  46923  dirkerre  46924  dirkertrigeqlem1  46927  fourierdlem66  47001  fourierdlem73  47008  fourierdlem83  47018  fourierdlem87  47022  fourierdlem103  47038  fourierdlem104  47039  fourierdlem111  47046  fouriersw  47060  etransclem24  47087  sge0rpcpnf  47250  hoicvr  47377  hoicvrrex  47385  vonioolem2  47510  vonicclem2  47513  fsupdm  47671  finfdm  47675  smfinfdmmbllem  47677  subsubelfzo0  48216  ceilhalfelfzo1  48223  2tceilhalfelfzo1  48225  ceilhalfnn  48229  addmodne  48239  submodlt  48245  modn0mul  48252  m1modmmod  48253  difmodm1lt  48254  modlt0b  48258  fmtnodvds  48448  2pwp1prm  48493  lighneallem2  48510  nn0oALTV  48613  nneven  48615  nnsum4primes4  48706  nnsum4primesprm  48708  nnsum4primesgbe  48710  nnsum4primesle9  48712  bgoldbachlt  48730  tgoldbach  48734  gpgusgralem  48973  gpgedgvtx0  48978  gpg3kgrtriexlem1  49000  gpg3kgrtriexlem2  49001  gpg3kgrtriexlem3  49002  gpg3kgrtriexlem4  49003  gpg3kgrtriexlem6  49005  altgsumbcALT  49284  nnlog2ge0lt1  49497  logbpw2m1  49498  blennn  49506  blennnelnn  49507  nnpw2pmod  49514  nnolog2flm1  49521  digvalnn0  49530  dignn0fr  49532  dignn0ldlem  49533  dignnld  49534  dig2nn1st  49536