Axiom ax-resscn 11084

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11026	. 2 class ℝ
2		cc 11025	. 2 class ℂ
3	1, 2	wss 3885	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11117  reex  11118  recni  11148  qsscn  12899  ioosscn  13350  unitsscn  13442  reexpcl  14029  rpexpcl  14031  reexpclz  14033  expge0  14049  expge1  14050  rlimrecl  15531  abscn2  15550  recn2  15552  imcn2  15553  climabs  15555  climre  15557  climim  15558  rlimabs  15560  rlimre  15562  rlimim  15563  caurcvgr  15625  caucvgrlem2  15626  caurcvg  15628  fsumrecl  15685  fsumrpcl  15688  fsumge0  15747  fsumre  15760  fsumim  15761  fprodrecl  15907  fprodrpcl  15910  fprodreclf  15913  fprodge0  15947  fprodge1  15949  rerisefaccl  15971  refallfaccl  15972  rprisefaccl  15977  reeff1  16076  nthruc  16208  regsumfsum  21404  rge0srg  21407  rebase  21575  re0g  21581  regsumsupp  21591  remet  24743  tgioo2  24756  xrsdsre  24764  recld2  24768  reperf  24773  iitopon  24834  dfii3  24838  abscncf  24856  recncf  24857  imcncf  24858  abscncfALT  24879  cnmptre  24882  icchmeo  24896  cnrehmeo  24908  evth  24914  evth2  24915  lebnumlem2  24917  lebnumii  24921  cphsqrtcl  25139  resscdrg  25313  ishl2  25325  recms  25335  reust  25336  evthicc  25414  evthicc2  25415  ovolfsf  25426  volcn  25561  volivth  25562  ismbf  25583  cncombf  25613  cnmbf  25614  0plef  25627  itg1ge0  25641  i1faddlem  25648  i1fmul  25651  itg1addlem4  25654  i1fsub  25663  itg1sub  25664  mbfi1fseqlem5  25674  xrge0f  25686  itg20  25692  itg2const  25695  itg2mulc  25702  itg2addlem  25713  i1fibl  25763  itgitg1  25764  iblabslem  25783  iblabs  25784  bddmulibl  25794  recnprss  25859  dvmptresicc  25871  dvcjbr  25904  dvfre  25906  dvnfre  25907  dvferm1  25940  dvferm2  25942  rolle  25945  cmvth  25946  mvth  25947  dvlip  25948  dvlipcn  25949  dvlip2  25950  c1liplem1  25951  c1lip2  25953  dvgt0lem1  25957  dvle  25962  dvivthlem1  25963  dvivth  25965  dvne0  25966  lhop1lem  25968  lhop1  25969  lhop2  25970  lhop  25971  dvcnvrelem1  25972  dvcnvrelem2  25973  dvcnvre  25974  dvcvx  25975  dvfsumle  25976  dvfsumge  25977  dvfsumabs  25978  dvfsumlem2  25982  dvfsumrlim  25986  ftc1a  25992  ftc1lem3  25993  ftc1lem6  25996  ftc1  25997  ftc1cn  25998  ftc2  25999  ftc2ditglem  26000  itgparts  26002  itgsubstlem  26003  itgsubst  26004  itgpowd  26005  aacjcl  26281  aalioulem3  26288  taylthlem2  26327  taylth  26328  abelth2  26395  reeff1olem  26399  efcvx  26402  pilem3  26406  pige3ALT  26472  recosf1o  26487  resinf1o  26488  dvrelog  26589  relogcn  26590  logcnlem5  26598  logcn  26599  dvloglem  26600  dvlog2lem  26604  logccv  26615  dvcxp1  26692  cxpcn3  26700  resqrtcn  26701  loglesqrt  26713  ssscongptld  26774  ressatans  26886  rlimcnp  26917  efrlim  26921  jensenlem1  26938  jensenlem2  26939  jensen  26940  amgm  26942  lgamgulmlem2  26981  ftalem3  27026  basellem9  27040  efnnfsumcl  27054  efchtdvds  27110  lgsdchr  27306  dchrvmasumlem1  27446  dchrisum0lem3  27470  pntlem3  27560  cchhllem  28943  ex-fpar  30520  ipasslem7  30895  fprodex01  32886  indsumin  32909  rexdiv  32973  fsumrp0cl  33069  xrge0slmod  33396  ccfldsrarelvec  33803  ccfldextdgrr  33804  rmulccn  34060  raddcn  34061  xrge0iifhom  34069  lmlimxrge0  34080  rezh  34101  esumpfinvallem  34206  esumpfinval  34207  esumpfinvalf  34208  esumcvg  34218  plymulx0  34679  plymulx  34680  signsplypnf  34682  signsply0  34683  iblidicc  34724  rpsqrtcn  34725  ftc2re  34730  fdvposlt  34731  fdvneggt  34732  fdvposle  34733  fdvnegge  34734  itgexpif  34738  circlemeth  34772  circlemethnat  34773  circlevma  34774  circlemethhgt  34775  logdivsqrle  34782  resconn  35416  ivthALT  36505  dnicn  36740  knoppcnlem10  36750  knoppcnlem11  36751  unbdqndv2  36759  knoppndv  36782  knoppcn2  36784  broucube  37963  mblfinlem2  37967  mbfresfi  37975  ftc1cnnclem  38000  ftc1cnnc  38001  ftc1anclem3  38004  ftc1anclem5  38006  ftc1anclem7  38008  ftc1anclem8  38009  ftc1anc  38010  ftc2nc  38011  asindmre  38012  dvreasin  38015  dvreacos  38016  areacirclem1  38017  areacirclem2  38018  areacirclem3  38019  areacirclem4  38020  areacirc  38022  repwsmet  38143  rrnequiv  38144  rrntotbnd  38145  reheibor  38148  iccbnd  38149  intlewftc  42488  dvrelog2  42491  dvrelog3  42492  aks4d1p1p5  42502  rpsscn  42719  redvmptabs  42780  readvrec2  42781  resuppsinopn  42783  readvcot  42784  resubeqsub  42850  subresre  42851  arearect  43631  areaquad  43632  k0004val0  44569  extoimad  44579  imo72b2lem0  44580  imo72b2lem2  44582  imo72b2lem1  44584  imo72b2  44587  ssrecnpr  44723  sblpnf  44725  radcnvrat  44729  lhe4.4ex1a  44744  refsumcn  45449  rr2sscn2  45783  uzsscn  45891  evthiccabs  45914  climreeq  46031  limciccioolb  46039  limcrecl  46047  limcicciooub  46053  limcleqr  46060  lptioo2cn  46061  lptioo1cn  46062  limclner  46067  liminflimsupclim  46223  resincncf  46291  cncficcgt0  46304  cncfiooicclem1  46309  cncfiooiccre  46311  jumpncnp  46314  dvcosre  46328  dvmptconst  46331  dvmptidg  46333  fperdvper  46335  dvresioo  46337  dvmulcncf  46341  dvdivcncf  46343  dvbdfbdioolem1  46344  ioodvbdlimc1lem1  46347  ioodvbdlimc1lem2  46348  ioodvbdlimc1  46349  ioodvbdlimc2lem  46350  ioodvbdlimc2  46351  itgsin0pilem1  46366  ibliccsinexp  46367  iblioosinexp  46369  itgsinexplem1  46370  itgsinexp  46371  itgcoscmulx  46385  itgsincmulx  46390  itgsubsticclem  46391  itgiccshift  46396  itgperiod  46397  itgsbtaddcnst  46398  dirkeritg  46518  dirkercncflem2  46520  dirkercncflem3  46521  dirkercncflem4  46522  dirkercncf  46523  fourierdlem16  46539  fourierdlem18  46541  fourierdlem21  46544  fourierdlem22  46545  fourierdlem39  46562  fourierdlem42  46565  fourierdlem48  46570  fourierdlem49  46571  fourierdlem53  46575  fourierdlem57  46579  fourierdlem58  46580  fourierdlem59  46581  fourierdlem60  46582  fourierdlem61  46583  fourierdlem62  46584  fourierdlem68  46590  fourierdlem70  46592  fourierdlem72  46594  fourierdlem73  46595  fourierdlem74  46596  fourierdlem75  46597  fourierdlem76  46598  fourierdlem78  46600  fourierdlem80  46602  fourierdlem83  46605  fourierdlem84  46606  fourierdlem85  46607  fourierdlem88  46610  fourierdlem89  46611  fourierdlem90  46612  fourierdlem91  46613  fourierdlem93  46615  fourierdlem94  46616  fourierdlem95  46617  fourierdlem96  46618  fourierdlem97  46619  fourierdlem98  46620  fourierdlem99  46621  fourierdlem101  46623  fourierdlem103  46625  fourierdlem104  46626  fourierdlem111  46633  fourierdlem112  46634  fourierdlem113  46635  fouriercnp  46642  sqwvfoura  46644  sqwvfourb  46645  fouriersw  46647  fouriercn  46648  etransclem2  46652  etransclem18  46668  etransclem23  46673  etransclem46  46696  rrxtopnfi  46703  rrndistlt  46706  sge0sn  46795  sge0tsms  46796  sge0f1o  46798  sge0pr  46810  sge0resplit  46822  sge0iunmptlemre  46831  sge0isummpt2  46848  hoicvr  46964  hoidmvlelem2  47012  lamberte  47324  refdivmptf  49006  refdivmptfv  49010  amgmlemALT  50266