Proof of Theorem ledivp1
| Step | Hyp | Ref
| Expression |
| 1 | | simprl 771 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 𝐵 ∈ ℝ) |
| 2 | | peano2re 11434 |
. . . 4
⊢ (𝐵 ∈ ℝ → (𝐵 + 1) ∈
ℝ) |
| 3 | 2 | ad2antrl 728 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐵 + 1) ∈ ℝ) |
| 4 | | simpll 767 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 𝐴 ∈ ℝ) |
| 5 | | ltp1 12107 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ → 𝐵 < (𝐵 + 1)) |
| 6 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 7 | | lelttr 11351 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ ∧ (𝐵 +
1) ∈ ℝ) → ((0 ≤ 𝐵 ∧ 𝐵 < (𝐵 + 1)) → 0 < (𝐵 + 1))) |
| 8 | 6, 7 | mp3an1 1450 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ (𝐵 + 1) ∈ ℝ) → ((0
≤ 𝐵 ∧ 𝐵 < (𝐵 + 1)) → 0 < (𝐵 + 1))) |
| 9 | 2, 8 | mpdan 687 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ → ((0 ≤
𝐵 ∧ 𝐵 < (𝐵 + 1)) → 0 < (𝐵 + 1))) |
| 10 | 5, 9 | mpan2d 694 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → (0 ≤
𝐵 → 0 < (𝐵 + 1))) |
| 11 | 10 | imp 406 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 0 ≤
𝐵) → 0 < (𝐵 + 1)) |
| 12 | 11 | gt0ne0d 11827 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 0 ≤
𝐵) → (𝐵 + 1) ≠ 0) |
| 13 | 12 | adantl 481 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐵 + 1) ≠ 0) |
| 14 | 4, 3, 13 | redivcld 12095 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 / (𝐵 + 1)) ∈ ℝ) |
| 15 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 0 ≤
𝐵) → (𝐵 + 1) ∈
ℝ) |
| 16 | 15, 11 | jca 511 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 0 ≤
𝐵) → ((𝐵 + 1) ∈ ℝ ∧ 0
< (𝐵 +
1))) |
| 17 | | divge0 12137 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ ((𝐵 + 1) ∈ ℝ ∧ 0
< (𝐵 + 1))) → 0
≤ (𝐴 / (𝐵 + 1))) |
| 18 | 16, 17 | sylan2 593 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 / (𝐵 + 1))) |
| 19 | 14, 18 | jca 511 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 / (𝐵 + 1)) ∈ ℝ ∧ 0 ≤ (𝐴 / (𝐵 + 1)))) |
| 20 | | lep1 12108 |
. . . 4
⊢ (𝐵 ∈ ℝ → 𝐵 ≤ (𝐵 + 1)) |
| 21 | 20 | ad2antrl 728 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 𝐵 ≤ (𝐵 + 1)) |
| 22 | | lemul2a 12122 |
. . 3
⊢ (((𝐵 ∈ ℝ ∧ (𝐵 + 1) ∈ ℝ ∧
((𝐴 / (𝐵 + 1)) ∈ ℝ ∧ 0 ≤ (𝐴 / (𝐵 + 1)))) ∧ 𝐵 ≤ (𝐵 + 1)) → ((𝐴 / (𝐵 + 1)) · 𝐵) ≤ ((𝐴 / (𝐵 + 1)) · (𝐵 + 1))) |
| 23 | 1, 3, 19, 21, 22 | syl31anc 1375 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 / (𝐵 + 1)) · 𝐵) ≤ ((𝐴 / (𝐵 + 1)) · (𝐵 + 1))) |
| 24 | | recn 11245 |
. . . 4
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
| 25 | 24 | ad2antrr 726 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 𝐴 ∈ ℂ) |
| 26 | 2 | recnd 11289 |
. . . 4
⊢ (𝐵 ∈ ℝ → (𝐵 + 1) ∈
ℂ) |
| 27 | 26 | ad2antrl 728 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐵 + 1) ∈ ℂ) |
| 28 | 25, 27, 13 | divcan1d 12044 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 / (𝐵 + 1)) · (𝐵 + 1)) = 𝐴) |
| 29 | 23, 28 | breqtrd 5169 |
1
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 / (𝐵 + 1)) · 𝐵) ≤ 𝐴) |