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

Theorem mulge0 11733
Description: The product of two nonnegative numbers is nonnegative. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.)
Assertion
Ref Expression
mulge0 (((๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 โ‰ค ๐ต)) โ†’ 0 โ‰ค (๐ด ยท ๐ต))

Proof of Theorem mulge0
StepHypRef Expression
1 0red 11218 . . . . . 6 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ 0 โˆˆ โ„)
2 simpl 482 . . . . . 6 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ ๐ด โˆˆ โ„)
31, 2leloed 11358 . . . . 5 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (0 โ‰ค ๐ด โ†” (0 < ๐ด โˆจ 0 = ๐ด)))
4 simpr 484 . . . . . 6 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ ๐ต โˆˆ โ„)
51, 4leloed 11358 . . . . 5 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (0 โ‰ค ๐ต โ†” (0 < ๐ต โˆจ 0 = ๐ต)))
63, 5anbi12d 630 . . . 4 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ ((0 โ‰ค ๐ด โˆง 0 โ‰ค ๐ต) โ†” ((0 < ๐ด โˆจ 0 = ๐ด) โˆง (0 < ๐ต โˆจ 0 = ๐ต))))
7 0red 11218 . . . . . . 7 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง (0 < ๐ด โˆง 0 < ๐ต)) โ†’ 0 โˆˆ โ„)
8 simpll 764 . . . . . . . 8 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง (0 < ๐ด โˆง 0 < ๐ต)) โ†’ ๐ด โˆˆ โ„)
9 simplr 766 . . . . . . . 8 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง (0 < ๐ด โˆง 0 < ๐ต)) โ†’ ๐ต โˆˆ โ„)
108, 9remulcld 11245 . . . . . . 7 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง (0 < ๐ด โˆง 0 < ๐ต)) โ†’ (๐ด ยท ๐ต) โˆˆ โ„)
11 mulgt0 11292 . . . . . . . 8 (((๐ด โˆˆ โ„ โˆง 0 < ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต)) โ†’ 0 < (๐ด ยท ๐ต))
1211an4s 657 . . . . . . 7 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง (0 < ๐ด โˆง 0 < ๐ต)) โ†’ 0 < (๐ด ยท ๐ต))
137, 10, 12ltled 11363 . . . . . 6 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง (0 < ๐ด โˆง 0 < ๐ต)) โ†’ 0 โ‰ค (๐ด ยท ๐ต))
1413ex 412 . . . . 5 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ ((0 < ๐ด โˆง 0 < ๐ต) โ†’ 0 โ‰ค (๐ด ยท ๐ต)))
15 0re 11217 . . . . . . . . 9 0 โˆˆ โ„
16 leid 11311 . . . . . . . . 9 (0 โˆˆ โ„ โ†’ 0 โ‰ค 0)
1715, 16ax-mp 5 . . . . . . . 8 0 โ‰ค 0
184recnd 11243 . . . . . . . . 9 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ ๐ต โˆˆ โ„‚)
1918mul02d 11413 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (0 ยท ๐ต) = 0)
2017, 19breqtrrid 5179 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ 0 โ‰ค (0 ยท ๐ต))
21 oveq1 7411 . . . . . . . 8 (0 = ๐ด โ†’ (0 ยท ๐ต) = (๐ด ยท ๐ต))
2221breq2d 5153 . . . . . . 7 (0 = ๐ด โ†’ (0 โ‰ค (0 ยท ๐ต) โ†” 0 โ‰ค (๐ด ยท ๐ต)))
2320, 22syl5ibcom 244 . . . . . 6 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (0 = ๐ด โ†’ 0 โ‰ค (๐ด ยท ๐ต)))
2423adantrd 491 . . . . 5 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ ((0 = ๐ด โˆง 0 < ๐ต) โ†’ 0 โ‰ค (๐ด ยท ๐ต)))
252recnd 11243 . . . . . . . . 9 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ ๐ด โˆˆ โ„‚)
2625mul01d 11414 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (๐ด ยท 0) = 0)
2717, 26breqtrrid 5179 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ 0 โ‰ค (๐ด ยท 0))
28 oveq2 7412 . . . . . . . 8 (0 = ๐ต โ†’ (๐ด ยท 0) = (๐ด ยท ๐ต))
2928breq2d 5153 . . . . . . 7 (0 = ๐ต โ†’ (0 โ‰ค (๐ด ยท 0) โ†” 0 โ‰ค (๐ด ยท ๐ต)))
3027, 29syl5ibcom 244 . . . . . 6 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (0 = ๐ต โ†’ 0 โ‰ค (๐ด ยท ๐ต)))
3130adantld 490 . . . . 5 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ ((0 < ๐ด โˆง 0 = ๐ต) โ†’ 0 โ‰ค (๐ด ยท ๐ต)))
3230adantld 490 . . . . 5 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ ((0 = ๐ด โˆง 0 = ๐ต) โ†’ 0 โ‰ค (๐ด ยท ๐ต)))
3314, 24, 31, 32ccased 1035 . . . 4 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (((0 < ๐ด โˆจ 0 = ๐ด) โˆง (0 < ๐ต โˆจ 0 = ๐ต)) โ†’ 0 โ‰ค (๐ด ยท ๐ต)))
346, 33sylbid 239 . . 3 ((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ ((0 โ‰ค ๐ด โˆง 0 โ‰ค ๐ต) โ†’ 0 โ‰ค (๐ด ยท ๐ต)))
3534imp 406 . 2 (((๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง (0 โ‰ค ๐ด โˆง 0 โ‰ค ๐ต)) โ†’ 0 โ‰ค (๐ด ยท ๐ต))
3635an4s 657 1 (((๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 โ‰ค ๐ต)) โ†’ 0 โ‰ค (๐ด ยท ๐ต))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   โˆจ wo 844   = wceq 1533   โˆˆ wcel 2098   class class class wbr 5141  (class class class)co 7404  โ„cr 11108  0cc0 11109   ยท cmul 11114   < clt 11249   โ‰ค cle 11250
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 2697  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186
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 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-po 5581  df-so 5582  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7407  df-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255
This theorem is referenced by:  mulge0i  11762  mulge0d  11792  mulge0b  12085  ge0mulcl  13441  expge0  14067  bernneq  14195  sqrtmul  15210  sqreulem  15310  amgm2  15320  nmoco  24605  iihalf1  24803  iimulcl  24811  mbfi1fseqlem1  25596  mbfi1fseqlem3  25598  mbfi1fseqlem5  25600  2lgslem1a1  27273  dchrisumlem3  27375  dchrvmasumlem2  27382  chpdifbndlem2  27438  cnlnadjlem7  31831  leopmuli  31891  reofld  32962  stoweidlem24  45293  hoidmvlelem1  45864
  Copyright terms: Public domain W3C validator