Axiom ax-resscn 11184

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

Assertion

Ref	Expression
ax-resscn	⊢ ℝ ⊆ ℂ

Detailed syntax breakdown of Axiom ax-resscn

Step	Hyp	Ref	Expression
1		cr 11126	. 2 class ℝ
2		cc 11125	. 2 class ℂ
3	1, 2	wss 3926	1 wff ℝ ⊆ ℂ

This axiom is referenced by:  recn  11217  reex  11218  recni  11247  qsscn  12974  ioosscn  13423  unitsscn  13515  reexpcl  14094  rpexpcl  14096  reexpclz  14098  expge0  14114  expge1  14115  rlimrecl  15594  abscn2  15613  recn2  15615  imcn2  15616  climabs  15618  climre  15620  climim  15621  rlimabs  15623  rlimre  15625  rlimim  15626  caurcvgr  15688  caucvgrlem2  15689  caurcvg  15691  fsumrecl  15748  fsumrpcl  15751  fsumge0  15809  fsumre  15822  fsumim  15823  fprodrecl  15967  fprodrpcl  15970  fprodreclf  15973  fprodge0  16007  fprodge1  16009  rerisefaccl  16031  refallfaccl  16032  rprisefaccl  16037  reeff1  16136  nthruc  16268  regsumfsum  21401  rge0srg  21404  rebase  21564  re0g  21570  regsumsupp  21580  remet  24727  tgioo2  24740  xrsdsre  24748  recld2  24752  reperf  24757  iitopon  24821  dfii3  24825  abscncf  24843  recncf  24844  imcncf  24845  abscncfALT  24867  cnmptre  24870  iimulcnOLD  24884  icchmeo  24887  icchmeoOLD  24888  cnrehmeo  24900  cnrehmeoOLD  24901  evth  24907  evth2  24908  lebnumlem2  24910  lebnumii  24914  reparphtiOLD  24946  cphsqrtcl  25134  resscdrg  25308  ishl2  25320  recms  25330  reust  25331  evthicc  25410  evthicc2  25411  ovolfsf  25422  volcn  25557  volivth  25558  ismbf  25579  cncombf  25609  cnmbf  25610  0plef  25623  itg1ge0  25637  i1faddlem  25644  i1fmul  25647  itg1addlem4  25650  i1fsub  25659  itg1sub  25660  mbfi1fseqlem5  25670  xrge0f  25682  itg20  25688  itg2const  25691  itg2mulc  25698  itg2addlem  25709  i1fibl  25759  itgitg1  25760  iblabslem  25779  iblabs  25780  bddmulibl  25790  recnprss  25855  dvmptresicc  25867  dvcjbr  25903  dvfre  25905  dvnfre  25906  dvferm1  25939  dvferm2  25941  rolle  25944  cmvth  25945  cmvthOLD  25946  mvth  25947  dvlip  25948  dvlipcn  25949  dvlip2  25950  c1liplem1  25951  c1lip2  25953  dvgt0lem1  25957  dvle  25962  dvivthlem1  25963  dvivth  25965  dvne0  25966  lhop1lem  25968  lhop1  25969  lhop2  25970  lhop  25971  dvcnvrelem1  25972  dvcnvrelem2  25973  dvcnvre  25974  dvcvx  25975  dvfsumle  25976  dvfsumleOLD  25977  dvfsumge  25978  dvfsumabs  25979  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumrlim  25988  ftc1a  25994  ftc1lem3  25995  ftc1lem6  25998  ftc1  25999  ftc1cn  26000  ftc2  26001  ftc2ditglem  26002  itgparts  26004  itgsubstlem  26005  itgsubst  26006  itgpowd  26007  aacjcl  26285  aalioulem3  26292  taylthlem2  26332  taylthlem2OLD  26333  taylth  26334  abelth2  26402  reeff1olem  26406  efcvx  26409  pilem3  26413  pige3ALT  26479  recosf1o  26494  resinf1o  26495  dvrelog  26596  relogcn  26597  logcnlem5  26605  logcn  26606  dvloglem  26607  dvlog2lem  26611  logccv  26622  dvcxp1  26699  cxpcn3  26708  resqrtcn  26709  loglesqrt  26721  ssscongptld  26782  ressatans  26894  rlimcnp  26925  efrlim  26929  efrlimOLD  26930  jensenlem1  26947  jensenlem2  26948  jensen  26949  amgm  26951  lgamgulmlem2  26990  ftalem3  27035  basellem9  27049  efnnfsumcl  27063  efchtdvds  27119  lgsdchr  27316  dchrvmasumlem1  27456  dchrisum0lem3  27480  pntlem3  27570  cchhllem  28812  ex-fpar  30389  ipasslem7  30763  fprodex01  32750  indsumin  32785  rexdiv  32846  fsumrp0cl  32962  xrge0slmod  33309  ccfldsrarelvec  33658  ccfldextdgrr  33659  rmulccn  33905  raddcn  33906  xrge0iifhom  33914  lmlimxrge0  33925  rezh  33946  esumpfinvallem  34051  esumpfinval  34052  esumpfinvalf  34053  esumcvg  34063  plymulx0  34525  plymulx  34526  signsplypnf  34528  signsply0  34529  iblidicc  34570  rpsqrtcn  34571  ftc2re  34576  fdvposlt  34577  fdvneggt  34578  fdvposle  34579  fdvnegge  34580  itgexpif  34584  circlemeth  34618  circlemethnat  34619  circlevma  34620  circlemethhgt  34621  logdivsqrle  34628  resconn  35214  ivthALT  36299  dnicn  36456  knoppcnlem10  36466  knoppcnlem11  36467  unbdqndv2  36475  knoppndv  36498  knoppcn2  36500  broucube  37624  mblfinlem2  37628  mbfresfi  37636  ftc1cnnclem  37661  ftc1cnnc  37662  ftc1anclem3  37665  ftc1anclem5  37667  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  ftc2nc  37672  asindmre  37673  dvreasin  37676  dvreacos  37677  areacirclem1  37678  areacirclem2  37679  areacirclem3  37680  areacirclem4  37681  areacirc  37683  repwsmet  37804  rrnequiv  37805  rrntotbnd  37806  reheibor  37809  iccbnd  37810  intlewftc  42020  dvrelog2  42023  dvrelog3  42024  aks4d1p1p5  42034  rpsscn  42295  redvmptabs  42350  readvrec2  42351  resuppsinopn  42353  readvcot  42354  resubeqsub  42419  subresre  42420  arearect  43186  areaquad  43187  k0004val0  44125  extoimad  44135  imo72b2lem0  44136  imo72b2lem2  44138  imo72b2lem1  44140  imo72b2  44143  ssrecnpr  44280  sblpnf  44282  radcnvrat  44286  lhe4.4ex1a  44301  refsumcn  45002  rr2sscn2  45341  uzsscn  45450  evthiccabs  45473  climreeq  45590  limciccioolb  45598  limcrecl  45606  limcicciooub  45614  limcleqr  45621  lptioo2cn  45622  lptioo1cn  45623  limclner  45628  liminflimsupclim  45784  resincncf  45852  cncficcgt0  45865  cncfiooicclem1  45870  cncfiooiccre  45872  jumpncnp  45875  dvcosre  45889  dvmptconst  45892  dvmptidg  45894  fperdvper  45896  dvresioo  45898  dvmulcncf  45902  dvdivcncf  45904  dvbdfbdioolem1  45905  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc1  45910  ioodvbdlimc2lem  45911  ioodvbdlimc2  45912  itgsin0pilem1  45927  ibliccsinexp  45928  iblioosinexp  45930  itgsinexplem1  45931  itgsinexp  45932  itgcoscmulx  45946  itgsincmulx  45951  itgsubsticclem  45952  itgiccshift  45957  itgperiod  45958  itgsbtaddcnst  45959  dirkeritg  46079  dirkercncflem2  46081  dirkercncflem3  46082  dirkercncflem4  46083  dirkercncf  46084  fourierdlem16  46100  fourierdlem18  46102  fourierdlem21  46105  fourierdlem22  46106  fourierdlem39  46123  fourierdlem42  46126  fourierdlem48  46131  fourierdlem49  46132  fourierdlem53  46136  fourierdlem57  46140  fourierdlem58  46141  fourierdlem59  46142  fourierdlem60  46143  fourierdlem61  46144  fourierdlem62  46145  fourierdlem68  46151  fourierdlem70  46153  fourierdlem72  46155  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem78  46161  fourierdlem80  46163  fourierdlem83  46166  fourierdlem84  46167  fourierdlem85  46168  fourierdlem88  46171  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem93  46176  fourierdlem94  46177  fourierdlem95  46178  fourierdlem96  46179  fourierdlem97  46180  fourierdlem98  46181  fourierdlem99  46182  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem112  46195  fourierdlem113  46196  fouriercnp  46203  sqwvfoura  46205  sqwvfourb  46206  fouriersw  46208  fouriercn  46209  etransclem2  46213  etransclem18  46229  etransclem23  46234  etransclem46  46257  rrxtopnfi  46264  rrndistlt  46267  sge0sn  46356  sge0tsms  46357  sge0f1o  46359  sge0pr  46371  sge0resplit  46383  sge0iunmptlemre  46392  sge0isummpt2  46409  hoicvr  46525  hoidmvlelem2  46573  lamberte  46868  refdivmptf  48470  refdivmptfv  48474  amgmlemALT  49615