Proof of Theorem ledivp1i
Step | Hyp | Ref
| Expression |
1 | | ltplus1.1 |
. . . 4
⊢ 𝐴 ∈ ℝ |
2 | | ltmul1.3 |
. . . . 5
⊢ 𝐶 ∈ ℝ |
3 | | 1re 10833 |
. . . . . 6
⊢ 1 ∈
ℝ |
4 | 2, 3 | readdcli 10848 |
. . . . 5
⊢ (𝐶 + 1) ∈
ℝ |
5 | 2 | ltp1i 11736 |
. . . . . . 7
⊢ 𝐶 < (𝐶 + 1) |
6 | 2, 4, 5 | ltleii 10955 |
. . . . . 6
⊢ 𝐶 ≤ (𝐶 + 1) |
7 | | lemul2a 11687 |
. . . . . 6
⊢ (((𝐶 ∈ ℝ ∧ (𝐶 + 1) ∈ ℝ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝐶 ≤ (𝐶 + 1)) → (𝐴 · 𝐶) ≤ (𝐴 · (𝐶 + 1))) |
8 | 6, 7 | mpan2 691 |
. . . . 5
⊢ ((𝐶 ∈ ℝ ∧ (𝐶 + 1) ∈ ℝ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) → (𝐴 · 𝐶) ≤ (𝐴 · (𝐶 + 1))) |
9 | 2, 4, 8 | mp3an12 1453 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (𝐴 · 𝐶) ≤ (𝐴 · (𝐶 + 1))) |
10 | 1, 9 | mpan 690 |
. . 3
⊢ (0 ≤
𝐴 → (𝐴 · 𝐶) ≤ (𝐴 · (𝐶 + 1))) |
11 | 10 | 3ad2ant1 1135 |
. 2
⊢ ((0 ≤
𝐴 ∧ 0 ≤ 𝐶 ∧ 𝐴 ≤ (𝐵 / (𝐶 + 1))) → (𝐴 · 𝐶) ≤ (𝐴 · (𝐶 + 1))) |
12 | | 0re 10835 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
13 | 12, 2, 4 | lelttri 10959 |
. . . . . . 7
⊢ ((0 ≤
𝐶 ∧ 𝐶 < (𝐶 + 1)) → 0 < (𝐶 + 1)) |
14 | 5, 13 | mpan2 691 |
. . . . . 6
⊢ (0 ≤
𝐶 → 0 < (𝐶 + 1)) |
15 | 4 | gt0ne0i 11367 |
. . . . . . . . 9
⊢ (0 <
(𝐶 + 1) → (𝐶 + 1) ≠ 0) |
16 | | prodgt0.2 |
. . . . . . . . . 10
⊢ 𝐵 ∈ ℝ |
17 | 16, 4 | redivclzi 11598 |
. . . . . . . . 9
⊢ ((𝐶 + 1) ≠ 0 → (𝐵 / (𝐶 + 1)) ∈ ℝ) |
18 | 15, 17 | syl 17 |
. . . . . . . 8
⊢ (0 <
(𝐶 + 1) → (𝐵 / (𝐶 + 1)) ∈ ℝ) |
19 | | lemul1 11684 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 / (𝐶 + 1)) ∈ ℝ ∧ ((𝐶 + 1) ∈ ℝ ∧ 0
< (𝐶 + 1))) →
(𝐴 ≤ (𝐵 / (𝐶 + 1)) ↔ (𝐴 · (𝐶 + 1)) ≤ ((𝐵 / (𝐶 + 1)) · (𝐶 + 1)))) |
20 | 1, 19 | mp3an1 1450 |
. . . . . . . . . 10
⊢ (((𝐵 / (𝐶 + 1)) ∈ ℝ ∧ ((𝐶 + 1) ∈ ℝ ∧ 0
< (𝐶 + 1))) →
(𝐴 ≤ (𝐵 / (𝐶 + 1)) ↔ (𝐴 · (𝐶 + 1)) ≤ ((𝐵 / (𝐶 + 1)) · (𝐶 + 1)))) |
21 | 20 | ex 416 |
. . . . . . . . 9
⊢ ((𝐵 / (𝐶 + 1)) ∈ ℝ → (((𝐶 + 1) ∈ ℝ ∧ 0
< (𝐶 + 1)) → (𝐴 ≤ (𝐵 / (𝐶 + 1)) ↔ (𝐴 · (𝐶 + 1)) ≤ ((𝐵 / (𝐶 + 1)) · (𝐶 + 1))))) |
22 | 4, 21 | mpani 696 |
. . . . . . . 8
⊢ ((𝐵 / (𝐶 + 1)) ∈ ℝ → (0 < (𝐶 + 1) → (𝐴 ≤ (𝐵 / (𝐶 + 1)) ↔ (𝐴 · (𝐶 + 1)) ≤ ((𝐵 / (𝐶 + 1)) · (𝐶 + 1))))) |
23 | 18, 22 | mpcom 38 |
. . . . . . 7
⊢ (0 <
(𝐶 + 1) → (𝐴 ≤ (𝐵 / (𝐶 + 1)) ↔ (𝐴 · (𝐶 + 1)) ≤ ((𝐵 / (𝐶 + 1)) · (𝐶 + 1)))) |
24 | 23 | biimpd 232 |
. . . . . 6
⊢ (0 <
(𝐶 + 1) → (𝐴 ≤ (𝐵 / (𝐶 + 1)) → (𝐴 · (𝐶 + 1)) ≤ ((𝐵 / (𝐶 + 1)) · (𝐶 + 1)))) |
25 | 14, 24 | syl 17 |
. . . . 5
⊢ (0 ≤
𝐶 → (𝐴 ≤ (𝐵 / (𝐶 + 1)) → (𝐴 · (𝐶 + 1)) ≤ ((𝐵 / (𝐶 + 1)) · (𝐶 + 1)))) |
26 | 25 | imp 410 |
. . . 4
⊢ ((0 ≤
𝐶 ∧ 𝐴 ≤ (𝐵 / (𝐶 + 1))) → (𝐴 · (𝐶 + 1)) ≤ ((𝐵 / (𝐶 + 1)) · (𝐶 + 1))) |
27 | 16 | recni 10847 |
. . . . . . 7
⊢ 𝐵 ∈ ℂ |
28 | 4 | recni 10847 |
. . . . . . 7
⊢ (𝐶 + 1) ∈
ℂ |
29 | 27, 28 | divcan1zi 11568 |
. . . . . 6
⊢ ((𝐶 + 1) ≠ 0 → ((𝐵 / (𝐶 + 1)) · (𝐶 + 1)) = 𝐵) |
30 | 14, 15, 29 | 3syl 18 |
. . . . 5
⊢ (0 ≤
𝐶 → ((𝐵 / (𝐶 + 1)) · (𝐶 + 1)) = 𝐵) |
31 | 30 | adantr 484 |
. . . 4
⊢ ((0 ≤
𝐶 ∧ 𝐴 ≤ (𝐵 / (𝐶 + 1))) → ((𝐵 / (𝐶 + 1)) · (𝐶 + 1)) = 𝐵) |
32 | 26, 31 | breqtrd 5079 |
. . 3
⊢ ((0 ≤
𝐶 ∧ 𝐴 ≤ (𝐵 / (𝐶 + 1))) → (𝐴 · (𝐶 + 1)) ≤ 𝐵) |
33 | 32 | 3adant1 1132 |
. 2
⊢ ((0 ≤
𝐴 ∧ 0 ≤ 𝐶 ∧ 𝐴 ≤ (𝐵 / (𝐶 + 1))) → (𝐴 · (𝐶 + 1)) ≤ 𝐵) |
34 | 1, 2 | remulcli 10849 |
. . 3
⊢ (𝐴 · 𝐶) ∈ ℝ |
35 | 1, 4 | remulcli 10849 |
. . 3
⊢ (𝐴 · (𝐶 + 1)) ∈ ℝ |
36 | 34, 35, 16 | letri 10961 |
. 2
⊢ (((𝐴 · 𝐶) ≤ (𝐴 · (𝐶 + 1)) ∧ (𝐴 · (𝐶 + 1)) ≤ 𝐵) → (𝐴 · 𝐶) ≤ 𝐵) |
37 | 11, 33, 36 | syl2anc 587 |
1
⊢ ((0 ≤
𝐴 ∧ 0 ≤ 𝐶 ∧ 𝐴 ≤ (𝐵 / (𝐶 + 1))) → (𝐴 · 𝐶) ≤ 𝐵) |