Axiom ax-resscn 10834

Description: The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by Theorem axresscn 10810. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 10776	. 2 class ℝ
2		cc 10775	. 2 class ℂ
3	1, 2	wss 3884	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  10867  reex  10868  recni  10895  qsscn  12604  ioosscn  13045  unitsscn  13136  reexpcl  13702  rpexpcl  13704  reexpclz  13705  expge0  13722  expge1  13723  rlimrecl  15192  abscn2  15211  recn2  15213  imcn2  15214  climabs  15216  climre  15218  climim  15219  rlimabs  15221  rlimre  15223  rlimim  15224  caurcvgr  15288  caucvgrlem2  15289  caurcvg  15291  fsumrecl  15349  fsumrpcl  15352  fsumge0  15410  fsumre  15423  fsumim  15424  fprodrecl  15566  fprodrpcl  15569  fprodreclf  15572  fprodge0  15606  fprodge1  15608  rerisefaccl  15630  refallfaccl  15631  rprisefaccl  15636  reeff1  15732  nthruc  15864  regsumfsum  20553  rge0srg  20556  rebase  20698  re0g  20704  regsumsupp  20714  remet  23834  tgioo2  23847  xrsdsre  23854  recld2  23858  reperf  23863  iitopon  23923  dfii3  23927  abscncf  23945  recncf  23946  imcncf  23947  abscncfALT  23968  cnmptre  23971  iimulcn  23982  icchmeo  23985  cnrehmeo  23997  evth  24003  evth2  24004  lebnumlem2  24006  lebnumii  24010  reparphti  24041  cphsqrtcl  24228  resscdrg  24402  ishl2  24414  recms  24424  reust  24425  evthicc  24503  evthicc2  24504  ovolfsf  24515  volcn  24650  volivth  24651  ismbf  24672  cncombf  24702  cnmbf  24703  0plef  24716  itg1ge0  24730  i1faddlem  24737  i1fmul  24740  itg1addlem4  24743  itg1addlem4OLD  24744  i1fsub  24753  itg1sub  24754  mbfi1fseqlem5  24764  xrge0f  24776  itg20  24782  itg2const  24785  itg2mulc  24792  itg2addlem  24803  i1fibl  24852  itgitg1  24853  iblabslem  24872  iblabs  24873  bddmulibl  24883  recnprss  24948  dvmptresicc  24960  dvcjbr  24993  dvfre  24995  dvnfre  24996  dvferm1  25029  dvferm2  25031  rolle  25034  cmvth  25035  mvth  25036  dvlip  25037  dvlipcn  25038  dvlip2  25039  c1liplem1  25040  c1lip2  25042  dvgt0lem1  25046  dvle  25051  dvivthlem1  25052  dvivth  25054  dvne0  25055  lhop1lem  25057  lhop1  25058  lhop2  25059  lhop  25060  dvcnvrelem1  25061  dvcnvrelem2  25062  dvcnvre  25063  dvcvx  25064  dvfsumle  25065  dvfsumge  25066  dvfsumabs  25067  dvfsumlem2  25071  dvfsumrlim  25075  ftc1a  25081  ftc1lem3  25082  ftc1lem6  25085  ftc1  25086  ftc1cn  25087  ftc2  25088  ftc2ditglem  25089  itgparts  25091  itgsubstlem  25092  itgsubst  25093  itgpowd  25094  aacjcl  25367  aalioulem3  25374  taylthlem2  25413  taylth  25414  abelth2  25481  reeff1olem  25485  efcvx  25488  pilem3  25492  pige3ALT  25556  recosf1o  25571  resinf1o  25572  dvrelog  25672  relogcn  25673  logcnlem5  25681  logcn  25682  dvloglem  25683  dvlog2lem  25687  logccv  25698  dvcxp1  25773  cxpcn3  25781  resqrtcn  25782  loglesqrt  25791  ssscongptld  25852  ressatans  25964  rlimcnp  25995  efrlim  25999  jensenlem1  26016  jensenlem2  26017  jensen  26018  amgm  26020  lgamgulmlem2  26059  ftalem3  26104  basellem9  26118  efnnfsumcl  26132  efchtdvds  26188  lgsdchr  26383  dchrvmasumlem1  26523  dchrisum0lem3  26547  pntlem3  26637  cchhllem  27132  cchhllemOLD  27133  ex-fpar  28702  ipasslem7  29074  fprodex01  31016  rexdiv  31077  fsumrp0cl  31181  xrge0slmod  31425  ccfldsrarelvec  31618  ccfldextdgrr  31619  rmulccn  31755  raddcn  31756  xrge0iifhom  31764  lmlimxrge0  31775  rezh  31796  indsumin  31865  esumpfinvallem  31917  esumpfinval  31918  esumpfinvalf  31919  esumcvg  31929  plymulx0  32401  plymulx  32402  signsplypnf  32404  signsply0  32405  iblidicc  32447  rpsqrtcn  32448  ftc2re  32453  fdvposlt  32454  fdvneggt  32455  fdvposle  32456  fdvnegge  32457  itgexpif  32461  circlemeth  32495  circlemethnat  32496  circlevma  32497  circlemethhgt  32498  logdivsqrle  32505  cvxpconn  33079  cvxsconn  33080  resconn  33083  ivthALT  34426  dnicn  34574  knoppcnlem10  34584  knoppcnlem11  34585  unbdqndv2  34593  knoppndv  34616  knoppcn2  34618  broucube  35717  mblfinlem2  35721  mbfresfi  35729  ftc1cnnclem  35754  ftc1cnnc  35755  ftc1anclem3  35758  ftc1anclem5  35760  ftc1anclem7  35762  ftc1anclem8  35763  ftc1anc  35764  ftc2nc  35765  asindmre  35766  dvreasin  35769  dvreacos  35770  areacirclem1  35771  areacirclem2  35772  areacirclem3  35773  areacirclem4  35774  areacirc  35776  repwsmet  35898  rrnequiv  35899  rrntotbnd  35900  reheibor  35903  iccbnd  35904  intlewftc  39976  dvrelog2  39978  dvrelog3  39979  aks4d1p1p5  39989  resubeqsub  40304  subresre  40305  arearect  40934  areaquad  40935  k0004val0  41626  extoimad  41637  imo72b2lem0  41638  imo72b2lem2  41640  imo72b2lem1  41642  imo72b2  41645  ssrecnpr  41788  sblpnf  41790  radcnvrat  41794  lhe4.4ex1a  41809  refsumcn  42435  rr2sscn2  42768  uzsscn  42879  evthiccabs  42897  climreeq  43017  limciccioolb  43025  limcrecl  43033  limcicciooub  43041  limcleqr  43048  lptioo2cn  43049  lptioo1cn  43050  limclner  43055  liminflimsupclim  43211  resincncf  43279  cncficcgt0  43292  cncfiooicclem1  43297  cncfiooiccre  43299  jumpncnp  43302  dvcosre  43316  dvmptconst  43319  dvmptidg  43321  fperdvper  43323  dvresioo  43325  dvmulcncf  43329  dvdivcncf  43331  dvbdfbdioolem1  43332  ioodvbdlimc1lem1  43335  ioodvbdlimc1lem2  43336  ioodvbdlimc1  43337  ioodvbdlimc2lem  43338  ioodvbdlimc2  43339  itgsin0pilem1  43354  ibliccsinexp  43355  iblioosinexp  43357  itgsinexplem1  43358  itgsinexp  43359  itgcoscmulx  43373  itgsincmulx  43378  itgsubsticclem  43379  itgiccshift  43384  itgperiod  43385  itgsbtaddcnst  43386  dirkeritg  43506  dirkercncflem2  43508  dirkercncflem3  43509  dirkercncflem4  43510  dirkercncf  43511  fourierdlem16  43527  fourierdlem18  43529  fourierdlem21  43532  fourierdlem22  43533  fourierdlem39  43550  fourierdlem42  43553  fourierdlem48  43558  fourierdlem49  43559  fourierdlem53  43563  fourierdlem57  43567  fourierdlem58  43568  fourierdlem59  43569  fourierdlem60  43570  fourierdlem61  43571  fourierdlem62  43572  fourierdlem68  43578  fourierdlem70  43580  fourierdlem72  43582  fourierdlem73  43583  fourierdlem74  43584  fourierdlem75  43585  fourierdlem76  43586  fourierdlem78  43588  fourierdlem80  43590  fourierdlem83  43593  fourierdlem84  43594  fourierdlem85  43595  fourierdlem88  43598  fourierdlem89  43599  fourierdlem90  43600  fourierdlem91  43601  fourierdlem93  43603  fourierdlem94  43604  fourierdlem95  43605  fourierdlem96  43606  fourierdlem97  43607  fourierdlem98  43608  fourierdlem99  43609  fourierdlem101  43611  fourierdlem103  43613  fourierdlem104  43614  fourierdlem111  43621  fourierdlem112  43622  fourierdlem113  43623  fouriercnp  43630  sqwvfoura  43632  sqwvfourb  43633  fouriersw  43635  fouriercn  43636  etransclem2  43640  etransclem18  43656  etransclem23  43661  etransclem46  43684  rrxtopnfi  43691  rrndistlt  43694  sge0sn  43780  sge0tsms  43781  sge0f1o  43783  sge0pr  43795  sge0resplit  43807  sge0iunmptlemre  43816  sge0isummpt2  43833  hoicvr  43949  hoidmvlelem2  43997  refdivmptf  45749  refdivmptfv  45753  amgmlemALT  46366