Axiom ax-resscn 11169

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11111	. 2 class ℝ
2		cc 11110	. 2 class ℂ
3	1, 2	wss 3943	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11202  reex  11203  recni  11232  qsscn  12948  ioosscn  13392  unitsscn  13483  reexpcl  14049  rpexpcl  14051  reexpclz  14053  expge0  14069  expge1  14070  rlimrecl  15530  abscn2  15549  recn2  15551  imcn2  15552  climabs  15554  climre  15556  climim  15557  rlimabs  15559  rlimre  15561  rlimim  15562  caurcvgr  15626  caucvgrlem2  15627  caurcvg  15629  fsumrecl  15686  fsumrpcl  15689  fsumge0  15747  fsumre  15760  fsumim  15761  fprodrecl  15903  fprodrpcl  15906  fprodreclf  15909  fprodge0  15943  fprodge1  15945  rerisefaccl  15967  refallfaccl  15968  rprisefaccl  15973  reeff1  16070  nthruc  16202  regsumfsum  21329  rge0srg  21332  rebase  21499  re0g  21505  regsumsupp  21515  remet  24661  tgioo2  24674  xrsdsre  24681  recld2  24685  reperf  24690  iitopon  24754  dfii3  24758  abscncf  24776  recncf  24777  imcncf  24778  abscncfALT  24800  cnmptre  24803  iimulcnOLD  24817  icchmeo  24820  icchmeoOLD  24821  cnrehmeo  24833  cnrehmeoOLD  24834  evth  24840  evth2  24841  lebnumlem2  24843  lebnumii  24847  reparphtiOLD  24879  cphsqrtcl  25067  resscdrg  25241  ishl2  25253  recms  25263  reust  25264  evthicc  25343  evthicc2  25344  ovolfsf  25355  volcn  25490  volivth  25491  ismbf  25512  cncombf  25542  cnmbf  25543  0plef  25556  itg1ge0  25570  i1faddlem  25577  i1fmul  25580  itg1addlem4  25583  itg1addlem4OLD  25584  i1fsub  25593  itg1sub  25594  mbfi1fseqlem5  25604  xrge0f  25616  itg20  25622  itg2const  25625  itg2mulc  25632  itg2addlem  25643  i1fibl  25692  itgitg1  25693  iblabslem  25712  iblabs  25713  bddmulibl  25723  recnprss  25788  dvmptresicc  25800  dvcjbr  25836  dvfre  25838  dvnfre  25839  dvferm1  25872  dvferm2  25874  rolle  25877  cmvth  25878  cmvthOLD  25879  mvth  25880  dvlip  25881  dvlipcn  25882  dvlip2  25883  c1liplem1  25884  c1lip2  25886  dvgt0lem1  25890  dvle  25895  dvivthlem1  25896  dvivth  25898  dvne0  25899  lhop1lem  25901  lhop1  25902  lhop2  25903  lhop  25904  dvcnvrelem1  25905  dvcnvrelem2  25906  dvcnvre  25907  dvcvx  25908  dvfsumle  25909  dvfsumleOLD  25910  dvfsumge  25911  dvfsumabs  25912  dvfsumlem2  25916  dvfsumlem2OLD  25917  dvfsumrlim  25921  ftc1a  25927  ftc1lem3  25928  ftc1lem6  25931  ftc1  25932  ftc1cn  25933  ftc2  25934  ftc2ditglem  25935  itgparts  25937  itgsubstlem  25938  itgsubst  25939  itgpowd  25940  aacjcl  26217  aalioulem3  26224  taylthlem2  26264  taylthlem2OLD  26265  taylth  26266  abelth2  26334  reeff1olem  26338  efcvx  26341  pilem3  26345  pige3ALT  26409  recosf1o  26424  resinf1o  26425  dvrelog  26526  relogcn  26527  logcnlem5  26535  logcn  26536  dvloglem  26537  dvlog2lem  26541  logccv  26552  dvcxp1  26629  cxpcn3  26638  resqrtcn  26639  loglesqrt  26648  ssscongptld  26709  ressatans  26821  rlimcnp  26852  efrlim  26856  efrlimOLD  26857  jensenlem1  26874  jensenlem2  26875  jensen  26876  amgm  26878  lgamgulmlem2  26917  ftalem3  26962  basellem9  26976  efnnfsumcl  26990  efchtdvds  27046  lgsdchr  27243  dchrvmasumlem1  27383  dchrisum0lem3  27407  pntlem3  27497  cchhllem  28652  cchhllemOLD  28653  ex-fpar  30224  ipasslem7  30598  fprodex01  32536  rexdiv  32597  fsumrp0cl  32699  xrge0slmod  32966  ccfldsrarelvec  33264  ccfldextdgrr  33265  rmulccn  33438  raddcn  33439  xrge0iifhom  33447  lmlimxrge0  33458  rezh  33481  indsumin  33550  esumpfinvallem  33602  esumpfinval  33603  esumpfinvalf  33604  esumcvg  33614  plymulx0  34088  plymulx  34089  signsplypnf  34091  signsply0  34092  iblidicc  34133  rpsqrtcn  34134  ftc2re  34139  fdvposlt  34140  fdvneggt  34141  fdvposle  34142  fdvnegge  34143  itgexpif  34147  circlemeth  34181  circlemethnat  34182  circlevma  34183  circlemethhgt  34184  logdivsqrle  34191  resconn  34765  ivthALT  35728  dnicn  35876  knoppcnlem10  35886  knoppcnlem11  35887  unbdqndv2  35895  knoppndv  35918  knoppcn2  35920  broucube  37035  mblfinlem2  37039  mbfresfi  37047  ftc1cnnclem  37072  ftc1cnnc  37073  ftc1anclem3  37076  ftc1anclem5  37078  ftc1anclem7  37080  ftc1anclem8  37081  ftc1anc  37082  ftc2nc  37083  asindmre  37084  dvreasin  37087  dvreacos  37088  areacirclem1  37089  areacirclem2  37090  areacirclem3  37091  areacirclem4  37092  areacirc  37094  repwsmet  37215  rrnequiv  37216  rrntotbnd  37217  reheibor  37220  iccbnd  37221  intlewftc  41443  dvrelog2  41446  dvrelog3  41447  aks4d1p1p5  41457  resubeqsub  41885  subresre  41886  arearect  42545  areaquad  42546  k0004val0  43486  extoimad  43497  imo72b2lem0  43498  imo72b2lem2  43500  imo72b2lem1  43502  imo72b2  43505  ssrecnpr  43648  sblpnf  43650  radcnvrat  43654  lhe4.4ex1a  43669  refsumcn  44295  rr2sscn2  44653  uzsscn  44763  evthiccabs  44786  climreeq  44906  limciccioolb  44914  limcrecl  44922  limcicciooub  44930  limcleqr  44937  lptioo2cn  44938  lptioo1cn  44939  limclner  44944  liminflimsupclim  45100  resincncf  45168  cncficcgt0  45181  cncfiooicclem1  45186  cncfiooiccre  45188  jumpncnp  45191  dvcosre  45205  dvmptconst  45208  dvmptidg  45210  fperdvper  45212  dvresioo  45214  dvmulcncf  45218  dvdivcncf  45220  dvbdfbdioolem1  45221  ioodvbdlimc1lem1  45224  ioodvbdlimc1lem2  45225  ioodvbdlimc1  45226  ioodvbdlimc2lem  45227  ioodvbdlimc2  45228  itgsin0pilem1  45243  ibliccsinexp  45244  iblioosinexp  45246  itgsinexplem1  45247  itgsinexp  45248  itgcoscmulx  45262  itgsincmulx  45267  itgsubsticclem  45268  itgiccshift  45273  itgperiod  45274  itgsbtaddcnst  45275  dirkeritg  45395  dirkercncflem2  45397  dirkercncflem3  45398  dirkercncflem4  45399  dirkercncf  45400  fourierdlem16  45416  fourierdlem18  45418  fourierdlem21  45421  fourierdlem22  45422  fourierdlem39  45439  fourierdlem42  45442  fourierdlem48  45447  fourierdlem49  45448  fourierdlem53  45452  fourierdlem57  45456  fourierdlem58  45457  fourierdlem59  45458  fourierdlem60  45459  fourierdlem61  45460  fourierdlem62  45461  fourierdlem68  45467  fourierdlem70  45469  fourierdlem72  45471  fourierdlem73  45472  fourierdlem74  45473  fourierdlem75  45474  fourierdlem76  45475  fourierdlem78  45477  fourierdlem80  45479  fourierdlem83  45482  fourierdlem84  45483  fourierdlem85  45484  fourierdlem88  45487  fourierdlem89  45488  fourierdlem90  45489  fourierdlem91  45490  fourierdlem93  45492  fourierdlem94  45493  fourierdlem95  45494  fourierdlem96  45495  fourierdlem97  45496  fourierdlem98  45497  fourierdlem99  45498  fourierdlem101  45500  fourierdlem103  45502  fourierdlem104  45503  fourierdlem111  45510  fourierdlem112  45511  fourierdlem113  45512  fouriercnp  45519  sqwvfoura  45521  sqwvfourb  45522  fouriersw  45524  fouriercn  45525  etransclem2  45529  etransclem18  45545  etransclem23  45550  etransclem46  45573  rrxtopnfi  45580  rrndistlt  45583  sge0sn  45672  sge0tsms  45673  sge0f1o  45675  sge0pr  45687  sge0resplit  45699  sge0iunmptlemre  45708  sge0isummpt2  45725  hoicvr  45841  hoidmvlelem2  45889  refdivmptf  47508  refdivmptfv  47512  amgmlemALT  48129