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

Theorem ledivp1i 9936
 Description: Less-than-or-equal-to and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 17-Sep-2005.)
Hypotheses
Ref Expression
ltplus1.1
prodgt0.2
ltmul1.3
Assertion
Ref Expression
ledivp1i

Proof of Theorem ledivp1i
StepHypRef Expression
1 ltplus1.1 . . . 4
2 ltmul1.3 . . . . 5
3 1re 9090 . . . . . 6
42, 3readdcli 9103 . . . . 5
52ltp1i 9914 . . . . . . 7
62, 4, 5ltleii 9196 . . . . . 6
7 lemul2a 9865 . . . . . 6
86, 7mpan2 653 . . . . 5
92, 4, 8mp3an12 1269 . . . 4
101, 9mpan 652 . . 3
12 0re 9091 . . . . . . . 8
1312, 2, 4lelttri 9200 . . . . . . 7
145, 13mpan2 653 . . . . . 6
154gt0ne0i 9562 . . . . . . . . 9
16 prodgt0.2 . . . . . . . . . 10
1716, 4redivclzi 9780 . . . . . . . . 9
1815, 17syl 16 . . . . . . . 8
19 lemul1 9862 . . . . . . . . . . 11
201, 19mp3an1 1266 . . . . . . . . . 10
2120ex 424 . . . . . . . . 9
224, 21mpani 658 . . . . . . . 8
2318, 22mpcom 34 . . . . . . 7
2423biimpd 199 . . . . . 6
2514, 24syl 16 . . . . 5
2625imp 419 . . . 4
2716recni 9102 . . . . . . 7
284recni 9102 . . . . . . 7
2927, 28divcan1zi 9750 . . . . . 6
3014, 15, 293syl 19 . . . . 5
3130adantr 452 . . . 4
3226, 31breqtrd 4236 . . 3