MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-resscn Structured version   Unicode version

Axiom ax-resscn 9049
Description: The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by theorem axresscn 9025. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-resscn  |-  RR  C_  CC

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 8991 . 2  class  RR
2 cc 8990 . 2  class  CC
31, 2wss 3322 1  wff  RR  C_  CC
Colors of variables: wff set class
This axiom is referenced by:  recn  9082  reex  9083  recni  9104  nnsscn  10007  nn0sscn  10228  qsscn  10587  reexpcl  11400  rpexpcl  11402  reexpclz  11403  expge0  11418  expge1  11419  rlimrecl  12376  abscn2  12394  recn2  12396  imcn2  12397  climabs  12399  climre  12401  climim  12402  rlimabs  12404  rlimre  12406  rlimim  12407  caurcvgr  12469  caucvgrlem2  12470  caurcvg  12472  fsumrecl  12530  fsumrpcl  12533  fsumge0  12576  fsumre  12589  fsumim  12590  reeff1  12723  nthruc  12852  remet  18823  tgioo2  18836  xrsdsre  18843  recld2  18847  reperf  18852  iitopon  18911  dfii3  18915  abscncf  18933  recncf  18934  imcncf  18935  abscncfALT  18952  cnmptre  18954  iimulcn  18965  icchmeo  18968  cnrehmeo  18980  evth  18986  evth2  18987  lebnumlem2  18989  lebnumii  18993  reparphti  19024  cphsqrcl  19149  resscdrg  19314  ishl2  19326  evthicc  19358  evthicc2  19359  ovolfsf  19370  volcn  19500  volivth  19501  ismbf  19524  cncombf  19552  cnmbf  19553  0plef  19566  itg1ge0  19580  i1faddlem  19587  i1fmul  19590  itg1addlem4  19593  i1fsub  19602  itg1sub  19603  mbfi1fseqlem5  19613  xrge0f  19625  itg20  19631  itg2const  19634  itg2mulc  19641  itg2addlem  19652  i1fibl  19701  itgitg1  19702  iblabslem  19721  iblabs  19722  bddmulibl  19732  recnprss  19793  dvcjbr  19837  dvfre  19839  dvnfre  19840  dvferm1  19871  dvferm2  19873  rolle  19876  cmvth  19877  mvth  19878  dvlip  19879  dvlipcn  19880  dvlip2  19881  c1liplem1  19882  c1lip2  19884  dvgt0lem1  19888  dvle  19893  dvivthlem1  19894  dvivth  19896  dvne0  19897  lhop1lem  19899  lhop1  19900  lhop2  19901  lhop  19902  dvcnvrelem1  19903  dvcnvrelem2  19904  dvcnvre  19905  dvcvx  19906  dvfsumle  19907  dvfsumge  19908  dvfsumabs  19909  dvfsumlem2  19913  dvfsumrlim  19917  ftc1a  19923  ftc1lem3  19924  ftc1lem6  19927  ftc1  19928  ftc1cn  19929  ftc2  19930  ftc2ditglem  19931  itgparts  19933  itgsubstlem  19934  itgsubst  19935  aacjcl  20246  aalioulem3  20253  taylthlem2  20292  taylth  20293  abelth2  20360  reeff1olem  20364  efcvx  20367  pilem3  20371  pige3  20427  recosf1o  20439  resinf1o  20440  dvrelog  20530  relogcn  20531  logcnlem5  20539  logcn  20540  dvloglem  20541  dvlog2lem  20545  logccv  20556  dvcxp1  20628  cxpcn3  20634  resqrcn  20635  loglesqr  20644  ssscongptld  20668  ressatans  20776  rlimcnp  20806  efrlim  20810  jensenlem1  20827  jensenlem2  20828  jensen  20829  amgm  20831  ftalem3  20859  basellem9  20873  efnnfsumcl  20887  efchtdvds  20944  lgsdchr  21134  dchrvmasumlem1  21191  dchrisum0lem3  21215  pntlem3  21305  readdsubgo  21943  circgrp  21964  ipasslem7  22339  rexdiv  24174  fsumrp0cl  24219  rebase  24271  re0g  24275  unitsscn  24296  rmulccn  24316  raddcn  24317  xrge0iifhom  24325  lmlimxrge0  24336  recms  24345  reust  24346  rezh  24357  rrhre  24389  esumpfinvallem  24466  esumpfinval  24467  esumpfinvalf  24468  esumcvg  24478  lgamgulmlem2  24816  cvxpcon  24931  cvxscon  24932  rescon  24935  fprodrecl  25281  fprodrpcl  25284  rerisefaccl  25335  refallfaccl  25336  rprisefaccl  25341  mblfinlem2  26246  mbfresfi  26255  ftc1cnnclem  26280  ftc1cnnc  26281  ftc1anclem3  26284  ftc1anclem5  26286  ftc1anclem7  26288  ftc1anclem8  26289  ftc1anc  26290  ftc2nc  26291  dvreasin  26292  dvreacos  26293  areacirclem1  26294  areacirclem2  26295  areacirclem3  26296  areacirclem4  26297  areacirc  26299  ivthALT  26340  repwsmet  26545  rrnequiv  26546  rrntotbnd  26547  reheibor  26550  iccbnd  26551  ssrecnpr  27516  sblpnf  27518  lhe4.4ex1a  27525  refsumcn  27679  climreeq  27717  dvcosre  27719  itgsin0pilem1  27722  ibliccsinexp  27723  iblioosinexp  27725  itgsinexplem1  27726  itgsinexp  27727  wallispilem2  27793
  Copyright terms: Public domain W3C validator