Proof of Theorem ledivdiv
| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → 𝐵 ∈ ℝ) |
| 2 | | gt0ne0 11728 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → 𝐵 ≠ 0) |
| 3 | 1, 2 | jca 511 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0)) |
| 4 | | redivcl 11986 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℝ) |
| 5 | 4 | 3expb 1121 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) ∈ ℝ) |
| 6 | 3, 5 | sylan2 593 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) → (𝐴 / 𝐵) ∈ ℝ) |
| 7 | 6 | adantlr 715 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 / 𝐵) ∈ ℝ) |
| 8 | | divgt0 12136 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 < (𝐴 / 𝐵)) |
| 9 | 7, 8 | jca 511 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((𝐴 / 𝐵) ∈ ℝ ∧ 0 < (𝐴 / 𝐵))) |
| 10 | | simpl 482 |
. . . . . . 7
⊢ ((𝐷 ∈ ℝ ∧ 0 <
𝐷) → 𝐷 ∈ ℝ) |
| 11 | | gt0ne0 11728 |
. . . . . . 7
⊢ ((𝐷 ∈ ℝ ∧ 0 <
𝐷) → 𝐷 ≠ 0) |
| 12 | 10, 11 | jca 511 |
. . . . . 6
⊢ ((𝐷 ∈ ℝ ∧ 0 <
𝐷) → (𝐷 ∈ ℝ ∧ 𝐷 ≠ 0)) |
| 13 | | redivcl 11986 |
. . . . . . 7
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ∧ 𝐷 ≠ 0) → (𝐶 / 𝐷) ∈ ℝ) |
| 14 | 13 | 3expb 1121 |
. . . . . 6
⊢ ((𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 𝐷 ≠ 0)) → (𝐶 / 𝐷) ∈ ℝ) |
| 15 | 12, 14 | sylan2 593 |
. . . . 5
⊢ ((𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 <
𝐷)) → (𝐶 / 𝐷) ∈ ℝ) |
| 16 | 15 | adantlr 715 |
. . . 4
⊢ (((𝐶 ∈ ℝ ∧ 0 <
𝐶) ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷)) → (𝐶 / 𝐷) ∈ ℝ) |
| 17 | | divgt0 12136 |
. . . 4
⊢ (((𝐶 ∈ ℝ ∧ 0 <
𝐶) ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷)) → 0 < (𝐶 / 𝐷)) |
| 18 | 16, 17 | jca 511 |
. . 3
⊢ (((𝐶 ∈ ℝ ∧ 0 <
𝐶) ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷)) → ((𝐶 / 𝐷) ∈ ℝ ∧ 0 < (𝐶 / 𝐷))) |
| 19 | | lerec 12151 |
. . 3
⊢ ((((𝐴 / 𝐵) ∈ ℝ ∧ 0 < (𝐴 / 𝐵)) ∧ ((𝐶 / 𝐷) ∈ ℝ ∧ 0 < (𝐶 / 𝐷))) → ((𝐴 / 𝐵) ≤ (𝐶 / 𝐷) ↔ (1 / (𝐶 / 𝐷)) ≤ (1 / (𝐴 / 𝐵)))) |
| 20 | 9, 18, 19 | syl2an 596 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 0 < 𝐶) ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷))) → ((𝐴 / 𝐵) ≤ (𝐶 / 𝐷) ↔ (1 / (𝐶 / 𝐷)) ≤ (1 / (𝐴 / 𝐵)))) |
| 21 | | recn 11245 |
. . . . . 6
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℂ) |
| 22 | 21 | adantr 480 |
. . . . 5
⊢ ((𝐶 ∈ ℝ ∧ 0 <
𝐶) → 𝐶 ∈ ℂ) |
| 23 | | gt0ne0 11728 |
. . . . 5
⊢ ((𝐶 ∈ ℝ ∧ 0 <
𝐶) → 𝐶 ≠ 0) |
| 24 | 22, 23 | jca 511 |
. . . 4
⊢ ((𝐶 ∈ ℝ ∧ 0 <
𝐶) → (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) |
| 25 | | recn 11245 |
. . . . . 6
⊢ (𝐷 ∈ ℝ → 𝐷 ∈
ℂ) |
| 26 | 25 | adantr 480 |
. . . . 5
⊢ ((𝐷 ∈ ℝ ∧ 0 <
𝐷) → 𝐷 ∈ ℂ) |
| 27 | 26, 11 | jca 511 |
. . . 4
⊢ ((𝐷 ∈ ℝ ∧ 0 <
𝐷) → (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0)) |
| 28 | | recdiv 11973 |
. . . 4
⊢ (((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0)) → (1 / (𝐶 / 𝐷)) = (𝐷 / 𝐶)) |
| 29 | 24, 27, 28 | syl2an 596 |
. . 3
⊢ (((𝐶 ∈ ℝ ∧ 0 <
𝐶) ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷)) → (1 / (𝐶 / 𝐷)) = (𝐷 / 𝐶)) |
| 30 | | recn 11245 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
| 31 | 30 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 𝐴 ∈ ℂ) |
| 32 | | gt0ne0 11728 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 𝐴 ≠ 0) |
| 33 | 31, 32 | jca 511 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) |
| 34 | | recn 11245 |
. . . . . 6
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
| 35 | 34 | adantr 480 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → 𝐵 ∈ ℂ) |
| 36 | 35, 2 | jca 511 |
. . . 4
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) |
| 37 | | recdiv 11973 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (1 / (𝐴 / 𝐵)) = (𝐵 / 𝐴)) |
| 38 | 33, 36, 37 | syl2an 596 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (1 / (𝐴 / 𝐵)) = (𝐵 / 𝐴)) |
| 39 | 29, 38 | breqan12rd 5160 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 0 < 𝐶) ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷))) → ((1 / (𝐶 / 𝐷)) ≤ (1 / (𝐴 / 𝐵)) ↔ (𝐷 / 𝐶) ≤ (𝐵 / 𝐴))) |
| 40 | 20, 39 | bitrd 279 |
1
⊢ ((((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 0 < 𝐶) ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷))) → ((𝐴 / 𝐵) ≤ (𝐶 / 𝐷) ↔ (𝐷 / 𝐶) ≤ (𝐵 / 𝐴))) |