Axiom ax-resscn 11257

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11199	. 2 class ℝ
2		cc 11198	. 2 class ℂ
3	1, 2	wss 3895	1 wff ℝ ⊆ ℂ

This axiom is used by:  recn  11290  reex  11291  recni  11323  qsscn  13087  ioosscn  13539  unitsscn  13631  reexpcl  14221  rpexpcl  14223  reexpclz  14225  expge0  14241  expge1  14242  rlimrecl  15747  abscn2  15766  recn2  15768  imcn2  15769  climabs  15771  climre  15773  climim  15774  rlimabs  15776  rlimre  15778  rlimim  15779  caurcvgr  15841  caucvgrlem2  15842  caurcvg  15844  fsumrecl  15900  fsumrpcl  15903  fsumge0  15962  fsumre  15975  fsumim  15976  fprodrecl  16120  fprodrpcl  16123  fprodreclf  16126  fprodge0  16160  fprodge1  16162  rerisefaccl  16184  refallfaccl  16185  rprisefaccl  16190  reeff1  16288  nthruc  16420  regsumfsum  21741  rge0srg  21744  rebase  21912  re0g  21918  regsumsupp  21928  remet  25109  tgioo2  25122  xrsdsre  25130  recld2  25134  reperf  25139  iitopon  25200  dfii3  25204  abscncf  25222  recncf  25223  imcncf  25224  abscncfALT  25245  cnmptre  25248  icchmeo  25262  cnrehmeo  25274  evth  25280  evth2  25281  lebnumlem2  25283  lebnumii  25287  cphsqrtcl  25505  resscdrg  25679  ishl2  25691  recms  25701  reust  25702  evthicc  25780  evthicc2  25781  ovolfsf  25792  volcn  25927  volivth  25928  ismbf  25949  cncombf  25979  cnmbf  25980  0plef  25993  itg1ge0  26007  i1faddlem  26014  i1fmul  26017  itg1addlem4  26020  i1fsub  26029  itg1sub  26030  mbfi1fseqlem5  26040  xrge0f  26052  itg20  26058  itg2const  26061  itg2mulc  26068  itg2addlem  26079  i1fibl  26128  itgitg1  26129  iblabslem  26148  iblabs  26149  bddmulibl  26159  recnprss  26224  dvmptresicc  26236  dvcjbr  26269  dvfre  26271  dvnfre  26272  dvferm1  26305  dvferm2  26307  rolle  26310  cmvth  26311  mvth  26312  dvlip  26313  dvlipcn  26314  dvlip2  26315  c1liplem1  26316  c1lip2  26318  dvgt0lem1  26322  dvle  26327  dvivthlem1  26328  dvivth  26330  dvne0  26331  lhop1lem  26333  lhop1  26334  lhop2  26335  lhop  26336  dvcnvrelem1  26337  dvcnvrelem2  26338  dvcnvre  26339  dvcvx  26340  dvfsumle  26341  dvfsumge  26342  dvfsumabs  26343  dvfsumlem2  26347  dvfsumrlim  26351  ftc1a  26357  ftc1lem3  26358  ftc1lem6  26361  ftc1  26362  ftc1cn  26363  ftc2  26364  ftc2ditglem  26365  itgparts  26367  itgsubstlem  26368  itgsubst  26369  itgpowd  26370  plyn0mulidp  26602  plymulidp  26603  aacjcl  26654  aalioulem3  26661  taylthlem2  26701  taylth  26702  abelth2  26769  reeff1olem  26773  efcvx  26776  pilem3  26780  pige3ALT  26848  recosf1o  26863  resinf1o  26864  dvrelog  26965  relogcn  26966  logcnlem5  26974  logcn  26975  dvloglem  26976  dvlog2lem  26980  logccv  26991  dvcxp1  27068  cxpcn3  27076  resqrtcn  27077  loglesqrt  27089  ssscongptld  27150  ressatans  27262  rlimcnp  27293  efrlim  27297  jensenlem1  27314  jensenlem2  27315  jensen  27316  amgm  27318  lgamgulmlem2  27357  ftalem3  27402  basellem9  27416  efnnfsumcl  27430  efchtdvds  27486  lgsdchr  27682  dchrvmasumlem1  27822  dchrisum0lem3  27846  pntlem3  27936  cchhllem  29464  ex-fpar  31063  ipasslem7  31438  fprodex01  33458  indsumin  33470  rexdiv  33534  fsumrp0cl  33624  xrge0slmod  33951  ccfldsrarelvec  34345  ccfldextdgrr  34346  rmulccn  34602  raddcn  34603  xrge0iifhom  34611  lmlimxrge0  34622  rezh  34643  esumpfinvallem  34748  esumpfinval  34749  esumpfinvalf  34750  esumcvg  34760  signsplypnf  35221  signsply0  35222  iblidicc  35263  rpsqrtcn  35264  ftc2re  35269  fdvposlt  35270  fdvneggt  35271  fdvposle  35272  fdvnegge  35273  itgexpif  35277  circlemeth  35311  circlemethnat  35312  circlevma  35313  circlemethhgt  35314  logdivsqrle  35321  resconn  36053  ivthALT  37165  dnicn  37400  knoppcnlem10  37410  knoppcnlem11  37411  unbdqndv2  37419  knoppndv  37442  knoppcn2  37444  broucube  38615  mblfinlem2  38619  mbfresfi  38627  ftc1cnnclem  38652  ftc1cnnc  38653  ftc1anclem3  38656  ftc1anclem5  38658  ftc1anclem7  38660  ftc1anclem8  38661  ftc1anc  38662  ftc2nc  38663  asindmre  38664  dvreasin  38667  dvreacos  38668  areacirclem1  38669  areacirclem2  38670  areacirclem3  38671  areacirclem4  38672  areacirc  38674  repwsmet  38811  rrnequiv  38812  rrntotbnd  38813  reheibor  38816  iccbnd  38817  intlewftc  43154  dvrelog2  43157  dvrelog3  43158  aks4d1p1p5  43168  rpsscn  43399  redvmptabs  43454  readvrec2  43455  resuppsinopn  43457  readvcot  43458  resubeqsub  43524  subresre  43525  arearect  44259  areaquad  44260  k0004val0  45196  extoimad  45206  imo72b2lem0  45207  imo72b2lem2  45209  imo72b2lem1  45211  imo72b2  45214  ssrecnpr  45334  sblpnf  45336  radcnvrat  45340  lhe4.4ex1a  45355  refsumcn  46089  rr2sscn2  46419  uzsscn  46527  evthiccabs  46550  climreeq  46667  limciccioolb  46675  limcrecl  46683  limcicciooub  46689  limcleqr  46696  lptioo2cn  46697  lptioo1cn  46698  limclner  46703  liminflimsupclim  46859  resincncf  46927  cncficcgt0  46940  cncfiooicclem1  46945  cncfiooiccre  46947  jumpncnp  46950  dvcosre  46964  dvmptconst  46967  dvmptidg  46969  fperdvper  46971  dvresioo  46973  dvmulcncf  46977  dvdivcncf  46979  dvbdfbdioolem1  46980  ioodvbdlimc1lem1  46983  ioodvbdlimc1lem2  46984  ioodvbdlimc1  46985  ioodvbdlimc2lem  46986  ioodvbdlimc2  46987  itgsin0pilem1  47002  ibliccsinexp  47003  iblioosinexp  47005  itgsinexplem1  47006  itgsinexp  47007  itgcoscmulx  47021  itgsincmulx  47026  itgsubsticclem  47027  itgiccshift  47032  itgperiod  47033  itgsbtaddcnst  47034  dirkeritg  47154  dirkercncflem2  47156  dirkercncflem3  47157  dirkercncflem4  47158  dirkercncf  47159  fourierdlem16  47175  fourierdlem18  47177  fourierdlem21  47180  fourierdlem22  47181  fourierdlem39  47198  fourierdlem42  47201  fourierdlem48  47206  fourierdlem49  47207  fourierdlem53  47211  fourierdlem57  47215  fourierdlem58  47216  fourierdlem59  47217  fourierdlem60  47218  fourierdlem61  47219  fourierdlem62  47220  fourierdlem68  47226  fourierdlem70  47228  fourierdlem72  47230  fourierdlem73  47231  fourierdlem74  47232  fourierdlem75  47233  fourierdlem76  47234  fourierdlem78  47236  fourierdlem80  47238  fourierdlem83  47241  fourierdlem84  47242  fourierdlem85  47243  fourierdlem88  47246  fourierdlem89  47247  fourierdlem90  47248  fourierdlem91  47249  fourierdlem93  47251  fourierdlem94  47252  fourierdlem95  47253  fourierdlem96  47254  fourierdlem97  47255  fourierdlem98  47256  fourierdlem99  47257  fourierdlem101  47259  fourierdlem103  47261  fourierdlem104  47262  fourierdlem111  47269  fourierdlem112  47270  fourierdlem113  47271  fouriercnp  47278  sqwvfoura  47280  sqwvfourb  47281  fouriersw  47283  fouriercn  47284  etransclem2  47288  etransclem18  47304  etransclem23  47309  etransclem46  47332  rrxtopnfi  47339  rrndistlt  47342  sge0sn  47431  sge0tsms  47432  sge0f1o  47434  sge0pr  47446  sge0resplit  47458  sge0iunmptlemre  47467  sge0isummpt2  47484  hoicvr  47600  hoidmvlelem2  47648  lamberte  47980  refdivmptf  49696  refdivmptfv  49700  amgmlemALT  51030