Axiom ax-resscn 11117

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11059	. 2 class ℝ
2		cc 11058	. 2 class ℂ
3	1, 2	wss 3913	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11150  reex  11151  recni  11178  qsscn  12894  ioosscn  13336  unitsscn  13427  reexpcl  13994  rpexpcl  13996  reexpclz  13998  expge0  14014  expge1  14015  rlimrecl  15474  abscn2  15493  recn2  15495  imcn2  15496  climabs  15498  climre  15500  climim  15501  rlimabs  15503  rlimre  15505  rlimim  15506  caurcvgr  15570  caucvgrlem2  15571  caurcvg  15573  fsumrecl  15630  fsumrpcl  15633  fsumge0  15691  fsumre  15704  fsumim  15705  fprodrecl  15847  fprodrpcl  15850  fprodreclf  15853  fprodge0  15887  fprodge1  15889  rerisefaccl  15911  refallfaccl  15912  rprisefaccl  15917  reeff1  16013  nthruc  16145  regsumfsum  20902  rge0srg  20905  rebase  21047  re0g  21053  regsumsupp  21063  remet  24190  tgioo2  24203  xrsdsre  24210  recld2  24214  reperf  24219  iitopon  24279  dfii3  24283  abscncf  24301  recncf  24302  imcncf  24303  abscncfALT  24324  cnmptre  24327  iimulcn  24338  icchmeo  24341  cnrehmeo  24353  evth  24359  evth2  24360  lebnumlem2  24362  lebnumii  24366  reparphti  24397  cphsqrtcl  24585  resscdrg  24759  ishl2  24771  recms  24781  reust  24782  evthicc  24860  evthicc2  24861  ovolfsf  24872  volcn  25007  volivth  25008  ismbf  25029  cncombf  25059  cnmbf  25060  0plef  25073  itg1ge0  25087  i1faddlem  25094  i1fmul  25097  itg1addlem4  25100  itg1addlem4OLD  25101  i1fsub  25110  itg1sub  25111  mbfi1fseqlem5  25121  xrge0f  25133  itg20  25139  itg2const  25142  itg2mulc  25149  itg2addlem  25160  i1fibl  25209  itgitg1  25210  iblabslem  25229  iblabs  25230  bddmulibl  25240  recnprss  25305  dvmptresicc  25317  dvcjbr  25350  dvfre  25352  dvnfre  25353  dvferm1  25386  dvferm2  25388  rolle  25391  cmvth  25392  mvth  25393  dvlip  25394  dvlipcn  25395  dvlip2  25396  c1liplem1  25397  c1lip2  25399  dvgt0lem1  25403  dvle  25408  dvivthlem1  25409  dvivth  25411  dvne0  25412  lhop1lem  25414  lhop1  25415  lhop2  25416  lhop  25417  dvcnvrelem1  25418  dvcnvrelem2  25419  dvcnvre  25420  dvcvx  25421  dvfsumle  25422  dvfsumge  25423  dvfsumabs  25424  dvfsumlem2  25428  dvfsumrlim  25432  ftc1a  25438  ftc1lem3  25439  ftc1lem6  25442  ftc1  25443  ftc1cn  25444  ftc2  25445  ftc2ditglem  25446  itgparts  25448  itgsubstlem  25449  itgsubst  25450  itgpowd  25451  aacjcl  25724  aalioulem3  25731  taylthlem2  25770  taylth  25771  abelth2  25838  reeff1olem  25842  efcvx  25845  pilem3  25849  pige3ALT  25913  recosf1o  25928  resinf1o  25929  dvrelog  26029  relogcn  26030  logcnlem5  26038  logcn  26039  dvloglem  26040  dvlog2lem  26044  logccv  26055  dvcxp1  26130  cxpcn3  26138  resqrtcn  26139  loglesqrt  26148  ssscongptld  26209  ressatans  26321  rlimcnp  26352  efrlim  26356  jensenlem1  26373  jensenlem2  26374  jensen  26375  amgm  26377  lgamgulmlem2  26416  ftalem3  26461  basellem9  26475  efnnfsumcl  26489  efchtdvds  26545  lgsdchr  26740  dchrvmasumlem1  26880  dchrisum0lem3  26904  pntlem3  26994  cchhllem  27898  cchhllemOLD  27899  ex-fpar  29469  ipasslem7  29841  fprodex01  31791  rexdiv  31852  fsumrp0cl  31956  xrge0slmod  32211  ccfldsrarelvec  32442  ccfldextdgrr  32443  rmulccn  32598  raddcn  32599  xrge0iifhom  32607  lmlimxrge0  32618  rezh  32641  indsumin  32710  esumpfinvallem  32762  esumpfinval  32763  esumpfinvalf  32764  esumcvg  32774  plymulx0  33248  plymulx  33249  signsplypnf  33251  signsply0  33252  iblidicc  33294  rpsqrtcn  33295  ftc2re  33300  fdvposlt  33301  fdvneggt  33302  fdvposle  33303  fdvnegge  33304  itgexpif  33308  circlemeth  33342  circlemethnat  33343  circlevma  33344  circlemethhgt  33345  logdivsqrle  33352  cvxpconn  33923  cvxsconn  33924  resconn  33927  ivthALT  34883  dnicn  35031  knoppcnlem10  35041  knoppcnlem11  35042  unbdqndv2  35050  knoppndv  35073  knoppcn2  35075  broucube  36185  mblfinlem2  36189  mbfresfi  36197  ftc1cnnclem  36222  ftc1cnnc  36223  ftc1anclem3  36226  ftc1anclem5  36228  ftc1anclem7  36230  ftc1anclem8  36231  ftc1anc  36232  ftc2nc  36233  asindmre  36234  dvreasin  36237  dvreacos  36238  areacirclem1  36239  areacirclem2  36240  areacirclem3  36241  areacirclem4  36242  areacirc  36244  repwsmet  36366  rrnequiv  36367  rrntotbnd  36368  reheibor  36371  iccbnd  36372  intlewftc  40591  dvrelog2  40594  dvrelog3  40595  aks4d1p1p5  40605  resubeqsub  40956  subresre  40957  arearect  41607  areaquad  41608  k0004val0  42548  extoimad  42559  imo72b2lem0  42560  imo72b2lem2  42562  imo72b2lem1  42564  imo72b2  42567  ssrecnpr  42710  sblpnf  42712  radcnvrat  42716  lhe4.4ex1a  42731  refsumcn  43357  rr2sscn2  43721  uzsscn  43831  evthiccabs  43854  climreeq  43974  limciccioolb  43982  limcrecl  43990  limcicciooub  43998  limcleqr  44005  lptioo2cn  44006  lptioo1cn  44007  limclner  44012  liminflimsupclim  44168  resincncf  44236  cncficcgt0  44249  cncfiooicclem1  44254  cncfiooiccre  44256  jumpncnp  44259  dvcosre  44273  dvmptconst  44276  dvmptidg  44278  fperdvper  44280  dvresioo  44282  dvmulcncf  44286  dvdivcncf  44288  dvbdfbdioolem1  44289  ioodvbdlimc1lem1  44292  ioodvbdlimc1lem2  44293  ioodvbdlimc1  44294  ioodvbdlimc2lem  44295  ioodvbdlimc2  44296  itgsin0pilem1  44311  ibliccsinexp  44312  iblioosinexp  44314  itgsinexplem1  44315  itgsinexp  44316  itgcoscmulx  44330  itgsincmulx  44335  itgsubsticclem  44336  itgiccshift  44341  itgperiod  44342  itgsbtaddcnst  44343  dirkeritg  44463  dirkercncflem2  44465  dirkercncflem3  44466  dirkercncflem4  44467  dirkercncf  44468  fourierdlem16  44484  fourierdlem18  44486  fourierdlem21  44489  fourierdlem22  44490  fourierdlem39  44507  fourierdlem42  44510  fourierdlem48  44515  fourierdlem49  44516  fourierdlem53  44520  fourierdlem57  44524  fourierdlem58  44525  fourierdlem59  44526  fourierdlem60  44527  fourierdlem61  44528  fourierdlem62  44529  fourierdlem68  44535  fourierdlem70  44537  fourierdlem72  44539  fourierdlem73  44540  fourierdlem74  44541  fourierdlem75  44542  fourierdlem76  44543  fourierdlem78  44545  fourierdlem80  44547  fourierdlem83  44550  fourierdlem84  44551  fourierdlem85  44552  fourierdlem88  44555  fourierdlem89  44556  fourierdlem90  44557  fourierdlem91  44558  fourierdlem93  44560  fourierdlem94  44561  fourierdlem95  44562  fourierdlem96  44563  fourierdlem97  44564  fourierdlem98  44565  fourierdlem99  44566  fourierdlem101  44568  fourierdlem103  44570  fourierdlem104  44571  fourierdlem111  44578  fourierdlem112  44579  fourierdlem113  44580  fouriercnp  44587  sqwvfoura  44589  sqwvfourb  44590  fouriersw  44592  fouriercn  44593  etransclem2  44597  etransclem18  44613  etransclem23  44618  etransclem46  44641  rrxtopnfi  44648  rrndistlt  44651  sge0sn  44740  sge0tsms  44741  sge0f1o  44743  sge0pr  44755  sge0resplit  44767  sge0iunmptlemre  44776  sge0isummpt2  44793  hoicvr  44909  hoidmvlelem2  44957  refdivmptf  46748  refdivmptfv  46752  amgmlemALT  47370