Axiom ax-resscn 11063

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11005	. 2 class ℝ
2		cc 11004	. 2 class ℂ
3	1, 2	wss 3897	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11096  reex  11097  recni  11126  qsscn  12858  ioosscn  13308  unitsscn  13400  reexpcl  13985  rpexpcl  13987  reexpclz  13989  expge0  14005  expge1  14006  rlimrecl  15487  abscn2  15506  recn2  15508  imcn2  15509  climabs  15511  climre  15513  climim  15514  rlimabs  15516  rlimre  15518  rlimim  15519  caurcvgr  15581  caucvgrlem2  15582  caurcvg  15584  fsumrecl  15641  fsumrpcl  15644  fsumge0  15702  fsumre  15715  fsumim  15716  fprodrecl  15860  fprodrpcl  15863  fprodreclf  15866  fprodge0  15900  fprodge1  15902  rerisefaccl  15924  refallfaccl  15925  rprisefaccl  15930  reeff1  16029  nthruc  16161  regsumfsum  21372  rge0srg  21375  rebase  21543  re0g  21549  regsumsupp  21559  remet  24705  tgioo2  24718  xrsdsre  24726  recld2  24730  reperf  24735  iitopon  24799  dfii3  24803  abscncf  24821  recncf  24822  imcncf  24823  abscncfALT  24845  cnmptre  24848  iimulcnOLD  24862  icchmeo  24865  icchmeoOLD  24866  cnrehmeo  24878  cnrehmeoOLD  24879  evth  24885  evth2  24886  lebnumlem2  24888  lebnumii  24892  reparphtiOLD  24924  cphsqrtcl  25111  resscdrg  25285  ishl2  25297  recms  25307  reust  25308  evthicc  25387  evthicc2  25388  ovolfsf  25399  volcn  25534  volivth  25535  ismbf  25556  cncombf  25586  cnmbf  25587  0plef  25600  itg1ge0  25614  i1faddlem  25621  i1fmul  25624  itg1addlem4  25627  i1fsub  25636  itg1sub  25637  mbfi1fseqlem5  25647  xrge0f  25659  itg20  25665  itg2const  25668  itg2mulc  25675  itg2addlem  25686  i1fibl  25736  itgitg1  25737  iblabslem  25756  iblabs  25757  bddmulibl  25767  recnprss  25832  dvmptresicc  25844  dvcjbr  25880  dvfre  25882  dvnfre  25883  dvferm1  25916  dvferm2  25918  rolle  25921  cmvth  25922  cmvthOLD  25923  mvth  25924  dvlip  25925  dvlipcn  25926  dvlip2  25927  c1liplem1  25928  c1lip2  25930  dvgt0lem1  25934  dvle  25939  dvivthlem1  25940  dvivth  25942  dvne0  25943  lhop1lem  25945  lhop1  25946  lhop2  25947  lhop  25948  dvcnvrelem1  25949  dvcnvrelem2  25950  dvcnvre  25951  dvcvx  25952  dvfsumle  25953  dvfsumleOLD  25954  dvfsumge  25955  dvfsumabs  25956  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsumrlim  25965  ftc1a  25971  ftc1lem3  25972  ftc1lem6  25975  ftc1  25976  ftc1cn  25977  ftc2  25978  ftc2ditglem  25979  itgparts  25981  itgsubstlem  25982  itgsubst  25983  itgpowd  25984  aacjcl  26262  aalioulem3  26269  taylthlem2  26309  taylthlem2OLD  26310  taylth  26311  abelth2  26379  reeff1olem  26383  efcvx  26386  pilem3  26390  pige3ALT  26456  recosf1o  26471  resinf1o  26472  dvrelog  26573  relogcn  26574  logcnlem5  26582  logcn  26583  dvloglem  26584  dvlog2lem  26588  logccv  26599  dvcxp1  26676  cxpcn3  26685  resqrtcn  26686  loglesqrt  26698  ssscongptld  26759  ressatans  26871  rlimcnp  26902  efrlim  26906  efrlimOLD  26907  jensenlem1  26924  jensenlem2  26925  jensen  26926  amgm  26928  lgamgulmlem2  26967  ftalem3  27012  basellem9  27026  efnnfsumcl  27040  efchtdvds  27096  lgsdchr  27293  dchrvmasumlem1  27433  dchrisum0lem3  27457  pntlem3  27547  cchhllem  28865  ex-fpar  30442  ipasslem7  30816  fprodex01  32808  indsumin  32843  rexdiv  32906  fsumrp0cl  33002  xrge0slmod  33313  ccfldsrarelvec  33684  ccfldextdgrr  33685  rmulccn  33941  raddcn  33942  xrge0iifhom  33950  lmlimxrge0  33961  rezh  33982  esumpfinvallem  34087  esumpfinval  34088  esumpfinvalf  34089  esumcvg  34099  plymulx0  34560  plymulx  34561  signsplypnf  34563  signsply0  34564  iblidicc  34605  rpsqrtcn  34606  ftc2re  34611  fdvposlt  34612  fdvneggt  34613  fdvposle  34614  fdvnegge  34615  itgexpif  34619  circlemeth  34653  circlemethnat  34654  circlevma  34655  circlemethhgt  34656  logdivsqrle  34663  resconn  35290  ivthALT  36379  dnicn  36536  knoppcnlem10  36546  knoppcnlem11  36547  unbdqndv2  36555  knoppndv  36578  knoppcn2  36580  broucube  37704  mblfinlem2  37708  mbfresfi  37716  ftc1cnnclem  37741  ftc1cnnc  37742  ftc1anclem3  37745  ftc1anclem5  37747  ftc1anclem7  37749  ftc1anclem8  37750  ftc1anc  37751  ftc2nc  37752  asindmre  37753  dvreasin  37756  dvreacos  37757  areacirclem1  37758  areacirclem2  37759  areacirclem3  37760  areacirclem4  37761  areacirc  37763  repwsmet  37884  rrnequiv  37885  rrntotbnd  37886  reheibor  37889  iccbnd  37890  intlewftc  42164  dvrelog2  42167  dvrelog3  42168  aks4d1p1p5  42178  rpsscn  42402  redvmptabs  42463  readvrec2  42464  resuppsinopn  42466  readvcot  42467  resubeqsub  42533  subresre  42534  arearect  43318  areaquad  43319  k0004val0  44257  extoimad  44267  imo72b2lem0  44268  imo72b2lem2  44270  imo72b2lem1  44272  imo72b2  44275  ssrecnpr  44411  sblpnf  44413  radcnvrat  44417  lhe4.4ex1a  44432  refsumcn  45137  rr2sscn2  45474  uzsscn  45583  evthiccabs  45606  climreeq  45723  limciccioolb  45731  limcrecl  45739  limcicciooub  45745  limcleqr  45752  lptioo2cn  45753  lptioo1cn  45754  limclner  45759  liminflimsupclim  45915  resincncf  45983  cncficcgt0  45996  cncfiooicclem1  46001  cncfiooiccre  46003  jumpncnp  46006  dvcosre  46020  dvmptconst  46023  dvmptidg  46025  fperdvper  46027  dvresioo  46029  dvmulcncf  46033  dvdivcncf  46035  dvbdfbdioolem1  46036  ioodvbdlimc1lem1  46039  ioodvbdlimc1lem2  46040  ioodvbdlimc1  46041  ioodvbdlimc2lem  46042  ioodvbdlimc2  46043  itgsin0pilem1  46058  ibliccsinexp  46059  iblioosinexp  46061  itgsinexplem1  46062  itgsinexp  46063  itgcoscmulx  46077  itgsincmulx  46082  itgsubsticclem  46083  itgiccshift  46088  itgperiod  46089  itgsbtaddcnst  46090  dirkeritg  46210  dirkercncflem2  46212  dirkercncflem3  46213  dirkercncflem4  46214  dirkercncf  46215  fourierdlem16  46231  fourierdlem18  46233  fourierdlem21  46236  fourierdlem22  46237  fourierdlem39  46254  fourierdlem42  46257  fourierdlem48  46262  fourierdlem49  46263  fourierdlem53  46267  fourierdlem57  46271  fourierdlem58  46272  fourierdlem59  46273  fourierdlem60  46274  fourierdlem61  46275  fourierdlem62  46276  fourierdlem68  46282  fourierdlem70  46284  fourierdlem72  46286  fourierdlem73  46287  fourierdlem74  46288  fourierdlem75  46289  fourierdlem76  46290  fourierdlem78  46292  fourierdlem80  46294  fourierdlem83  46297  fourierdlem84  46298  fourierdlem85  46299  fourierdlem88  46302  fourierdlem89  46303  fourierdlem90  46304  fourierdlem91  46305  fourierdlem93  46307  fourierdlem94  46308  fourierdlem95  46309  fourierdlem96  46310  fourierdlem97  46311  fourierdlem98  46312  fourierdlem99  46313  fourierdlem101  46315  fourierdlem103  46317  fourierdlem104  46318  fourierdlem111  46325  fourierdlem112  46326  fourierdlem113  46327  fouriercnp  46334  sqwvfoura  46336  sqwvfourb  46337  fouriersw  46339  fouriercn  46340  etransclem2  46344  etransclem18  46360  etransclem23  46365  etransclem46  46388  rrxtopnfi  46395  rrndistlt  46398  sge0sn  46487  sge0tsms  46488  sge0f1o  46490  sge0pr  46502  sge0resplit  46514  sge0iunmptlemre  46523  sge0isummpt2  46540  hoicvr  46656  hoidmvlelem2  46704  lamberte  46998  refdivmptf  48653  refdivmptfv  48657  amgmlemALT  49914