MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  redivcld Structured version   Unicode version

Theorem redivcld 10435
Description: Closure law for division of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
redivcld.1  |-  ( ph  ->  A  e.  RR )
redivcld.2  |-  ( ph  ->  B  e.  RR )
redivcld.3  |-  ( ph  ->  B  =/=  0 )
Assertion
Ref Expression
redivcld  |-  ( ph  ->  ( A  /  B
)  e.  RR )

Proof of Theorem redivcld
StepHypRef Expression
1 redivcld.1 . 2  |-  ( ph  ->  A  e.  RR )
2 redivcld.2 . 2  |-  ( ph  ->  B  e.  RR )
3 redivcld.3 . 2  |-  ( ph  ->  B  =/=  0 )
4 redivcl 10326 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  B  =/=  0 )  ->  ( A  /  B )  e.  RR )
51, 2, 3, 4syl3anc 1264 1  |-  ( ph  ->  ( A  /  B
)  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1868    =/= wne 2618  (class class class)co 6301   RRcr 9538   0cc0 9539    / cdiv 10269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-po 4770  df-so 4771  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-er 7367  df-en 7574  df-dom 7575  df-sdom 7576  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270
This theorem is referenced by:  recp1lt1  10504  ledivp1  10508  supmul1  10576  rimul  10600  divelunit  11774  quoremz  12081  intfracq  12085  fldiv  12086  modmulnn  12113  expnbnd  12400  discr1  12407  discr  12408  sqreulem  13410  fprodle  14037  iccpnfhmeo  21959  ipcau2  22194  mbfmulc2lem  22589  i1fmulc  22647  itg1mulc  22648  itg2monolem3  22696  dvferm2lem  22924  dvcvx  22958  radcnvlem1  23354  tanord1  23472  logf1o2  23581  relogbcl  23696  ang180lem2  23725  chordthmlem2  23745  jensenlem2  23899  regamcl  23972  selberg3lem1  24381  selberg4lem1  24384  ostth2  24461  ttgcontlem1  24901  colinearalg  24926  axsegconlem8  24940  axpaschlem  24956  axeuclidlem  24978  nmophmi  27669  unitdivcld  28702  dya2icoseg  29094  dya2iocucvr  29101  signsply0  29435  sinccvglem  30311  circum  30313  poimirlem31  31884  itg2addnclem  31906  itg2addnclem2  31907  areacirclem1  31945  areacirclem4  31948  pellexlem1  35592  pellexlem6  35597  reglogcl  35657  modabsdifz  35758  areaquad  36020  imo72b2  36476  hashnzfzclim  36528  sineq0ALT  37194  suplesup  37403  0ellimcdiv  37549  dvdivbd  37614  ioodvbdlimc1lem1  37622  ioodvbdlimc1lem2  37623  ioodvbdlimc1lem1OLD  37624  ioodvbdlimc1lem2OLD  37625  ioodvbdlimc2lem  37627  ioodvbdlimc2lemOLD  37628  stoweidlem1  37680  stoweidlem13  37692  stoweidlem26  37705  stoweidlem34  37714  stoweidlem36  37716  stoweidlem51  37731  stoweidlem60  37740  wallispilem4  37749  wallispilem5  37750  stirlingr  37771  dirker2re  37773  dirkerval2  37775  dirkerre  37776  dirkertrigeq  37782  dirkeritg  37783  dirkercncflem1  37784  dirkercncflem4  37787  fourierdlem4  37792  fourierdlem7  37795  fourierdlem9  37797  fourierdlem16  37804  fourierdlem19  37807  fourierdlem21  37809  fourierdlem22  37810  fourierdlem24  37812  fourierdlem26  37814  fourierdlem30  37818  fourierdlem39  37828  fourierdlem41  37830  fourierdlem42  37831  fourierdlem42OLD  37832  fourierdlem43  37833  fourierdlem47  37836  fourierdlem48  37837  fourierdlem49  37838  fourierdlem51  37840  fourierdlem56  37845  fourierdlem57  37846  fourierdlem58  37847  fourierdlem59  37848  fourierdlem63  37852  fourierdlem64  37853  fourierdlem66  37855  fourierdlem71  37860  fourierdlem72  37861  fourierdlem78  37867  fourierdlem83  37872  fourierdlem87  37876  fourierdlem89  37878  fourierdlem90  37879  fourierdlem91  37880  fourierdlem95  37884  fourierdlem103  37892  fourierdlem104  37893  etransclem48OLD  37966  etransclem48  37967  sge0rpcpnf  38050  sge0ad2en  38060  ovnsubaddlem1  38166  sigardiv  38182  modn0mul  39596  refdivmptf  39626  fldivexpfllog2  39649  dignnld  39687  dig2nn1st  39689  dig2bits  39698  dignn0flhalflem2  39700
  Copyright terms: Public domain W3C validator