Metamath Proof Explorer

Theorem ledivp1

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, 28-Sep-2005)

Ref Expression
Assertion ledivp1 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 / ( 𝐵 + 1 ) ) · 𝐵 ) ≤ 𝐴 )

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 𝐵 ∈ ℝ )
2 peano2re ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 + 1 ) ∈ ℝ )
3 2 ad2antrl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐵 + 1 ) ∈ ℝ )
4 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 𝐴 ∈ ℝ )
5 ltp1 ⊢ ( 𝐵 ∈ ℝ → 𝐵 < ( 𝐵 + 1 ) )
6 0re ⊢ 0 ∈ ℝ
7 lelttr ⊢ ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐵 + 1 ) ∈ ℝ ) → ( ( 0 ≤ 𝐵 ∧ 𝐵 < ( 𝐵 + 1 ) ) → 0 < ( 𝐵 + 1 ) ) )
8 6 7 mp3an1 ⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐵 + 1 ) ∈ ℝ ) → ( ( 0 ≤ 𝐵 ∧ 𝐵 < ( 𝐵 + 1 ) ) → 0 < ( 𝐵 + 1 ) ) )
9 2 8 mpdan ⊢ ( 𝐵 ∈ ℝ → ( ( 0 ≤ 𝐵 ∧ 𝐵 < ( 𝐵 + 1 ) ) → 0 < ( 𝐵 + 1 ) ) )
10 5 9 mpan2d ⊢ ( 𝐵 ∈ ℝ → ( 0 ≤ 𝐵 → 0 < ( 𝐵 + 1 ) ) )
11 10 imp ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) → 0 < ( 𝐵 + 1 ) )
12 11 gt0ne0d ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) → ( 𝐵 + 1 ) ≠ 0 )
13 12 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐵 + 1 ) ≠ 0 )
14 4 3 13 redivcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐴 / ( 𝐵 + 1 ) ) ∈ ℝ )
15 2 adantr ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) → ( 𝐵 + 1 ) ∈ ℝ )
16 15 11 jca ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) → ( ( 𝐵 + 1 ) ∈ ℝ ∧ 0 < ( 𝐵 + 1 ) ) )
17 divge0 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( ( 𝐵 + 1 ) ∈ ℝ ∧ 0 < ( 𝐵 + 1 ) ) ) → 0 ≤ ( 𝐴 / ( 𝐵 + 1 ) ) )
18 16 17 sylan2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 𝐴 / ( 𝐵 + 1 ) ) )
19 14 18 jca ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 / ( 𝐵 + 1 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / ( 𝐵 + 1 ) ) ) )
20 lep1 ⊢ ( 𝐵 ∈ ℝ → 𝐵 ≤ ( 𝐵 + 1 ) )
21 20 ad2antrl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 𝐵 ≤ ( 𝐵 + 1 ) )
22 lemul2a ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐵 + 1 ) ∈ ℝ ∧ ( ( 𝐴 / ( 𝐵 + 1 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / ( 𝐵 + 1 ) ) ) ) ∧ 𝐵 ≤ ( 𝐵 + 1 ) ) → ( ( 𝐴 / ( 𝐵 + 1 ) ) · 𝐵 ) ≤ ( ( 𝐴 / ( 𝐵 + 1 ) ) · ( 𝐵 + 1 ) ) )
23 1 3 19 21 22 syl31anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 / ( 𝐵 + 1 ) ) · 𝐵 ) ≤ ( ( 𝐴 / ( 𝐵 + 1 ) ) · ( 𝐵 + 1 ) ) )
24 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
25 24 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 𝐴 ∈ ℂ )
26 2 recnd ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 + 1 ) ∈ ℂ )
27 26 ad2antrl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐵 + 1 ) ∈ ℂ )
28 25 27 13 divcan1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 / ( 𝐵 + 1 ) ) · ( 𝐵 + 1 ) ) = 𝐴 )
29 23 28 breqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 / ( 𝐵 + 1 ) ) · 𝐵 ) ≤ 𝐴 )