Theorem divge0d 13174

Description: The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
rpgecld.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
rpgecld.2	⊢ (𝜑 → 𝐵 ∈ ℝ+)
divge0d.3	⊢ (𝜑 → 0 ≤ 𝐴)

Assertion

Ref	Expression
divge0d	⊢ (𝜑 → 0 ≤ (𝐴 / 𝐵))

Proof of Theorem divge0d

Step	Hyp	Ref	Expression
1		rpgecld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		divge0d.3	. 2 ⊢ (𝜑 → 0 ≤ 𝐴)
3		rpgecld.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ+)
4	3	rpregt0d 13140	. 2 ⊢ (𝜑 → (𝐵 ∈ ℝ ∧ 0 < 𝐵))
5		divge0 12156	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ (𝐴 / 𝐵))
6	1, 2, 4, 5	syl21anc 851	1 ⊢ (𝜑 → 0 ≤ (𝐴 / 𝐵))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   class class class wbr 5102  (class class class)co 7408  ℝcr 11171  0cc0 11172   < clt 11315   ≤ cle 11316   / cdiv 11943  ℝ⁺crp 13090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-resscn 11229  ax-1cn 11230  ax-icn 11231  ax-addcl 11232  ax-addrcl 11233  ax-mulcl 11234  ax-mulrcl 11235  ax-mulcom 11236  ax-addass 11237  ax-mulass 11238  ax-distr 11239  ax-i2m1 11240  ax-1ne0 11241  ax-1rid 11242  ax-rnegex 11243  ax-rrecex 11244  ax-cnre 11245  ax-pre-lttri 11246  ax-pre-lttrn 11247  ax-pre-ltadd 11248  ax-pre-mulgt0 11249

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8695  df-en 8952  df-dom 8953  df-sdom 8954  df-pnf 11317  df-mnf 11318  df-xr 11319  df-ltxr 11320  df-le 11321  df-sub 11515  df-neg 11516  df-div 11944  df-rp 13091

This theorem is used by:  iseralt  15820  nn0ehalf  16516  nn0oddm1d2  16523  bitsfzo  16573  bitsmod  16574  iserodd  16975  icopnfcnv  25225  logdiflbnd  27286  lgamgulmlem3  27322  chpo1ubb  27772  vmadivsumb  27774  rpvmasumlem  27778  dchrisumlem1  27780  dchrvmasumlem2  27789  rplogsum  27818  dirith2  27819  mulog2sumlem2  27826  vmalogdivsum2  27829  2vmadivsumlem  27831  selbergb  27840  selberg2b  27843  selberg4lem1  27851  pntrlog2bndlem2  27869  pntrlog2bndlem4  27871  pntrlog2bndlem5  27872  pntrlog2bndlem6  27874  pntrlog2bnd  27875  pntibndlem2  27882  ttgcontlem1  29396  constrresqrtcl  34343  sqsscirc1  34474  faclimlem1  36429  knoppndvlem14  37313  itg2addnclem2  38510  geomcau  38613  3lexlogpow5ineq2  43025  aks4d1p1p7  43044  aks6d1c2lem4  43097  aks6d1c7lem1  43150  areaquad  44161  sqrtcvallem2  44581  sqrtcvallem4  44583  stirlinglem11  47016  stirlinglem12  47017  fourierdlem26  47065  fourierdlem30  47069  fourierdlem47  47085  sge0ad2en  47363  eenglngeehlnmlem2  49772