Proof of Theorem lediv23
Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → 𝐵 ∈ ℝ) |
2 | | gt0ne0 10372 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → 𝐵 ≠ 0) |
3 | 1, 2 | jca 553 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0)) |
4 | | redivcl 10623 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℝ) |
5 | 4 | 3expb 1258 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) ∈ ℝ) |
6 | 3, 5 | sylan2 490 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) → (𝐴 / 𝐵) ∈ ℝ) |
7 | 6 | 3adant3 1074 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ 𝐶 ∈ ℝ) → (𝐴 / 𝐵) ∈ ℝ) |
8 | | simp3 1056 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ) |
9 | | simp2 1055 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ 𝐶 ∈ ℝ) → (𝐵 ∈ ℝ ∧ 0 < 𝐵)) |
10 | | lemul1 10754 |
. . . 4
⊢ (((𝐴 / 𝐵) ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((𝐴 / 𝐵) ≤ 𝐶 ↔ ((𝐴 / 𝐵) · 𝐵) ≤ (𝐶 · 𝐵))) |
11 | 7, 8, 9, 10 | syl3anc 1318 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ 𝐶 ∈ ℝ) → ((𝐴 / 𝐵) ≤ 𝐶 ↔ ((𝐴 / 𝐵) · 𝐵) ≤ (𝐶 · 𝐵))) |
12 | 11 | 3adant3r 1315 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐵) ≤ 𝐶 ↔ ((𝐴 / 𝐵) · 𝐵) ≤ (𝐶 · 𝐵))) |
13 | | recn 9905 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
14 | 13 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) → 𝐴 ∈
ℂ) |
15 | | recn 9905 |
. . . . . 6
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
16 | 15 | ad2antrl 760 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) → 𝐵 ∈
ℂ) |
17 | 2 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) → 𝐵 ≠ 0) |
18 | 14, 16, 17 | divcan1d 10681 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) → ((𝐴 / 𝐵) · 𝐵) = 𝐴) |
19 | 18 | 3adant3 1074 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐵) · 𝐵) = 𝐴) |
20 | 19 | breq1d 4593 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (((𝐴 / 𝐵) · 𝐵) ≤ (𝐶 · 𝐵) ↔ 𝐴 ≤ (𝐶 · 𝐵))) |
21 | | remulcl 9900 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 · 𝐵) ∈ ℝ) |
22 | 21 | ancoms 468 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 · 𝐵) ∈ ℝ) |
23 | 22 | adantrr 749 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → (𝐶 · 𝐵) ∈ ℝ) |
24 | 23 | 3adant1 1072 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → (𝐶 · 𝐵) ∈ ℝ) |
25 | | lediv1 10767 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 · 𝐵) ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ (𝐶 · 𝐵) ↔ (𝐴 / 𝐶) ≤ ((𝐶 · 𝐵) / 𝐶))) |
26 | 24, 25 | syld3an2 1365 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → (𝐴 ≤ (𝐶 · 𝐵) ↔ (𝐴 / 𝐶) ≤ ((𝐶 · 𝐵) / 𝐶))) |
27 | | recn 9905 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℂ) |
28 | 27 | adantr 480 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ ∧ 0 <
𝐶) → 𝐶 ∈ ℂ) |
29 | | gt0ne0 10372 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ ∧ 0 <
𝐶) → 𝐶 ≠ 0) |
30 | 28, 29 | jca 553 |
. . . . . . 7
⊢ ((𝐶 ∈ ℝ ∧ 0 <
𝐶) → (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) |
31 | | divcan3 10590 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) → ((𝐶 · 𝐵) / 𝐶) = 𝐵) |
32 | 31 | 3expb 1258 |
. . . . . . 7
⊢ ((𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐶 · 𝐵) / 𝐶) = 𝐵) |
33 | 15, 30, 32 | syl2an 493 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → ((𝐶 · 𝐵) / 𝐶) = 𝐵) |
34 | 33 | 3adant1 1072 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → ((𝐶 · 𝐵) / 𝐶) = 𝐵) |
35 | 34 | breq2d 4595 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → ((𝐴 / 𝐶) ≤ ((𝐶 · 𝐵) / 𝐶) ↔ (𝐴 / 𝐶) ≤ 𝐵)) |
36 | 26, 35 | bitrd 267 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → (𝐴 ≤ (𝐶 · 𝐵) ↔ (𝐴 / 𝐶) ≤ 𝐵)) |
37 | 36 | 3adant2r 1313 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ (𝐶 · 𝐵) ↔ (𝐴 / 𝐶) ≤ 𝐵)) |
38 | 12, 20, 37 | 3bitrd 293 |
1
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐵) ≤ 𝐶 ↔ (𝐴 / 𝐶) ≤ 𝐵)) |