Proof of Theorem lediv12a
Step | Hyp | Ref
| Expression |
1 | | simplrr 506 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 𝐴 ≤ 𝐵) |
2 | | simprrr 510 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 𝐶 ≤ 𝐷) |
3 | | simprll 507 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 𝐶 ∈ ℝ) |
4 | | simprrl 509 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 0 < 𝐶) |
5 | | simprlr 508 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 𝐷 ∈ ℝ) |
6 | | 0red 7639 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 0 ∈
ℝ) |
7 | 6, 3, 5, 4, 2 | ltletrd 8052 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 0 < 𝐷) |
8 | | lerec 8500 |
. . . . 5
⊢ (((𝐶 ∈ ℝ ∧ 0 <
𝐶) ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷)) → (𝐶 ≤ 𝐷 ↔ (1 / 𝐷) ≤ (1 / 𝐶))) |
9 | 3, 4, 5, 7, 8 | syl22anc 1185 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → (𝐶 ≤ 𝐷 ↔ (1 / 𝐷) ≤ (1 / 𝐶))) |
10 | 2, 9 | mpbid 146 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → (1 / 𝐷) ≤ (1 / 𝐶)) |
11 | | simplll 503 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 𝐴 ∈ ℝ) |
12 | | simplrl 505 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 0 ≤ 𝐴) |
13 | 11, 12 | jca 302 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) |
14 | | simpllr 504 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 𝐵 ∈ ℝ) |
15 | 5, 7 | gt0ap0d 8257 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 𝐷 # 0) |
16 | 5, 15 | rerecclapd 8454 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → (1 / 𝐷) ∈ ℝ) |
17 | | recgt0 8466 |
. . . . . . 7
⊢ ((𝐷 ∈ ℝ ∧ 0 <
𝐷) → 0 < (1 / 𝐷)) |
18 | 5, 7, 17 | syl2anc 406 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 0 < (1 / 𝐷)) |
19 | 6, 16, 18 | ltled 7752 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 0 ≤ (1 / 𝐷)) |
20 | 16, 19 | jca 302 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → ((1 / 𝐷) ∈ ℝ ∧ 0 ≤ (1 / 𝐷))) |
21 | 3, 4 | gt0ap0d 8257 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 𝐶 # 0) |
22 | 3, 21 | rerecclapd 8454 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → (1 / 𝐶) ∈ ℝ) |
23 | | lemul12a 8478 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℝ) ∧ (((1 / 𝐷) ∈ ℝ ∧ 0 ≤ (1
/ 𝐷)) ∧ (1 / 𝐶) ∈ ℝ)) →
((𝐴 ≤ 𝐵 ∧ (1 / 𝐷) ≤ (1 / 𝐶)) → (𝐴 · (1 / 𝐷)) ≤ (𝐵 · (1 / 𝐶)))) |
24 | 13, 14, 20, 22, 23 | syl22anc 1185 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → ((𝐴 ≤ 𝐵 ∧ (1 / 𝐷) ≤ (1 / 𝐶)) → (𝐴 · (1 / 𝐷)) ≤ (𝐵 · (1 / 𝐶)))) |
25 | 1, 10, 24 | mp2and 427 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → (𝐴 · (1 / 𝐷)) ≤ (𝐵 · (1 / 𝐶))) |
26 | 11 | recnd 7666 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 𝐴 ∈ ℂ) |
27 | 5 | recnd 7666 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 𝐷 ∈ ℂ) |
28 | 26, 27, 15 | divrecapd 8414 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → (𝐴 / 𝐷) = (𝐴 · (1 / 𝐷))) |
29 | 14 | recnd 7666 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 𝐵 ∈ ℂ) |
30 | 3 | recnd 7666 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → 𝐶 ∈ ℂ) |
31 | 29, 30, 21 | divrecapd 8414 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → (𝐵 / 𝐶) = (𝐵 · (1 / 𝐶))) |
32 | 25, 28, 31 | 3brtr4d 3905 |
1
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 < 𝐶 ∧ 𝐶 ≤ 𝐷))) → (𝐴 / 𝐷) ≤ (𝐵 / 𝐶)) |