Theorem mulge0d 11788

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 11729	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 · 𝐵))
6	1, 2, 3, 4, 5	syl22anc 836	1 ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2098   class class class wbr 5138  (class class class)co 7401  ℝcr 11105  0cc0 11106   · cmul 11111   ≤ cle 11246

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-po 5578  df-so 5579  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251

This theorem is referenced by:  supmul1  12180  mul2lt0bi  13077  faclbnd6  14256  sqrtmul  15203  sqreulem  15303  climcnds  15794  efcllem  16018  lcmgcdlem  16540  nmoi  24567  nmoleub2lem3  24964  ipcau2  25084  trirn  25250  itg1ge0  25537  itg1ge0a  25563  itgmulc2lem1  25683  bddmulibl  25690  dvlip  25848  dvfsumlem4  25886  dvfsum2  25891  plyeq0lem  26064  radcnvlem1  26266  dvradcnv  26274  cxpsqrtlem  26552  abscxpbnd  26604  heron  26686  asinlem3  26719  vmadivsum  27331  rpvmasumlem  27336  dchrisumlem2  27339  dchrisum0flblem2  27358  dchrisum0re  27362  mulog2sumlem2  27384  vmalogdivsum2  27387  2vmadivsumlem  27389  selbergb  27398  selberg2lem  27399  selberg2b  27401  chpdifbndlem1  27402  selberg3lem2  27407  selberg4lem1  27409  pntrlog2bndlem1  27426  pntrlog2bndlem2  27427  pntrlog2bndlem4  27429  pntrlog2bndlem6  27432  pntrlog2bnd  27433  pntlemn  27449  ostth2lem3  27484  ttgcontlem1  28611  brbtwn2  28632  colinearalglem4  28636  ax5seglem3  28658  branmfn  31827  wrdt2ind  32584  eulerpartlemgc  33850  hgt750lemf  34154  hgt750lemb  34157  hgt750lema  34158  iblmulc2nc  37043  itgmulc2nclem1  37044  geomcau  37117  rrnequiv  37193  aks4d1p1p7  41432  pellexlem2  42057  pellexlem6  42061  pell1qrge1  42097  rmxypos  42175  ltrmxnn0  42177  nzprmdif  43567  xralrple3  44569  fmul01  44781  dvbdfbdioolem2  45130  stoweidlem1  45202  stoweidlem16  45217  stoweidlem26  45227  stoweidlem38  45239  wallispilem4  45269  wallispi  45271  wallispi2lem1  45272  stirlinglem1  45275  stirlinglem5  45279  stirlinglem6  45280  stirlinglem7  45281  stirlinglem10  45284  stirlinglem11  45285  stirlinglem15  45289  stirlingr  45291  fourierdlem42  45350  rrndistlt  45491  itsclc0yqsollem2  47637  2itscp  47655