Theorem nnret 5828

Description: A natural number is a real number.

Assertion

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

Proof of Theorem nnret

Step	Hyp	Ref	Expression
1		nnssre 5826	. 2 |- NN (_ RR
2	1	sseli 2036	1 |- (A e. NN -> A e. RR)

Syntax hints:   -> wi 3   e. wcel 1105  RRcr 5156  NNcn 5219

This theorem is referenced by:  nnre 5830  nn2get 5841  nnge1t 5842  nngt1ne1t 5843  nnle1eq1t 5844  nngt0t 5845  nnrecgt0t 5851  nnleltp1t 5852  nnltp1let 5853  nnsub 5854  nnaddm1clt 5856  nnunb 5968  arch 5969  nnreclt 5970  bndndx 5971  nn0ltp1let 6025  nnnegz 6036  elnnz 6043  nn0subt 6059  zltp1let 6079  gtndivt 6091  primet 6093  btwnz 6114  qret 6148  qbtwnre 6167  monoord 6182  seq1lem2 6198  ser1add2 6226  ser1add 6227  indstr 6344  sqr2irr 6610  seq1bnd 6798  cau2 6801  caubnd 6814  facdivt 6830  facndivt 6831  facwordit 6832  faclbnd 6833  faclbnd2 6834  faclbnd3 6835  faclbnd4lem4 6839  faclbnd5 6841  faclbnd6 6842  facavgt 6843  bccl2t 6860  bcxmas 6965  climubi 7040  climcau 7043  caucvglem2 7045  caucvglem6 7049  ser1cmp2 7064  reccnv 7104  expcnvlem1 7113  cvgratlem2ALT 7134  cvgratlem1 7136  cvgratlem2 7137  cvgratlem4 7139  efcltlem1 7197  reefcl 7210  erelem1 7212  erelem3 7214  efcj 7229  efaddlem15 7245  efaddlem17 7247  reeftclt 7267  eftabs 7268  eftlubclt 7269  ef1tllem 7274  ef01tllem2 7277  eirrlem4 7284  effsumle 7289  absefm1le 7303  eflegeolem1 7304  infpnlem1 7400  infpn2 7403  lmnn 7821  caun0 7828  lmuni 7834  metelcls 7848  metcnp4 7852  xplm 7857  iscms2lem4 7874  bcthlem2 7882  bcthlem16 7896  bcthlem18 7898  bcthlem20 7900  nmobndseqi 8307  ubthlem3 8397  ubthlem5 8399  ubthlem11 8405  ubthlem12 8406  ubthlem13 8407  ubthlem14 8408  minveclem27 8437  projlem1 9316  projlem2 9317  projlem26 9341  projlem28 9343  nmcopexlem1 10080  nmcopexlem3 10082  nmcopexlem5 10084  nmcopexlem6 10085  nmcfnexlem1 10109  nmcfnexlem3 10111  nmcfnexlem5 10113  nmcfnexlem6 10114  nlelch 10123  hmopidmch 10204

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-rep 2661  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747  ax-un 2830  ax-inf2 4549

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 773  df-3an 774  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-reu 1627  df-rab 1628  df-v 1787  df-sbc 1913  df-csb 1973  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-pss 2026  df-nul 2252  df-if 2333  df-pw 2373  df-sn 2383  df-pr 2384  df-tp 2386  df-op 2387  df-uni 2472  df-int 2502  df-iun 2536  df-br 2588  df-opab 2635  df-tr 2649  df-eprel 2794  df-id 2797  df-po 2804  df-so 2814  df-fr 2880  df-we 2897  df-ord 2914  df-on 2915  df-lim 2916  df-suc 2917  df-om 3095  df-xp 3147  df-rel 3148  df-cnv 3149  df-co 3150  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fun 3155  df-fn 3156  df-f 3157  df-fv 3161  df-rdg 3871  df-opr 3904  df-oprab 3905  df-1st 4017  df-2nd 4018  df-1o 4071  df-oadd 4073  df-omul 4074  df-er 4199  df-ec 4201  df-qs 4204  df-ni 4923  df-pli 4924  df-mi 4925  df-lti 4926  df-plpq 4958  df-mpq 4959  df-enq 4960  df-nq 4961  df-plq 4962  df-mq 4963  df-rq 4964  df-ltq 4965  df-1q 4966  df-np 5009  df-1p 5010  df-plp 5011  df-mp 5012  df-ltp 5013  df-plpr 5087  df-mpr 5088  df-enr 5089  df-nr 5090  df-plr 5091  df-mr 5092  df-ltr 5093  df-0r 5094  df-1r 5095  df-m1r 5096  df-c 5163  df-0 5164  df-1 5165  df-i 5166  df-r 5167  df-plus 5168  df-mul 5169  df-sub 5279  df-neg 5281  df-n 5824

Copyright terms: Public domain