Axiom ax-resscn 9993

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 9935	. 2 class ℝ
2		cc 9934	. 2 class ℂ
3	1, 2	wss 3574	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  10026  reex  10027  recni  10052  nnsscn  11025  nn0sscn  11297  qsscn  11799  reexpcl  12877  rpexpcl  12879  reexpclz  12880  expge0  12896  expge1  12897  rlimrecl  14311  abscn2  14329  recn2  14331  imcn2  14332  climabs  14334  climre  14336  climim  14337  rlimabs  14339  rlimre  14341  rlimim  14342  caurcvgr  14404  caucvgrlem2  14405  caurcvg  14407  fsumrecl  14465  fsumrpcl  14468  fsumge0  14527  fsumre  14540  fsumim  14541  fprodrecl  14683  fprodrpcl  14686  fprodreclf  14689  fprodge0  14724  fprodge1  14726  rerisefaccl  14748  refallfaccl  14749  rprisefaccl  14754  reeff1  14850  nthruc  14981  regsumfsum  19814  rge0srg  19817  rebase  19952  re0g  19958  regsumsupp  19968  remet  22593  tgioo2  22606  xrsdsre  22613  recld2  22617  reperf  22622  iitopon  22682  dfii3  22686  abscncf  22704  recncf  22705  imcncf  22706  abscncfALT  22723  cnmptre  22726  iimulcn  22737  icchmeo  22740  cnrehmeo  22752  evth  22758  evth2  22759  lebnumlem2  22761  lebnumii  22765  reparphti  22797  cphsqrtcl  22984  resscdrg  23154  ishl2  23166  recms  23168  reust  23169  evthicc  23228  evthicc2  23229  ovolfsf  23240  volcn  23374  volivth  23375  ismbf  23397  cncombf  23425  cnmbf  23426  0plef  23439  itg1ge0  23453  i1faddlem  23460  i1fmul  23463  itg1addlem4  23466  i1fsub  23475  itg1sub  23476  mbfi1fseqlem5  23486  xrge0f  23498  itg20  23504  itg2const  23507  itg2mulc  23514  itg2addlem  23525  i1fibl  23574  itgitg1  23575  iblabslem  23594  iblabs  23595  bddmulibl  23605  recnprss  23668  dvcjbr  23712  dvfre  23714  dvnfre  23715  dvferm1  23748  dvferm2  23750  rolle  23753  cmvth  23754  mvth  23755  dvlip  23756  dvlipcn  23757  dvlip2  23758  c1liplem1  23759  c1lip2  23761  dvgt0lem1  23765  dvle  23770  dvivthlem1  23771  dvivth  23773  dvne0  23774  lhop1lem  23776  lhop1  23777  lhop2  23778  lhop  23779  dvcnvrelem1  23780  dvcnvrelem2  23781  dvcnvre  23782  dvcvx  23783  dvfsumle  23784  dvfsumge  23785  dvfsumabs  23786  dvfsumlem2  23790  dvfsumrlim  23794  ftc1a  23800  ftc1lem3  23801  ftc1lem6  23804  ftc1  23805  ftc1cn  23806  ftc2  23807  ftc2ditglem  23808  itgparts  23810  itgsubstlem  23811  itgsubst  23812  aacjcl  24082  aalioulem3  24089  taylthlem2  24128  taylth  24129  abelth2  24196  reeff1olem  24200  efcvx  24203  pilem3  24207  pige3  24269  recosf1o  24281  resinf1o  24282  dvrelog  24383  relogcn  24384  logcnlem5  24392  logcn  24393  dvloglem  24394  dvlog2lem  24398  logccv  24409  dvcxp1  24481  cxpcn3  24489  resqrtcn  24490  loglesqrt  24499  ssscongptld  24552  ressatans  24661  rlimcnp  24692  efrlim  24696  jensenlem1  24713  jensenlem2  24714  jensen  24715  amgm  24717  lgamgulmlem2  24756  ftalem3  24801  basellem9  24815  efnnfsumcl  24829  efchtdvds  24885  lgsdchr  25080  dchrvmasumlem1  25184  dchrisum0lem3  25208  pntlem3  25298  cchhllem  25767  ipasslem7  27691  fprodex01  29571  rexdiv  29634  fsumrp0cl  29695  xrge0slmod  29844  unitsscn  29942  rmulccn  29974  raddcn  29975  xrge0iifhom  29983  lmlimxrge0  29994  rezh  30015  indsumin  30084  esumpfinvallem  30136  esumpfinval  30137  esumpfinvalf  30138  esumcvg  30148  plymulx0  30624  plymulx  30625  signsplypnf  30627  signsply0  30628  iblidicc  30670  rpsqrtcn  30671  ftc2re  30676  fdvposlt  30677  fdvneggt  30678  fdvposle  30679  fdvnegge  30680  itgexpif  30684  circlemeth  30718  circlemethnat  30719  circlevma  30720  circlemethhgt  30721  logdivsqrle  30728  cvxpconn  31224  cvxsconn  31225  resconn  31228  ivthALT  32330  dnicn  32482  knoppcnlem10  32492  knoppcnlem11  32493  unbdqndv2  32502  knoppndv  32525  knoppcn2  32527  broucube  33443  mblfinlem2  33447  mbfresfi  33456  ftc1cnnclem  33483  ftc1cnnc  33484  ftc1anclem3  33487  ftc1anclem5  33489  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  ftc2nc  33494  asindmre  33495  dvreasin  33498  dvreacos  33499  areacirclem1  33500  areacirclem2  33501  areacirclem3  33502  areacirclem4  33503  areacirc  33505  repwsmet  33633  rrnequiv  33634  rrntotbnd  33635  reheibor  33638  iccbnd  33639  itgpowd  37800  arearect  37801  areaquad  37802  k0004val0  38452  extoimad  38464  imo72b2lem0  38465  imo72b2lem2  38467  imo72b2lem1  38471  imo72b2  38475  ssrecnpr  38507  sblpnf  38509  radcnvrat  38513  lhe4.4ex1a  38528  refsumcn  39189  rr2sscn2  39582  uzsscn  39706  ioosscn  39716  evthiccabs  39718  climreeq  39845  limciccioolb  39853  limcrecl  39861  limcicciooub  39869  limcleqr  39876  lptioo2cn  39877  lptioo1cn  39878  limclner  39883  liminflimsupclim  40039  resincncf  40088  cncficcgt0  40101  cncfiooicclem1  40106  cncfiooiccre  40108  jumpncnp  40111  dvcosre  40126  dvmptconst  40129  dvmptidg  40131  fperdvper  40133  dvmptresicc  40134  dvresioo  40136  dvmulcncf  40140  dvdivcncf  40142  dvbdfbdioolem1  40143  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc1  40148  ioodvbdlimc2lem  40149  ioodvbdlimc2  40150  itgsin0pilem1  40165  ibliccsinexp  40166  iblioosinexp  40168  itgsinexplem1  40169  itgsinexp  40170  itgcoscmulx  40185  itgsincmulx  40190  itgsubsticclem  40191  itgiccshift  40196  itgperiod  40197  itgsbtaddcnst  40198  dirkeritg  40319  dirkercncflem2  40321  dirkercncflem3  40322  dirkercncflem4  40323  dirkercncf  40324  fourierdlem16  40340  fourierdlem18  40342  fourierdlem21  40345  fourierdlem22  40346  fourierdlem39  40363  fourierdlem42  40366  fourierdlem48  40371  fourierdlem49  40372  fourierdlem53  40376  fourierdlem57  40380  fourierdlem58  40381  fourierdlem59  40382  fourierdlem60  40383  fourierdlem61  40384  fourierdlem62  40385  fourierdlem68  40391  fourierdlem70  40393  fourierdlem72  40395  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem78  40401  fourierdlem80  40403  fourierdlem83  40406  fourierdlem84  40407  fourierdlem85  40408  fourierdlem88  40411  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem93  40416  fourierdlem94  40417  fourierdlem95  40418  fourierdlem96  40419  fourierdlem97  40420  fourierdlem98  40421  fourierdlem99  40422  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem112  40435  fourierdlem113  40436  fouriercnp  40443  sqwvfoura  40445  sqwvfourb  40446  fouriersw  40448  fouriercn  40449  etransclem2  40453  etransclem18  40469  etransclem23  40474  etransclem46  40497  rrxtopnfi  40506  rrndistlt  40510  sge0sn  40596  sge0tsms  40597  sge0f1o  40599  sge0pr  40611  sge0resplit  40623  sge0iunmptlemre  40632  sge0isummpt2  40649  hoicvr  40762  hoidmvlelem2  40810  refdivmptf  42336  refdivmptfv  42340  amgmlemALT  42549