Proof of Theorem ltdiv2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ltrec 12151 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴))) | 
| 2 | 1 | 3adant3 1132 | . 2
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴))) | 
| 3 |  | gt0ne0 11729 | . . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → 𝐵 ≠ 0) | 
| 4 |  | rereccl 11986 | . . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (1 / 𝐵) ∈
ℝ) | 
| 5 | 3, 4 | syldan 591 | . . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → (1 / 𝐵) ∈
ℝ) | 
| 6 |  | gt0ne0 11729 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 𝐴 ≠ 0) | 
| 7 |  | rereccl 11986 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈
ℝ) | 
| 8 | 6, 7 | syldan 591 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (1 / 𝐴) ∈
ℝ) | 
| 9 |  | ltmul2 12119 | . . . . . 6
⊢ (((1 /
𝐵) ∈ ℝ ∧ (1
/ 𝐴) ∈ ℝ ∧
(𝐶 ∈ ℝ ∧ 0
< 𝐶)) → ((1 / 𝐵) < (1 / 𝐴) ↔ (𝐶 · (1 / 𝐵)) < (𝐶 · (1 / 𝐴)))) | 
| 10 | 8, 9 | syl3an2 1164 | . . . . 5
⊢ (((1 /
𝐵) ∈ ℝ ∧
(𝐴 ∈ ℝ ∧ 0
< 𝐴) ∧ (𝐶 ∈ ℝ ∧ 0 <
𝐶)) → ((1 / 𝐵) < (1 / 𝐴) ↔ (𝐶 · (1 / 𝐵)) < (𝐶 · (1 / 𝐴)))) | 
| 11 | 5, 10 | syl3an1 1163 | . . . 4
⊢ (((𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((1 / 𝐵) < (1 / 𝐴) ↔ (𝐶 · (1 / 𝐵)) < (𝐶 · (1 / 𝐴)))) | 
| 12 |  | recn 11246 | . . . . . . 7
⊢ (𝐶 ∈ ℝ → 𝐶 ∈
ℂ) | 
| 13 | 12 | adantr 480 | . . . . . 6
⊢ ((𝐶 ∈ ℝ ∧ 0 <
𝐶) → 𝐶 ∈ ℂ) | 
| 14 |  | recn 11246 | . . . . . . . 8
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) | 
| 15 | 14 | adantr 480 | . . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → 𝐵 ∈ ℂ) | 
| 16 | 15, 3 | jca 511 | . . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) | 
| 17 |  | recn 11246 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) | 
| 18 | 17 | adantr 480 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 𝐴 ∈ ℂ) | 
| 19 | 18, 6 | jca 511 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) | 
| 20 |  | divrec 11939 | . . . . . . . . 9
⊢ ((𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐶 / 𝐵) = (𝐶 · (1 / 𝐵))) | 
| 21 | 20 | 3expb 1120 | . . . . . . . 8
⊢ ((𝐶 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐶 / 𝐵) = (𝐶 · (1 / 𝐵))) | 
| 22 | 21 | 3adant3 1132 | . . . . . . 7
⊢ ((𝐶 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) → (𝐶 / 𝐵) = (𝐶 · (1 / 𝐵))) | 
| 23 |  | divrec 11939 | . . . . . . . . 9
⊢ ((𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝐶 / 𝐴) = (𝐶 · (1 / 𝐴))) | 
| 24 | 23 | 3expb 1120 | . . . . . . . 8
⊢ ((𝐶 ∈ ℂ ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) → (𝐶 / 𝐴) = (𝐶 · (1 / 𝐴))) | 
| 25 | 24 | 3adant2 1131 | . . . . . . 7
⊢ ((𝐶 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) → (𝐶 / 𝐴) = (𝐶 · (1 / 𝐴))) | 
| 26 | 22, 25 | breq12d 5155 | . . . . . 6
⊢ ((𝐶 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) → ((𝐶 / 𝐵) < (𝐶 / 𝐴) ↔ (𝐶 · (1 / 𝐵)) < (𝐶 · (1 / 𝐴)))) | 
| 27 | 13, 16, 19, 26 | syl3an 1160 | . . . . 5
⊢ (((𝐶 ∈ ℝ ∧ 0 <
𝐶) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → ((𝐶 / 𝐵) < (𝐶 / 𝐴) ↔ (𝐶 · (1 / 𝐵)) < (𝐶 · (1 / 𝐴)))) | 
| 28 | 27 | 3coml 1127 | . . . 4
⊢ (((𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 / 𝐵) < (𝐶 / 𝐴) ↔ (𝐶 · (1 / 𝐵)) < (𝐶 · (1 / 𝐴)))) | 
| 29 | 11, 28 | bitr4d 282 | . . 3
⊢ (((𝐵 ∈ ℝ ∧ 0 <
𝐵) ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((1 / 𝐵) < (1 / 𝐴) ↔ (𝐶 / 𝐵) < (𝐶 / 𝐴))) | 
| 30 | 29 | 3com12 1123 | . 2
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((1 / 𝐵) < (1 / 𝐴) ↔ (𝐶 / 𝐵) < (𝐶 / 𝐴))) | 
| 31 | 2, 30 | bitrd 279 | 1
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 < 𝐵 ↔ (𝐶 / 𝐵) < (𝐶 / 𝐴))) |