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

Axiom ax-resscn 9003
Description: The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by theorem axresscn 8979. (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 8945 . 2  class  RR
2 cc 8944 . 2  class  CC
31, 2wss 3280 1  wff  RR  C_  CC
Colors of variables: wff set class
This axiom is referenced by:  recn  9036  reex  9037  recni  9058  nnsscn  9961  nn0sscn  10182  qsscn  10541  reexpcl  11353  rpexpcl  11355  reexpclz  11356  expge0  11371  expge1  11372  rlimrecl  12329  abscn2  12347  recn2  12349  imcn2  12350  climabs  12352  climre  12354  climim  12355  rlimabs  12357  rlimre  12359  rlimim  12360  caurcvgr  12422  caucvgrlem2  12423  caurcvg  12425  fsumrecl  12483  fsumrpcl  12486  fsumge0  12529  fsumre  12542  fsumim  12543  reeff1  12676  nthruc  12805  remet  18774  tgioo2  18787  xrsdsre  18794  recld2  18798  reperf  18803  iitopon  18862  dfii3  18866  abscncf  18884  recncf  18885  imcncf  18886  abscncfALT  18903  cnmptre  18905  iimulcn  18916  icchmeo  18919  cnrehmeo  18931  evth  18937  evth2  18938  lebnumlem2  18940  lebnumii  18944  reparphti  18975  cphsqrcl  19100  resscdrg  19265  ishl2  19277  evthicc  19309  evthicc2  19310  ovolfsf  19321  volcn  19451  volivth  19452  ismbf  19475  cncombf  19503  cnmbf  19504  0plef  19517  itg1ge0  19531  i1faddlem  19538  i1fmul  19541  itg1addlem4  19544  i1fsub  19553  itg1sub  19554  mbfi1fseqlem5  19564  xrge0f  19576  itg20  19582  itg2const  19585  itg2mulc  19592  itg2addlem  19603  i1fibl  19652  itgitg1  19653  iblabslem  19672  iblabs  19673  bddmulibl  19683  recnprss  19744  dvcjbr  19788  dvfre  19790  dvnfre  19791  dvferm1  19822  dvferm2  19824  rolle  19827  cmvth  19828  mvth  19829  dvlip  19830  dvlipcn  19831  dvlip2  19832  c1liplem1  19833  c1lip2  19835  dvgt0lem1  19839  dvle  19844  dvivthlem1  19845  dvivth  19847  dvne0  19848  lhop1lem  19850  lhop1  19851  lhop2  19852  lhop  19853  dvcnvrelem1  19854  dvcnvrelem2  19855  dvcnvre  19856  dvcvx  19857  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  dvfsumlem2  19864  dvfsumrlim  19868  ftc1a  19874  ftc1lem3  19875  ftc1lem6  19878  ftc1  19879  ftc1cn  19880  ftc2  19881  ftc2ditglem  19882  itgparts  19884  itgsubstlem  19885  itgsubst  19886  aacjcl  20197  aalioulem3  20204  taylthlem2  20243  taylth  20244  abelth2  20311  reeff1olem  20315  efcvx  20318  pilem3  20322  pige3  20378  recosf1o  20390  resinf1o  20391  dvrelog  20481  relogcn  20482  logcnlem5  20490  logcn  20491  dvloglem  20492  dvlog2lem  20496  logccv  20507  dvcxp1  20579  cxpcn3  20585  resqrcn  20586  loglesqr  20595  ssscongptld  20619  ressatans  20727  rlimcnp  20757  efrlim  20761  jensenlem1  20778  jensenlem2  20779  jensen  20780  amgm  20782  ftalem3  20810  basellem9  20824  efnnfsumcl  20838  efchtdvds  20895  lgsdchr  21085  dchrvmasumlem1  21142  dchrisum0lem3  21166  pntlem3  21256  readdsubgo  21894  circgrp  21915  ipasslem7  22290  rexdiv  24125  fsumrp0cl  24170  rebase  24222  re0g  24226  unitsscn  24247  rmulccn  24267  raddcn  24268  xrge0iifhom  24276  lmlimxrge0  24287  recms  24296  reust  24297  rezh  24308  rrhre  24340  esumpfinvallem  24417  esumpfinval  24418  esumpfinvalf  24419  esumcvg  24429  lgamgulmlem2  24767  cvxpcon  24882  cvxscon  24883  rescon  24886  fprodrecl  25232  fprodrpcl  25235  rerisefaccl  25285  refallfaccl  25286  rprisefaccl  25291  mblfinlem  26143  mbfresfi  26152  ftc1cnnclem  26177  ftc1cnnc  26178  dvreasin  26179  dvreacos  26180  areacirclem2  26181  areacirclem3  26182  areacirclem4  26183  areacirclem1  26184  areacirclem5  26185  areacirc  26187  ivthALT  26228  repwsmet  26433  rrnequiv  26434  rrntotbnd  26435  reheibor  26438  iccbnd  26439  ssrecnpr  27405  sblpnf  27407  lhe4.4ex1a  27414  refsumcn  27568  climreeq  27606  dvcosre  27608  itgsin0pilem1  27611  ibliccsinexp  27612  iblioosinexp  27614  itgsinexplem1  27615  itgsinexp  27616  wallispilem2  27682
  Copyright terms: Public domain W3C validator