Axiom ax-resscn 11132

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11074	. 2 class ℝ
2		cc 11073	. 2 class ℂ
3	1, 2	wss 3906	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11165  reex  11166  recni  11198  qsscn  12963  ioosscn  13414  unitsscn  13506  reexpcl  14093  rpexpcl  14095  reexpclz  14097  expge0  14113  expge1  14114  rlimrecl  15609  abscn2  15628  recn2  15630  imcn2  15631  climabs  15633  climre  15635  climim  15636  rlimabs  15638  rlimre  15640  rlimim  15641  caurcvgr  15703  caucvgrlem2  15704  caurcvg  15706  fsumrecl  15763  fsumrpcl  15766  fsumge0  15825  fsumre  15838  fsumim  15839  fprodrecl  15985  fprodrpcl  15988  fprodreclf  15991  fprodge0  16025  fprodge1  16027  rerisefaccl  16049  refallfaccl  16050  rprisefaccl  16055  reeff1  16154  nthruc  16286  regsumfsum  21489  rge0srg  21492  rebase  21660  re0g  21666  regsumsupp  21676  remet  24852  tgioo2  24865  xrsdsre  24873  recld2  24877  reperf  24882  iitopon  24943  dfii3  24947  abscncf  24965  recncf  24966  imcncf  24967  abscncfALT  24988  cnmptre  24991  icchmeo  25005  cnrehmeo  25017  evth  25023  evth2  25024  lebnumlem2  25026  lebnumii  25030  cphsqrtcl  25248  resscdrg  25422  ishl2  25434  recms  25444  reust  25445  evthicc  25523  evthicc2  25524  ovolfsf  25535  volcn  25670  volivth  25671  ismbf  25692  cncombf  25722  cnmbf  25723  0plef  25736  itg1ge0  25750  i1faddlem  25757  i1fmul  25760  itg1addlem4  25763  i1fsub  25772  itg1sub  25773  mbfi1fseqlem5  25783  xrge0f  25795  itg20  25801  itg2const  25804  itg2mulc  25811  itg2addlem  25822  i1fibl  25872  itgitg1  25873  iblabslem  25892  iblabs  25893  bddmulibl  25903  recnprss  25968  dvmptresicc  25980  dvcjbr  26013  dvfre  26015  dvnfre  26016  dvferm1  26049  dvferm2  26051  rolle  26054  cmvth  26055  mvth  26056  dvlip  26057  dvlipcn  26058  dvlip2  26059  c1liplem1  26060  c1lip2  26062  dvgt0lem1  26066  dvle  26071  dvivthlem1  26072  dvivth  26074  dvne0  26075  lhop1lem  26077  lhop1  26078  lhop2  26079  lhop  26080  dvcnvrelem1  26081  dvcnvrelem2  26082  dvcnvre  26083  dvcvx  26084  dvfsumle  26085  dvfsumge  26086  dvfsumabs  26087  dvfsumlem2  26091  dvfsumrlim  26095  ftc1a  26101  ftc1lem3  26102  ftc1lem6  26105  ftc1  26106  ftc1cn  26107  ftc2  26108  ftc2ditglem  26109  itgparts  26111  itgsubstlem  26112  itgsubst  26113  itgpowd  26114  plyn0mulidp  26347  plymulidp  26348  aacjcl  26393  aalioulem3  26400  taylthlem2  26439  taylth  26440  abelth2  26507  reeff1olem  26511  efcvx  26514  pilem3  26518  pige3ALT  26587  recosf1o  26602  resinf1o  26603  dvrelog  26704  relogcn  26705  logcnlem5  26713  logcn  26714  dvloglem  26715  dvlog2lem  26719  logccv  26730  dvcxp1  26807  cxpcn3  26815  resqrtcn  26816  loglesqrt  26828  ssscongptld  26889  ressatans  27001  rlimcnp  27032  efrlim  27036  jensenlem1  27053  jensenlem2  27054  jensen  27055  amgm  27057  lgamgulmlem2  27096  ftalem3  27141  basellem9  27155  efnnfsumcl  27169  efchtdvds  27225  lgsdchr  27421  dchrvmasumlem1  27561  dchrisum0lem3  27585  pntlem3  27675  cchhllem  29089  ex-fpar  30666  ipasslem7  31041  fprodex01  33029  indsumin  33041  rexdiv  33105  fsumrp0cl  33201  xrge0slmod  33536  ccfldsrarelvec  33970  ccfldextdgrr  33971  rmulccn  34227  raddcn  34228  xrge0iifhom  34236  lmlimxrge0  34247  rezh  34268  esumpfinvallem  34373  esumpfinval  34374  esumpfinvalf  34375  esumcvg  34385  signsplypnf  34846  signsply0  34847  iblidicc  34888  rpsqrtcn  34889  ftc2re  34894  fdvposlt  34895  fdvneggt  34896  fdvposle  34897  fdvnegge  34898  itgexpif  34902  circlemeth  34936  circlemethnat  34937  circlevma  34938  circlemethhgt  34939  logdivsqrle  34946  resconn  35601  ivthALT  36700  dnicn  36935  knoppcnlem10  36945  knoppcnlem11  36946  unbdqndv2  36954  knoppndv  36977  knoppcn2  36979  broucube  38158  mblfinlem2  38162  mbfresfi  38170  ftc1cnnclem  38195  ftc1cnnc  38196  ftc1anclem3  38199  ftc1anclem5  38201  ftc1anclem7  38203  ftc1anclem8  38204  ftc1anc  38205  ftc2nc  38206  asindmre  38207  dvreasin  38210  dvreacos  38211  areacirclem1  38212  areacirclem2  38213  areacirclem3  38214  areacirclem4  38215  areacirc  38217  repwsmet  38338  rrnequiv  38339  rrntotbnd  38340  reheibor  38343  iccbnd  38344  intlewftc  42683  dvrelog2  42686  dvrelog3  42687  aks4d1p1p5  42697  rpsscn  42913  redvmptabs  42974  readvrec2  42975  resuppsinopn  42977  readvcot  42978  resubeqsub  43044  subresre  43045  arearect  43797  areaquad  43798  k0004val0  44735  extoimad  44745  imo72b2lem0  44746  imo72b2lem2  44748  imo72b2lem1  44750  imo72b2  44753  ssrecnpr  44889  sblpnf  44891  radcnvrat  44895  lhe4.4ex1a  44910  refsumcn  45615  rr2sscn2  45946  uzsscn  46054  evthiccabs  46077  climreeq  46194  limciccioolb  46202  limcrecl  46210  limcicciooub  46216  limcleqr  46223  lptioo2cn  46224  lptioo1cn  46225  limclner  46230  liminflimsupclim  46386  resincncf  46454  cncficcgt0  46467  cncfiooicclem1  46472  cncfiooiccre  46474  jumpncnp  46477  dvcosre  46491  dvmptconst  46494  dvmptidg  46496  fperdvper  46498  dvresioo  46500  dvmulcncf  46504  dvdivcncf  46506  dvbdfbdioolem1  46507  ioodvbdlimc1lem1  46510  ioodvbdlimc1lem2  46511  ioodvbdlimc1  46512  ioodvbdlimc2lem  46513  ioodvbdlimc2  46514  itgsin0pilem1  46529  ibliccsinexp  46530  iblioosinexp  46532  itgsinexplem1  46533  itgsinexp  46534  itgcoscmulx  46548  itgsincmulx  46553  itgsubsticclem  46554  itgiccshift  46559  itgperiod  46560  itgsbtaddcnst  46561  dirkeritg  46681  dirkercncflem2  46683  dirkercncflem3  46684  dirkercncflem4  46685  dirkercncf  46686  fourierdlem16  46702  fourierdlem18  46704  fourierdlem21  46707  fourierdlem22  46708  fourierdlem39  46725  fourierdlem42  46728  fourierdlem48  46733  fourierdlem49  46734  fourierdlem53  46738  fourierdlem57  46742  fourierdlem58  46743  fourierdlem59  46744  fourierdlem60  46745  fourierdlem61  46746  fourierdlem62  46747  fourierdlem68  46753  fourierdlem70  46755  fourierdlem72  46757  fourierdlem73  46758  fourierdlem74  46759  fourierdlem75  46760  fourierdlem76  46761  fourierdlem78  46763  fourierdlem80  46765  fourierdlem83  46768  fourierdlem84  46769  fourierdlem85  46770  fourierdlem88  46773  fourierdlem89  46774  fourierdlem90  46775  fourierdlem91  46776  fourierdlem93  46778  fourierdlem94  46779  fourierdlem95  46780  fourierdlem96  46781  fourierdlem97  46782  fourierdlem98  46783  fourierdlem99  46784  fourierdlem101  46786  fourierdlem103  46788  fourierdlem104  46789  fourierdlem111  46796  fourierdlem112  46797  fourierdlem113  46798  fouriercnp  46805  sqwvfoura  46807  sqwvfourb  46808  fouriersw  46810  fouriercn  46811  etransclem2  46815  etransclem18  46831  etransclem23  46836  etransclem46  46859  rrxtopnfi  46866  rrndistlt  46869  sge0sn  46958  sge0tsms  46959  sge0f1o  46961  sge0pr  46973  sge0resplit  46985  sge0iunmptlemre  46994  sge0isummpt2  47011  hoicvr  47127  hoidmvlelem2  47175  lamberte  47487  refdivmptf  49169  refdivmptfv  49173  amgmlemALT  50429