This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ ℝ
prodgt0.2 ⊢ 𝐵 ∈ ℝ
ltmul1.3 ⊢ 𝐶 ∈ ℝ
Assertion ltdivp1i ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ∧ 𝐴 < ( 𝐵 / ( 𝐶 + 1 ) ) ) → ( 𝐴 · 𝐶 ) < 𝐵 )

Proof

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