Theorem mulge0d 11798

Description: The product of two nonnegative numbers is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
leidd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltnegd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
addge0d.3	⊢ (𝜑 → 0 ≤ 𝐴)
addge0d.4	⊢ (𝜑 → 0 ≤ 𝐵)

Assertion

Ref	Expression
mulge0d	⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵))

Proof of Theorem mulge0d

Step	Hyp	Ref	Expression
1		leidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		addge0d.3	. 2 ⊢ (𝜑 → 0 ≤ 𝐴)
3		ltnegd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4		addge0d.4	. 2 ⊢ (𝜑 → 0 ≤ 𝐵)
5		mulge0 11739	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 · 𝐵))
6	1, 2, 3, 4, 5	syl22anc 836	1 ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2105   class class class wbr 5148  (class class class)co 7412  ℝcr 11115  0cc0 11116   · cmul 11121   ≤ cle 11256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192  ax-pre-mulgt0 11193

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7415  df-er 8709  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261

This theorem is referenced by:  supmul1  12190  mul2lt0bi  13087  faclbnd6  14266  sqrtmul  15213  sqreulem  15313  climcnds  15804  efcllem  16028  lcmgcdlem  16550  nmoi  24566  nmoleub2lem3  24963  ipcau2  25083  trirn  25249  itg1ge0  25536  itg1ge0a  25562  itgmulc2lem1  25682  bddmulibl  25689  dvlip  25847  dvfsumlem4  25885  dvfsum2  25890  plyeq0lem  26063  radcnvlem1  26265  dvradcnv  26273  cxpsqrtlem  26551  abscxpbnd  26603  heron  26685  asinlem3  26718  vmadivsum  27330  rpvmasumlem  27335  dchrisumlem2  27338  dchrisum0flblem2  27357  dchrisum0re  27361  mulog2sumlem2  27383  vmalogdivsum2  27386  2vmadivsumlem  27388  selbergb  27397  selberg2lem  27398  selberg2b  27400  chpdifbndlem1  27401  selberg3lem2  27406  selberg4lem1  27408  pntrlog2bndlem1  27425  pntrlog2bndlem2  27426  pntrlog2bndlem4  27428  pntrlog2bndlem6  27431  pntrlog2bnd  27432  pntlemn  27448  ostth2lem3  27483  ttgcontlem1  28577  brbtwn2  28598  colinearalglem4  28602  ax5seglem3  28624  branmfn  31793  wrdt2ind  32552  eulerpartlemgc  33827  hgt750lemf  34131  hgt750lemb  34134  hgt750lema  34135  iblmulc2nc  37020  itgmulc2nclem1  37021  geomcau  37094  rrnequiv  37170  aks4d1p1p7  41409  pellexlem2  42034  pellexlem6  42038  pell1qrge1  42074  rmxypos  42152  ltrmxnn0  42154  nzprmdif  43544  xralrple3  44546  fmul01  44758  dvbdfbdioolem2  45107  stoweidlem1  45179  stoweidlem16  45194  stoweidlem26  45204  stoweidlem38  45216  wallispilem4  45246  wallispi  45248  wallispi2lem1  45249  stirlinglem1  45252  stirlinglem5  45256  stirlinglem6  45257  stirlinglem7  45258  stirlinglem10  45261  stirlinglem11  45262  stirlinglem15  45266  stirlingr  45268  fourierdlem42  45327  rrndistlt  45468  itsclc0yqsollem2  47614  2itscp  47632