Axiom ax-resscn 11281

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11223	. 2 class ℝ
2		cc 11222	. 2 class ℂ
3	1, 2	wss 3900	1 wff ℝ ⊆ ℂ

This axiom is used by:  recn  11314  reex  11315  recni  11347  qsscn  13111  ioosscn  13563  unitsscn  13655  reexpcl  14245  rpexpcl  14247  reexpclz  14249  expge0  14265  expge1  14266  rlimrecl  15773  abscn2  15792  recn2  15794  imcn2  15795  climabs  15797  climre  15799  climim  15800  rlimabs  15802  rlimre  15804  rlimim  15805  caurcvgr  15867  caucvgrlem2  15868  caurcvg  15870  fsumrecl  15926  fsumrpcl  15929  fsumge0  15988  fsumre  16001  fsumim  16002  fprodrecl  16146  fprodrpcl  16149  fprodreclf  16152  fprodge0  16186  fprodge1  16188  rerisefaccl  16210  refallfaccl  16211  rprisefaccl  16216  reeff1  16314  nthruc  16446  regsumfsum  21768  rge0srg  21771  rebase  21939  re0g  21945  regsumsupp  21955  remet  25136  tgioo2  25149  xrsdsre  25157  recld2  25161  reperf  25166  abscncf  25249  recncf  25250  imcncf  25251  abscncfALT  25272  cnmptre  25275  icchmeo  25289  cnrehmeo  25301  evth  25307  evth2  25308  lebnumlem2  25310  lebnumii  25314  cphsqrtcl  25532  resscdrg  25706  ishl2  25718  recms  25728  reust  25729  evthicc  25807  evthicc2  25808  ovolfsf  25819  volcn  25954  volivth  25955  ismbf  25976  cncombf  26006  cnmbf  26007  0plef  26020  itg1ge0  26034  i1faddlem  26041  i1fmul  26044  itg1addlem4  26047  i1fsub  26056  itg1sub  26057  mbfi1fseqlem5  26067  xrge0f  26079  itg20  26085  itg2const  26088  itg2mulc  26095  itg2addlem  26106  i1fibl  26155  itgitg1  26156  iblabslem  26175  iblabs  26176  bddmulibl  26186  recnprss  26251  dvmptresicc  26263  dvcjbr  26296  dvfre  26298  dvnfre  26299  dvferm1  26332  dvferm2  26334  rolle  26337  cmvth  26338  mvth  26339  dvlip  26340  dvlipcn  26341  dvlip2  26342  c1liplem1  26343  c1lip2  26345  dvgt0lem1  26349  dvle  26354  dvivthlem1  26355  dvivth  26357  dvne0  26358  lhop1lem  26360  lhop1  26361  lhop2  26362  lhop  26363  dvcnvrelem1  26364  dvcnvrelem2  26365  dvcnvre  26366  dvcvx  26367  dvfsumle  26368  dvfsumge  26369  dvfsumabs  26370  dvfsumlem2  26374  dvfsumrlim  26378  ftc1a  26384  ftc1lem3  26385  ftc1lem6  26388  ftc1  26389  ftc1cn  26390  ftc2  26391  ftc2ditglem  26392  itgparts  26394  itgsubstlem  26395  itgsubst  26396  itgpowd  26397  plyn0mulidp  26629  plymulidp  26630  aacjcl  26681  aalioulem3  26688  taylthlem2  26728  taylth  26729  abelth2  26796  reeff1olem  26800  efcvx  26803  pilem3  26807  pige3ALT  26875  recosf1o  26890  resinf1o  26891  dvrelog  26992  relogcn  26993  logcnlem5  27001  logcn  27002  dvloglem  27003  dvlog2lem  27007  logccv  27018  dvcxp1  27095  cxpcn3  27103  resqrtcn  27104  loglesqrt  27116  ssscongptld  27177  ressatans  27289  rlimcnp  27320  efrlim  27324  jensenlem1  27341  jensenlem2  27342  jensen  27343  amgm  27345  lgamgulmlem2  27384  ftalem3  27429  basellem9  27443  efnnfsumcl  27457  efchtdvds  27513  lgsdchr  27709  dchrvmasumlem1  27849  dchrisum0lem3  27873  pntlem3  27963  cchhllem  29491  ex-fpar  31090  ipasslem7  31465  fprodex01  33483  indsumin  33495  rexdiv  33559  fsumrp0cl  33649  xrge0slmod  33976  ccfldsrarelvec  34370  ccfldextdgrr  34371  rmulccn  34627  raddcn  34628  xrge0iifhom  34636  lmlimxrge0  34647  rezh  34668  esumpfinvallem  34773  esumpfinval  34774  esumpfinvalf  34775  esumcvg  34785  signsplypnf  35246  signsply0  35247  iblidicc  35288  rpsqrtcn  35289  ftc2re  35294  fdvposlt  35295  fdvneggt  35296  fdvposle  35297  fdvnegge  35298  itgexpif  35302  circlemeth  35336  circlemethnat  35337  circlevma  35338  circlemethhgt  35339  logdivsqrle  35346  resconn  36177  ivthALT  37300  dnicn  37535  knoppcnlem10  37545  knoppcnlem11  37546  unbdqndv2  37554  knoppndv  37577  knoppcn2  37579  broucube  38763  mblfinlem2  38767  mbfresfi  38775  ftc1cnnclem  38800  ftc1cnnc  38801  ftc1anclem3  38804  ftc1anclem5  38806  ftc1anclem7  38808  ftc1anclem8  38809  ftc1anc  38810  ftc2nc  38811  asindmre  38812  dvreasin  38815  dvreacos  38816  areacirclem1  38817  areacirclem2  38818  areacirclem3  38819  areacirclem4  38820  areacirc  38822  repwsmet  38959  rrnequiv  38960  rrntotbnd  38961  reheibor  38964  iccbnd  38965  intlewftc  43302  dvrelog2  43305  dvrelog3  43306  aks4d1p1p5  43316  rpsscn  43547  redvmptabs  43602  readvrec2  43603  resuppsinopn  43605  readvcot  43606  resubeqsub  43672  subresre  43673  arearect  44407  areaquad  44408  extoimad  45354  imo72b2lem0  45355  imo72b2lem2  45357  imo72b2lem1  45359  imo72b2  45362  ssrecnpr  45482  sblpnf  45484  radcnvrat  45488  lhe4.4ex1a  45503  refsumcn  46250  rr2sscn2  46580  uzsscn  46688  evthiccabs  46711  climreeq  46828  limciccioolb  46836  limcrecl  46844  limcicciooub  46850  limcleqr  46857  lptioo2cn  46858  lptioo1cn  46859  limclner  46864  liminflimsupclim  47020  resincncf  47088  cncficcgt0  47101  cncfiooicclem1  47106  cncfiooiccre  47108  jumpncnp  47111  dvcosre  47125  dvmptconst  47128  dvmptidg  47130  fperdvper  47132  dvresioo  47134  dvmulcncf  47138  dvdivcncf  47140  dvbdfbdioolem1  47141  ioodvbdlimc1lem1  47144  ioodvbdlimc1lem2  47145  ioodvbdlimc1  47146  ioodvbdlimc2lem  47147  ioodvbdlimc2  47148  itgsin0pilem1  47163  ibliccsinexp  47164  iblioosinexp  47166  itgsinexplem1  47167  itgsinexp  47168  itgcoscmulx  47182  itgsincmulx  47187  itgsubsticclem  47188  itgiccshift  47193  itgperiod  47194  itgsbtaddcnst  47195  dirkeritg  47315  dirkercncflem2  47317  dirkercncflem3  47318  dirkercncflem4  47319  dirkercncf  47320  fourierdlem16  47336  fourierdlem18  47338  fourierdlem21  47341  fourierdlem22  47342  fourierdlem39  47359  fourierdlem42  47362  fourierdlem48  47367  fourierdlem49  47368  fourierdlem53  47372  fourierdlem57  47376  fourierdlem58  47377  fourierdlem59  47378  fourierdlem60  47379  fourierdlem61  47380  fourierdlem62  47381  fourierdlem68  47387  fourierdlem70  47389  fourierdlem72  47391  fourierdlem73  47392  fourierdlem74  47393  fourierdlem75  47394  fourierdlem76  47395  fourierdlem78  47397  fourierdlem80  47399  fourierdlem83  47402  fourierdlem84  47403  fourierdlem85  47404  fourierdlem88  47407  fourierdlem89  47408  fourierdlem90  47409  fourierdlem91  47410  fourierdlem93  47412  fourierdlem94  47413  fourierdlem95  47414  fourierdlem96  47415  fourierdlem97  47416  fourierdlem98  47417  fourierdlem99  47418  fourierdlem101  47420  fourierdlem103  47422  fourierdlem104  47423  fourierdlem111  47430  fourierdlem112  47431  fourierdlem113  47432  fouriercnp  47439  sqwvfoura  47441  sqwvfourb  47442  fouriersw  47444  fouriercn  47445  etransclem2  47449  etransclem18  47465  etransclem23  47470  etransclem46  47493  rrxtopnfi  47500  rrndistlt  47503  sge0sn  47592  sge0tsms  47593  sge0f1o  47595  sge0pr  47607  sge0resplit  47619  sge0iunmptlemre  47628  sge0isummpt2  47645  hoicvr  47761  hoidmvlelem2  47809  lamberte  48141  refdivmptf  49857  refdivmptfv  49861  amgmlemALT  51266