Proof of Theorem mulgt0b2d
Step | Hyp | Ref
| Expression |
1 | | mulgt0b2d.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | 1 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝐵) → 𝐴 ∈ ℝ) |
3 | | mulgt0b2d.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
4 | 3 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝐵) → 𝐵 ∈ ℝ) |
5 | | mulgt0b2d.1 |
. . . . 5
⊢ (𝜑 → 0 < 𝐴) |
6 | 5 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝐵) → 0 < 𝐴) |
7 | | simpr 485 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝐵) → 0 < 𝐵) |
8 | 2, 4, 6, 7 | mulgt0d 11310 |
. . 3
⊢ ((𝜑 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)) |
9 | 8 | ex 413 |
. 2
⊢ (𝜑 → (0 < 𝐵 → 0 < (𝐴 · 𝐵))) |
10 | 1 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ((𝐴 · 𝐵) · (0 −ℝ 1))
< 0) → 𝐴 ∈
ℝ) |
11 | | 1re 11155 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
12 | | rernegcl 40826 |
. . . . . . . 8
⊢ (1 ∈
ℝ → (0 −ℝ 1) ∈ ℝ) |
13 | 11, 12 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → (0
−ℝ 1) ∈ ℝ) |
14 | 3, 13 | remulcld 11185 |
. . . . . 6
⊢ (𝜑 → (𝐵 · (0 −ℝ 1))
∈ ℝ) |
15 | 14 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ((𝐴 · 𝐵) · (0 −ℝ 1))
< 0) → (𝐵 ·
(0 −ℝ 1)) ∈ ℝ) |
16 | 5 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ((𝐴 · 𝐵) · (0 −ℝ 1))
< 0) → 0 < 𝐴) |
17 | 1 | recnd 11183 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
18 | 3 | recnd 11183 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) |
19 | 13 | recnd 11183 |
. . . . . . . 8
⊢ (𝜑 → (0
−ℝ 1) ∈ ℂ) |
20 | 17, 18, 19 | mulassd 11178 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 · 𝐵) · (0 −ℝ 1))
= (𝐴 · (𝐵 · (0
−ℝ 1)))) |
21 | 20 | breq1d 5115 |
. . . . . 6
⊢ (𝜑 → (((𝐴 · 𝐵) · (0 −ℝ 1))
< 0 ↔ (𝐴 ·
(𝐵 · (0
−ℝ 1))) < 0)) |
22 | 21 | biimpa 477 |
. . . . 5
⊢ ((𝜑 ∧ ((𝐴 · 𝐵) · (0 −ℝ 1))
< 0) → (𝐴 ·
(𝐵 · (0
−ℝ 1))) < 0) |
23 | 10, 15, 16, 22 | mulgt0con2d 40914 |
. . . 4
⊢ ((𝜑 ∧ ((𝐴 · 𝐵) · (0 −ℝ 1))
< 0) → (𝐵 ·
(0 −ℝ 1)) < 0) |
24 | 23 | ex 413 |
. . 3
⊢ (𝜑 → (((𝐴 · 𝐵) · (0 −ℝ 1))
< 0 → (𝐵 ·
(0 −ℝ 1)) < 0)) |
25 | 1, 3 | remulcld 11185 |
. . . . 5
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ) |
26 | | relt0neg2 40900 |
. . . . 5
⊢ ((𝐴 · 𝐵) ∈ ℝ → (0 < (𝐴 · 𝐵) ↔ (0 −ℝ (𝐴 · 𝐵)) < 0)) |
27 | 25, 26 | syl 17 |
. . . 4
⊢ (𝜑 → (0 < (𝐴 · 𝐵) ↔ (0 −ℝ (𝐴 · 𝐵)) < 0)) |
28 | | 1red 11156 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℝ) |
29 | 25, 28 | remulneg2d 40869 |
. . . . . 6
⊢ (𝜑 → ((𝐴 · 𝐵) · (0 −ℝ 1))
= (0 −ℝ ((𝐴 · 𝐵) · 1))) |
30 | | ax-1rid 11121 |
. . . . . . . 8
⊢ ((𝐴 · 𝐵) ∈ ℝ → ((𝐴 · 𝐵) · 1) = (𝐴 · 𝐵)) |
31 | 25, 30 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 · 𝐵) · 1) = (𝐴 · 𝐵)) |
32 | 31 | oveq2d 7373 |
. . . . . 6
⊢ (𝜑 → (0
−ℝ ((𝐴 · 𝐵) · 1)) = (0
−ℝ (𝐴 · 𝐵))) |
33 | 29, 32 | eqtrd 2776 |
. . . . 5
⊢ (𝜑 → ((𝐴 · 𝐵) · (0 −ℝ 1))
= (0 −ℝ (𝐴 · 𝐵))) |
34 | 33 | breq1d 5115 |
. . . 4
⊢ (𝜑 → (((𝐴 · 𝐵) · (0 −ℝ 1))
< 0 ↔ (0 −ℝ (𝐴 · 𝐵)) < 0)) |
35 | 27, 34 | bitr4d 281 |
. . 3
⊢ (𝜑 → (0 < (𝐴 · 𝐵) ↔ ((𝐴 · 𝐵) · (0 −ℝ 1))
< 0)) |
36 | | relt0neg2 40900 |
. . . . 5
⊢ (𝐵 ∈ ℝ → (0 <
𝐵 ↔ (0
−ℝ 𝐵) < 0)) |
37 | 3, 36 | syl 17 |
. . . 4
⊢ (𝜑 → (0 < 𝐵 ↔ (0 −ℝ 𝐵) < 0)) |
38 | 3, 28 | remulneg2d 40869 |
. . . . . 6
⊢ (𝜑 → (𝐵 · (0 −ℝ 1)) =
(0 −ℝ (𝐵 · 1))) |
39 | | ax-1rid 11121 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → (𝐵 · 1) = 𝐵) |
40 | 3, 39 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐵 · 1) = 𝐵) |
41 | 40 | oveq2d 7373 |
. . . . . 6
⊢ (𝜑 → (0
−ℝ (𝐵 · 1)) = (0 −ℝ
𝐵)) |
42 | 38, 41 | eqtrd 2776 |
. . . . 5
⊢ (𝜑 → (𝐵 · (0 −ℝ 1)) =
(0 −ℝ 𝐵)) |
43 | 42 | breq1d 5115 |
. . . 4
⊢ (𝜑 → ((𝐵 · (0 −ℝ 1))
< 0 ↔ (0 −ℝ 𝐵) < 0)) |
44 | 37, 43 | bitr4d 281 |
. . 3
⊢ (𝜑 → (0 < 𝐵 ↔ (𝐵 · (0 −ℝ 1))
< 0)) |
45 | 24, 35, 44 | 3imtr4d 293 |
. 2
⊢ (𝜑 → (0 < (𝐴 · 𝐵) → 0 < 𝐵)) |
46 | 9, 45 | impbid 211 |
1
⊢ (𝜑 → (0 < 𝐵 ↔ 0 < (𝐴 · 𝐵))) |