Axiom ax-resscn 11228

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11170	. 2 class ℝ
2		cc 11169	. 2 class ℂ
3	1, 2	wss 3898	1 wff ℝ ⊆ ℂ

This axiom is used by:  recn  11261  reex  11262  recni  11294  qsscn  13056  ioosscn  13508  unitsscn  13600  reexpcl  14189  rpexpcl  14191  reexpclz  14193  expge0  14209  expge1  14210  rlimrecl  15714  abscn2  15733  recn2  15735  imcn2  15736  climabs  15738  climre  15740  climim  15741  rlimabs  15743  rlimre  15745  rlimim  15746  caurcvgr  15808  caucvgrlem2  15809  caurcvg  15811  fsumrecl  15867  fsumrpcl  15870  fsumge0  15929  fsumre  15942  fsumim  15943  fprodrecl  16087  fprodrpcl  16090  fprodreclf  16093  fprodge0  16127  fprodge1  16129  rerisefaccl  16151  refallfaccl  16152  rprisefaccl  16157  reeff1  16255  nthruc  16387  regsumfsum  21702  rge0srg  21705  rebase  21873  re0g  21879  regsumsupp  21889  remet  25070  tgioo2  25083  xrsdsre  25091  recld2  25095  reperf  25100  iitopon  25161  dfii3  25165  abscncf  25183  recncf  25184  imcncf  25185  abscncfALT  25206  cnmptre  25209  icchmeo  25223  cnrehmeo  25235  evth  25241  evth2  25242  lebnumlem2  25244  lebnumii  25248  cphsqrtcl  25466  resscdrg  25640  ishl2  25652  recms  25662  reust  25663  evthicc  25741  evthicc2  25742  ovolfsf  25753  volcn  25888  volivth  25889  ismbf  25910  cncombf  25940  cnmbf  25941  0plef  25954  itg1ge0  25968  i1faddlem  25975  i1fmul  25978  itg1addlem4  25981  i1fsub  25990  itg1sub  25991  mbfi1fseqlem5  26001  xrge0f  26013  itg20  26019  itg2const  26022  itg2mulc  26029  itg2addlem  26040  i1fibl  26089  itgitg1  26090  iblabslem  26109  iblabs  26110  bddmulibl  26120  recnprss  26185  dvmptresicc  26197  dvcjbr  26230  dvfre  26232  dvnfre  26233  dvferm1  26266  dvferm2  26268  rolle  26271  cmvth  26272  mvth  26273  dvlip  26274  dvlipcn  26275  dvlip2  26276  c1liplem1  26277  c1lip2  26279  dvgt0lem1  26283  dvle  26288  dvivthlem1  26289  dvivth  26291  dvne0  26292  lhop1lem  26294  lhop1  26295  lhop2  26296  lhop  26297  dvcnvrelem1  26298  dvcnvrelem2  26299  dvcnvre  26300  dvcvx  26301  dvfsumle  26302  dvfsumge  26303  dvfsumabs  26304  dvfsumlem2  26308  dvfsumrlim  26312  ftc1a  26318  ftc1lem3  26319  ftc1lem6  26322  ftc1  26323  ftc1cn  26324  ftc2  26325  ftc2ditglem  26326  itgparts  26328  itgsubstlem  26329  itgsubst  26330  itgpowd  26331  plyn0mulidp  26565  plymulidp  26566  aacjcl  26617  aalioulem3  26624  taylthlem2  26664  taylth  26665  abelth2  26732  reeff1olem  26736  efcvx  26739  pilem3  26743  pige3ALT  26811  recosf1o  26826  resinf1o  26827  dvrelog  26928  relogcn  26929  logcnlem5  26937  logcn  26938  dvloglem  26939  dvlog2lem  26943  logccv  26954  dvcxp1  27031  cxpcn3  27039  resqrtcn  27040  loglesqrt  27052  ssscongptld  27113  ressatans  27225  rlimcnp  27256  efrlim  27260  jensenlem1  27277  jensenlem2  27278  jensen  27279  amgm  27281  lgamgulmlem2  27320  ftalem3  27365  basellem9  27379  efnnfsumcl  27393  efchtdvds  27449  lgsdchr  27645  dchrvmasumlem1  27785  dchrisum0lem3  27809  pntlem3  27899  cchhllem  29397  ex-fpar  30996  ipasslem7  31371  fprodex01  33349  indsumin  33361  rexdiv  33425  fsumrp0cl  33515  xrge0slmod  33842  ccfldsrarelvec  34236  ccfldextdgrr  34237  rmulccn  34493  raddcn  34494  xrge0iifhom  34502  lmlimxrge0  34513  rezh  34534  esumpfinvallem  34639  esumpfinval  34640  esumpfinvalf  34641  esumcvg  34651  signsplypnf  35113  signsply0  35114  iblidicc  35155  rpsqrtcn  35156  ftc2re  35161  fdvposlt  35162  fdvneggt  35163  fdvposle  35164  fdvnegge  35165  itgexpif  35169  circlemeth  35203  circlemethnat  35204  circlevma  35205  circlemethhgt  35206  logdivsqrle  35213  resconn  35932  ivthALT  37045  dnicn  37280  knoppcnlem10  37290  knoppcnlem11  37291  unbdqndv2  37299  knoppndv  37322  knoppcn2  37324  broucube  38492  mblfinlem2  38496  mbfresfi  38504  ftc1cnnclem  38529  ftc1cnnc  38530  ftc1anclem3  38533  ftc1anclem5  38535  ftc1anclem7  38537  ftc1anclem8  38538  ftc1anc  38539  ftc2nc  38540  asindmre  38541  dvreasin  38544  dvreacos  38545  areacirclem1  38546  areacirclem2  38547  areacirclem3  38548  areacirclem4  38549  areacirc  38551  repwsmet  38688  rrnequiv  38689  rrntotbnd  38690  reheibor  38693  iccbnd  38694  intlewftc  43031  dvrelog2  43034  dvrelog3  43035  aks4d1p1p5  43045  rpsscn  43278  redvmptabs  43339  readvrec2  43340  resuppsinopn  43342  readvcot  43343  resubeqsub  43409  subresre  43410  arearect  44160  areaquad  44161  k0004val0  45098  extoimad  45108  imo72b2lem0  45109  imo72b2lem2  45111  imo72b2lem1  45113  imo72b2  45116  ssrecnpr  45236  sblpnf  45238  radcnvrat  45242  lhe4.4ex1a  45257  refsumcn  45968  rr2sscn2  46299  uzsscn  46407  evthiccabs  46430  climreeq  46547  limciccioolb  46555  limcrecl  46563  limcicciooub  46569  limcleqr  46576  lptioo2cn  46577  lptioo1cn  46578  limclner  46583  liminflimsupclim  46739  resincncf  46807  cncficcgt0  46820  cncfiooicclem1  46825  cncfiooiccre  46827  jumpncnp  46830  dvcosre  46844  dvmptconst  46847  dvmptidg  46849  fperdvper  46851  dvresioo  46853  dvmulcncf  46857  dvdivcncf  46859  dvbdfbdioolem1  46860  ioodvbdlimc1lem1  46863  ioodvbdlimc1lem2  46864  ioodvbdlimc1  46865  ioodvbdlimc2lem  46866  ioodvbdlimc2  46867  itgsin0pilem1  46882  ibliccsinexp  46883  iblioosinexp  46885  itgsinexplem1  46886  itgsinexp  46887  itgcoscmulx  46901  itgsincmulx  46906  itgsubsticclem  46907  itgiccshift  46912  itgperiod  46913  itgsbtaddcnst  46914  dirkeritg  47034  dirkercncflem2  47036  dirkercncflem3  47037  dirkercncflem4  47038  dirkercncf  47039  fourierdlem16  47055  fourierdlem18  47057  fourierdlem21  47060  fourierdlem22  47061  fourierdlem39  47078  fourierdlem42  47081  fourierdlem48  47086  fourierdlem49  47087  fourierdlem53  47091  fourierdlem57  47095  fourierdlem58  47096  fourierdlem59  47097  fourierdlem60  47098  fourierdlem61  47099  fourierdlem62  47100  fourierdlem68  47106  fourierdlem70  47108  fourierdlem72  47110  fourierdlem73  47111  fourierdlem74  47112  fourierdlem75  47113  fourierdlem76  47114  fourierdlem78  47116  fourierdlem80  47118  fourierdlem83  47121  fourierdlem84  47122  fourierdlem85  47123  fourierdlem88  47126  fourierdlem89  47127  fourierdlem90  47128  fourierdlem91  47129  fourierdlem93  47131  fourierdlem94  47132  fourierdlem95  47133  fourierdlem96  47134  fourierdlem97  47135  fourierdlem98  47136  fourierdlem99  47137  fourierdlem101  47139  fourierdlem103  47141  fourierdlem104  47142  fourierdlem111  47149  fourierdlem112  47150  fourierdlem113  47151  fouriercnp  47158  sqwvfoura  47160  sqwvfourb  47161  fouriersw  47163  fouriercn  47164  etransclem2  47168  etransclem18  47184  etransclem23  47189  etransclem46  47212  rrxtopnfi  47219  rrndistlt  47222  sge0sn  47311  sge0tsms  47312  sge0f1o  47314  sge0pr  47326  sge0resplit  47338  sge0iunmptlemre  47347  sge0isummpt2  47364  hoicvr  47480  hoidmvlelem2  47528  lamberte  47860  refdivmptf  49576  refdivmptfv  49580  amgmlemALT  50910