Metamath Proof Explorer

Theorem ledivp1i

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)

Ref Expression
Hypotheses ltplus1.1 ⊢A∈ℝ
prodgt0.2 ⊢B∈ℝ
ltmul1.3 ⊢C∈ℝ
Assertion ledivp1i ⊢0≤A∧0≤C∧A≤BC+1→A⁢C≤B

Proof

Step Hyp Ref Expression
1 ltplus1.1 ⊢A∈ℝ
2 prodgt0.2 ⊢B∈ℝ
3 ltmul1.3 ⊢C∈ℝ
4 1re ⊢1∈ℝ
5 3 4 readdcli ⊢C+1∈ℝ
6 3 ltp1i ⊢C<C+1
7 3 5 6 ltleii ⊢C≤C+1
8 lemul2a ⊢C∈ℝ∧C+1∈ℝ∧A∈ℝ∧0≤A∧C≤C+1→A⁢C≤A⁢C+1
9 7 8 mpan2 ⊢C∈ℝ∧C+1∈ℝ∧A∈ℝ∧0≤A→A⁢C≤A⁢C+1
10 3 5 9 mp3an12 ⊢A∈ℝ∧0≤A→A⁢C≤A⁢C+1
11 1 10 mpan ⊢0≤A→A⁢C≤A⁢C+1
12 11 3ad2ant1 ⊢0≤A∧0≤C∧A≤BC+1→A⁢C≤A⁢C+1
13 0re ⊢0∈ℝ
14 13 3 5 lelttri ⊢0≤C∧C<C+1→0<C+1
15 6 14 mpan2 ⊢0≤C→0<C+1
16 5 gt0ne0i ⊢0<C+1→C+1≠0
17 2 5 redivclzi ⊢C+1≠0→BC+1∈ℝ
18 16 17 syl ⊢0<C+1→BC+1∈ℝ
19 lemul1 ⊢A∈ℝ∧BC+1∈ℝ∧C+1∈ℝ∧0<C+1→A≤BC+1↔A⁢C+1≤BC+1⁢C+1
20 1 19 mp3an1 ⊢BC+1∈ℝ∧C+1∈ℝ∧0<C+1→A≤BC+1↔A⁢C+1≤BC+1⁢C+1
21 20 ex ⊢BC+1∈ℝ→C+1∈ℝ∧0<C+1→A≤BC+1↔A⁢C+1≤BC+1⁢C+1
22 5 21 mpani ⊢BC+1∈ℝ→0<C+1→A≤BC+1↔A⁢C+1≤BC+1⁢C+1
23 18 22 mpcom ⊢0<C+1→A≤BC+1↔A⁢C+1≤BC+1⁢C+1
24 23 biimpd ⊢0<C+1→A≤BC+1→A⁢C+1≤BC+1⁢C+1
25 15 24 syl ⊢0≤C→A≤BC+1→A⁢C+1≤BC+1⁢C+1
26 25 imp ⊢0≤C∧A≤BC+1→A⁢C+1≤BC+1⁢C+1
27 2 recni ⊢B∈ℂ
28 5 recni ⊢C+1∈ℂ
29 27 28 divcan1zi ⊢C+1≠0→BC+1⁢C+1=B
30 15 16 29 3syl ⊢0≤C→BC+1⁢C+1=B
31 30 adantr ⊢0≤C∧A≤BC+1→BC+1⁢C+1=B
32 26 31 breqtrd ⊢0≤C∧A≤BC+1→A⁢C+1≤B
33 32 3adant1 ⊢0≤A∧0≤C∧A≤BC+1→A⁢C+1≤B
34 1 3 remulcli ⊢A⁢C∈ℝ
35 1 5 remulcli ⊢A⁢C+1∈ℝ
36 34 35 2 letri ⊢A⁢C≤A⁢C+1∧A⁢C+1≤B→A⁢C≤B
37 12 33 36 syl2anc ⊢0≤A∧0≤C∧A≤BC+1→A⁢C≤B