Axiom ax-resscn 11091

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11033	. 2 class ℝ
2		cc 11032	. 2 class ℂ
3	1, 2	wss 3884	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11124  reex  11125  recni  11155  qsscn  12905  ioosscn  13356  unitsscn  13448  reexpcl  14035  rpexpcl  14037  reexpclz  14039  expge0  14055  expge1  14056  rlimrecl  15537  abscn2  15556  recn2  15558  imcn2  15559  climabs  15561  climre  15563  climim  15564  rlimabs  15566  rlimre  15568  rlimim  15569  caurcvgr  15631  caucvgrlem2  15632  caurcvg  15634  fsumrecl  15691  fsumrpcl  15694  fsumge0  15753  fsumre  15766  fsumim  15767  fprodrecl  15913  fprodrpcl  15916  fprodreclf  15919  fprodge0  15953  fprodge1  15955  rerisefaccl  15977  refallfaccl  15978  rprisefaccl  15983  reeff1  16082  nthruc  16214  regsumfsum  21413  rge0srg  21416  rebase  21584  re0g  21590  regsumsupp  21600  remet  24776  tgioo2  24789  xrsdsre  24797  recld2  24801  reperf  24806  iitopon  24867  dfii3  24871  abscncf  24889  recncf  24890  imcncf  24891  abscncfALT  24912  cnmptre  24915  icchmeo  24929  cnrehmeo  24941  evth  24947  evth2  24948  lebnumlem2  24950  lebnumii  24954  cphsqrtcl  25172  resscdrg  25346  ishl2  25358  recms  25368  reust  25369  evthicc  25447  evthicc2  25448  ovolfsf  25459  volcn  25594  volivth  25595  ismbf  25616  cncombf  25646  cnmbf  25647  0plef  25660  itg1ge0  25674  i1faddlem  25681  i1fmul  25684  itg1addlem4  25687  i1fsub  25696  itg1sub  25697  mbfi1fseqlem5  25707  xrge0f  25719  itg20  25725  itg2const  25728  itg2mulc  25735  itg2addlem  25746  i1fibl  25796  itgitg1  25797  iblabslem  25816  iblabs  25817  bddmulibl  25827  recnprss  25892  dvmptresicc  25904  dvcjbr  25937  dvfre  25939  dvnfre  25940  dvferm1  25973  dvferm2  25975  rolle  25978  cmvth  25979  mvth  25980  dvlip  25981  dvlipcn  25982  dvlip2  25983  c1liplem1  25984  c1lip2  25986  dvgt0lem1  25990  dvle  25995  dvivthlem1  25996  dvivth  25998  dvne0  25999  lhop1lem  26001  lhop1  26002  lhop2  26003  lhop  26004  dvcnvrelem1  26005  dvcnvrelem2  26006  dvcnvre  26007  dvcvx  26008  dvfsumle  26009  dvfsumge  26010  dvfsumabs  26011  dvfsumlem2  26015  dvfsumrlim  26019  ftc1a  26025  ftc1lem3  26026  ftc1lem6  26029  ftc1  26030  ftc1cn  26031  ftc2  26032  ftc2ditglem  26033  itgparts  26035  itgsubstlem  26036  itgsubst  26037  itgpowd  26038  aacjcl  26314  aalioulem3  26321  taylthlem2  26360  taylth  26361  abelth2  26428  reeff1olem  26432  efcvx  26435  pilem3  26439  pige3ALT  26505  recosf1o  26520  resinf1o  26521  dvrelog  26622  relogcn  26623  logcnlem5  26631  logcn  26632  dvloglem  26633  dvlog2lem  26637  logccv  26648  dvcxp1  26725  cxpcn3  26733  resqrtcn  26734  loglesqrt  26746  ssscongptld  26807  ressatans  26919  rlimcnp  26950  efrlim  26954  jensenlem1  26971  jensenlem2  26972  jensen  26973  amgm  26975  lgamgulmlem2  27014  ftalem3  27059  basellem9  27073  efnnfsumcl  27087  efchtdvds  27143  lgsdchr  27339  dchrvmasumlem1  27479  dchrisum0lem3  27503  pntlem3  27593  cchhllem  28975  ex-fpar  30552  ipasslem7  30927  fprodex01  32919  indsumin  32942  rexdiv  33006  fsumrp0cl  33102  xrge0slmod  33433  ccfldsrarelvec  33865  ccfldextdgrr  33866  rmulccn  34122  raddcn  34123  xrge0iifhom  34131  lmlimxrge0  34142  rezh  34163  esumpfinvallem  34268  esumpfinval  34269  esumpfinvalf  34270  esumcvg  34280  plymulx0  34741  plymulx  34742  signsplypnf  34744  signsply0  34745  iblidicc  34786  rpsqrtcn  34787  ftc2re  34792  fdvposlt  34793  fdvneggt  34794  fdvposle  34795  fdvnegge  34796  itgexpif  34800  circlemeth  34834  circlemethnat  34835  circlevma  34836  circlemethhgt  34837  logdivsqrle  34844  resconn  35487  ivthALT  36576  dnicn  36811  knoppcnlem10  36821  knoppcnlem11  36822  unbdqndv2  36830  knoppndv  36853  knoppcn2  36855  broucube  38034  mblfinlem2  38038  mbfresfi  38046  ftc1cnnclem  38071  ftc1cnnc  38072  ftc1anclem3  38075  ftc1anclem5  38077  ftc1anclem7  38079  ftc1anclem8  38080  ftc1anc  38081  ftc2nc  38082  asindmre  38083  dvreasin  38086  dvreacos  38087  areacirclem1  38088  areacirclem2  38089  areacirclem3  38090  areacirclem4  38091  areacirc  38093  repwsmet  38214  rrnequiv  38215  rrntotbnd  38216  reheibor  38219  iccbnd  38220  intlewftc  42559  dvrelog2  42562  dvrelog3  42563  aks4d1p1p5  42573  rpsscn  42789  redvmptabs  42850  readvrec2  42851  resuppsinopn  42853  readvcot  42854  resubeqsub  42920  subresre  42921  arearect  43673  areaquad  43674  k0004val0  44611  extoimad  44621  imo72b2lem0  44622  imo72b2lem2  44624  imo72b2lem1  44626  imo72b2  44629  ssrecnpr  44765  sblpnf  44767  radcnvrat  44771  lhe4.4ex1a  44786  refsumcn  45491  rr2sscn2  45822  uzsscn  45930  evthiccabs  45953  climreeq  46070  limciccioolb  46078  limcrecl  46086  limcicciooub  46092  limcleqr  46099  lptioo2cn  46100  lptioo1cn  46101  limclner  46106  liminflimsupclim  46262  resincncf  46330  cncficcgt0  46343  cncfiooicclem1  46348  cncfiooiccre  46350  jumpncnp  46353  dvcosre  46367  dvmptconst  46370  dvmptidg  46372  fperdvper  46374  dvresioo  46376  dvmulcncf  46380  dvdivcncf  46382  dvbdfbdioolem1  46383  ioodvbdlimc1lem1  46386  ioodvbdlimc1lem2  46387  ioodvbdlimc1  46388  ioodvbdlimc2lem  46389  ioodvbdlimc2  46390  itgsin0pilem1  46405  ibliccsinexp  46406  iblioosinexp  46408  itgsinexplem1  46409  itgsinexp  46410  itgcoscmulx  46424  itgsincmulx  46429  itgsubsticclem  46430  itgiccshift  46435  itgperiod  46436  itgsbtaddcnst  46437  dirkeritg  46557  dirkercncflem2  46559  dirkercncflem3  46560  dirkercncflem4  46561  dirkercncf  46562  fourierdlem16  46578  fourierdlem18  46580  fourierdlem21  46583  fourierdlem22  46584  fourierdlem39  46601  fourierdlem42  46604  fourierdlem48  46609  fourierdlem49  46610  fourierdlem53  46614  fourierdlem57  46618  fourierdlem58  46619  fourierdlem59  46620  fourierdlem60  46621  fourierdlem61  46622  fourierdlem62  46623  fourierdlem68  46629  fourierdlem70  46631  fourierdlem72  46633  fourierdlem73  46634  fourierdlem74  46635  fourierdlem75  46636  fourierdlem76  46637  fourierdlem78  46639  fourierdlem80  46641  fourierdlem83  46644  fourierdlem84  46645  fourierdlem85  46646  fourierdlem88  46649  fourierdlem89  46650  fourierdlem90  46651  fourierdlem91  46652  fourierdlem93  46654  fourierdlem94  46655  fourierdlem95  46656  fourierdlem96  46657  fourierdlem97  46658  fourierdlem98  46659  fourierdlem99  46660  fourierdlem101  46662  fourierdlem103  46664  fourierdlem104  46665  fourierdlem111  46672  fourierdlem112  46673  fourierdlem113  46674  fouriercnp  46681  sqwvfoura  46683  sqwvfourb  46684  fouriersw  46686  fouriercn  46687  etransclem2  46691  etransclem18  46707  etransclem23  46712  etransclem46  46735  rrxtopnfi  46742  rrndistlt  46745  sge0sn  46834  sge0tsms  46835  sge0f1o  46837  sge0pr  46849  sge0resplit  46861  sge0iunmptlemre  46870  sge0isummpt2  46887  hoicvr  47003  hoidmvlelem2  47051  lamberte  47363  refdivmptf  49045  refdivmptfv  49049  amgmlemALT  50305