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

Theorem lediv2 9900
 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

Proof of Theorem lediv2
StepHypRef Expression
1 gt0ne0 9493 . . . . 5
2 rereccl 9732 . . . . 5
31, 2syldan 457 . . . 4
5 gt0ne0 9493 . . . . 5
6 rereccl 9732 . . . . 5
75, 6syldan 457 . . . 4
9 simp3l 985 . . 3
10 simp3r 986 . . 3
11 lemul2 9863 . . 3
124, 8, 9, 10, 11syl112anc 1188 . 2
13 lerec 9892 . . 3
15 recn 9080 . . . . . . 7
16 recn 9080 . . . . . . . . 9
1716adantr 452 . . . . . . . 8
1817, 1jca 519 . . . . . . 7
19 divrec 9694 . . . . . . . 8
20193expb 1154 . . . . . . 7
2115, 18, 20syl2an 464 . . . . . 6
22213adant2 976 . . . . 5
23 recn 9080 . . . . . . . . 9
2423adantr 452 . . . . . . . 8
2524, 5jca 519 . . . . . . 7
26 divrec 9694 . . . . . . . 8
27263expb 1154 . . . . . . 7
2815, 25, 27syl2an 464 . . . . . 6
29283adant3 977 . . . . 5
3022, 29breq12d 4225 . . . 4
31303coml 1160 . . 3