Metamath Proof Explorer

Theorem ltdivp1i

Description: Less-than 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 ltdivp1i ⊢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 ltmul1 ⊢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 5 20 mpanr1 ⊢BC+1∈ℝ∧0<C+1→A<BC+1↔A⁢C+1<BC+1⁢C+1
22 18 21 mpancom ⊢0<C+1→A<BC+1↔A⁢C+1<BC+1⁢C+1
23 22 biimpd ⊢0<C+1→A<BC+1→A⁢C+1<BC+1⁢C+1
24 15 23 syl ⊢0≤C→A<BC+1→A⁢C+1<BC+1⁢C+1
25 24 imp ⊢0≤C∧A<BC+1→A⁢C+1<BC+1⁢C+1
26 2 recni ⊢B∈ℂ
27 5 recni ⊢C+1∈ℂ
28 26 27 divcan1zi ⊢C+1≠0→BC+1⁢C+1=B
29 15 16 28 3syl ⊢0≤C→BC+1⁢C+1=B
30 29 adantr ⊢0≤C∧A<BC+1→BC+1⁢C+1=B
31 25 30 breqtrd ⊢0≤C∧A<BC+1→A⁢C+1<B
32 31 3adant1 ⊢0≤A∧0≤C∧A<BC+1→A⁢C+1<B
33 1 3 remulcli ⊢A⁢C∈ℝ
34 1 5 remulcli ⊢A⁢C+1∈ℝ
35 33 34 2 lelttri ⊢A⁢C≤A⁢C+1∧A⁢C+1<B→A⁢C<B
36 12 32 35 syl2anc ⊢0≤A∧0≤C∧A<BC+1→A⁢C<B