Theorem nnre 6907

Description: A natural number is a real number.

Assertion

Ref	Expression
nnre	|- (A e. NN -> A e. RR)

Proof of Theorem nnre

Step	Hyp	Ref	Expression
1		nnssre 6905	. 2 |- NN C_ RR
2	1	sseli 2450	1 |- (A e. NN -> A e. RR)

Syntax hints:   -> wi 3   e. wcel 1138  RRcr 6181  NNcn 6245

This theorem is referenced by:  nnrei 6909  nn2ge 6920  nnge1 6921  nngt1ne1 6922  nnle1eq1 6923  nngt0 6924  nndivre 6930  nnrecgt0 6932  nnleltp1 6933  nnltp1le 6934  nnsubi 6935  nnaddm1cl 6937  nnrp 7033  nnunb 7074  arch 7075  nnrecl 7076  bndndx 7077  nn0ltp1le 7131  nnnegz 7142  elnnz 7149  nn0sub 7165  zltp1le 7185  gtndiv 7200  prime 7202  btwnz 7223  qre 7234  qbtwnre 7254  quoremz 7287  quoremnn0ALT 7288  quoremnn0 7289  intfracq 7291  fldiv 7292  fldiv2 7293  modmulnn 7305  monoord 7318  indstr 7425  seq1lem2 7518  ser1add2i 7546  ser1addi 7547  digit2 7699  digit1 7700  sqr2irr 7774  seq1bndi 7957  cau2i 7960  caubndi 7973  facdiv 7989  facndiv 7990  facwordi 7991  faclbnd 7992  faclbnd2 7993  faclbnd3 7994  faclbnd4lem4 7998  faclbnd5 8000  faclbnd6 8001  facavg 8002  bccl2 8018  bcxmas 8131  climubii 8208  climcaui 8211  caucvglem2 8213  caucvglem6 8217  ser1cmp2i 8232  reccnv 8274  expcnvlem1 8283  cvgratlem2ALT 8305  cvgratlem1 8307  cvgratlem2 8308  cvgratlem4 8310  efcltlem1 8361  reefcli 8374  erelem1 8376  erelem3 8378  efcji 8393  efaddlem15 8409  efaddlem17 8411  reeftcl 8431  eftabsi 8432  eftlubcl 8433  ef1tllem 8438  ef01tllem2 8441  ef01tllem2OLD 8442  eirrlem4 8449  effsumlei 8457  absefm1lei 8472  eflegeolem1 8473  infpnlem1 8570  infpn2 8573  lmnn 9008  caun0 9018  lmuni 9024  metelcls 9038  metcnp4 9043  xplm 9048  iscms2lem4 9065  bcthlem2 9073  bcthlem16 9087  bcthlem18 9089  bcthlem20 9091  gxnn0neg 9181  gxmodid 9197  nmounbseqi 9574  nmobndseqi 9575  ubthlem3 9669  ubthlem5 9671  ubthlem11 9677  ubthlem12 9678  ubthlem12OLD 9679  ubthlem13 9680  ubthlem13OLD 9681  ubthlem14 9682  minveclem27 9711  projlem1 10611  projlem2 10612  projlem26 10636  projlem28 10638  nmcopexlem1 11380  nmcopexlem3 11382  nmcopexlem5 11384  nmcopexlem6 11385  nmcfnexlem1 11409  nmcfnexlem3 11411  nmcfnexlem5 11413  nmcfnexlem6 11414  nlelchi 11423  hmopidmchi 11515  dvdsle 13485  divalg2 13500  divalgmod 13501  ndvdsadd 13503  modgcd 13530  mulgcdlem3 13550  1nprm 13561  zgt1b1 13563  coprm 13574  nndivlub 13989  fzmul 15472  incsequz 15497  nnubfi 15500  nninfnub 15501  mettrifi 15529  geomcau 15531  heiborlem16 15652  heiborlem32 15668  heiborlem35 15671  rrndstprj2 15700  rrncms 15701  rrntotbndlem1 15702  strssp1 16472  fnelstr 16476  strdif 16478

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-13 1149  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-rep 3243  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339  ax-un 3601  ax-inf2 5540

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3or 856  df-3an 857  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-ral 1943  df-rex 1944  df-reu 1945  df-rab 1946  df-v 2127  df-sbc 2287  df-csb 2374  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-pss 2440  df-nul 2702  df-if 2807  df-pw 2859  df-sn 2873  df-pr 2874  df-tp 2876  df-op 2877  df-uni 3000  df-int 3037  df-iun 3079  df-br 3159  df-opab 3214  df-tr 3230  df-eprel 3398  df-id 3401  df-po 3406  df-so 3419  df-fr 3440  df-we 3459  df-ord 3475  df-on 3476  df-lim 3477  df-suc 3478  df-om 3761  df-xp 3811  df-rel 3812  df-cnv 3813  df-co 3814  df-dm 3815  df-rn 3816  df-res 3817  df-ima 3818  df-fun 3819  df-fn 3820  df-f 3821  df-f1 3822  df-fo 3823  df-f1o 3824  df-fv 3825  df-opr 4697  df-oprab 4698  df-mpt 4817  df-1st 4831  df-2nd 4832  df-iota 4900  df-rdg 4951  df-1o 4988  df-oadd 4990  df-omul 4991  df-er 5129  df-ec 5131  df-qs 5134  df-en 5238  df-dom 5239  df-sdom 5240  df-undef 5367  df-riota 5371  df-ni 5948  df-pli 5949  df-mi 5950  df-lti 5951  df-plpq 5983  df-mpq 5984  df-enq 5985  df-nq 5986  df-plq 5987  df-mq 5988  df-rq 5989  df-ltq 5990  df-1q 5991  df-np 6034  df-1p 6035  df-plp 6036  df-mp 6037  df-ltp 6038  df-plpr 6112  df-mpr 6113  df-enr 6114  df-nr 6115  df-plr 6116  df-mr 6117  df-ltr 6118  df-0r 6119  df-1r 6120  df-m1r 6121  df-c 6188  df-0 6189  df-1 6190  df-i 6191  df-r 6192  df-plus 6193  df-mul 6194  df-sub 6307  df-neg 6309  df-n 6903

Copyright terms: Public domain