Proof of Theorem ledivp1
Step | Hyp | Ref
| Expression |
1 | | simprl 770 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 𝐵 ∈ ℝ) |
2 | | peano2re 10802 |
. . . 4
⊢ (𝐵 ∈ ℝ → (𝐵 + 1) ∈
ℝ) |
3 | 2 | ad2antrl 727 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐵 + 1) ∈ ℝ) |
4 | | simpll 766 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 𝐴 ∈ ℝ) |
5 | | ltp1 11469 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ → 𝐵 < (𝐵 + 1)) |
6 | | 0re 10632 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
7 | | lelttr 10720 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ ∧ (𝐵 +
1) ∈ ℝ) → ((0 ≤ 𝐵 ∧ 𝐵 < (𝐵 + 1)) → 0 < (𝐵 + 1))) |
8 | 6, 7 | mp3an1 1445 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ (𝐵 + 1) ∈ ℝ) → ((0
≤ 𝐵 ∧ 𝐵 < (𝐵 + 1)) → 0 < (𝐵 + 1))) |
9 | 2, 8 | mpdan 686 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ → ((0 ≤
𝐵 ∧ 𝐵 < (𝐵 + 1)) → 0 < (𝐵 + 1))) |
10 | 5, 9 | mpan2d 693 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → (0 ≤
𝐵 → 0 < (𝐵 + 1))) |
11 | 10 | imp 410 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 0 ≤
𝐵) → 0 < (𝐵 + 1)) |
12 | 11 | gt0ne0d 11193 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 0 ≤
𝐵) → (𝐵 + 1) ≠ 0) |
13 | 12 | adantl 485 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐵 + 1) ≠ 0) |
14 | 4, 3, 13 | redivcld 11457 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 / (𝐵 + 1)) ∈ ℝ) |
15 | 2 | adantr 484 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 0 ≤
𝐵) → (𝐵 + 1) ∈
ℝ) |
16 | 15, 11 | jca 515 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 0 ≤
𝐵) → ((𝐵 + 1) ∈ ℝ ∧ 0
< (𝐵 +
1))) |
17 | | divge0 11498 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ ((𝐵 + 1) ∈ ℝ ∧ 0
< (𝐵 + 1))) → 0
≤ (𝐴 / (𝐵 + 1))) |
18 | 16, 17 | sylan2 595 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 / (𝐵 + 1))) |
19 | 14, 18 | jca 515 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 / (𝐵 + 1)) ∈ ℝ ∧ 0 ≤ (𝐴 / (𝐵 + 1)))) |
20 | | lep1 11470 |
. . . 4
⊢ (𝐵 ∈ ℝ → 𝐵 ≤ (𝐵 + 1)) |
21 | 20 | ad2antrl 727 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 𝐵 ≤ (𝐵 + 1)) |
22 | | lemul2a 11484 |
. . 3
⊢ (((𝐵 ∈ ℝ ∧ (𝐵 + 1) ∈ ℝ ∧
((𝐴 / (𝐵 + 1)) ∈ ℝ ∧ 0 ≤ (𝐴 / (𝐵 + 1)))) ∧ 𝐵 ≤ (𝐵 + 1)) → ((𝐴 / (𝐵 + 1)) · 𝐵) ≤ ((𝐴 / (𝐵 + 1)) · (𝐵 + 1))) |
23 | 1, 3, 19, 21, 22 | syl31anc 1370 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 / (𝐵 + 1)) · 𝐵) ≤ ((𝐴 / (𝐵 + 1)) · (𝐵 + 1))) |
24 | | recn 10616 |
. . . 4
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
25 | 24 | ad2antrr 725 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 𝐴 ∈ ℂ) |
26 | 2 | recnd 10658 |
. . . 4
⊢ (𝐵 ∈ ℝ → (𝐵 + 1) ∈
ℂ) |
27 | 26 | ad2antrl 727 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐵 + 1) ∈ ℂ) |
28 | 25, 27, 13 | divcan1d 11406 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 / (𝐵 + 1)) · (𝐵 + 1)) = 𝐴) |
29 | 23, 28 | breqtrd 5056 |
1
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 / (𝐵 + 1)) · 𝐵) ≤ 𝐴) |