Proof of Theorem lt2mul2div
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | recn 11246 | . . . . . . . . 9
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℂ) | 
| 2 |  | recn 11246 | . . . . . . . . 9
⊢ (𝐷 ∈ ℝ → 𝐷 ∈
ℂ) | 
| 3 |  | mulcom 11242 | . . . . . . . . 9
⊢ ((𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (𝐶 · 𝐷) = (𝐷 · 𝐶)) | 
| 4 | 1, 2, 3 | syl2an 596 | . . . . . . . 8
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝐶 · 𝐷) = (𝐷 · 𝐶)) | 
| 5 | 4 | oveq1d 7447 | . . . . . . 7
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝐶 · 𝐷) / 𝐵) = ((𝐷 · 𝐶) / 𝐵)) | 
| 6 | 5 | adantl 481 | . . . . . 6
⊢ (((𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐶 · 𝐷) / 𝐵) = ((𝐷 · 𝐶) / 𝐵)) | 
| 7 | 2 | ad2antll 729 | . . . . . . 7
⊢ (((𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐷 ∈ ℂ) | 
| 8 | 1 | ad2antrl 728 | . . . . . . 7
⊢ (((𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐶 ∈ ℂ) | 
| 9 |  | recn 11246 | . . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) | 
| 10 | 9 | adantr 480 | . . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → 𝐵 ∈ ℂ) | 
| 11 |  | gt0ne0 11729 | . . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → 𝐵 ≠ 0) | 
| 12 | 10, 11 | jca 511 | . . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) | 
| 13 | 12 | adantr 480 | . . . . . . 7
⊢ (((𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) | 
| 14 |  | divass 11941 | . . . . . . 7
⊢ ((𝐷 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((𝐷 · 𝐶) / 𝐵) = (𝐷 · (𝐶 / 𝐵))) | 
| 15 | 7, 8, 13, 14 | syl3anc 1372 | . . . . . 6
⊢ (((𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐷 · 𝐶) / 𝐵) = (𝐷 · (𝐶 / 𝐵))) | 
| 16 | 6, 15 | eqtrd 2776 | . . . . 5
⊢ (((𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐶 · 𝐷) / 𝐵) = (𝐷 · (𝐶 / 𝐵))) | 
| 17 | 16 | adantrrr 725 | . . . 4
⊢ (((𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷))) → ((𝐶 · 𝐷) / 𝐵) = (𝐷 · (𝐶 / 𝐵))) | 
| 18 | 17 | adantll 714 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 <
𝐷))) → ((𝐶 · 𝐷) / 𝐵) = (𝐷 · (𝐶 / 𝐵))) | 
| 19 | 18 | breq2d 5154 | . 2
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 <
𝐷))) → (𝐴 < ((𝐶 · 𝐷) / 𝐵) ↔ 𝐴 < (𝐷 · (𝐶 / 𝐵)))) | 
| 20 |  | simpll 766 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 <
𝐷))) → 𝐴 ∈
ℝ) | 
| 21 |  | remulcl 11241 | . . . . 5
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝐶 · 𝐷) ∈ ℝ) | 
| 22 | 21 | adantrr 717 | . . . 4
⊢ ((𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 <
𝐷)) → (𝐶 · 𝐷) ∈ ℝ) | 
| 23 | 22 | adantl 481 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 <
𝐷))) → (𝐶 · 𝐷) ∈ ℝ) | 
| 24 |  | simplr 768 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 <
𝐷))) → (𝐵 ∈ ℝ ∧ 0 <
𝐵)) | 
| 25 |  | ltmuldiv 12142 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 · 𝐷) ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ 𝐴 < ((𝐶 · 𝐷) / 𝐵))) | 
| 26 | 20, 23, 24, 25 | syl3anc 1372 | . 2
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 <
𝐷))) → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ 𝐴 < ((𝐶 · 𝐷) / 𝐵))) | 
| 27 |  | simpl 482 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → 𝐵 ∈ ℝ) | 
| 28 | 27, 11 | jca 511 | . . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0)) | 
| 29 |  | redivcl 11987 | . . . . . . 7
⊢ ((𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐶 / 𝐵) ∈ ℝ) | 
| 30 | 29 | 3expb 1120 | . . . . . 6
⊢ ((𝐶 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0)) → (𝐶 / 𝐵) ∈ ℝ) | 
| 31 | 28, 30 | sylan2 593 | . . . . 5
⊢ ((𝐶 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) → (𝐶 / 𝐵) ∈ ℝ) | 
| 32 | 31 | ancoms 458 | . . . 4
⊢ (((𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ 𝐶 ∈ ℝ) → (𝐶 / 𝐵) ∈ ℝ) | 
| 33 | 32 | ad2ant2lr 748 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 <
𝐷))) → (𝐶 / 𝐵) ∈ ℝ) | 
| 34 |  | simprr 772 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 <
𝐷))) → (𝐷 ∈ ℝ ∧ 0 <
𝐷)) | 
| 35 |  | ltdivmul 12144 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ (𝐶 / 𝐵) ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷)) → ((𝐴 / 𝐷) < (𝐶 / 𝐵) ↔ 𝐴 < (𝐷 · (𝐶 / 𝐵)))) | 
| 36 | 20, 33, 34, 35 | syl3anc 1372 | . 2
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 <
𝐷))) → ((𝐴 / 𝐷) < (𝐶 / 𝐵) ↔ 𝐴 < (𝐷 · (𝐶 / 𝐵)))) | 
| 37 | 19, 26, 36 | 3bitr4d 311 | 1
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 <
𝐷))) → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ (𝐴 / 𝐷) < (𝐶 / 𝐵))) |