Axiom ax-resscn 11163

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11105	. 2 class ℝ
2		cc 11104	. 2 class ℂ
3	1, 2	wss 3904	1 wff ℝ ⊆ ℂ

This axiom is used by:  recn  11196  reex  11197  recni  11229  qsscn  12990  ioosscn  13441  unitsscn  13533  reexpcl  14121  rpexpcl  14123  reexpclz  14125  expge0  14141  expge1  14142  rlimrecl  15638  abscn2  15657  recn2  15659  imcn2  15660  climabs  15662  climre  15664  climim  15665  rlimabs  15667  rlimre  15669  rlimim  15670  caurcvgr  15732  caucvgrlem2  15733  caurcvg  15735  fsumrecl  15792  fsumrpcl  15795  fsumge0  15854  fsumre  15867  fsumim  15868  fprodrecl  16014  fprodrpcl  16017  fprodreclf  16020  fprodge0  16054  fprodge1  16056  rerisefaccl  16078  refallfaccl  16079  rprisefaccl  16084  reeff1  16182  nthruc  16314  regsumfsum  21596  rge0srg  21599  rebase  21767  re0g  21773  regsumsupp  21783  remet  24958  tgioo2  24971  xrsdsre  24979  recld2  24983  reperf  24988  iitopon  25049  dfii3  25053  abscncf  25071  recncf  25072  imcncf  25073  abscncfALT  25094  cnmptre  25097  icchmeo  25111  cnrehmeo  25123  evth  25129  evth2  25130  lebnumlem2  25132  lebnumii  25136  cphsqrtcl  25354  resscdrg  25528  ishl2  25540  recms  25550  reust  25551  evthicc  25629  evthicc2  25630  ovolfsf  25641  volcn  25776  volivth  25777  ismbf  25798  cncombf  25828  cnmbf  25829  0plef  25842  itg1ge0  25856  i1faddlem  25863  i1fmul  25866  itg1addlem4  25869  i1fsub  25878  itg1sub  25879  mbfi1fseqlem5  25889  xrge0f  25901  itg20  25907  itg2const  25910  itg2mulc  25917  itg2addlem  25928  i1fibl  25978  itgitg1  25979  iblabslem  25998  iblabs  25999  bddmulibl  26009  recnprss  26074  dvmptresicc  26086  dvcjbr  26119  dvfre  26121  dvnfre  26122  dvferm1  26155  dvferm2  26157  rolle  26160  cmvth  26161  mvth  26162  dvlip  26163  dvlipcn  26164  dvlip2  26165  c1liplem1  26166  c1lip2  26168  dvgt0lem1  26172  dvle  26177  dvivthlem1  26178  dvivth  26180  dvne0  26181  lhop1lem  26183  lhop1  26184  lhop2  26185  lhop  26186  dvcnvrelem1  26187  dvcnvrelem2  26188  dvcnvre  26189  dvcvx  26190  dvfsumle  26191  dvfsumge  26192  dvfsumabs  26193  dvfsumlem2  26197  dvfsumrlim  26201  ftc1a  26207  ftc1lem3  26208  ftc1lem6  26211  ftc1  26212  ftc1cn  26213  ftc2  26214  ftc2ditglem  26215  itgparts  26217  itgsubstlem  26218  itgsubst  26219  itgpowd  26220  plyn0mulidp  26453  plymulidp  26454  aacjcl  26501  aalioulem3  26508  taylthlem2  26548  taylth  26549  abelth2  26616  reeff1olem  26620  efcvx  26623  pilem3  26627  pige3ALT  26696  recosf1o  26711  resinf1o  26712  dvrelog  26813  relogcn  26814  logcnlem5  26822  logcn  26823  dvloglem  26824  dvlog2lem  26828  logccv  26839  dvcxp1  26916  cxpcn3  26924  resqrtcn  26925  loglesqrt  26937  ssscongptld  26998  ressatans  27110  rlimcnp  27141  efrlim  27145  jensenlem1  27162  jensenlem2  27163  jensen  27164  amgm  27166  lgamgulmlem2  27205  ftalem3  27250  basellem9  27264  efnnfsumcl  27278  efchtdvds  27334  lgsdchr  27530  dchrvmasumlem1  27670  dchrisum0lem3  27694  pntlem3  27784  cchhllem  29247  ex-fpar  30824  ipasslem7  31199  fprodex01  33180  indsumin  33192  rexdiv  33256  fsumrp0cl  33350  xrge0slmod  33677  ccfldsrarelvec  34070  ccfldextdgrr  34071  rmulccn  34327  raddcn  34328  xrge0iifhom  34336  lmlimxrge0  34347  rezh  34368  esumpfinvallem  34473  esumpfinval  34474  esumpfinvalf  34475  esumcvg  34485  signsplypnf  34946  signsply0  34947  iblidicc  34988  rpsqrtcn  34989  ftc2re  34994  fdvposlt  34995  fdvneggt  34996  fdvposle  34997  fdvnegge  34998  itgexpif  35002  circlemeth  35036  circlemethnat  35037  circlevma  35038  circlemethhgt  35039  logdivsqrle  35046  resconn  35746  ivthALT  36874  dnicn  37109  knoppcnlem10  37119  knoppcnlem11  37120  unbdqndv2  37128  knoppndv  37151  knoppcn2  37153  broucube  38333  mblfinlem2  38337  mbfresfi  38345  ftc1cnnclem  38370  ftc1cnnc  38371  ftc1anclem3  38374  ftc1anclem5  38376  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  ftc2nc  38381  asindmre  38382  dvreasin  38385  dvreacos  38386  areacirclem1  38387  areacirclem2  38388  areacirclem3  38389  areacirclem4  38390  areacirc  38392  repwsmet  38513  rrnequiv  38514  rrntotbnd  38515  reheibor  38518  iccbnd  38519  intlewftc  42856  dvrelog2  42859  dvrelog3  42860  aks4d1p1p5  42870  rpsscn  43088  redvmptabs  43149  readvrec2  43150  resuppsinopn  43152  readvcot  43153  resubeqsub  43219  subresre  43220  arearect  43970  areaquad  43971  k0004val0  44908  extoimad  44918  imo72b2lem0  44919  imo72b2lem2  44921  imo72b2lem1  44923  imo72b2  44926  ssrecnpr  45046  sblpnf  45048  radcnvrat  45052  lhe4.4ex1a  45067  refsumcn  45778  rr2sscn2  46109  uzsscn  46217  evthiccabs  46240  climreeq  46357  limciccioolb  46365  limcrecl  46373  limcicciooub  46379  limcleqr  46386  lptioo2cn  46387  lptioo1cn  46388  limclner  46393  liminflimsupclim  46549  resincncf  46617  cncficcgt0  46630  cncfiooicclem1  46635  cncfiooiccre  46637  jumpncnp  46640  dvcosre  46654  dvmptconst  46657  dvmptidg  46659  fperdvper  46661  dvresioo  46663  dvmulcncf  46667  dvdivcncf  46669  dvbdfbdioolem1  46670  ioodvbdlimc1lem1  46673  ioodvbdlimc1lem2  46674  ioodvbdlimc1  46675  ioodvbdlimc2lem  46676  ioodvbdlimc2  46677  itgsin0pilem1  46692  ibliccsinexp  46693  iblioosinexp  46695  itgsinexplem1  46696  itgsinexp  46697  itgcoscmulx  46711  itgsincmulx  46716  itgsubsticclem  46717  itgiccshift  46722  itgperiod  46723  itgsbtaddcnst  46724  dirkeritg  46844  dirkercncflem2  46846  dirkercncflem3  46847  dirkercncflem4  46848  dirkercncf  46849  fourierdlem16  46865  fourierdlem18  46867  fourierdlem21  46870  fourierdlem22  46871  fourierdlem39  46888  fourierdlem42  46891  fourierdlem48  46896  fourierdlem49  46897  fourierdlem53  46901  fourierdlem57  46905  fourierdlem58  46906  fourierdlem59  46907  fourierdlem60  46908  fourierdlem61  46909  fourierdlem62  46910  fourierdlem68  46916  fourierdlem70  46918  fourierdlem72  46920  fourierdlem73  46921  fourierdlem74  46922  fourierdlem75  46923  fourierdlem76  46924  fourierdlem78  46926  fourierdlem80  46928  fourierdlem83  46931  fourierdlem84  46932  fourierdlem85  46933  fourierdlem88  46936  fourierdlem89  46937  fourierdlem90  46938  fourierdlem91  46939  fourierdlem93  46941  fourierdlem94  46942  fourierdlem95  46943  fourierdlem96  46944  fourierdlem97  46945  fourierdlem98  46946  fourierdlem99  46947  fourierdlem101  46949  fourierdlem103  46951  fourierdlem104  46952  fourierdlem111  46959  fourierdlem112  46960  fourierdlem113  46961  fouriercnp  46968  sqwvfoura  46970  sqwvfourb  46971  fouriersw  46973  fouriercn  46974  etransclem2  46978  etransclem18  46994  etransclem23  46999  etransclem46  47022  rrxtopnfi  47029  rrndistlt  47032  sge0sn  47121  sge0tsms  47122  sge0f1o  47124  sge0pr  47136  sge0resplit  47148  sge0iunmptlemre  47157  sge0isummpt2  47174  hoicvr  47290  hoidmvlelem2  47338  lamberte  47653  refdivmptf  49350  refdivmptfv  49354  amgmlemALT  50678