MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulge0d Structured version   Visualization version   GIF version

Theorem mulge0d 10717
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
StepHypRef Expression
1 leidd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 addge0d.3 . 2 (𝜑 → 0 ≤ 𝐴)
3 ltnegd.2 . 2 (𝜑𝐵 ∈ ℝ)
4 addge0d.4 . 2 (𝜑 → 0 ≤ 𝐵)
5 mulge0 10659 . 2 (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 · 𝐵))
61, 2, 3, 4, 5syl22anc 1440 1 (𝜑 → 0 ≤ (𝐴 · 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2103   class class class wbr 4760  (class class class)co 6765  cr 10048  0cc0 10049   · cmul 10054  cle 10188
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-opab 4821  df-mpt 4838  df-id 5128  df-po 5139  df-so 5140  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-ov 6768  df-er 7862  df-en 8073  df-dom 8074  df-sdom 8075  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193
This theorem is referenced by:  supmul1  11105  mul2lt0bi  12050  faclbnd6  13201  sqrtmul  14120  sqreulem  14219  climcnds  14703  lcmgcdlem  15442  nmoi  22654  nmoleub2lem3  23036  ipcau2  23154  trirn  23304  itg1ge0  23573  itg1ge0a  23598  itgmulc2lem1  23718  bddmulibl  23725  dvlip  23876  dvfsumlem4  23912  dvfsum2  23917  plyeq0lem  24086  radcnvlem1  24287  dvradcnv  24295  cxpsqrtlem  24568  abscxpbnd  24614  heron  24685  asinlem3  24718  vmadivsum  25291  rpvmasumlem  25296  dchrisumlem2  25299  dchrisum0flblem2  25318  dchrisum0re  25322  mulog2sumlem2  25344  vmalogdivsum2  25347  2vmadivsumlem  25349  selbergb  25358  selberg2lem  25359  selberg2b  25361  chpdifbndlem1  25362  selberg3lem2  25367  selberg4lem1  25369  pntrlog2bndlem1  25386  pntrlog2bndlem2  25387  pntrlog2bndlem4  25389  pntrlog2bndlem6  25392  pntrlog2bnd  25393  pntlemn  25409  ostth2lem3  25444  ttgcontlem1  25885  brbtwn2  25905  colinearalglem4  25909  ax5seglem3  25931  branmfn  29194  eulerpartlemgc  30654  hgt750lemf  30961  hgt750lemb  30964  hgt750lema  30965  iblmulc2nc  33707  itgmulc2nclem1  33708  geomcau  33787  rrnequiv  33866  pellexlem2  37813  pellexlem6  37817  pell1qrge1  37853  rmxypos  37933  ltrmxnn0  37935  nzprmdif  38937  xralrple3  40005  fmul01  40232  dvbdfbdioolem2  40564  stoweidlem1  40638  stoweidlem16  40653  stoweidlem26  40663  stoweidlem38  40675  wallispilem4  40705  wallispi  40707  wallispi2lem1  40708  stirlinglem1  40711  stirlinglem5  40715  stirlinglem6  40716  stirlinglem7  40717  stirlinglem10  40720  stirlinglem11  40721  stirlinglem15  40725  stirlingr  40727  fourierdlem42  40786  rrndistlt  40930
  Copyright terms: Public domain W3C validator