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 ⊢ 𝐴 ∈ ℝ
prodgt0.2 ⊢ 𝐵 ∈ ℝ
ltmul1.3 ⊢ 𝐶 ∈ ℝ
Assertion ledivp1i ( ( 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 lemul1 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 / ( 𝐶 + 1 ) ) ∈ ℝ ∧ ( ( 𝐶 + 1 ) ∈ ℝ ∧ 0 < ( 𝐶 + 1 ) ) ) → ( 𝐴 ≤ ( 𝐵 / ( 𝐶 + 1 ) ) ↔ ( 𝐴 · ( 𝐶 + 1 ) ) ≤ ( ( 𝐵 / ( 𝐶 + 1 ) ) · ( 𝐶 + 1 ) ) ) )
20 1 19 mp3an1 ⊢ ( ( ( 𝐵 / ( 𝐶 + 1 ) ) ∈ ℝ ∧ ( ( 𝐶 + 1 ) ∈ ℝ ∧ 0 < ( 𝐶 + 1 ) ) ) → ( 𝐴 ≤ ( 𝐵 / ( 𝐶 + 1 ) ) ↔ ( 𝐴 · ( 𝐶 + 1 ) ) ≤ ( ( 𝐵 / ( 𝐶 + 1 ) ) · ( 𝐶 + 1 ) ) ) )
21 20 ex ⊢ ( ( 𝐵 / ( 𝐶 + 1 ) ) ∈ ℝ → ( ( ( 𝐶 + 1 ) ∈ ℝ ∧ 0 < ( 𝐶 + 1 ) ) → ( 𝐴 ≤ ( 𝐵 / ( 𝐶 + 1 ) ) ↔ ( 𝐴 · ( 𝐶 + 1 ) ) ≤ ( ( 𝐵 / ( 𝐶 + 1 ) ) · ( 𝐶 + 1 ) ) ) ) )
22 5 21 mpani ⊢ ( ( 𝐵 / ( 𝐶 + 1 ) ) ∈ ℝ → ( 0 < ( 𝐶 + 1 ) → ( 𝐴 ≤ ( 𝐵 / ( 𝐶 + 1 ) ) ↔ ( 𝐴 · ( 𝐶 + 1 ) ) ≤ ( ( 𝐵 / ( 𝐶 + 1 ) ) · ( 𝐶 + 1 ) ) ) ) )
23 18 22 mpcom ⊢ ( 0 < ( 𝐶 + 1 ) → ( 𝐴 ≤ ( 𝐵 / ( 𝐶 + 1 ) ) ↔ ( 𝐴 · ( 𝐶 + 1 ) ) ≤ ( ( 𝐵 / ( 𝐶 + 1 ) ) · ( 𝐶 + 1 ) ) ) )
24 23 biimpd ⊢ ( 0 < ( 𝐶 + 1 ) → ( 𝐴 ≤ ( 𝐵 / ( 𝐶 + 1 ) ) → ( 𝐴 · ( 𝐶 + 1 ) ) ≤ ( ( 𝐵 / ( 𝐶 + 1 ) ) · ( 𝐶 + 1 ) ) ) )
25 15 24 syl ⊢ ( 0 ≤ 𝐶 → ( 𝐴 ≤ ( 𝐵 / ( 𝐶 + 1 ) ) → ( 𝐴 · ( 𝐶 + 1 ) ) ≤ ( ( 𝐵 / ( 𝐶 + 1 ) ) · ( 𝐶 + 1 ) ) ) )
26 25 imp ⊢ ( ( 0 ≤ 𝐶 ∧ 𝐴 ≤ ( 𝐵 / ( 𝐶 + 1 ) ) ) → ( 𝐴 · ( 𝐶 + 1 ) ) ≤ ( ( 𝐵 / ( 𝐶 + 1 ) ) · ( 𝐶 + 1 ) ) )
27 2 recni ⊢ 𝐵 ∈ ℂ
28 5 recni ⊢ ( 𝐶 + 1 ) ∈ ℂ
29 27 28 divcan1zi ⊢ ( ( 𝐶 + 1 ) ≠ 0 → ( ( 𝐵 / ( 𝐶 + 1 ) ) · ( 𝐶 + 1 ) ) = 𝐵 )
30 15 16 29 3syl ⊢ ( 0 ≤ 𝐶 → ( ( 𝐵 / ( 𝐶 + 1 ) ) · ( 𝐶 + 1 ) ) = 𝐵 )
31 30 adantr ⊢ ( ( 0 ≤ 𝐶 ∧ 𝐴 ≤ ( 𝐵 / ( 𝐶 + 1 ) ) ) → ( ( 𝐵 / ( 𝐶 + 1 ) ) · ( 𝐶 + 1 ) ) = 𝐵 )
32 26 31 breqtrd ⊢ ( ( 0 ≤ 𝐶 ∧ 𝐴 ≤ ( 𝐵 / ( 𝐶 + 1 ) ) ) → ( 𝐴 · ( 𝐶 + 1 ) ) ≤ 𝐵 )
33 32 3adant1 ⊢ ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ∧ 𝐴 ≤ ( 𝐵 / ( 𝐶 + 1 ) ) ) → ( 𝐴 · ( 𝐶 + 1 ) ) ≤ 𝐵 )
34 1 3 remulcli ⊢ ( 𝐴 · 𝐶 ) ∈ ℝ
35 1 5 remulcli ⊢ ( 𝐴 · ( 𝐶 + 1 ) ) ∈ ℝ
36 34 35 2 letri ⊢ ( ( ( 𝐴 · 𝐶 ) ≤ ( 𝐴 · ( 𝐶 + 1 ) ) ∧ ( 𝐴 · ( 𝐶 + 1 ) ) ≤ 𝐵 ) → ( 𝐴 · 𝐶 ) ≤ 𝐵 )
37 12 33 36 syl2anc ⊢ ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ∧ 𝐴 ≤ ( 𝐵 / ( 𝐶 + 1 ) ) ) → ( 𝐴 · 𝐶 ) ≤ 𝐵 )