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 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A B + 1 ⁢ B ≤ A

Proof

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