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

Theorem divge0 10420
Description: The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 27-Sep-1999.)
Assertion
Ref Expression
divge0  |-  ( ( ( A  e.  RR  /\  0  <_  A )  /\  ( B  e.  RR  /\  0  <  B ) )  ->  0  <_  ( A  /  B ) )

Proof of Theorem divge0
StepHypRef Expression
1 ge0div 10418 . . . . . 6  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  0  <  B )  ->  (
0  <_  A  <->  0  <_  ( A  /  B ) ) )
21biimpd 210 . . . . 5  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  0  <  B )  ->  (
0  <_  A  ->  0  <_  ( A  /  B ) ) )
323exp 1204 . . . 4  |-  ( A  e.  RR  ->  ( B  e.  RR  ->  ( 0  <  B  -> 
( 0  <_  A  ->  0  <_  ( A  /  B ) ) ) ) )
43com34 86 . . 3  |-  ( A  e.  RR  ->  ( B  e.  RR  ->  ( 0  <_  A  ->  ( 0  <  B  -> 
0  <_  ( A  /  B ) ) ) ) )
54com23 81 . 2  |-  ( A  e.  RR  ->  (
0  <_  A  ->  ( B  e.  RR  ->  ( 0  <  B  -> 
0  <_  ( A  /  B ) ) ) ) )
65imp43 598 1  |-  ( ( ( A  e.  RR  /\  0  <_  A )  /\  ( B  e.  RR  /\  0  <  B ) )  ->  0  <_  ( A  /  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982    e. wcel 1872   class class class wbr 4361  (class class class)co 6244   RRcr 9484   0cc0 9485    < clt 9621    <_ cle 9622    / cdiv 10215
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562
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 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-opab 4421  df-mpt 4422  df-id 4706  df-po 4712  df-so 4713  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-er 7313  df-en 7520  df-dom 7521  df-sdom 7522  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-div 10216
This theorem is referenced by:  mulge0b  10421  ledivp1  10454  divge0i  10462  divge0d  11324  divelunit  11720  fldiv  12032  modid  12066  expnbnd  12346  sqrtdiv  13268  sqreulem  13361  iseralt  13689  efcllem  14070  ege2le3  14082  iserodd  14723  fldivp1  14780  4sqlem14OLD  14840  4sqlem14  14846  odmodnn0  17127  prmirredlem  19001  icopnfcnv  21907  lebnumii  21934  nmoleub2lem3  22066  minveclem4  22311  minveclem4OLD  22323  mbfi1fseqlem1  22610  mbfi1fseqlem5  22614  radcnvlem1  23305  cxpaddle  23629  leibpilem1  23803  log2tlbnd  23808  birthdaylem3  23816  jensenlem2  23850  amgm  23853  basellem3  23946  ppiub  24069  logfac2  24082  chto1ub  24251  vmadivsum  24257  rpvmasumlem  24262  dchrvmasumlem2  24273  dchrvmasumiflem1  24276  dchrisum0fno1  24286  dchrisum0re  24288  mulog2sumlem2  24310  selberg2lem  24325  pntrmax  24339  pntrsumo1  24340  pntpbnd1  24361  ostth2lem2  24409  axpaschlem  24907  axcontlem2  24932  nv1  26242  siii  26431  minvecolem4  26459  minvecolem4OLD  26469  norm1  26839  strlem1  27840  unitdivcld  28654  cvmliftlem2  29956  cvmliftlem10  29964  cvmliftlem13  29966  snmlff  29999  poimirlem29  31876  poimirlem30  31877  poimirlem31  31878  poimirlem32  31879  pellexlem1  35586  pellexlem6  35591  jm2.22  35763  jm2.23  35764  hashgcdlem  35987  stoweidlem36  37780  stoweidlem38  37782  nn0eo  39928  dignn0flhalf  40022
  Copyright terms: Public domain W3C validator