Axiom ax-resscn 11095

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11037	. 2 class ℝ
2		cc 11036	. 2 class ℂ
3	1, 2	wss 3889	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11128  reex  11129  recni  11159  qsscn  12910  ioosscn  13361  unitsscn  13453  reexpcl  14040  rpexpcl  14042  reexpclz  14044  expge0  14060  expge1  14061  rlimrecl  15542  abscn2  15561  recn2  15563  imcn2  15564  climabs  15566  climre  15568  climim  15569  rlimabs  15571  rlimre  15573  rlimim  15574  caurcvgr  15636  caucvgrlem2  15637  caurcvg  15639  fsumrecl  15696  fsumrpcl  15699  fsumge0  15758  fsumre  15771  fsumim  15772  fprodrecl  15918  fprodrpcl  15921  fprodreclf  15924  fprodge0  15958  fprodge1  15960  rerisefaccl  15982  refallfaccl  15983  rprisefaccl  15988  reeff1  16087  nthruc  16219  regsumfsum  21415  rge0srg  21418  rebase  21586  re0g  21592  regsumsupp  21602  remet  24755  tgioo2  24768  xrsdsre  24776  recld2  24780  reperf  24785  iitopon  24846  dfii3  24850  abscncf  24868  recncf  24869  imcncf  24870  abscncfALT  24891  cnmptre  24894  icchmeo  24908  cnrehmeo  24920  evth  24926  evth2  24927  lebnumlem2  24929  lebnumii  24933  cphsqrtcl  25151  resscdrg  25325  ishl2  25337  recms  25347  reust  25348  evthicc  25426  evthicc2  25427  ovolfsf  25438  volcn  25573  volivth  25574  ismbf  25595  cncombf  25625  cnmbf  25626  0plef  25639  itg1ge0  25653  i1faddlem  25660  i1fmul  25663  itg1addlem4  25666  i1fsub  25675  itg1sub  25676  mbfi1fseqlem5  25686  xrge0f  25698  itg20  25704  itg2const  25707  itg2mulc  25714  itg2addlem  25725  i1fibl  25775  itgitg1  25776  iblabslem  25795  iblabs  25796  bddmulibl  25806  recnprss  25871  dvmptresicc  25883  dvcjbr  25916  dvfre  25918  dvnfre  25919  dvferm1  25952  dvferm2  25954  rolle  25957  cmvth  25958  mvth  25959  dvlip  25960  dvlipcn  25961  dvlip2  25962  c1liplem1  25963  c1lip2  25965  dvgt0lem1  25969  dvle  25974  dvivthlem1  25975  dvivth  25977  dvne0  25978  lhop1lem  25980  lhop1  25981  lhop2  25982  lhop  25983  dvcnvrelem1  25984  dvcnvrelem2  25985  dvcnvre  25986  dvcvx  25987  dvfsumle  25988  dvfsumge  25989  dvfsumabs  25990  dvfsumlem2  25994  dvfsumrlim  25998  ftc1a  26004  ftc1lem3  26005  ftc1lem6  26008  ftc1  26009  ftc1cn  26010  ftc2  26011  ftc2ditglem  26012  itgparts  26014  itgsubstlem  26015  itgsubst  26016  itgpowd  26017  aacjcl  26293  aalioulem3  26300  taylthlem2  26339  taylth  26340  abelth2  26407  reeff1olem  26411  efcvx  26414  pilem3  26418  pige3ALT  26484  recosf1o  26499  resinf1o  26500  dvrelog  26601  relogcn  26602  logcnlem5  26610  logcn  26611  dvloglem  26612  dvlog2lem  26616  logccv  26627  dvcxp1  26704  cxpcn3  26712  resqrtcn  26713  loglesqrt  26725  ssscongptld  26786  ressatans  26898  rlimcnp  26929  efrlim  26933  jensenlem1  26950  jensenlem2  26951  jensen  26952  amgm  26954  lgamgulmlem2  26993  ftalem3  27038  basellem9  27052  efnnfsumcl  27066  efchtdvds  27122  lgsdchr  27318  dchrvmasumlem1  27458  dchrisum0lem3  27482  pntlem3  27572  cchhllem  28955  ex-fpar  30532  ipasslem7  30907  fprodex01  32898  indsumin  32921  rexdiv  32985  fsumrp0cl  33081  xrge0slmod  33408  ccfldsrarelvec  33815  ccfldextdgrr  33816  rmulccn  34072  raddcn  34073  xrge0iifhom  34081  lmlimxrge0  34092  rezh  34113  esumpfinvallem  34218  esumpfinval  34219  esumpfinvalf  34220  esumcvg  34230  plymulx0  34691  plymulx  34692  signsplypnf  34694  signsply0  34695  iblidicc  34736  rpsqrtcn  34737  ftc2re  34742  fdvposlt  34743  fdvneggt  34744  fdvposle  34745  fdvnegge  34746  itgexpif  34750  circlemeth  34784  circlemethnat  34785  circlevma  34786  circlemethhgt  34787  logdivsqrle  34794  resconn  35428  ivthALT  36517  dnicn  36752  knoppcnlem10  36762  knoppcnlem11  36763  unbdqndv2  36771  knoppndv  36794  knoppcn2  36796  broucube  37975  mblfinlem2  37979  mbfresfi  37987  ftc1cnnclem  38012  ftc1cnnc  38013  ftc1anclem3  38016  ftc1anclem5  38018  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  ftc2nc  38023  asindmre  38024  dvreasin  38027  dvreacos  38028  areacirclem1  38029  areacirclem2  38030  areacirclem3  38031  areacirclem4  38032  areacirc  38034  repwsmet  38155  rrnequiv  38156  rrntotbnd  38157  reheibor  38160  iccbnd  38161  intlewftc  42500  dvrelog2  42503  dvrelog3  42504  aks4d1p1p5  42514  rpsscn  42731  redvmptabs  42792  readvrec2  42793  resuppsinopn  42795  readvcot  42796  resubeqsub  42862  subresre  42863  arearect  43643  areaquad  43644  k0004val0  44581  extoimad  44591  imo72b2lem0  44592  imo72b2lem2  44594  imo72b2lem1  44596  imo72b2  44599  ssrecnpr  44735  sblpnf  44737  radcnvrat  44741  lhe4.4ex1a  44756  refsumcn  45461  rr2sscn2  45795  uzsscn  45903  evthiccabs  45926  climreeq  46043  limciccioolb  46051  limcrecl  46059  limcicciooub  46065  limcleqr  46072  lptioo2cn  46073  lptioo1cn  46074  limclner  46079  liminflimsupclim  46235  resincncf  46303  cncficcgt0  46316  cncfiooicclem1  46321  cncfiooiccre  46323  jumpncnp  46326  dvcosre  46340  dvmptconst  46343  dvmptidg  46345  fperdvper  46347  dvresioo  46349  dvmulcncf  46353  dvdivcncf  46355  dvbdfbdioolem1  46356  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc1  46361  ioodvbdlimc2lem  46362  ioodvbdlimc2  46363  itgsin0pilem1  46378  ibliccsinexp  46379  iblioosinexp  46381  itgsinexplem1  46382  itgsinexp  46383  itgcoscmulx  46397  itgsincmulx  46402  itgsubsticclem  46403  itgiccshift  46408  itgperiod  46409  itgsbtaddcnst  46410  dirkeritg  46530  dirkercncflem2  46532  dirkercncflem3  46533  dirkercncflem4  46534  dirkercncf  46535  fourierdlem16  46551  fourierdlem18  46553  fourierdlem21  46556  fourierdlem22  46557  fourierdlem39  46574  fourierdlem42  46577  fourierdlem48  46582  fourierdlem49  46583  fourierdlem53  46587  fourierdlem57  46591  fourierdlem58  46592  fourierdlem59  46593  fourierdlem60  46594  fourierdlem61  46595  fourierdlem62  46596  fourierdlem68  46602  fourierdlem70  46604  fourierdlem72  46606  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem78  46612  fourierdlem80  46614  fourierdlem83  46617  fourierdlem84  46618  fourierdlem85  46619  fourierdlem88  46622  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem93  46627  fourierdlem94  46628  fourierdlem95  46629  fourierdlem96  46630  fourierdlem97  46631  fourierdlem98  46632  fourierdlem99  46633  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem112  46646  fourierdlem113  46647  fouriercnp  46654  sqwvfoura  46656  sqwvfourb  46657  fouriersw  46659  fouriercn  46660  etransclem2  46664  etransclem18  46680  etransclem23  46685  etransclem46  46708  rrxtopnfi  46715  rrndistlt  46718  sge0sn  46807  sge0tsms  46808  sge0f1o  46810  sge0pr  46822  sge0resplit  46834  sge0iunmptlemre  46843  sge0isummpt2  46860  hoicvr  46976  hoidmvlelem2  47024  lamberte  47336  refdivmptf  49018  refdivmptfv  49022  amgmlemALT  50278