Axiom ax-resscn 11258

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

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

This axiom is used by:  recn  11291  reex  11292  recni  11324  qsscn  13088  ioosscn  13540  unitsscn  13632  reexpcl  14222  rpexpcl  14224  reexpclz  14226  expge0  14242  expge1  14243  rlimrecl  15748  abscn2  15767  recn2  15769  imcn2  15770  climabs  15772  climre  15774  climim  15775  rlimabs  15777  rlimre  15779  rlimim  15780  caurcvgr  15842  caucvgrlem2  15843  caurcvg  15845  fsumrecl  15901  fsumrpcl  15904  fsumge0  15963  fsumre  15976  fsumim  15977  fprodrecl  16121  fprodrpcl  16124  fprodreclf  16127  fprodge0  16161  fprodge1  16163  rerisefaccl  16185  refallfaccl  16186  rprisefaccl  16191  reeff1  16289  nthruc  16421  regsumfsum  21742  rge0srg  21745  rebase  21913  re0g  21919  regsumsupp  21929  remet  25110  tgioo2  25123  xrsdsre  25131  recld2  25135  reperf  25140  iitopon  25201  dfii3  25205  abscncf  25223  recncf  25224  imcncf  25225  abscncfALT  25246  cnmptre  25249  icchmeo  25263  cnrehmeo  25275  evth  25281  evth2  25282  lebnumlem2  25284  lebnumii  25288  cphsqrtcl  25506  resscdrg  25680  ishl2  25692  recms  25702  reust  25703  evthicc  25781  evthicc2  25782  ovolfsf  25793  volcn  25928  volivth  25929  ismbf  25950  cncombf  25980  cnmbf  25981  0plef  25994  itg1ge0  26008  i1faddlem  26015  i1fmul  26018  itg1addlem4  26021  i1fsub  26030  itg1sub  26031  mbfi1fseqlem5  26041  xrge0f  26053  itg20  26059  itg2const  26062  itg2mulc  26069  itg2addlem  26080  i1fibl  26129  itgitg1  26130  iblabslem  26149  iblabs  26150  bddmulibl  26160  recnprss  26225  dvmptresicc  26237  dvcjbr  26270  dvfre  26272  dvnfre  26273  dvferm1  26306  dvferm2  26308  rolle  26311  cmvth  26312  mvth  26313  dvlip  26314  dvlipcn  26315  dvlip2  26316  c1liplem1  26317  c1lip2  26319  dvgt0lem1  26323  dvle  26328  dvivthlem1  26329  dvivth  26331  dvne0  26332  lhop1lem  26334  lhop1  26335  lhop2  26336  lhop  26337  dvcnvrelem1  26338  dvcnvrelem2  26339  dvcnvre  26340  dvcvx  26341  dvfsumle  26342  dvfsumge  26343  dvfsumabs  26344  dvfsumlem2  26348  dvfsumrlim  26352  ftc1a  26358  ftc1lem3  26359  ftc1lem6  26362  ftc1  26363  ftc1cn  26364  ftc2  26365  ftc2ditglem  26366  itgparts  26368  itgsubstlem  26369  itgsubst  26370  itgpowd  26371  plyn0mulidp  26603  plymulidp  26604  aacjcl  26655  aalioulem3  26662  taylthlem2  26702  taylth  26703  abelth2  26770  reeff1olem  26774  efcvx  26777  pilem3  26781  pige3ALT  26849  recosf1o  26864  resinf1o  26865  dvrelog  26966  relogcn  26967  logcnlem5  26975  logcn  26976  dvloglem  26977  dvlog2lem  26981  logccv  26992  dvcxp1  27069  cxpcn3  27077  resqrtcn  27078  loglesqrt  27090  ssscongptld  27151  ressatans  27263  rlimcnp  27294  efrlim  27298  jensenlem1  27315  jensenlem2  27316  jensen  27317  amgm  27319  lgamgulmlem2  27358  ftalem3  27403  basellem9  27417  efnnfsumcl  27431  efchtdvds  27487  lgsdchr  27683  dchrvmasumlem1  27823  dchrisum0lem3  27847  pntlem3  27937  cchhllem  29465  ex-fpar  31064  ipasslem7  31439  fprodex01  33459  indsumin  33471  rexdiv  33535  fsumrp0cl  33625  xrge0slmod  33952  ccfldsrarelvec  34346  ccfldextdgrr  34347  rmulccn  34603  raddcn  34604  xrge0iifhom  34612  lmlimxrge0  34623  rezh  34644  esumpfinvallem  34749  esumpfinval  34750  esumpfinvalf  34751  esumcvg  34761  signsplypnf  35222  signsply0  35223  iblidicc  35264  rpsqrtcn  35265  ftc2re  35270  fdvposlt  35271  fdvneggt  35272  fdvposle  35273  fdvnegge  35274  itgexpif  35278  circlemeth  35312  circlemethnat  35313  circlevma  35314  circlemethhgt  35315  logdivsqrle  35322  resconn  36080  ivthALT  37198  dnicn  37433  knoppcnlem10  37443  knoppcnlem11  37444  unbdqndv2  37452  knoppndv  37475  knoppcn2  37477  broucube  38648  mblfinlem2  38652  mbfresfi  38660  ftc1cnnclem  38685  ftc1cnnc  38686  ftc1anclem3  38689  ftc1anclem5  38691  ftc1anclem7  38693  ftc1anclem8  38694  ftc1anc  38695  ftc2nc  38696  asindmre  38697  dvreasin  38700  dvreacos  38701  areacirclem1  38702  areacirclem2  38703  areacirclem3  38704  areacirclem4  38705  areacirc  38707  repwsmet  38844  rrnequiv  38845  rrntotbnd  38846  reheibor  38849  iccbnd  38850  intlewftc  43187  dvrelog2  43190  dvrelog3  43191  aks4d1p1p5  43201  rpsscn  43432  redvmptabs  43487  readvrec2  43488  resuppsinopn  43490  readvcot  43491  resubeqsub  43557  subresre  43558  arearect  44293  areaquad  44294  k0004val0  45230  extoimad  45240  imo72b2lem0  45241  imo72b2lem2  45243  imo72b2lem1  45245  imo72b2  45248  ssrecnpr  45368  sblpnf  45370  radcnvrat  45374  lhe4.4ex1a  45389  refsumcn  46123  rr2sscn2  46453  uzsscn  46561  evthiccabs  46584  climreeq  46701  limciccioolb  46709  limcrecl  46717  limcicciooub  46723  limcleqr  46730  lptioo2cn  46731  lptioo1cn  46732  limclner  46737  liminflimsupclim  46893  resincncf  46961  cncficcgt0  46974  cncfiooicclem1  46979  cncfiooiccre  46981  jumpncnp  46984  dvcosre  46998  dvmptconst  47001  dvmptidg  47003  fperdvper  47005  dvresioo  47007  dvmulcncf  47011  dvdivcncf  47013  dvbdfbdioolem1  47014  ioodvbdlimc1lem1  47017  ioodvbdlimc1lem2  47018  ioodvbdlimc1  47019  ioodvbdlimc2lem  47020  ioodvbdlimc2  47021  itgsin0pilem1  47036  ibliccsinexp  47037  iblioosinexp  47039  itgsinexplem1  47040  itgsinexp  47041  itgcoscmulx  47055  itgsincmulx  47060  itgsubsticclem  47061  itgiccshift  47066  itgperiod  47067  itgsbtaddcnst  47068  dirkeritg  47188  dirkercncflem2  47190  dirkercncflem3  47191  dirkercncflem4  47192  dirkercncf  47193  fourierdlem16  47209  fourierdlem18  47211  fourierdlem21  47214  fourierdlem22  47215  fourierdlem39  47232  fourierdlem42  47235  fourierdlem48  47240  fourierdlem49  47241  fourierdlem53  47245  fourierdlem57  47249  fourierdlem58  47250  fourierdlem59  47251  fourierdlem60  47252  fourierdlem61  47253  fourierdlem62  47254  fourierdlem68  47260  fourierdlem70  47262  fourierdlem72  47264  fourierdlem73  47265  fourierdlem74  47266  fourierdlem75  47267  fourierdlem76  47268  fourierdlem78  47270  fourierdlem80  47272  fourierdlem83  47275  fourierdlem84  47276  fourierdlem85  47277  fourierdlem88  47280  fourierdlem89  47281  fourierdlem90  47282  fourierdlem91  47283  fourierdlem93  47285  fourierdlem94  47286  fourierdlem95  47287  fourierdlem96  47288  fourierdlem97  47289  fourierdlem98  47290  fourierdlem99  47291  fourierdlem101  47293  fourierdlem103  47295  fourierdlem104  47296  fourierdlem111  47303  fourierdlem112  47304  fourierdlem113  47305  fouriercnp  47312  sqwvfoura  47314  sqwvfourb  47315  fouriersw  47317  fouriercn  47318  etransclem2  47322  etransclem18  47338  etransclem23  47343  etransclem46  47366  rrxtopnfi  47373  rrndistlt  47376  sge0sn  47465  sge0tsms  47466  sge0f1o  47468  sge0pr  47480  sge0resplit  47492  sge0iunmptlemre  47501  sge0isummpt2  47518  hoicvr  47634  hoidmvlelem2  47682  lamberte  48014  refdivmptf  49730  refdivmptfv  49734  amgmlemALT  51064