Axiom ax-resscn 11066

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11008	. 2 class ℝ
2		cc 11007	. 2 class ℂ
3	1, 2	wss 3903	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11099  reex  11100  recni  11129  qsscn  12861  ioosscn  13311  unitsscn  13403  reexpcl  13985  rpexpcl  13987  reexpclz  13989  expge0  14005  expge1  14006  rlimrecl  15487  abscn2  15506  recn2  15508  imcn2  15509  climabs  15511  climre  15513  climim  15514  rlimabs  15516  rlimre  15518  rlimim  15519  caurcvgr  15581  caucvgrlem2  15582  caurcvg  15584  fsumrecl  15641  fsumrpcl  15644  fsumge0  15702  fsumre  15715  fsumim  15716  fprodrecl  15860  fprodrpcl  15863  fprodreclf  15866  fprodge0  15900  fprodge1  15902  rerisefaccl  15924  refallfaccl  15925  rprisefaccl  15930  reeff1  16029  nthruc  16161  regsumfsum  21342  rge0srg  21345  rebase  21513  re0g  21519  regsumsupp  21529  remet  24676  tgioo2  24689  xrsdsre  24697  recld2  24701  reperf  24706  iitopon  24770  dfii3  24774  abscncf  24792  recncf  24793  imcncf  24794  abscncfALT  24816  cnmptre  24819  iimulcnOLD  24833  icchmeo  24836  icchmeoOLD  24837  cnrehmeo  24849  cnrehmeoOLD  24850  evth  24856  evth2  24857  lebnumlem2  24859  lebnumii  24863  reparphtiOLD  24895  cphsqrtcl  25082  resscdrg  25256  ishl2  25268  recms  25278  reust  25279  evthicc  25358  evthicc2  25359  ovolfsf  25370  volcn  25505  volivth  25506  ismbf  25527  cncombf  25557  cnmbf  25558  0plef  25571  itg1ge0  25585  i1faddlem  25592  i1fmul  25595  itg1addlem4  25598  i1fsub  25607  itg1sub  25608  mbfi1fseqlem5  25618  xrge0f  25630  itg20  25636  itg2const  25639  itg2mulc  25646  itg2addlem  25657  i1fibl  25707  itgitg1  25708  iblabslem  25727  iblabs  25728  bddmulibl  25738  recnprss  25803  dvmptresicc  25815  dvcjbr  25851  dvfre  25853  dvnfre  25854  dvferm1  25887  dvferm2  25889  rolle  25892  cmvth  25893  cmvthOLD  25894  mvth  25895  dvlip  25896  dvlipcn  25897  dvlip2  25898  c1liplem1  25899  c1lip2  25901  dvgt0lem1  25905  dvle  25910  dvivthlem1  25911  dvivth  25913  dvne0  25914  lhop1lem  25916  lhop1  25917  lhop2  25918  lhop  25919  dvcnvrelem1  25920  dvcnvrelem2  25921  dvcnvre  25922  dvcvx  25923  dvfsumle  25924  dvfsumleOLD  25925  dvfsumge  25926  dvfsumabs  25927  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsumrlim  25936  ftc1a  25942  ftc1lem3  25943  ftc1lem6  25946  ftc1  25947  ftc1cn  25948  ftc2  25949  ftc2ditglem  25950  itgparts  25952  itgsubstlem  25953  itgsubst  25954  itgpowd  25955  aacjcl  26233  aalioulem3  26240  taylthlem2  26280  taylthlem2OLD  26281  taylth  26282  abelth2  26350  reeff1olem  26354  efcvx  26357  pilem3  26361  pige3ALT  26427  recosf1o  26442  resinf1o  26443  dvrelog  26544  relogcn  26545  logcnlem5  26553  logcn  26554  dvloglem  26555  dvlog2lem  26559  logccv  26570  dvcxp1  26647  cxpcn3  26656  resqrtcn  26657  loglesqrt  26669  ssscongptld  26730  ressatans  26842  rlimcnp  26873  efrlim  26877  efrlimOLD  26878  jensenlem1  26895  jensenlem2  26896  jensen  26897  amgm  26899  lgamgulmlem2  26938  ftalem3  26983  basellem9  26997  efnnfsumcl  27011  efchtdvds  27067  lgsdchr  27264  dchrvmasumlem1  27404  dchrisum0lem3  27428  pntlem3  27518  cchhllem  28832  ex-fpar  30406  ipasslem7  30780  fprodex01  32771  indsumin  32806  rexdiv  32867  fsumrp0cl  32976  xrge0slmod  33286  ccfldsrarelvec  33644  ccfldextdgrr  33645  rmulccn  33901  raddcn  33902  xrge0iifhom  33910  lmlimxrge0  33921  rezh  33942  esumpfinvallem  34047  esumpfinval  34048  esumpfinvalf  34049  esumcvg  34059  plymulx0  34521  plymulx  34522  signsplypnf  34524  signsply0  34525  iblidicc  34566  rpsqrtcn  34567  ftc2re  34572  fdvposlt  34573  fdvneggt  34574  fdvposle  34575  fdvnegge  34576  itgexpif  34580  circlemeth  34614  circlemethnat  34615  circlevma  34616  circlemethhgt  34617  logdivsqrle  34624  resconn  35229  ivthALT  36319  dnicn  36476  knoppcnlem10  36486  knoppcnlem11  36487  unbdqndv2  36495  knoppndv  36518  knoppcn2  36520  broucube  37644  mblfinlem2  37648  mbfresfi  37656  ftc1cnnclem  37681  ftc1cnnc  37682  ftc1anclem3  37685  ftc1anclem5  37687  ftc1anclem7  37689  ftc1anclem8  37690  ftc1anc  37691  ftc2nc  37692  asindmre  37693  dvreasin  37696  dvreacos  37697  areacirclem1  37698  areacirclem2  37699  areacirclem3  37700  areacirclem4  37701  areacirc  37703  repwsmet  37824  rrnequiv  37825  rrntotbnd  37826  reheibor  37829  iccbnd  37830  intlewftc  42044  dvrelog2  42047  dvrelog3  42048  aks4d1p1p5  42058  rpsscn  42282  redvmptabs  42343  readvrec2  42344  resuppsinopn  42346  readvcot  42347  resubeqsub  42413  subresre  42414  arearect  43198  areaquad  43199  k0004val0  44137  extoimad  44147  imo72b2lem0  44148  imo72b2lem2  44150  imo72b2lem1  44152  imo72b2  44155  ssrecnpr  44291  sblpnf  44293  radcnvrat  44297  lhe4.4ex1a  44312  refsumcn  45018  rr2sscn2  45355  uzsscn  45464  evthiccabs  45487  climreeq  45604  limciccioolb  45612  limcrecl  45620  limcicciooub  45628  limcleqr  45635  lptioo2cn  45636  lptioo1cn  45637  limclner  45642  liminflimsupclim  45798  resincncf  45866  cncficcgt0  45879  cncfiooicclem1  45884  cncfiooiccre  45886  jumpncnp  45889  dvcosre  45903  dvmptconst  45906  dvmptidg  45908  fperdvper  45910  dvresioo  45912  dvmulcncf  45916  dvdivcncf  45918  dvbdfbdioolem1  45919  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc1  45924  ioodvbdlimc2lem  45925  ioodvbdlimc2  45926  itgsin0pilem1  45941  ibliccsinexp  45942  iblioosinexp  45944  itgsinexplem1  45945  itgsinexp  45946  itgcoscmulx  45960  itgsincmulx  45965  itgsubsticclem  45966  itgiccshift  45971  itgperiod  45972  itgsbtaddcnst  45973  dirkeritg  46093  dirkercncflem2  46095  dirkercncflem3  46096  dirkercncflem4  46097  dirkercncf  46098  fourierdlem16  46114  fourierdlem18  46116  fourierdlem21  46119  fourierdlem22  46120  fourierdlem39  46137  fourierdlem42  46140  fourierdlem48  46145  fourierdlem49  46146  fourierdlem53  46150  fourierdlem57  46154  fourierdlem58  46155  fourierdlem59  46156  fourierdlem60  46157  fourierdlem61  46158  fourierdlem62  46159  fourierdlem68  46165  fourierdlem70  46167  fourierdlem72  46169  fourierdlem73  46170  fourierdlem74  46171  fourierdlem75  46172  fourierdlem76  46173  fourierdlem78  46175  fourierdlem80  46177  fourierdlem83  46180  fourierdlem84  46181  fourierdlem85  46182  fourierdlem88  46185  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fourierdlem93  46190  fourierdlem94  46191  fourierdlem95  46192  fourierdlem96  46193  fourierdlem97  46194  fourierdlem98  46195  fourierdlem99  46196  fourierdlem101  46198  fourierdlem103  46200  fourierdlem104  46201  fourierdlem111  46208  fourierdlem112  46209  fourierdlem113  46210  fouriercnp  46217  sqwvfoura  46219  sqwvfourb  46220  fouriersw  46222  fouriercn  46223  etransclem2  46227  etransclem18  46243  etransclem23  46248  etransclem46  46271  rrxtopnfi  46278  rrndistlt  46281  sge0sn  46370  sge0tsms  46371  sge0f1o  46373  sge0pr  46385  sge0resplit  46397  sge0iunmptlemre  46406  sge0isummpt2  46423  hoicvr  46539  hoidmvlelem2  46587  lamberte  46882  refdivmptf  48537  refdivmptfv  48541  amgmlemALT  49798