Axiom ax-resscn 11156

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

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

This axiom is referenced by:  recn  11189  reex  11190  recni  11222  qsscn  12983  ioosscn  13434  unitsscn  13526  reexpcl  14113  rpexpcl  14115  reexpclz  14117  expge0  14133  expge1  14134  rlimrecl  15630  abscn2  15649  recn2  15651  imcn2  15652  climabs  15654  climre  15656  climim  15657  rlimabs  15659  rlimre  15661  rlimim  15662  caurcvgr  15724  caucvgrlem2  15725  caurcvg  15727  fsumrecl  15784  fsumrpcl  15787  fsumge0  15846  fsumre  15859  fsumim  15860  fprodrecl  16006  fprodrpcl  16009  fprodreclf  16012  fprodge0  16046  fprodge1  16048  rerisefaccl  16070  refallfaccl  16071  rprisefaccl  16076  reeff1  16175  nthruc  16307  regsumfsum  21564  rge0srg  21567  rebase  21735  re0g  21741  regsumsupp  21751  remet  24926  tgioo2  24939  xrsdsre  24947  recld2  24951  reperf  24956  iitopon  25017  dfii3  25021  abscncf  25039  recncf  25040  imcncf  25041  abscncfALT  25062  cnmptre  25065  icchmeo  25079  cnrehmeo  25091  evth  25097  evth2  25098  lebnumlem2  25100  lebnumii  25104  cphsqrtcl  25322  resscdrg  25496  ishl2  25508  recms  25518  reust  25519  evthicc  25597  evthicc2  25598  ovolfsf  25609  volcn  25744  volivth  25745  ismbf  25766  cncombf  25796  cnmbf  25797  0plef  25810  itg1ge0  25824  i1faddlem  25831  i1fmul  25834  itg1addlem4  25837  i1fsub  25846  itg1sub  25847  mbfi1fseqlem5  25857  xrge0f  25869  itg20  25875  itg2const  25878  itg2mulc  25885  itg2addlem  25896  i1fibl  25946  itgitg1  25947  iblabslem  25966  iblabs  25967  bddmulibl  25977  recnprss  26042  dvmptresicc  26054  dvcjbr  26087  dvfre  26089  dvnfre  26090  dvferm1  26123  dvferm2  26125  rolle  26128  cmvth  26129  mvth  26130  dvlip  26131  dvlipcn  26132  dvlip2  26133  c1liplem1  26134  c1lip2  26136  dvgt0lem1  26140  dvle  26145  dvivthlem1  26146  dvivth  26148  dvne0  26149  lhop1lem  26151  lhop1  26152  lhop2  26153  lhop  26154  dvcnvrelem1  26155  dvcnvrelem2  26156  dvcnvre  26157  dvcvx  26158  dvfsumle  26159  dvfsumge  26160  dvfsumabs  26161  dvfsumlem2  26165  dvfsumrlim  26169  ftc1a  26175  ftc1lem3  26176  ftc1lem6  26179  ftc1  26180  ftc1cn  26181  ftc2  26182  ftc2ditglem  26183  itgparts  26185  itgsubstlem  26186  itgsubst  26187  itgpowd  26188  plyn0mulidp  26421  plymulidp  26422  aacjcl  26467  aalioulem3  26474  taylthlem2  26513  taylth  26514  abelth2  26581  reeff1olem  26585  efcvx  26588  pilem3  26592  pige3ALT  26661  recosf1o  26676  resinf1o  26677  dvrelog  26778  relogcn  26779  logcnlem5  26787  logcn  26788  dvloglem  26789  dvlog2lem  26793  logccv  26804  dvcxp1  26881  cxpcn3  26889  resqrtcn  26890  loglesqrt  26902  ssscongptld  26963  ressatans  27075  rlimcnp  27106  efrlim  27110  jensenlem1  27127  jensenlem2  27128  jensen  27129  amgm  27131  lgamgulmlem2  27170  ftalem3  27215  basellem9  27229  efnnfsumcl  27243  efchtdvds  27299  lgsdchr  27495  dchrvmasumlem1  27635  dchrisum0lem3  27659  pntlem3  27749  cchhllem  29202  ex-fpar  30779  ipasslem7  31154  fprodex01  33135  indsumin  33147  rexdiv  33211  fsumrp0cl  33307  xrge0slmod  33634  ccfldsrarelvec  34027  ccfldextdgrr  34028  rmulccn  34284  raddcn  34285  xrge0iifhom  34293  lmlimxrge0  34304  rezh  34325  esumpfinvallem  34430  esumpfinval  34431  esumpfinvalf  34432  esumcvg  34442  signsplypnf  34903  signsply0  34904  iblidicc  34945  rpsqrtcn  34946  ftc2re  34951  fdvposlt  34952  fdvneggt  34953  fdvposle  34954  fdvnegge  34955  itgexpif  34959  circlemeth  34993  circlemethnat  34994  circlevma  34995  circlemethhgt  34996  logdivsqrle  35003  resconn  35692  ivthALT  36790  dnicn  37025  knoppcnlem10  37035  knoppcnlem11  37036  unbdqndv2  37044  knoppndv  37067  knoppcn2  37069  broucube  38249  mblfinlem2  38253  mbfresfi  38261  ftc1cnnclem  38286  ftc1cnnc  38287  ftc1anclem3  38290  ftc1anclem5  38292  ftc1anclem7  38294  ftc1anclem8  38295  ftc1anc  38296  ftc2nc  38297  asindmre  38298  dvreasin  38301  dvreacos  38302  areacirclem1  38303  areacirclem2  38304  areacirclem3  38305  areacirclem4  38306  areacirc  38308  repwsmet  38429  rrnequiv  38430  rrntotbnd  38431  reheibor  38434  iccbnd  38435  intlewftc  42774  dvrelog2  42777  dvrelog3  42778  aks4d1p1p5  42788  rpsscn  43006  redvmptabs  43067  readvrec2  43068  resuppsinopn  43070  readvcot  43071  resubeqsub  43137  subresre  43138  arearect  43890  areaquad  43891  k0004val0  44828  extoimad  44838  imo72b2lem0  44839  imo72b2lem2  44841  imo72b2lem1  44843  imo72b2  44846  ssrecnpr  44966  sblpnf  44968  radcnvrat  44972  lhe4.4ex1a  44987  refsumcn  45698  rr2sscn2  46029  uzsscn  46137  evthiccabs  46160  climreeq  46277  limciccioolb  46285  limcrecl  46293  limcicciooub  46299  limcleqr  46306  lptioo2cn  46307  lptioo1cn  46308  limclner  46313  liminflimsupclim  46469  resincncf  46537  cncficcgt0  46550  cncfiooicclem1  46555  cncfiooiccre  46557  jumpncnp  46560  dvcosre  46574  dvmptconst  46577  dvmptidg  46579  fperdvper  46581  dvresioo  46583  dvmulcncf  46587  dvdivcncf  46589  dvbdfbdioolem1  46590  ioodvbdlimc1lem1  46593  ioodvbdlimc1lem2  46594  ioodvbdlimc1  46595  ioodvbdlimc2lem  46596  ioodvbdlimc2  46597  itgsin0pilem1  46612  ibliccsinexp  46613  iblioosinexp  46615  itgsinexplem1  46616  itgsinexp  46617  itgcoscmulx  46631  itgsincmulx  46636  itgsubsticclem  46637  itgiccshift  46642  itgperiod  46643  itgsbtaddcnst  46644  dirkeritg  46764  dirkercncflem2  46766  dirkercncflem3  46767  dirkercncflem4  46768  dirkercncf  46769  fourierdlem16  46785  fourierdlem18  46787  fourierdlem21  46790  fourierdlem22  46791  fourierdlem39  46808  fourierdlem42  46811  fourierdlem48  46816  fourierdlem49  46817  fourierdlem53  46821  fourierdlem57  46825  fourierdlem58  46826  fourierdlem59  46827  fourierdlem60  46828  fourierdlem61  46829  fourierdlem62  46830  fourierdlem68  46836  fourierdlem70  46838  fourierdlem72  46840  fourierdlem73  46841  fourierdlem74  46842  fourierdlem75  46843  fourierdlem76  46844  fourierdlem78  46846  fourierdlem80  46848  fourierdlem83  46851  fourierdlem84  46852  fourierdlem85  46853  fourierdlem88  46856  fourierdlem89  46857  fourierdlem90  46858  fourierdlem91  46859  fourierdlem93  46861  fourierdlem94  46862  fourierdlem95  46863  fourierdlem96  46864  fourierdlem97  46865  fourierdlem98  46866  fourierdlem99  46867  fourierdlem101  46869  fourierdlem103  46871  fourierdlem104  46872  fourierdlem111  46879  fourierdlem112  46880  fourierdlem113  46881  fouriercnp  46888  sqwvfoura  46890  sqwvfourb  46891  fouriersw  46893  fouriercn  46894  etransclem2  46898  etransclem18  46914  etransclem23  46919  etransclem46  46942  rrxtopnfi  46949  rrndistlt  46952  sge0sn  47041  sge0tsms  47042  sge0f1o  47044  sge0pr  47056  sge0resplit  47068  sge0iunmptlemre  47077  sge0isummpt2  47094  hoicvr  47210  hoidmvlelem2  47258  lamberte  47570  refdivmptf  49267  refdivmptfv  49271  amgmlemALT  50548