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

Theorem divge0 11725
Description: The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 27-Sep-1999.)
Assertion
Ref Expression
divge0 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ (𝐴 / 𝐵))

Proof of Theorem divge0
StepHypRef Expression
1 ge0div 11723 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 𝐵)))
21biimpd 232 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 ≤ 𝐴 → 0 ≤ (𝐴 / 𝐵)))
323exp 1121 . . . 4 (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (0 < 𝐵 → (0 ≤ 𝐴 → 0 ≤ (𝐴 / 𝐵)))))
43com34 91 . . 3 (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (0 ≤ 𝐴 → (0 < 𝐵 → 0 ≤ (𝐴 / 𝐵)))))
54com23 86 . 2 (𝐴 ∈ ℝ → (0 ≤ 𝐴 → (𝐵 ∈ ℝ → (0 < 𝐵 → 0 ≤ (𝐴 / 𝐵)))))
65imp43 431 1 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ (𝐴 / 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089  wcel 2111   class class class wbr 5067  (class class class)co 7231  cr 10752  0cc0 10753   < clt 10891  cle 10892   / cdiv 11513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541  ax-resscn 10810  ax-1cn 10811  ax-icn 10812  ax-addcl 10813  ax-addrcl 10814  ax-mulcl 10815  ax-mulrcl 10816  ax-mulcom 10817  ax-addass 10818  ax-mulass 10819  ax-distr 10820  ax-i2m1 10821  ax-1ne0 10822  ax-1rid 10823  ax-rnegex 10824  ax-rrecex 10825  ax-cnre 10826  ax-pre-lttri 10827  ax-pre-lttrn 10828  ax-pre-ltadd 10829  ax-pre-mulgt0 10830
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4834  df-br 5068  df-opab 5130  df-mpt 5150  df-id 5469  df-po 5482  df-so 5483  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-riota 7188  df-ov 7234  df-oprab 7235  df-mpo 7236  df-er 8411  df-en 8647  df-dom 8648  df-sdom 8649  df-pnf 10893  df-mnf 10894  df-xr 10895  df-ltxr 10896  df-le 10897  df-sub 11088  df-neg 11089  df-div 11514
This theorem is referenced by:  mulge0b  11726  ledivp1  11758  divge0i  11765  divge0d  12692  divelunit  13106  adddivflid  13417  fldiv4p1lem1div2  13434  fldiv  13457  modid  13493  modmuladdnn0  13512  expnbnd  13823  sqrtdiv  14853  sqreulem  14947  efcllem  15663  ege2le3  15675  flodddiv4  15998  hashgcdlem  16365  fldivp1  16474  4sqlem14  16535  odmodnn0  18956  prmirredlem  20483  icopnfcnv  23863  lebnumii  23887  nmoleub2lem3  24036  ncvs1  24078  minveclem4  24353  mbfi1fseqlem1  24637  mbfi1fseqlem5  24641  radcnvlem1  25329  cxpaddle  25662  log2tlbnd  25852  birthdaylem3  25860  jensenlem2  25894  amgm  25897  basellem3  25989  ppiub  26109  logfac2  26122  gausslemma2dlem0d  26264  chto1ub  26381  vmadivsum  26387  rpvmasumlem  26392  dchrvmasumlem2  26403  dchrvmasumiflem1  26406  dchrisum0fno1  26416  dchrisum0re  26418  mulog2sumlem2  26440  selberg2lem  26455  pntrmax  26469  pntrsumo1  26470  pntpbnd1  26491  ostth2lem2  26539  axpaschlem  27055  axcontlem2  27080  nv1  28780  siii  28958  minvecolem4  28985  norm1  29354  strlem1  30355  unitdivcld  31589  cvmliftlem2  32984  cvmliftlem10  32992  cvmliftlem13  32994  snmlff  33027  poimirlem29  35569  poimirlem30  35570  poimirlem31  35571  poimirlem32  35572  pellexlem1  40382  pellexlem6  40387  jm2.22  40548  jm2.23  40549  stoweidlem36  43280  stoweidlem38  43282  nn0eo  45575  dignn0flhalf  45665
  Copyright terms: Public domain W3C validator