Theorem nnre 12342

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

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

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 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7751  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-i2m1 11268  ax-1ne0 11269  ax-rrecex 11272  ax-cnre 11273

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  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 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-nn 12336

This theorem is used by:  nnrei  12344  nnmulcl  12359  nn2ge  12365  nnge1  12366  nngt1ne1  12367  nnle1eq1  12368  nngt0  12369  nnnlt1  12370  nnnle0  12371  nndivre  12379  nnrecgt0  12381  nnsub  12382  nnadddir  12394  nnmul1com  12395  nnunb  12602  arch  12603  nnrecl  12604  bndndx  12605  0mnnnnn0  12638  nnnegz  12696  elnnz  12703  elz2  12711  nnz  12714  gtndiv  12776  prime  12780  btwnz  12802  indstr  13043  qre  13080  elpq  13103  elpqb  13104  rpnnen1lem2  13105  rpnnen1lem1  13106  rpnnen1lem3  13107  rpnnen1lem5  13109  nnrp  13132  nnledivrp  13234  qbtwnre  13329  elfzo0le  13838  fzonmapblen  13843  fzo1fzo0n0  13850  ubmelfzo  13865  fzonn0p1p1  13879  ubmelm1fzo  13898  subfzo0  13928  adddivflid  13958  flltdivnn0lt  13973  quoremz  13995  quoremnn0ALT  13997  intfracq  13999  fldiv  14000  modmulnn  14029  m1modnnsub1  14060  addmodid  14062  modifeq2int  14076  modaddmodup  14077  modaddmodlo  14078  modfzo0difsn  14086  modsumfzodifsn  14087  addmodlteq  14089  nnlesq  14349  digit2  14380  digit1  14381  expnngt1  14385  facdiv  14431  facndiv  14432  faclbnd  14434  faclbnd3  14436  faclbnd4lem4  14440  faclbnd5  14442  bcval5  14462  seqcoll  14609  ccatval21sw  14731  cshwidxmod  14954  cshwidxm1  14958  repswcshw  14963  isercolllem1  15832  harmonic  16028  efaddlem  16259  rpnnen2lem9  16390  rpnnen2lem12  16393  sqrt2irr  16417  nndivdvds  16431  dvdsle  16480  fzm1ndvds  16492  nno  16552  nnoddm1d2  16556  divalg2  16575  divalgmod  16576  ndvdsadd  16580  modgcd  16705  gcdzeq  16725  nn0rppwr  16735  sqgcd  16736  nn0expgcd  16738  lcmgcdlem  16781  lcmf  16808  coprmgcdb  16824  qredeq  16832  qredeu  16833  isprm3  16858  ge2nprmge4  16877  prmdvdsfz  16881  isprm5  16883  ncoprmlnprm  16904  divdenle  16925  phibndlem  16947  eulerthlem2  16959  hashgcdlem  16965  oddprm  16988  pythagtriplem10  16998  pythagtriplem12  17004  pythagtriplem14  17006  pythagtriplem16  17008  pythagtriplem19  17011  pclem  17016  pc2dvds  17057  pcmpt  17070  fldivp1  17075  pcbc  17078  infpnlem1  17088  infpn2  17091  prmreclem1  17094  prmreclem3  17096  vdwlem3  17161  ram0  17200  prmgaplem4  17232  prmgaplem7  17235  cshwshashlem1  17273  cshwshashlem2  17274  setsstruct2  17352  mulgnegnn  19294  mulgmodid  19323  odmodnn0  19754  gexdvds  19798  sylow3lem6  19846  prmirredlem  21778  znidomb  21867  chfacfisf  23172  chfacfisfcpmat  23173  chfacffsupp  23174  chfacfscmul0  23176  chfacfpmmul0  23180  ovolunlem1a  25817  ovoliunlem2  25824  ovolicc2lem3  25840  ovolicc2lem4  25841  iundisj2  25870  dyadss  25915  volsup2  25926  volivth  25928  vitali  25934  ismbf3d  25975  mbfi1fseqlem3  26038  mbfi1fseqlem4  26039  mbfi1fseqlem5  26040  itg2seq  26063  itg2gt0  26081  itg2cnlem1  26082  idomrootle  26491  plyeq0lem  26529  dgreq0  26584  dgrcolem2  26593  elqaalem2  26643  elqaalem3  26644  logtayllem  26987  leibpi  27270  birthdaylem3  27281  zetacvg  27342  eldmgm  27349  basellem1  27408  basellem2  27409  basellem3  27410  basellem6  27413  basellem9  27416  prmorcht  27505  dvdsflsumcom  27515  muinv  27520  vmalelog  27532  chtublem  27538  logfac2  27544  logfaclbnd  27549  pcbcctr  27603  bcmono  27604  bposlem1  27611  bposlem5  27615  bposlem6  27616  bpos  27620  lgsval4a  27646  gausslemma2dlem0c  27685  gausslemma2dlem0d  27686  gausslemma2dlem1a  27692  gausslemma2dlem2  27694  gausslemma2dlem3  27695  gausslemma2dlem5  27698  lgsquadlem1  27707  lgsquadlem2  27708  2lgslem1a1  27716  2sqreunnlem1  27776  2sqreunnltlem  27777  dchrisum0re  27840  dchrisum0lem1  27843  logdivbnd  27883  ostth2lem1  27945  ostth2lem3  27962  pthdlem2lem  30353  crctcshwlkn0lem1  30399  crctcshwlkn0lem3  30401  crctcshwlkn0lem4  30402  crctcshwlkn0lem5  30403  crctcshwlkn0lem6  30404  crctcshwlkn0lem7  30405  crctcshwlkn0  30410  clwlkclwwlkf1lem2  30596  clwwisshclwwslem  30605  clwwlkel  30637  clwwlkf  30638  clwwlkf1  30640  wwlksext2clwwlk  30648  wwlksubclwwlk  30649  eucrctshift  30844  eucrct2eupth  30846  numclwlk2lem2f  30978  nmounbseqi  31379  nmounbseqiALT  31380  nmobndseqi  31381  nmobndseqiALT  31382  ubthlem1  31472  minvecolem3  31478  lnconi  32635  iundisj2f  33184  nnmulge  33331  xrsmulgzz  33570  esumpmono  34711  eulerpartlemb  35000  fibp1  35033  subfaclim  35953  subfacval3  35954  snmlff  36094  fz0n  36496  bcprod  36503  nn0prpwlem  37110  nn0prpw  37111  nndivsub  37245  nndivlub  37246  knoppcnlem2  37360  knoppcnlem4  37362  knoppndvlem11  37388  knoppndvlem12  37389  knoppndvlem14  37391  poimirlem13  38551  poimirlem14  38552  poimirlem31  38569  poimirlem32  38570  mblfinlem2  38576  fzmul  38675  incsequz  38682  nnubfi  38684  nninfnub  38685  2ap1caineq  43195  sticksstones1  43196  unitscyglem5  43249  sn-nnne0  43524  nn0addcom  43526  renegmulnnass  43529  nn0mulcom  43530  zmulcomlem  43531  fimgmcyc  43598  irrapxlem1  43828  irrapxlem2  43829  pellexlem1  43835  pellexlem5  43839  pellqrex  43885  monotoddzzfi  43948  jm2.24nn  43965  congabseq  43980  acongrep  43986  acongeq  43989  expdiophlem1  44027  idomodle  44192  relexpmulnn  44708  prmunb2  45294  hashnzfzclim  45305  fmuldfeq  46594  sumnnodd  46641  stoweidlem14  47023  stoweidlem17  47026  stoweidlem20  47029  stoweidlem49  47058  stoweidlem60  47069  wallispilem3  47076  wallispilem4  47077  wallispilem5  47078  wallispi  47079  wallispi2lem1  47080  wallispi2lem2  47081  stirlinglem1  47083  stirlinglem3  47085  stirlinglem4  47086  stirlinglem6  47088  stirlinglem7  47089  stirlinglem10  47092  stirlinglem11  47093  stirlinglem12  47094  stirlinglem13  47095  stirlingr  47099  dirker2re  47101  dirkerval2  47103  dirkerre  47104  dirkertrigeqlem1  47107  fourierdlem66  47181  fourierdlem73  47188  fourierdlem83  47198  fourierdlem87  47202  fourierdlem103  47218  fourierdlem104  47219  fourierdlem111  47226  fouriersw  47240  etransclem24  47267  sge0rpcpnf  47430  hoicvr  47557  hoicvrrex  47565  vonioolem2  47690  vonicclem2  47693  fsupdm  47851  finfdm  47855  smfinfdmmbllem  47857  subsubelfzo0  48396  ceilhalfelfzo1  48403  2tceilhalfelfzo1  48405  ceilhalfnn  48409  addmodne  48419  submodlt  48425  modn0mul  48432  m1modmmod  48433  difmodm1lt  48434  modlt0b  48438  fmtnodvds  48628  2pwp1prm  48673  lighneallem2  48690  nn0oALTV  48793  nneven  48795  nnsum4primes4  48886  nnsum4primesprm  48888  nnsum4primesgbe  48890  nnsum4primesle9  48892  bgoldbachlt  48910  tgoldbach  48914  gpgusgralem  49153  gpgedgvtx0  49158  gpg3kgrtriexlem1  49180  gpg3kgrtriexlem2  49181  gpg3kgrtriexlem3  49182  gpg3kgrtriexlem4  49183  gpg3kgrtriexlem6  49185  altgsumbcALT  49464  nnlog2ge0lt1  49677  logbpw2m1  49678  blennn  49686  blennnelnn  49687  nnpw2pmod  49694  nnolog2flm1  49701  digvalnn0  49710  dignn0fr  49712  dignn0ldlem  49713  dignnld  49714  dig2nn1st  49716