Proof of Theorem lemul12b
Step | Hyp | Ref
| Expression |
1 | | lemul2a 11585 |
. . . . . . . . 9
⊢ (((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 ≤
𝐴)) ∧ 𝐶 ≤ 𝐷) → (𝐴 · 𝐶) ≤ (𝐴 · 𝐷)) |
2 | 1 | ex 416 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 ≤
𝐴)) → (𝐶 ≤ 𝐷 → (𝐴 · 𝐶) ≤ (𝐴 · 𝐷))) |
3 | 2 | 3comr 1126 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝐶 ≤ 𝐷 → (𝐴 · 𝐶) ≤ (𝐴 · 𝐷))) |
4 | 3 | 3expb 1121 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐶 ≤ 𝐷 → (𝐴 · 𝐶) ≤ (𝐴 · 𝐷))) |
5 | 4 | adantrrr 725 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))) → (𝐶 ≤ 𝐷 → (𝐴 · 𝐶) ≤ (𝐴 · 𝐷))) |
6 | 5 | adantlr 715 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))) → (𝐶 ≤ 𝐷 → (𝐴 · 𝐶) ≤ (𝐴 · 𝐷))) |
7 | | lemul1a 11584 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤
𝐷)) ∧ 𝐴 ≤ 𝐵) → (𝐴 · 𝐷) ≤ (𝐵 · 𝐷)) |
8 | 7 | ex 416 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤
𝐷)) → (𝐴 ≤ 𝐵 → (𝐴 · 𝐷) ≤ (𝐵 · 𝐷))) |
9 | 8 | ad4ant134 1175 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℝ) ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷)) → (𝐴 ≤ 𝐵 → (𝐴 · 𝐷) ≤ (𝐵 · 𝐷))) |
10 | 9 | adantrl 716 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))) → (𝐴 ≤ 𝐵 → (𝐴 · 𝐷) ≤ (𝐵 · 𝐷))) |
11 | 6, 10 | anim12d 612 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))) → ((𝐶 ≤ 𝐷 ∧ 𝐴 ≤ 𝐵) → ((𝐴 · 𝐶) ≤ (𝐴 · 𝐷) ∧ (𝐴 · 𝐷) ≤ (𝐵 · 𝐷)))) |
12 | 11 | ancomsd 469 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))) → ((𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷) → ((𝐴 · 𝐶) ≤ (𝐴 · 𝐷) ∧ (𝐴 · 𝐷) ≤ (𝐵 · 𝐷)))) |
13 | | remulcl 10712 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐶) ∈ ℝ) |
14 | 13 | adantlr 715 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐶 ∈ ℝ) → (𝐴 · 𝐶) ∈ ℝ) |
15 | 14 | ad2ant2r 747 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))) → (𝐴 · 𝐶) ∈ ℝ) |
16 | | remulcl 10712 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝐴 · 𝐷) ∈ ℝ) |
17 | 16 | ad2ant2r 747 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷)) → (𝐴 · 𝐷) ∈ ℝ) |
18 | 17 | ad2ant2rl 749 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))) → (𝐴 · 𝐷) ∈ ℝ) |
19 | | remulcl 10712 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝐵 · 𝐷) ∈ ℝ) |
20 | 19 | adantrr 717 |
. . . 4
⊢ ((𝐵 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤
𝐷)) → (𝐵 · 𝐷) ∈ ℝ) |
21 | 20 | ad2ant2l 746 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))) → (𝐵 · 𝐷) ∈ ℝ) |
22 | | letr 10824 |
. . 3
⊢ (((𝐴 · 𝐶) ∈ ℝ ∧ (𝐴 · 𝐷) ∈ ℝ ∧ (𝐵 · 𝐷) ∈ ℝ) → (((𝐴 · 𝐶) ≤ (𝐴 · 𝐷) ∧ (𝐴 · 𝐷) ≤ (𝐵 · 𝐷)) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷))) |
23 | 15, 18, 21, 22 | syl3anc 1372 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))) → (((𝐴 · 𝐶) ≤ (𝐴 · 𝐷) ∧ (𝐴 · 𝐷) ≤ (𝐵 · 𝐷)) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷))) |
24 | 12, 23 | syld 47 |
1
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))) → ((𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷))) |