Axiom ax-resscn 11169

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11111	. 2 class ℝ
2		cc 11110	. 2 class ℂ
3	1, 2	wss 3948	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11202  reex  11203  recni  11230  qsscn  12946  ioosscn  13388  unitsscn  13479  reexpcl  14046  rpexpcl  14048  reexpclz  14050  expge0  14066  expge1  14067  rlimrecl  15526  abscn2  15545  recn2  15547  imcn2  15548  climabs  15550  climre  15552  climim  15553  rlimabs  15555  rlimre  15557  rlimim  15558  caurcvgr  15622  caucvgrlem2  15623  caurcvg  15625  fsumrecl  15682  fsumrpcl  15685  fsumge0  15743  fsumre  15756  fsumim  15757  fprodrecl  15899  fprodrpcl  15902  fprodreclf  15905  fprodge0  15939  fprodge1  15941  rerisefaccl  15963  refallfaccl  15964  rprisefaccl  15969  reeff1  16065  nthruc  16197  regsumfsum  21019  rge0srg  21022  rebase  21165  re0g  21171  regsumsupp  21181  remet  24313  tgioo2  24326  xrsdsre  24333  recld2  24337  reperf  24342  iitopon  24402  dfii3  24406  abscncf  24424  recncf  24425  imcncf  24426  abscncfALT  24447  cnmptre  24450  iimulcn  24461  icchmeo  24464  cnrehmeo  24476  evth  24482  evth2  24483  lebnumlem2  24485  lebnumii  24489  reparphti  24520  cphsqrtcl  24708  resscdrg  24882  ishl2  24894  recms  24904  reust  24905  evthicc  24983  evthicc2  24984  ovolfsf  24995  volcn  25130  volivth  25131  ismbf  25152  cncombf  25182  cnmbf  25183  0plef  25196  itg1ge0  25210  i1faddlem  25217  i1fmul  25220  itg1addlem4  25223  itg1addlem4OLD  25224  i1fsub  25233  itg1sub  25234  mbfi1fseqlem5  25244  xrge0f  25256  itg20  25262  itg2const  25265  itg2mulc  25272  itg2addlem  25283  i1fibl  25332  itgitg1  25333  iblabslem  25352  iblabs  25353  bddmulibl  25363  recnprss  25428  dvmptresicc  25440  dvcjbr  25473  dvfre  25475  dvnfre  25476  dvferm1  25509  dvferm2  25511  rolle  25514  cmvth  25515  mvth  25516  dvlip  25517  dvlipcn  25518  dvlip2  25519  c1liplem1  25520  c1lip2  25522  dvgt0lem1  25526  dvle  25531  dvivthlem1  25532  dvivth  25534  dvne0  25535  lhop1lem  25537  lhop1  25538  lhop2  25539  lhop  25540  dvcnvrelem1  25541  dvcnvrelem2  25542  dvcnvre  25543  dvcvx  25544  dvfsumle  25545  dvfsumge  25546  dvfsumabs  25547  dvfsumlem2  25551  dvfsumrlim  25555  ftc1a  25561  ftc1lem3  25562  ftc1lem6  25565  ftc1  25566  ftc1cn  25567  ftc2  25568  ftc2ditglem  25569  itgparts  25571  itgsubstlem  25572  itgsubst  25573  itgpowd  25574  aacjcl  25847  aalioulem3  25854  taylthlem2  25893  taylth  25894  abelth2  25961  reeff1olem  25965  efcvx  25968  pilem3  25972  pige3ALT  26036  recosf1o  26051  resinf1o  26052  dvrelog  26152  relogcn  26153  logcnlem5  26161  logcn  26162  dvloglem  26163  dvlog2lem  26167  logccv  26178  dvcxp1  26255  cxpcn3  26263  resqrtcn  26264  loglesqrt  26273  ssscongptld  26334  ressatans  26446  rlimcnp  26477  efrlim  26481  jensenlem1  26498  jensenlem2  26499  jensen  26500  amgm  26502  lgamgulmlem2  26541  ftalem3  26586  basellem9  26600  efnnfsumcl  26614  efchtdvds  26670  lgsdchr  26865  dchrvmasumlem1  27005  dchrisum0lem3  27029  pntlem3  27119  cchhllem  28182  cchhllemOLD  28183  ex-fpar  29753  ipasslem7  30127  fprodex01  32069  rexdiv  32130  fsumrp0cl  32234  xrge0slmod  32504  ccfldsrarelvec  32805  ccfldextdgrr  32806  rmulccn  32977  raddcn  32978  xrge0iifhom  32986  lmlimxrge0  32997  rezh  33020  indsumin  33089  esumpfinvallem  33141  esumpfinval  33142  esumpfinvalf  33143  esumcvg  33153  plymulx0  33627  plymulx  33628  signsplypnf  33630  signsply0  33631  iblidicc  33673  rpsqrtcn  33674  ftc2re  33679  fdvposlt  33680  fdvneggt  33681  fdvposle  33682  fdvnegge  33683  itgexpif  33687  circlemeth  33721  circlemethnat  33722  circlevma  33723  circlemethhgt  33724  logdivsqrle  33731  cvxpconn  34302  cvxsconn  34303  resconn  34306  gg-icchmeo  35239  gg-cnrehmeo  35240  gg-rmulccn  35248  gg-cmvth  35250  gg-dvfsumle  35251  gg-dvfsumlem2  35252  ivthALT  35306  dnicn  35454  knoppcnlem10  35464  knoppcnlem11  35465  unbdqndv2  35473  knoppndv  35496  knoppcn2  35498  broucube  36608  mblfinlem2  36612  mbfresfi  36620  ftc1cnnclem  36645  ftc1cnnc  36646  ftc1anclem3  36649  ftc1anclem5  36651  ftc1anclem7  36653  ftc1anclem8  36654  ftc1anc  36655  ftc2nc  36656  asindmre  36657  dvreasin  36660  dvreacos  36661  areacirclem1  36662  areacirclem2  36663  areacirclem3  36664  areacirclem4  36665  areacirc  36667  repwsmet  36788  rrnequiv  36789  rrntotbnd  36790  reheibor  36793  iccbnd  36794  intlewftc  41012  dvrelog2  41015  dvrelog3  41016  aks4d1p1p5  41026  resubeqsub  41384  subresre  41385  arearect  42046  areaquad  42047  k0004val0  42987  extoimad  42998  imo72b2lem0  42999  imo72b2lem2  43001  imo72b2lem1  43003  imo72b2  43006  ssrecnpr  43149  sblpnf  43151  radcnvrat  43155  lhe4.4ex1a  43170  refsumcn  43796  rr2sscn2  44155  uzsscn  44265  evthiccabs  44288  climreeq  44408  limciccioolb  44416  limcrecl  44424  limcicciooub  44432  limcleqr  44439  lptioo2cn  44440  lptioo1cn  44441  limclner  44446  liminflimsupclim  44602  resincncf  44670  cncficcgt0  44683  cncfiooicclem1  44688  cncfiooiccre  44690  jumpncnp  44693  dvcosre  44707  dvmptconst  44710  dvmptidg  44712  fperdvper  44714  dvresioo  44716  dvmulcncf  44720  dvdivcncf  44722  dvbdfbdioolem1  44723  ioodvbdlimc1lem1  44726  ioodvbdlimc1lem2  44727  ioodvbdlimc1  44728  ioodvbdlimc2lem  44729  ioodvbdlimc2  44730  itgsin0pilem1  44745  ibliccsinexp  44746  iblioosinexp  44748  itgsinexplem1  44749  itgsinexp  44750  itgcoscmulx  44764  itgsincmulx  44769  itgsubsticclem  44770  itgiccshift  44775  itgperiod  44776  itgsbtaddcnst  44777  dirkeritg  44897  dirkercncflem2  44899  dirkercncflem3  44900  dirkercncflem4  44901  dirkercncf  44902  fourierdlem16  44918  fourierdlem18  44920  fourierdlem21  44923  fourierdlem22  44924  fourierdlem39  44941  fourierdlem42  44944  fourierdlem48  44949  fourierdlem49  44950  fourierdlem53  44954  fourierdlem57  44958  fourierdlem58  44959  fourierdlem59  44960  fourierdlem60  44961  fourierdlem61  44962  fourierdlem62  44963  fourierdlem68  44969  fourierdlem70  44971  fourierdlem72  44973  fourierdlem73  44974  fourierdlem74  44975  fourierdlem75  44976  fourierdlem76  44977  fourierdlem78  44979  fourierdlem80  44981  fourierdlem83  44984  fourierdlem84  44985  fourierdlem85  44986  fourierdlem88  44989  fourierdlem89  44990  fourierdlem90  44991  fourierdlem91  44992  fourierdlem93  44994  fourierdlem94  44995  fourierdlem95  44996  fourierdlem96  44997  fourierdlem97  44998  fourierdlem98  44999  fourierdlem99  45000  fourierdlem101  45002  fourierdlem103  45004  fourierdlem104  45005  fourierdlem111  45012  fourierdlem112  45013  fourierdlem113  45014  fouriercnp  45021  sqwvfoura  45023  sqwvfourb  45024  fouriersw  45026  fouriercn  45027  etransclem2  45031  etransclem18  45047  etransclem23  45052  etransclem46  45075  rrxtopnfi  45082  rrndistlt  45085  sge0sn  45174  sge0tsms  45175  sge0f1o  45177  sge0pr  45189  sge0resplit  45201  sge0iunmptlemre  45210  sge0isummpt2  45227  hoicvr  45343  hoidmvlelem2  45391  refdivmptf  47306  refdivmptfv  47310  amgmlemALT  47928