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

Axiom ax-resscn 10206
Description: The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by theorem axresscn 10182. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-resscn ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 10148 . 2 class
2 cc 10147 . 2 class
31, 2wss 3716 1 wff ℝ ⊆ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  recn  10239  reex  10240  recni  10265  nnsscn  11238  nn0sscn  11510  qsscn  12013  reexpcl  13092  rpexpcl  13094  reexpclz  13095  expge0  13111  expge1  13112  rlimrecl  14531  abscn2  14549  recn2  14551  imcn2  14552  climabs  14554  climre  14556  climim  14557  rlimabs  14559  rlimre  14561  rlimim  14562  caurcvgr  14624  caucvgrlem2  14625  caurcvg  14627  fsumrecl  14685  fsumrpcl  14688  fsumge0  14747  fsumre  14760  fsumim  14761  fprodrecl  14903  fprodrpcl  14906  fprodreclf  14909  fprodge0  14944  fprodge1  14946  rerisefaccl  14968  refallfaccl  14969  rprisefaccl  14974  reeff1  15070  nthruc  15201  regsumfsum  20037  rge0srg  20040  rebase  20175  re0g  20181  regsumsupp  20191  remet  22815  tgioo2  22828  xrsdsre  22835  recld2  22839  reperf  22844  iitopon  22904  dfii3  22908  abscncf  22926  recncf  22927  imcncf  22928  abscncfALT  22945  cnmptre  22948  iimulcn  22959  icchmeo  22962  cnrehmeo  22974  evth  22980  evth2  22981  lebnumlem2  22983  lebnumii  22987  reparphti  23018  cphsqrtcl  23205  resscdrg  23375  ishl2  23387  recms  23389  reust  23390  evthicc  23449  evthicc2  23450  ovolfsf  23461  volcn  23595  volivth  23596  ismbf  23617  cncombf  23645  cnmbf  23646  0plef  23659  itg1ge0  23673  i1faddlem  23680  i1fmul  23683  itg1addlem4  23686  i1fsub  23695  itg1sub  23696  mbfi1fseqlem5  23706  xrge0f  23718  itg20  23724  itg2const  23727  itg2mulc  23734  itg2addlem  23745  i1fibl  23794  itgitg1  23795  iblabslem  23814  iblabs  23815  bddmulibl  23825  recnprss  23888  dvcjbr  23932  dvfre  23934  dvnfre  23935  dvferm1  23968  dvferm2  23970  rolle  23973  cmvth  23974  mvth  23975  dvlip  23976  dvlipcn  23977  dvlip2  23978  c1liplem1  23979  c1lip2  23981  dvgt0lem1  23985  dvle  23990  dvivthlem1  23991  dvivth  23993  dvne0  23994  lhop1lem  23996  lhop1  23997  lhop2  23998  lhop  23999  dvcnvrelem1  24000  dvcnvrelem2  24001  dvcnvre  24002  dvcvx  24003  dvfsumle  24004  dvfsumge  24005  dvfsumabs  24006  dvfsumlem2  24010  dvfsumrlim  24014  ftc1a  24020  ftc1lem3  24021  ftc1lem6  24024  ftc1  24025  ftc1cn  24026  ftc2  24027  ftc2ditglem  24028  itgparts  24030  itgsubstlem  24031  itgsubst  24032  aacjcl  24302  aalioulem3  24309  taylthlem2  24348  taylth  24349  abelth2  24416  reeff1olem  24420  efcvx  24423  pilem3  24427  pilem3OLD  24428  pige3  24490  recosf1o  24502  resinf1o  24503  dvrelog  24604  relogcn  24605  logcnlem5  24613  logcn  24614  dvloglem  24615  dvlog2lem  24619  logccv  24630  dvcxp1  24702  cxpcn3  24710  resqrtcn  24711  loglesqrt  24720  ssscongptld  24773  ressatans  24882  rlimcnp  24913  efrlim  24917  jensenlem1  24934  jensenlem2  24935  jensen  24936  amgm  24938  lgamgulmlem2  24977  ftalem3  25022  basellem9  25036  efnnfsumcl  25050  efchtdvds  25106  lgsdchr  25301  dchrvmasumlem1  25405  dchrisum0lem3  25429  pntlem3  25519  cchhllem  25988  ipasslem7  28022  fprodex01  29902  rexdiv  29965  fsumrp0cl  30026  xrge0slmod  30175  unitsscn  30273  rmulccn  30305  raddcn  30306  xrge0iifhom  30314  lmlimxrge0  30325  rezh  30346  indsumin  30415  esumpfinvallem  30467  esumpfinval  30468  esumpfinvalf  30469  esumcvg  30479  plymulx0  30955  plymulx  30956  signsplypnf  30958  signsply0  30959  iblidicc  31001  rpsqrtcn  31002  ftc2re  31007  fdvposlt  31008  fdvneggt  31009  fdvposle  31010  fdvnegge  31011  itgexpif  31015  circlemeth  31049  circlemethnat  31050  circlevma  31051  circlemethhgt  31052  logdivsqrle  31059  cvxpconn  31553  cvxsconn  31554  resconn  31557  ivthALT  32658  dnicn  32810  knoppcnlem10  32820  knoppcnlem11  32821  unbdqndv2  32830  knoppndv  32853  knoppcn2  32855  broucube  33775  mblfinlem2  33779  mbfresfi  33788  ftc1cnnclem  33815  ftc1cnnc  33816  ftc1anclem3  33819  ftc1anclem5  33821  ftc1anclem7  33823  ftc1anclem8  33824  ftc1anc  33825  ftc2nc  33826  asindmre  33827  dvreasin  33830  dvreacos  33831  areacirclem1  33832  areacirclem2  33833  areacirclem3  33834  areacirclem4  33835  areacirc  33837  repwsmet  33965  rrnequiv  33966  rrntotbnd  33967  reheibor  33970  iccbnd  33971  itgpowd  38321  arearect  38322  areaquad  38323  k0004val0  38973  extoimad  38985  imo72b2lem0  38986  imo72b2lem2  38988  imo72b2lem1  38992  imo72b2  38996  ssrecnpr  39028  sblpnf  39030  radcnvrat  39034  lhe4.4ex1a  39049  refsumcn  39707  rr2sscn2  40099  uzsscn  40223  ioosscn  40238  evthiccabs  40240  climreeq  40367  limciccioolb  40375  limcrecl  40383  limcicciooub  40391  limcleqr  40398  lptioo2cn  40399  lptioo1cn  40400  limclner  40405  liminflimsupclim  40561  resincncf  40610  cncficcgt0  40623  cncfiooicclem1  40628  cncfiooiccre  40630  jumpncnp  40633  dvcosre  40648  dvmptconst  40651  dvmptidg  40653  fperdvper  40655  dvmptresicc  40656  dvresioo  40658  dvmulcncf  40662  dvdivcncf  40664  dvbdfbdioolem1  40665  ioodvbdlimc1lem1  40668  ioodvbdlimc1lem2  40669  ioodvbdlimc1  40670  ioodvbdlimc2lem  40671  ioodvbdlimc2  40672  itgsin0pilem1  40687  ibliccsinexp  40688  iblioosinexp  40690  itgsinexplem1  40691  itgsinexp  40692  itgcoscmulx  40707  itgsincmulx  40712  itgsubsticclem  40713  itgiccshift  40718  itgperiod  40719  itgsbtaddcnst  40720  dirkeritg  40841  dirkercncflem2  40843  dirkercncflem3  40844  dirkercncflem4  40845  dirkercncf  40846  fourierdlem16  40862  fourierdlem18  40864  fourierdlem21  40867  fourierdlem22  40868  fourierdlem39  40885  fourierdlem42  40888  fourierdlem48  40893  fourierdlem49  40894  fourierdlem53  40898  fourierdlem57  40902  fourierdlem58  40903  fourierdlem59  40904  fourierdlem60  40905  fourierdlem61  40906  fourierdlem62  40907  fourierdlem68  40913  fourierdlem70  40915  fourierdlem72  40917  fourierdlem73  40918  fourierdlem74  40919  fourierdlem75  40920  fourierdlem76  40921  fourierdlem78  40923  fourierdlem80  40925  fourierdlem83  40928  fourierdlem84  40929  fourierdlem85  40930  fourierdlem88  40933  fourierdlem89  40934  fourierdlem90  40935  fourierdlem91  40936  fourierdlem93  40938  fourierdlem94  40939  fourierdlem95  40940  fourierdlem96  40941  fourierdlem97  40942  fourierdlem98  40943  fourierdlem99  40944  fourierdlem101  40946  fourierdlem103  40948  fourierdlem104  40949  fourierdlem111  40956  fourierdlem112  40957  fourierdlem113  40958  fouriercnp  40965  sqwvfoura  40967  sqwvfourb  40968  fouriersw  40970  fouriercn  40971  etransclem2  40975  etransclem18  40991  etransclem23  40996  etransclem46  41019  rrxtopnfi  41028  rrndistlt  41032  sge0sn  41118  sge0tsms  41119  sge0f1o  41121  sge0pr  41133  sge0resplit  41145  sge0iunmptlemre  41154  sge0isummpt2  41171  hoicvr  41287  hoidmvlelem2  41335  refdivmptf  42865  refdivmptfv  42869  amgmlemALT  43081
  Copyright terms: Public domain W3C validator