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

Theorem ledivp1i 10124
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 9264 . . . . . 6
42, 3readdcli 9278 . . . . 5
52ltp1i 10102 . . . . . . 7
62, 4, 5ltleii 9376 . . . . . 6
7 lemul2a 10053 . . . . . 6
86, 7mpan2 654 . . . . 5
92, 4, 8mp3an12 1277 . . . 4
101, 9mpan 653 . . 3
11103ad2ant1 983 . 2
12 0re 9265 . . . . . . . 8
1312, 2, 4lelttri 9380 . . . . . . 7
145, 13mpan2 654 . . . . . 6
154gt0ne0i 9748 . . . . . . . . 9
16 prodgt0.2 . . . . . . . . . 10
1716, 4redivclzi 9968 . . . . . . . . 9
1815, 17syl 16 . . . . . . . 8
19 lemul1 10050 . . . . . . . . . . 11
201, 19mp3an1 1274 . . . . . . . . . 10
2120ex 425 . . . . . . . . 9
224, 21mpani 659 . . . . . . . 8
2318, 22mpcom 35 . . . . . . 7
2423biimpd 200 . . . . . 6
2514, 24syl 16 . . . . 5
2625imp 420 . . . 4
2716recni 9277 . . . . . . 7
284recni 9277 . . . . . . 7
2927, 28divcan1zi 9938 . . . . . 6
3014, 15, 293syl 19 . . . . 5
3130adantr 453 . . . 4
3226, 31breqtrd 4342 . . 3
33323adant1 980 . 2
341, 2remulcli 9279 . . 3
351, 4remulcli 9279 . . 3
3634, 35, 16letri 9382 . 2
3711, 33, 36syl2anc 644 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  /\wa 360  /\w3a 939  =wceq 1670  e.wcel 1732  =/=wne 2652   class class class wbr 4318  (class class class)co 6103   cr 9160  0cc0 9161  1c1 9162   caddc 9164   cmul 9166   clt 9297   cle 9298   cdiv 9864
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pow 4493  ax-pr 4554  ax-un 6382  ax-resscn 9218  ax-1cn 9219  ax-icn 9220  ax-addcl 9221  ax-addrcl 9222  ax-mulcl 9223  ax-mulrcl 9224  ax-mulcom 9225  ax-addass 9226  ax-mulass 9227  ax-distr 9228  ax-i2m1 9229  ax-1ne0 9230  ax-1rid 9231  ax-rnegex 9232  ax-rrecex 9233  ax-cnre 9234  ax-pre-lttri 9235  ax-pre-lttrn 9236  ax-pre-ltadd 9237  ax-pre-mulgt0 9238
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-nel 2655  df-ral 2764  df-rex 2765  df-reu 2766  df-rmo 2767  df-rab 2768  df-v 3017  df-sbc 3225  df-csb 3326  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-nul 3674  df-if 3826  df-pw 3895  df-sn 3915  df-pr 3916  df-op 3918  df-uni 4118  df-br 4319  df-opab 4377  df-mpt 4378  df-id 4657  df-po 4662  df-so 4663  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-res 4874  df-ima 4875  df-iota 5401  df-fun 5440  df-fn 5441  df-f 5442  df-f1 5443  df-fo 5444  df-f1o 5445  df-fv 5446  df-riota 6062  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-er 7067  df-en 7274  df-dom 7275  df-sdom 7276  df-pnf 9299  df-mnf 9300  df-xr 9301  df-ltxr 9302  df-le 9303  df-sub 9474  df-neg 9475  df-div 9865
  Copyright terms: Public domain W3C validator