Axiom ax-resscn 11101

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11043	. 2 class ℝ
2		cc 11042	. 2 class ℂ
3	1, 2	wss 3911	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11134  reex  11135  recni  11164  qsscn  12895  ioosscn  13345  unitsscn  13437  reexpcl  14019  rpexpcl  14021  reexpclz  14023  expge0  14039  expge1  14040  rlimrecl  15522  abscn2  15541  recn2  15543  imcn2  15544  climabs  15546  climre  15548  climim  15549  rlimabs  15551  rlimre  15553  rlimim  15554  caurcvgr  15616  caucvgrlem2  15617  caurcvg  15619  fsumrecl  15676  fsumrpcl  15679  fsumge0  15737  fsumre  15750  fsumim  15751  fprodrecl  15895  fprodrpcl  15898  fprodreclf  15901  fprodge0  15935  fprodge1  15937  rerisefaccl  15959  refallfaccl  15960  rprisefaccl  15965  reeff1  16064  nthruc  16196  regsumfsum  21328  rge0srg  21331  rebase  21491  re0g  21497  regsumsupp  21507  remet  24654  tgioo2  24667  xrsdsre  24675  recld2  24679  reperf  24684  iitopon  24748  dfii3  24752  abscncf  24770  recncf  24771  imcncf  24772  abscncfALT  24794  cnmptre  24797  iimulcnOLD  24811  icchmeo  24814  icchmeoOLD  24815  cnrehmeo  24827  cnrehmeoOLD  24828  evth  24834  evth2  24835  lebnumlem2  24837  lebnumii  24841  reparphtiOLD  24873  cphsqrtcl  25060  resscdrg  25234  ishl2  25246  recms  25256  reust  25257  evthicc  25336  evthicc2  25337  ovolfsf  25348  volcn  25483  volivth  25484  ismbf  25505  cncombf  25535  cnmbf  25536  0plef  25549  itg1ge0  25563  i1faddlem  25570  i1fmul  25573  itg1addlem4  25576  i1fsub  25585  itg1sub  25586  mbfi1fseqlem5  25596  xrge0f  25608  itg20  25614  itg2const  25617  itg2mulc  25624  itg2addlem  25635  i1fibl  25685  itgitg1  25686  iblabslem  25705  iblabs  25706  bddmulibl  25716  recnprss  25781  dvmptresicc  25793  dvcjbr  25829  dvfre  25831  dvnfre  25832  dvferm1  25865  dvferm2  25867  rolle  25870  cmvth  25871  cmvthOLD  25872  mvth  25873  dvlip  25874  dvlipcn  25875  dvlip2  25876  c1liplem1  25877  c1lip2  25879  dvgt0lem1  25883  dvle  25888  dvivthlem1  25889  dvivth  25891  dvne0  25892  lhop1lem  25894  lhop1  25895  lhop2  25896  lhop  25897  dvcnvrelem1  25898  dvcnvrelem2  25899  dvcnvre  25900  dvcvx  25901  dvfsumle  25902  dvfsumleOLD  25903  dvfsumge  25904  dvfsumabs  25905  dvfsumlem2  25909  dvfsumlem2OLD  25910  dvfsumrlim  25914  ftc1a  25920  ftc1lem3  25921  ftc1lem6  25924  ftc1  25925  ftc1cn  25926  ftc2  25927  ftc2ditglem  25928  itgparts  25930  itgsubstlem  25931  itgsubst  25932  itgpowd  25933  aacjcl  26211  aalioulem3  26218  taylthlem2  26258  taylthlem2OLD  26259  taylth  26260  abelth2  26328  reeff1olem  26332  efcvx  26335  pilem3  26339  pige3ALT  26405  recosf1o  26420  resinf1o  26421  dvrelog  26522  relogcn  26523  logcnlem5  26531  logcn  26532  dvloglem  26533  dvlog2lem  26537  logccv  26548  dvcxp1  26625  cxpcn3  26634  resqrtcn  26635  loglesqrt  26647  ssscongptld  26708  ressatans  26820  rlimcnp  26851  efrlim  26855  efrlimOLD  26856  jensenlem1  26873  jensenlem2  26874  jensen  26875  amgm  26877  lgamgulmlem2  26916  ftalem3  26961  basellem9  26975  efnnfsumcl  26989  efchtdvds  27045  lgsdchr  27242  dchrvmasumlem1  27382  dchrisum0lem3  27406  pntlem3  27496  cchhllem  28790  ex-fpar  30364  ipasslem7  30738  fprodex01  32723  indsumin  32758  rexdiv  32819  fsumrp0cl  32935  xrge0slmod  33292  ccfldsrarelvec  33639  ccfldextdgrr  33640  rmulccn  33891  raddcn  33892  xrge0iifhom  33900  lmlimxrge0  33911  rezh  33932  esumpfinvallem  34037  esumpfinval  34038  esumpfinvalf  34039  esumcvg  34049  plymulx0  34511  plymulx  34512  signsplypnf  34514  signsply0  34515  iblidicc  34556  rpsqrtcn  34557  ftc2re  34562  fdvposlt  34563  fdvneggt  34564  fdvposle  34565  fdvnegge  34566  itgexpif  34570  circlemeth  34604  circlemethnat  34605  circlevma  34606  circlemethhgt  34607  logdivsqrle  34614  resconn  35206  ivthALT  36296  dnicn  36453  knoppcnlem10  36463  knoppcnlem11  36464  unbdqndv2  36472  knoppndv  36495  knoppcn2  36497  broucube  37621  mblfinlem2  37625  mbfresfi  37633  ftc1cnnclem  37658  ftc1cnnc  37659  ftc1anclem3  37662  ftc1anclem5  37664  ftc1anclem7  37666  ftc1anclem8  37667  ftc1anc  37668  ftc2nc  37669  asindmre  37670  dvreasin  37673  dvreacos  37674  areacirclem1  37675  areacirclem2  37676  areacirclem3  37677  areacirclem4  37678  areacirc  37680  repwsmet  37801  rrnequiv  37802  rrntotbnd  37803  reheibor  37806  iccbnd  37807  intlewftc  42022  dvrelog2  42025  dvrelog3  42026  aks4d1p1p5  42036  rpsscn  42260  redvmptabs  42321  readvrec2  42322  resuppsinopn  42324  readvcot  42325  resubeqsub  42391  subresre  42392  arearect  43177  areaquad  43178  k0004val0  44116  extoimad  44126  imo72b2lem0  44127  imo72b2lem2  44129  imo72b2lem1  44131  imo72b2  44134  ssrecnpr  44270  sblpnf  44272  radcnvrat  44276  lhe4.4ex1a  44291  refsumcn  44997  rr2sscn2  45335  uzsscn  45444  evthiccabs  45467  climreeq  45584  limciccioolb  45592  limcrecl  45600  limcicciooub  45608  limcleqr  45615  lptioo2cn  45616  lptioo1cn  45617  limclner  45622  liminflimsupclim  45778  resincncf  45846  cncficcgt0  45859  cncfiooicclem1  45864  cncfiooiccre  45866  jumpncnp  45869  dvcosre  45883  dvmptconst  45886  dvmptidg  45888  fperdvper  45890  dvresioo  45892  dvmulcncf  45896  dvdivcncf  45898  dvbdfbdioolem1  45899  ioodvbdlimc1lem1  45902  ioodvbdlimc1lem2  45903  ioodvbdlimc1  45904  ioodvbdlimc2lem  45905  ioodvbdlimc2  45906  itgsin0pilem1  45921  ibliccsinexp  45922  iblioosinexp  45924  itgsinexplem1  45925  itgsinexp  45926  itgcoscmulx  45940  itgsincmulx  45945  itgsubsticclem  45946  itgiccshift  45951  itgperiod  45952  itgsbtaddcnst  45953  dirkeritg  46073  dirkercncflem2  46075  dirkercncflem3  46076  dirkercncflem4  46077  dirkercncf  46078  fourierdlem16  46094  fourierdlem18  46096  fourierdlem21  46099  fourierdlem22  46100  fourierdlem39  46117  fourierdlem42  46120  fourierdlem48  46125  fourierdlem49  46126  fourierdlem53  46130  fourierdlem57  46134  fourierdlem58  46135  fourierdlem59  46136  fourierdlem60  46137  fourierdlem61  46138  fourierdlem62  46139  fourierdlem68  46145  fourierdlem70  46147  fourierdlem72  46149  fourierdlem73  46150  fourierdlem74  46151  fourierdlem75  46152  fourierdlem76  46153  fourierdlem78  46155  fourierdlem80  46157  fourierdlem83  46160  fourierdlem84  46161  fourierdlem85  46162  fourierdlem88  46165  fourierdlem89  46166  fourierdlem90  46167  fourierdlem91  46168  fourierdlem93  46170  fourierdlem94  46171  fourierdlem95  46172  fourierdlem96  46173  fourierdlem97  46174  fourierdlem98  46175  fourierdlem99  46176  fourierdlem101  46178  fourierdlem103  46180  fourierdlem104  46181  fourierdlem111  46188  fourierdlem112  46189  fourierdlem113  46190  fouriercnp  46197  sqwvfoura  46199  sqwvfourb  46200  fouriersw  46202  fouriercn  46203  etransclem2  46207  etransclem18  46223  etransclem23  46228  etransclem46  46251  rrxtopnfi  46258  rrndistlt  46261  sge0sn  46350  sge0tsms  46351  sge0f1o  46353  sge0pr  46365  sge0resplit  46377  sge0iunmptlemre  46386  sge0isummpt2  46403  hoicvr  46519  hoidmvlelem2  46567  lamberte  46862  refdivmptf  48504  refdivmptfv  48508  amgmlemALT  49765