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 10281
Description: The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by theorem axresscn 10257. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-resscn ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn
StepHypRef Expression
1 cr 10223 . 2 class
2 cc 10222 . 2 class
31, 2wss 3776 1 wff ℝ ⊆ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  recn  10314  reex  10315  recni  10342  nnsscn  11313  nn0sscn  11567  qsscn  12021  reexpcl  13103  rpexpcl  13105  reexpclz  13106  expge0  13122  expge1  13123  rlimrecl  14537  abscn2  14555  recn2  14557  imcn2  14558  climabs  14560  climre  14562  climim  14563  rlimabs  14565  rlimre  14567  rlimim  14568  caurcvgr  14630  caucvgrlem2  14631  caurcvg  14633  fsumrecl  14691  fsumrpcl  14694  fsumge0  14752  fsumre  14765  fsumim  14766  fprodrecl  14907  fprodrpcl  14910  fprodreclf  14913  fprodge0  14947  fprodge1  14949  rerisefaccl  14971  refallfaccl  14972  rprisefaccl  14977  reeff1  15073  nthruc  15204  regsumfsum  20025  rge0srg  20028  rebase  20164  re0g  20170  regsumsupp  20180  remet  22810  tgioo2  22823  xrsdsre  22830  recld2  22834  reperf  22839  iitopon  22899  dfii3  22903  abscncf  22921  recncf  22922  imcncf  22923  abscncfALT  22940  cnmptre  22943  iimulcn  22954  icchmeo  22957  cnrehmeo  22969  evth  22975  evth2  22976  lebnumlem2  22978  lebnumii  22982  reparphti  23013  cphsqrtcl  23200  resscdrg  23371  ishl2  23383  recms  23386  reust  23387  evthicc  23446  evthicc2  23447  ovolfsf  23458  volcn  23593  volivth  23594  ismbf  23615  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  24603  relogcn  24604  logcnlem5  24612  logcn  24613  dvloglem  24614  dvlog2lem  24618  logccv  24629  dvcxp1  24701  cxpcn3  24709  resqrtcn  24710  loglesqrt  24719  ssscongptld  24772  ressatans  24881  rlimcnp  24912  efrlim  24916  jensenlem1  24933  jensenlem2  24934  jensen  24935  amgm  24937  lgamgulmlem2  24976  ftalem3  25021  basellem9  25035  efnnfsumcl  25049  efchtdvds  25105  lgsdchr  25300  dchrvmasumlem1  25404  dchrisum0lem3  25428  pntlem3  25518  cchhllem  25987  ipasslem7  28025  fprodex01  29904  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  31552  cvxsconn  31553  resconn  31556  ivthALT  32656  dnicn  32804  knoppcnlem10  32814  knoppcnlem11  32815  unbdqndv2  32824  knoppndv  32847  knoppcn2  32849  broucube  33758  mblfinlem2  33762  mbfresfi  33770  ftc1cnnclem  33797  ftc1cnnc  33798  ftc1anclem3  33801  ftc1anclem5  33803  ftc1anclem7  33805  ftc1anclem8  33806  ftc1anc  33807  ftc2nc  33808  asindmre  33809  dvreasin  33812  dvreacos  33813  areacirclem1  33814  areacirclem2  33815  areacirclem3  33816  areacirclem4  33817  areacirc  33819  repwsmet  33946  rrnequiv  33947  rrntotbnd  33948  reheibor  33951  iccbnd  33952  itgpowd  38301  arearect  38302  areaquad  38303  k0004val0  38953  extoimad  38965  imo72b2lem0  38966  imo72b2lem2  38968  imo72b2lem1  38972  imo72b2  38976  ssrecnpr  39008  sblpnf  39010  radcnvrat  39014  lhe4.4ex1a  39029  refsumcn  39684  rr2sscn2  40063  uzsscn  40186  ioosscn  40201  evthiccabs  40203  climreeq  40326  limciccioolb  40334  limcrecl  40342  limcicciooub  40350  limcleqr  40357  lptioo2cn  40358  lptioo1cn  40359  limclner  40364  liminflimsupclim  40520  resincncf  40569  cncficcgt0  40582  cncfiooicclem1  40587  cncfiooiccre  40589  jumpncnp  40592  dvcosre  40607  dvmptconst  40610  dvmptidg  40612  fperdvper  40614  dvmptresicc  40615  dvresioo  40617  dvmulcncf  40621  dvdivcncf  40623  dvbdfbdioolem1  40624  ioodvbdlimc1lem1  40627  ioodvbdlimc1lem2  40628  ioodvbdlimc1  40629  ioodvbdlimc2lem  40630  ioodvbdlimc2  40631  itgsin0pilem1  40646  ibliccsinexp  40647  iblioosinexp  40649  itgsinexplem1  40650  itgsinexp  40651  itgcoscmulx  40665  itgsincmulx  40670  itgsubsticclem  40671  itgiccshift  40676  itgperiod  40677  itgsbtaddcnst  40678  dirkeritg  40799  dirkercncflem2  40801  dirkercncflem3  40802  dirkercncflem4  40803  dirkercncf  40804  fourierdlem16  40820  fourierdlem18  40822  fourierdlem21  40825  fourierdlem22  40826  fourierdlem39  40843  fourierdlem42  40846  fourierdlem48  40851  fourierdlem49  40852  fourierdlem53  40856  fourierdlem57  40860  fourierdlem58  40861  fourierdlem59  40862  fourierdlem60  40863  fourierdlem61  40864  fourierdlem62  40865  fourierdlem68  40871  fourierdlem70  40873  fourierdlem72  40875  fourierdlem73  40876  fourierdlem74  40877  fourierdlem75  40878  fourierdlem76  40879  fourierdlem78  40881  fourierdlem80  40883  fourierdlem83  40886  fourierdlem84  40887  fourierdlem85  40888  fourierdlem88  40891  fourierdlem89  40892  fourierdlem90  40893  fourierdlem91  40894  fourierdlem93  40896  fourierdlem94  40897  fourierdlem95  40898  fourierdlem96  40899  fourierdlem97  40900  fourierdlem98  40901  fourierdlem99  40902  fourierdlem101  40904  fourierdlem103  40906  fourierdlem104  40907  fourierdlem111  40914  fourierdlem112  40915  fourierdlem113  40916  fouriercnp  40923  sqwvfoura  40925  sqwvfourb  40926  fouriersw  40928  fouriercn  40929  etransclem2  40933  etransclem18  40949  etransclem23  40954  etransclem46  40977  rrxtopnfi  40986  rrndistlt  40990  sge0sn  41076  sge0tsms  41077  sge0f1o  41079  sge0pr  41091  sge0resplit  41103  sge0iunmptlemre  41112  sge0isummpt2  41129  hoicvr  41245  hoidmvlelem2  41293  refdivmptf  42905  refdivmptfv  42909  amgmlemALT  43121
  Copyright terms: Public domain W3C validator