Theorem lemul2ad 11913

Description: Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
ltp1d.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
divgt0d.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
lemul1ad.3	⊢ (𝜑 → 𝐶 ∈ ℝ)
lemul1ad.4	⊢ (𝜑 → 0 ≤ 𝐶)
lemul1ad.5	⊢ (𝜑 → 𝐴 ≤ 𝐵)

Assertion

Ref	Expression
lemul2ad	⊢ (𝜑 → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))

Proof of Theorem lemul2ad

Step	Hyp	Ref	Expression
1		ltp1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		divgt0d.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		lemul1ad.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
4		lemul1ad.4	. . 3 ⊢ (𝜑 → 0 ≤ 𝐶)
5	3, 4	jca 512	. 2 ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
6		lemul1ad.5	. 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
7		lemul2a 11828	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))
8	1, 2, 5, 6, 7	syl31anc 1372	1 ⊢ (𝜑 → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   class class class wbr 5076  (class class class)co 7277  ℝcr 10868  0cc0 10869   · cmul 10874   ≤ cle 11008

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5225  ax-nul 5232  ax-pow 5290  ax-pr 5354  ax-un 7588  ax-resscn 10926  ax-1cn 10927  ax-icn 10928  ax-addcl 10929  ax-addrcl 10930  ax-mulcl 10931  ax-mulrcl 10932  ax-mulcom 10933  ax-addass 10934  ax-mulass 10935  ax-distr 10936  ax-i2m1 10937  ax-1ne0 10938  ax-1rid 10939  ax-rnegex 10940  ax-rrecex 10941  ax-cnre 10942  ax-pre-lttri 10943  ax-pre-lttrn 10944  ax-pre-ltadd 10945  ax-pre-mulgt0 10946

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3433  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5077  df-opab 5139  df-mpt 5160  df-id 5491  df-po 5505  df-so 5506  df-xp 5597  df-rel 5598  df-cnv 5599  df-co 5600  df-dm 5601  df-rn 5602  df-res 5603  df-ima 5604  df-iota 6393  df-fun 6437  df-fn 6438  df-f 6439  df-f1 6440  df-fo 6441  df-f1o 6442  df-fv 6443  df-riota 7234  df-ov 7280  df-oprab 7281  df-mpo 7282  df-er 8496  df-en 8732  df-dom 8733  df-sdom 8734  df-pnf 11009  df-mnf 11010  df-xr 11011  df-ltxr 11012  df-le 11013  df-sub 11205  df-neg 11206

This theorem is referenced by:  flmulnn0  13545  leexp2r  13890  fprodle  15704  efcllem  15785  2expltfac  16792  nlmvscnlem2  23847  ipcnlem2  24406  dveflem  25141  dvfsumlem2  25189  plyeq0lem  25369  radcnvlem1  25570  pserulm  25579  abelthlem7  25595  abscxpbnd  25904  lgamgulmlem3  26178  ftalem1  26220  ftalem5  26224  chpub  26366  vmadivsum  26628  dchrisum0lem1a  26632  dchrisumlem2  26636  dchrisum0re  26659  vmalogdivsum2  26684  2vmadivsumlem  26686  selbergb  26695  selberg2b  26698  chpdifbndlem1  26699  selberg3lem1  26703  selberg4lem1  26706  pntrlog2bndlem1  26723  pntrlog2bndlem2  26724  pntrlog2bndlem4  26726  pntrlog2bndlem5  26727  pntrlog2bndlem6  26729  ostth2lem2  26780  axpaschlem  27306  wrdt2ind  31222  nexple  31974  hgt750lem  32628  hgt750lemb  32633  resconn  33205  knoppcnlem4  34673  unbdqndv2lem2  34687  knoppndvlem11  34699  knoppndvlem14  34702  knoppndvlem18  34706  knoppndvlem19  34707  iblmulc2nc  35839  aks4d1p1p2  40075  aks4d1p1p7  40079  sqrlearg  43061  fmul01  43091  fmul01lt1lem1  43095  sumnnodd  43141  ioodvbdlimc1lem2  43443  ioodvbdlimc2lem  43445  stoweidlem1  43512  wallispi  43581  wallispi2lem1  43582  wallispi2  43584  stirlinglem12  43596  fourierdlem30  43648  fourierdlem39  43657  fourierdlem47  43664  fourierdlem68  43685  fourierdlem73  43690  fourierdlem87  43704  fouriersw  43742  etransclem23  43768  hoidmvlelem1  44103  hoidmvlelem2  44104  hoidmvlelem4  44106