Axiom ax-resscn 10594

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 10536	. 2 class ℝ
2		cc 10535	. 2 class ℂ
3	1, 2	wss 3936	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  10627  reex  10628  recni  10655  qsscn  12360  reexpcl  13447  rpexpcl  13449  reexpclz  13450  expge0  13466  expge1  13467  rlimrecl  14937  abscn2  14955  recn2  14957  imcn2  14958  climabs  14960  climre  14962  climim  14963  rlimabs  14965  rlimre  14967  rlimim  14968  caurcvgr  15030  caucvgrlem2  15031  caurcvg  15033  fsumrecl  15091  fsumrpcl  15094  fsumge0  15150  fsumre  15163  fsumim  15164  fprodrecl  15307  fprodrpcl  15310  fprodreclf  15313  fprodge0  15347  fprodge1  15349  rerisefaccl  15371  refallfaccl  15372  rprisefaccl  15377  reeff1  15473  nthruc  15605  regsumfsum  20613  rge0srg  20616  rebase  20750  re0g  20756  regsumsupp  20766  remet  23398  tgioo2  23411  xrsdsre  23418  recld2  23422  reperf  23427  iitopon  23487  dfii3  23491  abscncf  23509  recncf  23510  imcncf  23511  abscncfALT  23528  cnmptre  23531  iimulcn  23542  icchmeo  23545  cnrehmeo  23557  evth  23563  evth2  23564  lebnumlem2  23566  lebnumii  23570  reparphti  23601  cphsqrtcl  23788  resscdrg  23961  ishl2  23973  recms  23983  reust  23984  evthicc  24060  evthicc2  24061  ovolfsf  24072  volcn  24207  volivth  24208  ismbf  24229  cncombf  24259  cnmbf  24260  0plef  24273  itg1ge0  24287  i1faddlem  24294  i1fmul  24297  itg1addlem4  24300  i1fsub  24309  itg1sub  24310  mbfi1fseqlem5  24320  xrge0f  24332  itg20  24338  itg2const  24341  itg2mulc  24348  itg2addlem  24359  i1fibl  24408  itgitg1  24409  iblabslem  24428  iblabs  24429  bddmulibl  24439  recnprss  24502  dvcjbr  24546  dvfre  24548  dvnfre  24549  dvferm1  24582  dvferm2  24584  rolle  24587  cmvth  24588  mvth  24589  dvlip  24590  dvlipcn  24591  dvlip2  24592  c1liplem1  24593  c1lip2  24595  dvgt0lem1  24599  dvle  24604  dvivthlem1  24605  dvivth  24607  dvne0  24608  lhop1lem  24610  lhop1  24611  lhop2  24612  lhop  24613  dvcnvrelem1  24614  dvcnvrelem2  24615  dvcnvre  24616  dvcvx  24617  dvfsumle  24618  dvfsumge  24619  dvfsumabs  24620  dvfsumlem2  24624  dvfsumrlim  24628  ftc1a  24634  ftc1lem3  24635  ftc1lem6  24638  ftc1  24639  ftc1cn  24640  ftc2  24641  ftc2ditglem  24642  itgparts  24644  itgsubstlem  24645  itgsubst  24646  aacjcl  24916  aalioulem3  24923  taylthlem2  24962  taylth  24963  abelth2  25030  reeff1olem  25034  efcvx  25037  pilem3  25041  pige3ALT  25105  recosf1o  25119  resinf1o  25120  dvrelog  25220  relogcn  25221  logcnlem5  25229  logcn  25230  dvloglem  25231  dvlog2lem  25235  logccv  25246  dvcxp1  25321  cxpcn3  25329  resqrtcn  25330  loglesqrt  25339  ssscongptld  25400  ressatans  25512  rlimcnp  25543  efrlim  25547  jensenlem1  25564  jensenlem2  25565  jensen  25566  amgm  25568  lgamgulmlem2  25607  ftalem3  25652  basellem9  25666  efnnfsumcl  25680  efchtdvds  25736  lgsdchr  25931  dchrvmasumlem1  26071  dchrisum0lem3  26095  pntlem3  26185  cchhllem  26673  ex-fpar  28241  ipasslem7  28613  fprodex01  30541  rexdiv  30602  fsumrp0cl  30682  xrge0slmod  30917  ccfldsrarelvec  31056  ccfldextdgrr  31057  unitsscn  31139  rmulccn  31171  raddcn  31172  xrge0iifhom  31180  lmlimxrge0  31191  rezh  31212  indsumin  31281  esumpfinvallem  31333  esumpfinval  31334  esumpfinvalf  31335  esumcvg  31345  plymulx0  31817  plymulx  31818  signsplypnf  31820  signsply0  31821  iblidicc  31863  rpsqrtcn  31864  ftc2re  31869  fdvposlt  31870  fdvneggt  31871  fdvposle  31872  fdvnegge  31873  itgexpif  31877  circlemeth  31911  circlemethnat  31912  circlevma  31913  circlemethhgt  31914  logdivsqrle  31921  cvxpconn  32489  cvxsconn  32490  resconn  32493  ivthALT  33683  dnicn  33831  knoppcnlem10  33841  knoppcnlem11  33842  unbdqndv2  33850  knoppndv  33873  knoppcn2  33875  broucube  34941  mblfinlem2  34945  mbfresfi  34953  ftc1cnnclem  34980  ftc1cnnc  34981  ftc1anclem3  34984  ftc1anclem5  34986  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  ftc2nc  34991  asindmre  34992  dvreasin  34995  dvreacos  34996  areacirclem1  34997  areacirclem2  34998  areacirclem3  34999  areacirclem4  35000  areacirc  35002  repwsmet  35127  rrnequiv  35128  rrntotbnd  35129  reheibor  35132  iccbnd  35133  itgpowd  39870  arearect  39871  areaquad  39872  k0004val0  40553  extoimad  40564  imo72b2lem0  40565  imo72b2lem2  40567  imo72b2lem1  40570  imo72b2  40574  ssrecnpr  40689  sblpnf  40691  radcnvrat  40695  lhe4.4ex1a  40710  refsumcn  41336  rr2sscn2  41683  uzsscn  41801  ioosscn  41818  evthiccabs  41820  climreeq  41943  limciccioolb  41951  limcrecl  41959  limcicciooub  41967  limcleqr  41974  lptioo2cn  41975  lptioo1cn  41976  limclner  41981  liminflimsupclim  42137  resincncf  42207  cncficcgt0  42220  cncfiooicclem1  42225  cncfiooiccre  42227  jumpncnp  42230  dvcosre  42245  dvmptconst  42248  dvmptidg  42250  fperdvper  42252  dvmptresicc  42253  dvresioo  42255  dvmulcncf  42259  dvdivcncf  42261  dvbdfbdioolem1  42262  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc1  42267  ioodvbdlimc2lem  42268  ioodvbdlimc2  42269  itgsin0pilem1  42284  ibliccsinexp  42285  iblioosinexp  42287  itgsinexplem1  42288  itgsinexp  42289  itgcoscmulx  42303  itgsincmulx  42308  itgsubsticclem  42309  itgiccshift  42314  itgperiod  42315  itgsbtaddcnst  42316  dirkeritg  42436  dirkercncflem2  42438  dirkercncflem3  42439  dirkercncflem4  42440  dirkercncf  42441  fourierdlem16  42457  fourierdlem18  42459  fourierdlem21  42462  fourierdlem22  42463  fourierdlem39  42480  fourierdlem42  42483  fourierdlem48  42488  fourierdlem49  42489  fourierdlem53  42493  fourierdlem57  42497  fourierdlem58  42498  fourierdlem59  42499  fourierdlem60  42500  fourierdlem61  42501  fourierdlem62  42502  fourierdlem68  42508  fourierdlem70  42510  fourierdlem72  42512  fourierdlem73  42513  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem78  42518  fourierdlem80  42520  fourierdlem83  42523  fourierdlem84  42524  fourierdlem85  42525  fourierdlem88  42528  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fourierdlem93  42533  fourierdlem94  42534  fourierdlem95  42535  fourierdlem96  42536  fourierdlem97  42537  fourierdlem98  42538  fourierdlem99  42539  fourierdlem101  42541  fourierdlem103  42543  fourierdlem104  42544  fourierdlem111  42551  fourierdlem112  42552  fourierdlem113  42553  fouriercnp  42560  sqwvfoura  42562  sqwvfourb  42563  fouriersw  42565  fouriercn  42566  etransclem2  42570  etransclem18  42586  etransclem23  42591  etransclem46  42614  rrxtopnfi  42621  rrndistlt  42624  sge0sn  42710  sge0tsms  42711  sge0f1o  42713  sge0pr  42725  sge0resplit  42737  sge0iunmptlemre  42746  sge0isummpt2  42763  hoicvr  42879  hoidmvlelem2  42927  refdivmptf  44651  refdivmptfv  44655  amgmlemALT  44953