HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: A natural number is a real number. |
| Ref | Expression |
|---|---|
| nnret |
   
 
  |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nnssre 5875 |
. 2
 | |
| 2 | 1 | sseli 2055 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wi 3 wcel 955 cr 5205 cn 5268 |
| This theorem is referenced by: nnre 5879 nn2get 5890 nnge1t 5891 nngt1ne1t 5892 nnle1eq1t 5893 nngt0t 5894 nnrecgt0t 5900 nnleltp1t 5901 nnltp1let 5902 nnsub 5903 nnaddm1clt 5905 nnunb 6017 arch 6018 nnreclt 6019 bndndx 6020 nn0ltp1let 6074 nnnegz 6085 elnnz 6092 nn0subt 6108 zltp1let 6128 gtndivt 6140 primet 6142 btwnz 6163 qret 6197 qbtwnre 6216 monoord 6231 seq1lem2 6247 ser1add2 6275 ser1add 6276 indstr 6393 sqr2irr 6659 seq1bnd 6847 cau2 6850 caubnd 6863 facdivt 6879 facndivt 6880 facwordit 6881 faclbnd 6882 faclbnd2 6883 faclbnd3 6884 faclbnd4lem4 6888 faclbnd5 6890 faclbnd6 6891 facavgt 6892 bccl2t 6909 bcxmas 7014 climubi 7089 climcau 7092 caucvglem2 7094 caucvglem6 7098 ser1cmp2 7113 reccnv 7153 expcnvlem1 7162 cvgratlem2ALT 7183 cvgratlem1 7185 cvgratlem2 7186 cvgratlem4 7188 efcltlem1 7246 reefcl 7259 erelem1 7261 erelem3 7263 efcj 7278 efaddlem15 7294 efaddlem17 7296 reeftclt 7316 eftabs 7317 eftlubclt 7318 ef1tllem 7323 ef01tllem2 7326 eirrlem4 7333 effsumle 7338 absefm1le 7352 eflegeolem1 7353 infpnlem1 7449 infpn2 7452 lmnn 7873 caun0 7880 lmuni 7886 metelcls 7900 metcnp4 7904 xplm 7909 iscms2lem4 7926 bcthlem2 7934 bcthlem16 7948 bcthlem18 7950 bcthlem20 7952 nmobndseqi 8372 ubthlem3 8462 ubthlem5 8464 ubthlem11 8470 ubthlem12 8471 ubthlem13 8472 ubthlem14 8473 minveclem27 8502 projlem1 9102 projlem2 9103 projlem26 9127 projlem28 9129 nmcopexlem1 9866 nmcopexlem3 9868 nmcopexlem5 9870 nmcopexlem6 9871 nmcfnexlem1 9895 nmcfnexlem3 9897 nmcfnexlem5 9899 nmcfnexlem6 9900 nlelch 9909 hmopidmch 9990 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-9 962 ax-10 963 ax-11 964 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452 ax-rep 2683 ax-sep 2693 ax-nul 2700 ax-pow 2732 ax-pr 2769 ax-un 2857 ax-inf2 4597 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 774 df-3an 775 df-ex 978 df-sb 1168 df-eu 1375 df-mo 1376 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-ral 1641 df-rex 1642 df-reu 1643 df-rab 1644 df-v 1803 df-sbc 1932 df-csb 1992 df-dif 2039 df-un 2040 df-in 2041 df-ss 2043 df-pss 2045 df-nul 2271 df-if 2352 df-pw 2392 df-sn 2402 df-pr 2403 df-tp 2405 df-op 2406 df-uni 2494 df-int 2524 df-iun 2558 df-br 2610 df-opab 2657 df-tr 2671 df-eprel 2821 df-id 2824 df-po 2831 df-so 2841 df-fr 2907 df-we 2924 df-ord 2941 df-on 2942 df-lim 2943 df-suc 2944 df-om 3122 df-xp 3174 df-rel 3175 df-cnv 3176 df-co 3177 df-dm 3178 df-rn 3179 df-res 3180 df-ima 3181 df-fun 3182 df-fn 3183 df-f 3184 df-fv 3188 df-rdg 3917 df-opr 3950 df-oprab 3951 df-1st 4063 df-2nd 4064 df-1o 4117 df-oadd 4119 df-omul 4120 df-er 4245 df-ec 4247 df-qs 4250 df-ni 4972 df-pli 4973 df-mi 4974 df-lti 4975 df-plpq 5007 df-mpq 5008 df-enq 5009 df-nq 5010 df-plq 5011 df-mq 5012 df-rq 5013 df-ltq 5014 df-1q 5015 df-np 5058 df-1p 5059 df-plp 5060 df-mp 5061 df-ltp 5062 df-plpr 5136 df-mpr 5137 df-enr 5138 df-nr 5139 df-plr 5140 df-mr 5141 df-ltr 5142 df-0r 5143 df-1r 5144 df-m1r 5145 df-c 5212 df-0 5213 df-1 5214 df-i 5215 df-r 5216 df-plus 5217 df-mul 5218 df-sub 5328 df-neg 5330 df-n 5873 |