Axiom ax-resscn 10583

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 10525	. 2 class ℝ
2		cc 10524	. 2 class ℂ
3	1, 2	wss 3881	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  10616  reex  10617  recni  10644  qsscn  12347  ioosscn  12787  unitsscn  12878  reexpcl  13442  rpexpcl  13444  reexpclz  13445  expge0  13461  expge1  13462  rlimrecl  14929  abscn2  14947  recn2  14949  imcn2  14950  climabs  14952  climre  14954  climim  14955  rlimabs  14957  rlimre  14959  rlimim  14960  caurcvgr  15022  caucvgrlem2  15023  caurcvg  15025  fsumrecl  15083  fsumrpcl  15086  fsumge0  15142  fsumre  15155  fsumim  15156  fprodrecl  15299  fprodrpcl  15302  fprodreclf  15305  fprodge0  15339  fprodge1  15341  rerisefaccl  15363  refallfaccl  15364  rprisefaccl  15369  reeff1  15465  nthruc  15597  regsumfsum  20159  rge0srg  20162  rebase  20295  re0g  20301  regsumsupp  20311  remet  23395  tgioo2  23408  xrsdsre  23415  recld2  23419  reperf  23424  iitopon  23484  dfii3  23488  abscncf  23506  recncf  23507  imcncf  23508  abscncfALT  23529  cnmptre  23532  iimulcn  23543  icchmeo  23546  cnrehmeo  23558  evth  23564  evth2  23565  lebnumlem2  23567  lebnumii  23571  reparphti  23602  cphsqrtcl  23789  resscdrg  23962  ishl2  23974  recms  23984  reust  23985  evthicc  24063  evthicc2  24064  ovolfsf  24075  volcn  24210  volivth  24211  ismbf  24232  cncombf  24262  cnmbf  24263  0plef  24276  itg1ge0  24290  i1faddlem  24297  i1fmul  24300  itg1addlem4  24303  i1fsub  24312  itg1sub  24313  mbfi1fseqlem5  24323  xrge0f  24335  itg20  24341  itg2const  24344  itg2mulc  24351  itg2addlem  24362  i1fibl  24411  itgitg1  24412  iblabslem  24431  iblabs  24432  bddmulibl  24442  recnprss  24507  dvmptresicc  24519  dvcjbr  24552  dvfre  24554  dvnfre  24555  dvferm1  24588  dvferm2  24590  rolle  24593  cmvth  24594  mvth  24595  dvlip  24596  dvlipcn  24597  dvlip2  24598  c1liplem1  24599  c1lip2  24601  dvgt0lem1  24605  dvle  24610  dvivthlem1  24611  dvivth  24613  dvne0  24614  lhop1lem  24616  lhop1  24617  lhop2  24618  lhop  24619  dvcnvrelem1  24620  dvcnvrelem2  24621  dvcnvre  24622  dvcvx  24623  dvfsumle  24624  dvfsumge  24625  dvfsumabs  24626  dvfsumlem2  24630  dvfsumrlim  24634  ftc1a  24640  ftc1lem3  24641  ftc1lem6  24644  ftc1  24645  ftc1cn  24646  ftc2  24647  ftc2ditglem  24648  itgparts  24650  itgsubstlem  24651  itgsubst  24652  itgpowd  24653  aacjcl  24923  aalioulem3  24930  taylthlem2  24969  taylth  24970  abelth2  25037  reeff1olem  25041  efcvx  25044  pilem3  25048  pige3ALT  25112  recosf1o  25127  resinf1o  25128  dvrelog  25228  relogcn  25229  logcnlem5  25237  logcn  25238  dvloglem  25239  dvlog2lem  25243  logccv  25254  dvcxp1  25329  cxpcn3  25337  resqrtcn  25338  loglesqrt  25347  ssscongptld  25408  ressatans  25520  rlimcnp  25551  efrlim  25555  jensenlem1  25572  jensenlem2  25573  jensen  25574  amgm  25576  lgamgulmlem2  25615  ftalem3  25660  basellem9  25674  efnnfsumcl  25688  efchtdvds  25744  lgsdchr  25939  dchrvmasumlem1  26079  dchrisum0lem3  26103  pntlem3  26193  cchhllem  26681  ex-fpar  28247  ipasslem7  28619  fprodex01  30567  rexdiv  30628  fsumrp0cl  30729  xrge0slmod  30968  ccfldsrarelvec  31144  ccfldextdgrr  31145  rmulccn  31281  raddcn  31282  xrge0iifhom  31290  lmlimxrge0  31301  rezh  31322  indsumin  31391  esumpfinvallem  31443  esumpfinval  31444  esumpfinvalf  31445  esumcvg  31455  plymulx0  31927  plymulx  31928  signsplypnf  31930  signsply0  31931  iblidicc  31973  rpsqrtcn  31974  ftc2re  31979  fdvposlt  31980  fdvneggt  31981  fdvposle  31982  fdvnegge  31983  itgexpif  31987  circlemeth  32021  circlemethnat  32022  circlevma  32023  circlemethhgt  32024  logdivsqrle  32031  cvxpconn  32602  cvxsconn  32603  resconn  32606  ivthALT  33796  dnicn  33944  knoppcnlem10  33954  knoppcnlem11  33955  unbdqndv2  33963  knoppndv  33986  knoppcn2  33988  broucube  35091  mblfinlem2  35095  mbfresfi  35103  ftc1cnnclem  35128  ftc1cnnc  35129  ftc1anclem3  35132  ftc1anclem5  35134  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  ftc2nc  35139  asindmre  35140  dvreasin  35143  dvreacos  35144  areacirclem1  35145  areacirclem2  35146  areacirclem3  35147  areacirclem4  35148  areacirc  35150  repwsmet  35272  rrnequiv  35273  rrntotbnd  35274  reheibor  35277  iccbnd  35278  intlewftc  39344  resubeqsub  39566  subresre  39567  arearect  40165  areaquad  40166  k0004val0  40857  extoimad  40868  imo72b2lem0  40869  imo72b2lem2  40871  imo72b2lem1  40874  imo72b2  40878  ssrecnpr  41012  sblpnf  41014  radcnvrat  41018  lhe4.4ex1a  41033  refsumcn  41659  rr2sscn2  41998  uzsscn  42115  evthiccabs  42133  climreeq  42255  limciccioolb  42263  limcrecl  42271  limcicciooub  42279  limcleqr  42286  lptioo2cn  42287  lptioo1cn  42288  limclner  42293  liminflimsupclim  42449  resincncf  42517  cncficcgt0  42530  cncfiooicclem1  42535  cncfiooiccre  42537  jumpncnp  42540  dvcosre  42554  dvmptconst  42557  dvmptidg  42559  fperdvper  42561  dvresioo  42563  dvmulcncf  42567  dvdivcncf  42569  dvbdfbdioolem1  42570  ioodvbdlimc1lem1  42573  ioodvbdlimc1lem2  42574  ioodvbdlimc1  42575  ioodvbdlimc2lem  42576  ioodvbdlimc2  42577  itgsin0pilem1  42592  ibliccsinexp  42593  iblioosinexp  42595  itgsinexplem1  42596  itgsinexp  42597  itgcoscmulx  42611  itgsincmulx  42616  itgsubsticclem  42617  itgiccshift  42622  itgperiod  42623  itgsbtaddcnst  42624  dirkeritg  42744  dirkercncflem2  42746  dirkercncflem3  42747  dirkercncflem4  42748  dirkercncf  42749  fourierdlem16  42765  fourierdlem18  42767  fourierdlem21  42770  fourierdlem22  42771  fourierdlem39  42788  fourierdlem42  42791  fourierdlem48  42796  fourierdlem49  42797  fourierdlem53  42801  fourierdlem57  42805  fourierdlem58  42806  fourierdlem59  42807  fourierdlem60  42808  fourierdlem61  42809  fourierdlem62  42810  fourierdlem68  42816  fourierdlem70  42818  fourierdlem72  42820  fourierdlem73  42821  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem78  42826  fourierdlem80  42828  fourierdlem83  42831  fourierdlem84  42832  fourierdlem85  42833  fourierdlem88  42836  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem93  42841  fourierdlem94  42842  fourierdlem95  42843  fourierdlem96  42844  fourierdlem97  42845  fourierdlem98  42846  fourierdlem99  42847  fourierdlem101  42849  fourierdlem103  42851  fourierdlem104  42852  fourierdlem111  42859  fourierdlem112  42860  fourierdlem113  42861  fouriercnp  42868  sqwvfoura  42870  sqwvfourb  42871  fouriersw  42873  fouriercn  42874  etransclem2  42878  etransclem18  42894  etransclem23  42899  etransclem46  42922  rrxtopnfi  42929  rrndistlt  42932  sge0sn  43018  sge0tsms  43019  sge0f1o  43021  sge0pr  43033  sge0resplit  43045  sge0iunmptlemre  43054  sge0isummpt2  43071  hoicvr  43187  hoidmvlelem2  43235  refdivmptf  44956  refdivmptfv  44960  amgmlemALT  45331