Theorem divge0 10973

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

Step	Hyp	Ref	Expression
1		ge0div 10971	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 𝐵)))
2	1	biimpd 219	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 ≤ 𝐴 → 0 ≤ (𝐴 / 𝐵)))
3	2	3exp 1112	. . . 4 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (0 < 𝐵 → (0 ≤ 𝐴 → 0 ≤ (𝐴 / 𝐵)))))
4	3	com34 91	. . 3 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (0 ≤ 𝐴 → (0 < 𝐵 → 0 ≤ (𝐴 / 𝐵)))))
5	4	com23 86	. 2 ⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐴 → (𝐵 ∈ ℝ → (0 < 𝐵 → 0 ≤ (𝐴 / 𝐵)))))
6	5	imp43 622	1 ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ (𝐴 / 𝐵))

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072   ∈ wcel 2071   class class class wbr 4728  (class class class)co 6733  ℝcr 10016  0cc0 10017   < clt 10155   ≤ cle 10156   / cdiv 10765

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1818  ax-5 1920  ax-6 1986  ax-7 2022  ax-8 2073  ax-9 2080  ax-10 2100  ax-11 2115  ax-12 2128  ax-13 2323  ax-ext 2672  ax-sep 4857  ax-nul 4865  ax-pow 4916  ax-pr 4979  ax-un 7034  ax-resscn 10074  ax-1cn 10075  ax-icn 10076  ax-addcl 10077  ax-addrcl 10078  ax-mulcl 10079  ax-mulrcl 10080  ax-mulcom 10081  ax-addass 10082  ax-mulass 10083  ax-distr 10084  ax-i2m1 10085  ax-1ne0 10086  ax-1rid 10087  ax-rnegex 10088  ax-rrecex 10089  ax-cnre 10090  ax-pre-lttri 10091  ax-pre-lttrn 10092  ax-pre-ltadd 10093  ax-pre-mulgt0 10094

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1567  df-ex 1786  df-nf 1791  df-sb 1979  df-eu 2543  df-mo 2544  df-clab 2679  df-cleq 2685  df-clel 2688  df-nfc 2823  df-ne 2865  df-nel 2968  df-ral 2987  df-rex 2988  df-reu 2989  df-rmo 2990  df-rab 2991  df-v 3274  df-sbc 3510  df-csb 3608  df-dif 3651  df-un 3653  df-in 3655  df-ss 3662  df-nul 3992  df-if 4163  df-pw 4236  df-sn 4254  df-pr 4256  df-op 4260  df-uni 4513  df-br 4729  df-opab 4789  df-mpt 4806  df-id 5096  df-po 5107  df-so 5108  df-xp 5192  df-rel 5193  df-cnv 5194  df-co 5195  df-dm 5196  df-rn 5197  df-res 5198  df-ima 5199  df-iota 5932  df-fun 5971  df-fn 5972  df-f 5973  df-f1 5974  df-fo 5975  df-f1o 5976  df-fv 5977  df-riota 6694  df-ov 6736  df-oprab 6737  df-mpt2 6738  df-er 7830  df-en 8041  df-dom 8042  df-sdom 8043  df-pnf 10157  df-mnf 10158  df-xr 10159  df-ltxr 10160  df-le 10161  df-sub 10349  df-neg 10350  df-div 10766

This theorem is referenced by:  mulge0b  10974  ledivp1  11006  divge0i  11014  divge0d  11994  divelunit  12396  adddivflid  12702  fldiv4p1lem1div2  12719  fldiv  12742  modid  12778  modmuladdnn0  12797  expnbnd  13076  sqrtdiv  14094  sqreulem  14187  iseralt  14503  efcllem  14896  ege2le3  14908  flodddiv4  15228  hashgcdlem  15584  iserodd  15631  fldivp1  15692  4sqlem14  15753  odmodnn0  18048  prmirredlem  19932  icopnfcnv  22831  lebnumii  22855  nmoleub2lem3  23004  ncvs1  23046  minveclem4  23292  mbfi1fseqlem1  23570  mbfi1fseqlem5  23574  radcnvlem1  24255  cxpaddle  24581  leibpilem1  24755  log2tlbnd  24760  birthdaylem3  24768  jensenlem2  24802  amgm  24805  basellem3  24897  ppiub  25017  logfac2  25030  gausslemma2dlem0d  25172  chto1ub  25253  vmadivsum  25259  rpvmasumlem  25264  dchrvmasumlem2  25275  dchrvmasumiflem1  25278  dchrisum0fno1  25288  dchrisum0re  25290  mulog2sumlem2  25312  selberg2lem  25327  pntrmax  25341  pntrsumo1  25342  pntpbnd1  25363  ostth2lem2  25411  axpaschlem  25908  axcontlem2  25933  nv1  27728  siii  27906  minvecolem4  27934  norm1  28304  strlem1  29307  unitdivcld  30145  cvmliftlem2  31464  cvmliftlem10  31472  cvmliftlem13  31474  snmlff  31507  poimirlem29  33638  poimirlem30  33639  poimirlem31  33640  poimirlem32  33641  pellexlem1  37780  pellexlem6  37785  jm2.22  37949  jm2.23  37950  stoweidlem36  40641  stoweidlem38  40643  nn0eo  42717  dignn0flhalf  42807