Theorem divge0 12051

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 12049	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 𝐵)))
2	1	biimpd 231	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 ≤ 𝐴 → 0 ≤ (𝐴 / 𝐵)))
3	2	3exp 1128	. . . 4 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (0 < 𝐵 → (0 ≤ 𝐴 → 0 ≤ (𝐴 / 𝐵)))))
4	3	com34 91	. . 3 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (0 ≤ 𝐴 → (0 < 𝐵 → 0 ≤ (𝐴 / 𝐵)))))
5	4	com23 86	. 2 ⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐴 → (𝐵 ∈ ℝ → (0 < 𝐵 → 0 ≤ (𝐴 / 𝐵)))))
6	5	imp43 430	1 ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ (𝐴 / 𝐵))

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095   ∈ wcel 2136   class class class wbr 5094  (class class class)co 7385  ℝcr 11062  0cc0 11063   < clt 11206   ≤ cle 11207   / cdiv 11834

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728  ax-sep 5240  ax-nul 5250  ax-pow 5316  ax-pr 5384  ax-un 7707  ax-resscn 11120  ax-1cn 11121  ax-icn 11122  ax-addcl 11123  ax-addrcl 11124  ax-mulcl 11125  ax-mulrcl 11126  ax-mulcom 11127  ax-addass 11128  ax-mulass 11129  ax-distr 11130  ax-i2m1 11131  ax-1ne0 11132  ax-1rid 11133  ax-rnegex 11134  ax-rrecex 11135  ax-cnre 11136  ax-pre-lttri 11137  ax-pre-lttrn 11138  ax-pre-ltadd 11139  ax-pre-mulgt0 11140

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-ne 2952  df-nel 3056  df-ral 3071  df-rex 3081  df-rmo 3361  df-reu 3362  df-rab 3409  df-v 3450  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-pw 4551  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-opab 5157  df-mpt 5176  df-id 5535  df-po 5548  df-so 5549  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6512  df-fn 6513  df-f 6514  df-f1 6515  df-fo 6516  df-f1o 6517  df-fv 6518  df-riota 7342  df-ov 7388  df-oprab 7389  df-mpo 7390  df-er 8666  df-en 8917  df-dom 8918  df-sdom 8919  df-pnf 11208  df-mnf 11209  df-xr 11210  df-ltxr 11211  df-le 11212  df-sub 11406  df-neg 11407  df-div 11835

This theorem is referenced by:  mulge0b  12052  ledivp1  12084  divge0i  12091  divge0d  13067  divelunit  13488  nnge2recico01  13501  adddivflid  13818  fldiv4p1lem1div2  13835  fldiv  13860  modid  13896  modmuladdnn0  13918  expnbnd  14235  sqrtdiv  15268  sqreulem  15363  efcllem  16083  ege2le3  16096  flodddiv4  16425  hashgcdlem  16799  fldivp1  16909  4sqlem14  16970  odmodnn0  19556  prmirredlem  21497  icopnfcnv  24977  lebnumii  25001  nmoleub2lem3  25150  ncvs1  25192  minveclem4  25467  mbfi1fseqlem1  25750  mbfi1fseqlem5  25754  radcnvlem1  26446  cxpaddle  26787  log2tlbnd  26980  birthdaylem3  26988  jensenlem2  27022  amgm  27025  basellem3  27117  ppiub  27238  logfac2  27251  gausslemma2dlem0d  27393  chto1ub  27510  vmadivsum  27516  rpvmasumlem  27521  dchrvmasumlem2  27532  dchrvmasumiflem1  27535  dchrisum0fno1  27545  dchrisum0re  27547  mulog2sumlem2  27569  selberg2lem  27584  pntrmax  27598  pntrsumo1  27599  pntpbnd1  27620  ostth2lem2  27668  axpaschlem  29080  axcontlem2  29105  nv1  30817  siii  30995  minvecolem4  31022  norm1  31391  strlem1  32392  unitdivcld  34152  cvmliftlem2  35584  cvmliftlem10  35592  cvmliftlem13  35594  snmlff  35627  poimirlem29  38096  poimirlem30  38097  poimirlem31  38098  poimirlem32  38099  pellexlem1  43354  pellexlem6  43359  jm2.22  43520  jm2.23  43521  stoweidlem36  46558  stoweidlem38  46560  nn0eo  49098  dignn0flhalf  49188