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

Theorem lediv2 12135
Description: Division of a positive number by both sides of 'less than or equal to'. (Contributed by NM, 10-Jan-2006.)
Assertion
Ref Expression
lediv2 (((๐ด โˆˆ โ„ โˆง 0 < ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต) โˆง (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ)) โ†’ (๐ด โ‰ค ๐ต โ†” (๐ถ / ๐ต) โ‰ค (๐ถ / ๐ด)))

Proof of Theorem lediv2
StepHypRef Expression
1 gt0ne0 11710 . . . . 5 ((๐ต โˆˆ โ„ โˆง 0 < ๐ต) โ†’ ๐ต โ‰  0)
2 rereccl 11963 . . . . 5 ((๐ต โˆˆ โ„ โˆง ๐ต โ‰  0) โ†’ (1 / ๐ต) โˆˆ โ„)
31, 2syldan 590 . . . 4 ((๐ต โˆˆ โ„ โˆง 0 < ๐ต) โ†’ (1 / ๐ต) โˆˆ โ„)
433ad2ant2 1132 . . 3 (((๐ด โˆˆ โ„ โˆง 0 < ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต) โˆง (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ)) โ†’ (1 / ๐ต) โˆˆ โ„)
5 gt0ne0 11710 . . . . 5 ((๐ด โˆˆ โ„ โˆง 0 < ๐ด) โ†’ ๐ด โ‰  0)
6 rereccl 11963 . . . . 5 ((๐ด โˆˆ โ„ โˆง ๐ด โ‰  0) โ†’ (1 / ๐ด) โˆˆ โ„)
75, 6syldan 590 . . . 4 ((๐ด โˆˆ โ„ โˆง 0 < ๐ด) โ†’ (1 / ๐ด) โˆˆ โ„)
873ad2ant1 1131 . . 3 (((๐ด โˆˆ โ„ โˆง 0 < ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต) โˆง (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ)) โ†’ (1 / ๐ด) โˆˆ โ„)
9 simp3l 1199 . . 3 (((๐ด โˆˆ โ„ โˆง 0 < ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต) โˆง (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ)) โ†’ ๐ถ โˆˆ โ„)
10 simp3r 1200 . . 3 (((๐ด โˆˆ โ„ โˆง 0 < ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต) โˆง (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ)) โ†’ 0 < ๐ถ)
11 lemul2 12098 . . 3 (((1 / ๐ต) โˆˆ โ„ โˆง (1 / ๐ด) โˆˆ โ„ โˆง (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ)) โ†’ ((1 / ๐ต) โ‰ค (1 / ๐ด) โ†” (๐ถ ยท (1 / ๐ต)) โ‰ค (๐ถ ยท (1 / ๐ด))))
124, 8, 9, 10, 11syl112anc 1372 . 2 (((๐ด โˆˆ โ„ โˆง 0 < ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต) โˆง (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ)) โ†’ ((1 / ๐ต) โ‰ค (1 / ๐ด) โ†” (๐ถ ยท (1 / ๐ต)) โ‰ค (๐ถ ยท (1 / ๐ด))))
13 lerec 12128 . . 3 (((๐ด โˆˆ โ„ โˆง 0 < ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต)) โ†’ (๐ด โ‰ค ๐ต โ†” (1 / ๐ต) โ‰ค (1 / ๐ด)))
14133adant3 1130 . 2 (((๐ด โˆˆ โ„ โˆง 0 < ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต) โˆง (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ)) โ†’ (๐ด โ‰ค ๐ต โ†” (1 / ๐ต) โ‰ค (1 / ๐ด)))
15 recn 11229 . . . . . . 7 (๐ถ โˆˆ โ„ โ†’ ๐ถ โˆˆ โ„‚)
16 recn 11229 . . . . . . . . 9 (๐ต โˆˆ โ„ โ†’ ๐ต โˆˆ โ„‚)
1716adantr 480 . . . . . . . 8 ((๐ต โˆˆ โ„ โˆง 0 < ๐ต) โ†’ ๐ต โˆˆ โ„‚)
1817, 1jca 511 . . . . . . 7 ((๐ต โˆˆ โ„ โˆง 0 < ๐ต) โ†’ (๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0))
19 divrec 11919 . . . . . . . 8 ((๐ถ โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0) โ†’ (๐ถ / ๐ต) = (๐ถ ยท (1 / ๐ต)))
20193expb 1118 . . . . . . 7 ((๐ถ โˆˆ โ„‚ โˆง (๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0)) โ†’ (๐ถ / ๐ต) = (๐ถ ยท (1 / ๐ต)))
2115, 18, 20syl2an 595 . . . . . 6 ((๐ถ โˆˆ โ„ โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต)) โ†’ (๐ถ / ๐ต) = (๐ถ ยท (1 / ๐ต)))
22213adant2 1129 . . . . 5 ((๐ถ โˆˆ โ„ โˆง (๐ด โˆˆ โ„ โˆง 0 < ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต)) โ†’ (๐ถ / ๐ต) = (๐ถ ยท (1 / ๐ต)))
23 recn 11229 . . . . . . . . 9 (๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„‚)
2423adantr 480 . . . . . . . 8 ((๐ด โˆˆ โ„ โˆง 0 < ๐ด) โ†’ ๐ด โˆˆ โ„‚)
2524, 5jca 511 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง 0 < ๐ด) โ†’ (๐ด โˆˆ โ„‚ โˆง ๐ด โ‰  0))
26 divrec 11919 . . . . . . . 8 ((๐ถ โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚ โˆง ๐ด โ‰  0) โ†’ (๐ถ / ๐ด) = (๐ถ ยท (1 / ๐ด)))
27263expb 1118 . . . . . . 7 ((๐ถ โˆˆ โ„‚ โˆง (๐ด โˆˆ โ„‚ โˆง ๐ด โ‰  0)) โ†’ (๐ถ / ๐ด) = (๐ถ ยท (1 / ๐ด)))
2815, 25, 27syl2an 595 . . . . . 6 ((๐ถ โˆˆ โ„ โˆง (๐ด โˆˆ โ„ โˆง 0 < ๐ด)) โ†’ (๐ถ / ๐ด) = (๐ถ ยท (1 / ๐ด)))
29283adant3 1130 . . . . 5 ((๐ถ โˆˆ โ„ โˆง (๐ด โˆˆ โ„ โˆง 0 < ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต)) โ†’ (๐ถ / ๐ด) = (๐ถ ยท (1 / ๐ด)))
3022, 29breq12d 5161 . . . 4 ((๐ถ โˆˆ โ„ โˆง (๐ด โˆˆ โ„ โˆง 0 < ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต)) โ†’ ((๐ถ / ๐ต) โ‰ค (๐ถ / ๐ด) โ†” (๐ถ ยท (1 / ๐ต)) โ‰ค (๐ถ ยท (1 / ๐ด))))
31303coml 1125 . . 3 (((๐ด โˆˆ โ„ โˆง 0 < ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต) โˆง ๐ถ โˆˆ โ„) โ†’ ((๐ถ / ๐ต) โ‰ค (๐ถ / ๐ด) โ†” (๐ถ ยท (1 / ๐ต)) โ‰ค (๐ถ ยท (1 / ๐ด))))
32313adant3r 1179 . 2 (((๐ด โˆˆ โ„ โˆง 0 < ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต) โˆง (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ)) โ†’ ((๐ถ / ๐ต) โ‰ค (๐ถ / ๐ด) โ†” (๐ถ ยท (1 / ๐ต)) โ‰ค (๐ถ ยท (1 / ๐ด))))
3312, 14, 323bitr4d 311 1 (((๐ด โˆˆ โ„ โˆง 0 < ๐ด) โˆง (๐ต โˆˆ โ„ โˆง 0 < ๐ต) โˆง (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ)) โ†’ (๐ด โ‰ค ๐ต โ†” (๐ถ / ๐ต) โ‰ค (๐ถ / ๐ด)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆง w3a 1085   = wceq 1534   โˆˆ wcel 2099   โ‰  wne 2937   class class class wbr 5148  (class class class)co 7420  โ„‚cc 11137  โ„cr 11138  0cc0 11139  1c1 11140   ยท cmul 11144   < clt 11279   โ‰ค cle 11280   / cdiv 11902
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-resscn 11196  ax-1cn 11197  ax-icn 11198  ax-addcl 11199  ax-addrcl 11200  ax-mulcl 11201  ax-mulrcl 11202  ax-mulcom 11203  ax-addass 11204  ax-mulass 11205  ax-distr 11206  ax-i2m1 11207  ax-1ne0 11208  ax-1rid 11209  ax-rnegex 11210  ax-rrecex 11211  ax-cnre 11212  ax-pre-lttri 11213  ax-pre-lttrn 11214  ax-pre-ltadd 11215  ax-pre-mulgt0 11216
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3373  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11281  df-mnf 11282  df-xr 11283  df-ltxr 11284  df-le 11285  df-sub 11477  df-neg 11478  df-div 11903
This theorem is referenced by:  lediv2d  13073  nnledivrp  13119  isprm6  16685  divdenle  16721  gexexlem  19807  znidomb  21495  aaliou2b  26289  log2tlbnd  26890  fsumharmonic  26957  bcmono  27223  dchrisum0lem1  27462  selberg3lem1  27503  pntrsumo1  27511  pntibndlem3  27538  nndivlub  35942  stoweidlem42  45430  stoweidlem51  45439  stoweidlem59  45447
  Copyright terms: Public domain W3C validator