Axiom ax-resscn 11097

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11039	. 2 class ℝ
2		cc 11038	. 2 class ℂ
3	1, 2	wss 3903	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11130  reex  11131  recni  11160  qsscn  12887  ioosscn  13338  unitsscn  13430  reexpcl  14015  rpexpcl  14017  reexpclz  14019  expge0  14035  expge1  14036  rlimrecl  15517  abscn2  15536  recn2  15538  imcn2  15539  climabs  15541  climre  15543  climim  15544  rlimabs  15546  rlimre  15548  rlimim  15549  caurcvgr  15611  caucvgrlem2  15612  caurcvg  15614  fsumrecl  15671  fsumrpcl  15674  fsumge0  15732  fsumre  15745  fsumim  15746  fprodrecl  15890  fprodrpcl  15893  fprodreclf  15896  fprodge0  15930  fprodge1  15932  rerisefaccl  15954  refallfaccl  15955  rprisefaccl  15960  reeff1  16059  nthruc  16191  regsumfsum  21407  rge0srg  21410  rebase  21578  re0g  21584  regsumsupp  21594  remet  24751  tgioo2  24764  xrsdsre  24772  recld2  24776  reperf  24781  iitopon  24845  dfii3  24849  abscncf  24867  recncf  24868  imcncf  24869  abscncfALT  24891  cnmptre  24894  iimulcnOLD  24908  icchmeo  24911  icchmeoOLD  24912  cnrehmeo  24924  cnrehmeoOLD  24925  evth  24931  evth2  24932  lebnumlem2  24934  lebnumii  24938  reparphtiOLD  24970  cphsqrtcl  25157  resscdrg  25331  ishl2  25343  recms  25353  reust  25354  evthicc  25433  evthicc2  25434  ovolfsf  25445  volcn  25580  volivth  25581  ismbf  25602  cncombf  25632  cnmbf  25633  0plef  25646  itg1ge0  25660  i1faddlem  25667  i1fmul  25670  itg1addlem4  25673  i1fsub  25682  itg1sub  25683  mbfi1fseqlem5  25693  xrge0f  25705  itg20  25711  itg2const  25714  itg2mulc  25721  itg2addlem  25732  i1fibl  25782  itgitg1  25783  iblabslem  25802  iblabs  25803  bddmulibl  25813  recnprss  25878  dvmptresicc  25890  dvcjbr  25926  dvfre  25928  dvnfre  25929  dvferm1  25962  dvferm2  25964  rolle  25967  cmvth  25968  cmvthOLD  25969  mvth  25970  dvlip  25971  dvlipcn  25972  dvlip2  25973  c1liplem1  25974  c1lip2  25976  dvgt0lem1  25980  dvle  25985  dvivthlem1  25986  dvivth  25988  dvne0  25989  lhop1lem  25991  lhop1  25992  lhop2  25993  lhop  25994  dvcnvrelem1  25995  dvcnvrelem2  25996  dvcnvre  25997  dvcvx  25998  dvfsumle  25999  dvfsumleOLD  26000  dvfsumge  26001  dvfsumabs  26002  dvfsumlem2  26006  dvfsumlem2OLD  26007  dvfsumrlim  26011  ftc1a  26017  ftc1lem3  26018  ftc1lem6  26021  ftc1  26022  ftc1cn  26023  ftc2  26024  ftc2ditglem  26025  itgparts  26027  itgsubstlem  26028  itgsubst  26029  itgpowd  26030  aacjcl  26308  aalioulem3  26315  taylthlem2  26355  taylthlem2OLD  26356  taylth  26357  abelth2  26425  reeff1olem  26429  efcvx  26432  pilem3  26436  pige3ALT  26502  recosf1o  26517  resinf1o  26518  dvrelog  26619  relogcn  26620  logcnlem5  26628  logcn  26629  dvloglem  26630  dvlog2lem  26634  logccv  26645  dvcxp1  26722  cxpcn3  26731  resqrtcn  26732  loglesqrt  26744  ssscongptld  26805  ressatans  26917  rlimcnp  26948  efrlim  26952  efrlimOLD  26953  jensenlem1  26970  jensenlem2  26971  jensen  26972  amgm  26974  lgamgulmlem2  27013  ftalem3  27058  basellem9  27072  efnnfsumcl  27086  efchtdvds  27142  lgsdchr  27339  dchrvmasumlem1  27479  dchrisum0lem3  27503  pntlem3  27593  cchhllem  28977  ex-fpar  30555  ipasslem7  30930  fprodex01  32923  indsumin  32960  rexdiv  33024  fsumrp0cl  33120  xrge0slmod  33447  ccfldsrarelvec  33855  ccfldextdgrr  33856  rmulccn  34112  raddcn  34113  xrge0iifhom  34121  lmlimxrge0  34132  rezh  34153  esumpfinvallem  34258  esumpfinval  34259  esumpfinvalf  34260  esumcvg  34270  plymulx0  34731  plymulx  34732  signsplypnf  34734  signsply0  34735  iblidicc  34776  rpsqrtcn  34777  ftc2re  34782  fdvposlt  34783  fdvneggt  34784  fdvposle  34785  fdvnegge  34786  itgexpif  34790  circlemeth  34824  circlemethnat  34825  circlevma  34826  circlemethhgt  34827  logdivsqrle  34834  resconn  35468  ivthALT  36557  dnicn  36720  knoppcnlem10  36730  knoppcnlem11  36731  unbdqndv2  36739  knoppndv  36762  knoppcn2  36764  broucube  37934  mblfinlem2  37938  mbfresfi  37946  ftc1cnnclem  37971  ftc1cnnc  37972  ftc1anclem3  37975  ftc1anclem5  37977  ftc1anclem7  37979  ftc1anclem8  37980  ftc1anc  37981  ftc2nc  37982  asindmre  37983  dvreasin  37986  dvreacos  37987  areacirclem1  37988  areacirclem2  37989  areacirclem3  37990  areacirclem4  37991  areacirc  37993  repwsmet  38114  rrnequiv  38115  rrntotbnd  38116  reheibor  38119  iccbnd  38120  intlewftc  42460  dvrelog2  42463  dvrelog3  42464  aks4d1p1p5  42474  rpsscn  42698  redvmptabs  42759  readvrec2  42760  resuppsinopn  42762  readvcot  42763  resubeqsub  42829  subresre  42830  arearect  43601  areaquad  43602  k0004val0  44539  extoimad  44549  imo72b2lem0  44550  imo72b2lem2  44552  imo72b2lem1  44554  imo72b2  44557  ssrecnpr  44693  sblpnf  44695  radcnvrat  44699  lhe4.4ex1a  44714  refsumcn  45419  rr2sscn2  45753  uzsscn  45862  evthiccabs  45885  climreeq  46002  limciccioolb  46010  limcrecl  46018  limcicciooub  46024  limcleqr  46031  lptioo2cn  46032  lptioo1cn  46033  limclner  46038  liminflimsupclim  46194  resincncf  46262  cncficcgt0  46275  cncfiooicclem1  46280  cncfiooiccre  46282  jumpncnp  46285  dvcosre  46299  dvmptconst  46302  dvmptidg  46304  fperdvper  46306  dvresioo  46308  dvmulcncf  46312  dvdivcncf  46314  dvbdfbdioolem1  46315  ioodvbdlimc1lem1  46318  ioodvbdlimc1lem2  46319  ioodvbdlimc1  46320  ioodvbdlimc2lem  46321  ioodvbdlimc2  46322  itgsin0pilem1  46337  ibliccsinexp  46338  iblioosinexp  46340  itgsinexplem1  46341  itgsinexp  46342  itgcoscmulx  46356  itgsincmulx  46361  itgsubsticclem  46362  itgiccshift  46367  itgperiod  46368  itgsbtaddcnst  46369  dirkeritg  46489  dirkercncflem2  46491  dirkercncflem3  46492  dirkercncflem4  46493  dirkercncf  46494  fourierdlem16  46510  fourierdlem18  46512  fourierdlem21  46515  fourierdlem22  46516  fourierdlem39  46533  fourierdlem42  46536  fourierdlem48  46541  fourierdlem49  46542  fourierdlem53  46546  fourierdlem57  46550  fourierdlem58  46551  fourierdlem59  46552  fourierdlem60  46553  fourierdlem61  46554  fourierdlem62  46555  fourierdlem68  46561  fourierdlem70  46563  fourierdlem72  46565  fourierdlem73  46566  fourierdlem74  46567  fourierdlem75  46568  fourierdlem76  46569  fourierdlem78  46571  fourierdlem80  46573  fourierdlem83  46576  fourierdlem84  46577  fourierdlem85  46578  fourierdlem88  46581  fourierdlem89  46582  fourierdlem90  46583  fourierdlem91  46584  fourierdlem93  46586  fourierdlem94  46587  fourierdlem95  46588  fourierdlem96  46589  fourierdlem97  46590  fourierdlem98  46591  fourierdlem99  46592  fourierdlem101  46594  fourierdlem103  46596  fourierdlem104  46597  fourierdlem111  46604  fourierdlem112  46605  fourierdlem113  46606  fouriercnp  46613  sqwvfoura  46615  sqwvfourb  46616  fouriersw  46618  fouriercn  46619  etransclem2  46623  etransclem18  46639  etransclem23  46644  etransclem46  46667  rrxtopnfi  46674  rrndistlt  46677  sge0sn  46766  sge0tsms  46767  sge0f1o  46769  sge0pr  46781  sge0resplit  46793  sge0iunmptlemre  46802  sge0isummpt2  46819  hoicvr  46935  hoidmvlelem2  46983  lamberte  47277  refdivmptf  48931  refdivmptfv  48935  amgmlemALT  50191