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

Theorem lemul2a 11169
Description: Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.)
Assertion
Ref Expression
lemul2a (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴𝐵) → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))

Proof of Theorem lemul2a
StepHypRef Expression
1 lemul1a 11168 . 2 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴𝐵) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))
2 recn 10313 . . . . . 6 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
3 recn 10313 . . . . . 6 (𝐶 ∈ ℝ → 𝐶 ∈ ℂ)
4 mulcom 10309 . . . . . 6 ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · 𝐶) = (𝐶 · 𝐴))
52, 3, 4syl2an 590 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐶) = (𝐶 · 𝐴))
65adantrr 709 . . . 4 ((𝐴 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) → (𝐴 · 𝐶) = (𝐶 · 𝐴))
763adant2 1162 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) → (𝐴 · 𝐶) = (𝐶 · 𝐴))
87adantr 473 . 2 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴𝐵) → (𝐴 · 𝐶) = (𝐶 · 𝐴))
9 recn 10313 . . . . . 6 (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
10 mulcom 10309 . . . . . 6 ((𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐵 · 𝐶) = (𝐶 · 𝐵))
119, 3, 10syl2an 590 . . . . 5 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 𝐶) = (𝐶 · 𝐵))
1211adantrr 709 . . . 4 ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) → (𝐵 · 𝐶) = (𝐶 · 𝐵))
13123adant1 1161 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) → (𝐵 · 𝐶) = (𝐶 · 𝐵))
1413adantr 473 . 2 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴𝐵) → (𝐵 · 𝐶) = (𝐶 · 𝐵))
151, 8, 143brtr3d 4873 1 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴𝐵) → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  w3a 1108   = wceq 1653  wcel 2157   class class class wbr 4842  (class class class)co 6877  cc 10221  cr 10222  0cc0 10223   · cmul 10228  cle 10363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776  ax-sep 4974  ax-nul 4982  ax-pow 5034  ax-pr 5096  ax-un 7182  ax-resscn 10280  ax-1cn 10281  ax-icn 10282  ax-addcl 10283  ax-addrcl 10284  ax-mulcl 10285  ax-mulrcl 10286  ax-mulcom 10287  ax-addass 10288  ax-mulass 10289  ax-distr 10290  ax-i2m1 10291  ax-1ne0 10292  ax-1rid 10293  ax-rnegex 10294  ax-rrecex 10295  ax-cnre 10296  ax-pre-lttri 10297  ax-pre-lttrn 10298  ax-pre-ltadd 10299  ax-pre-mulgt0 10300
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-ne 2971  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3386  df-sbc 3633  df-csb 3728  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-nul 4115  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-op 4374  df-uni 4628  df-br 4843  df-opab 4905  df-mpt 4922  df-id 5219  df-po 5232  df-so 5233  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6063  df-fun 6102  df-fn 6103  df-f 6104  df-f1 6105  df-fo 6106  df-f1o 6107  df-fv 6108  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-er 7981  df-en 8195  df-dom 8196  df-sdom 8197  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10557  df-neg 10558
This theorem is referenced by:  lemul12b  11171  ledivp1  11216  ledivp1i  11240  ltdivp1i  11241  lemul2ad  11255  supmul1  11283  facavg  13338  mulcn2  14664  cvgrat  14949  mertenslem1  14950  prmreclem3  15952  nmoco  22866  blcvx  22926  fsumharmonic  25087  bposlem1  25358  dchrvmasumiflem1  25539  nmoub3i  28146  htthlem  28292  nmopub2tALT  29286  nmfnleub2  29303  nmophmi  29408  nmopadjlem  29466  nmopcoadji  29478  lediv2aALT  32079  stoweidlem24  40973
  Copyright terms: Public domain W3C validator