Proof of Theorem mulgt0b2d
Step | Hyp | Ref
| Expression |
1 | | mulgt0b2d.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | 1 | adantr 485 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝐵) → 𝐴 ∈ ℝ) |
3 | | mulgt0b2d.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
4 | 3 | adantr 485 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝐵) → 𝐵 ∈ ℝ) |
5 | | mulgt0b2d.1 |
. . . . 5
⊢ (𝜑 → 0 < 𝐴) |
6 | 5 | adantr 485 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝐵) → 0 < 𝐴) |
7 | | simpr 489 |
. . . 4
⊢ ((𝜑 ∧ 0 < 𝐵) → 0 < 𝐵) |
8 | 2, 4, 6, 7 | mulgt0d 10818 |
. . 3
⊢ ((𝜑 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)) |
9 | 8 | ex 417 |
. 2
⊢ (𝜑 → (0 < 𝐵 → 0 < (𝐴 · 𝐵))) |
10 | 1 | adantr 485 |
. . . . 5
⊢ ((𝜑 ∧ ((𝐴 · 𝐵) · (0 −ℝ 1))
< 0) → 𝐴 ∈
ℝ) |
11 | | 1re 10664 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
12 | | rernegcl 39836 |
. . . . . . . 8
⊢ (1 ∈
ℝ → (0 −ℝ 1) ∈ ℝ) |
13 | 11, 12 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → (0
−ℝ 1) ∈ ℝ) |
14 | 3, 13 | remulcld 10694 |
. . . . . 6
⊢ (𝜑 → (𝐵 · (0 −ℝ 1))
∈ ℝ) |
15 | 14 | adantr 485 |
. . . . 5
⊢ ((𝜑 ∧ ((𝐴 · 𝐵) · (0 −ℝ 1))
< 0) → (𝐵 ·
(0 −ℝ 1)) ∈ ℝ) |
16 | 5 | adantr 485 |
. . . . 5
⊢ ((𝜑 ∧ ((𝐴 · 𝐵) · (0 −ℝ 1))
< 0) → 0 < 𝐴) |
17 | 1 | recnd 10692 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
18 | 3 | recnd 10692 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) |
19 | 13 | recnd 10692 |
. . . . . . . 8
⊢ (𝜑 → (0
−ℝ 1) ∈ ℂ) |
20 | 17, 18, 19 | mulassd 10687 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 · 𝐵) · (0 −ℝ 1))
= (𝐴 · (𝐵 · (0
−ℝ 1)))) |
21 | 20 | breq1d 5035 |
. . . . . 6
⊢ (𝜑 → (((𝐴 · 𝐵) · (0 −ℝ 1))
< 0 ↔ (𝐴 ·
(𝐵 · (0
−ℝ 1))) < 0)) |
22 | 21 | biimpa 481 |
. . . . 5
⊢ ((𝜑 ∧ ((𝐴 · 𝐵) · (0 −ℝ 1))
< 0) → (𝐴 ·
(𝐵 · (0
−ℝ 1))) < 0) |
23 | 10, 15, 16, 22 | mulgt0con2d 39911 |
. . . 4
⊢ ((𝜑 ∧ ((𝐴 · 𝐵) · (0 −ℝ 1))
< 0) → (𝐵 ·
(0 −ℝ 1)) < 0) |
24 | 23 | ex 417 |
. . 3
⊢ (𝜑 → (((𝐴 · 𝐵) · (0 −ℝ 1))
< 0 → (𝐵 ·
(0 −ℝ 1)) < 0)) |
25 | 1, 3 | remulcld 10694 |
. . . . 5
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ) |
26 | | relt0neg2 39908 |
. . . . 5
⊢ ((𝐴 · 𝐵) ∈ ℝ → (0 < (𝐴 · 𝐵) ↔ (0 −ℝ (𝐴 · 𝐵)) < 0)) |
27 | 25, 26 | syl 17 |
. . . 4
⊢ (𝜑 → (0 < (𝐴 · 𝐵) ↔ (0 −ℝ (𝐴 · 𝐵)) < 0)) |
28 | | 0red 10667 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) |
29 | | 1red 10665 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℝ) |
30 | | resubdi 39861 |
. . . . . . 7
⊢ (((𝐴 · 𝐵) ∈ ℝ ∧ 0 ∈ ℝ
∧ 1 ∈ ℝ) → ((𝐴 · 𝐵) · (0 −ℝ 1))
= (((𝐴 · 𝐵) · 0)
−ℝ ((𝐴 · 𝐵) · 1))) |
31 | 25, 28, 29, 30 | syl3anc 1369 |
. . . . . 6
⊢ (𝜑 → ((𝐴 · 𝐵) · (0 −ℝ 1))
= (((𝐴 · 𝐵) · 0)
−ℝ ((𝐴 · 𝐵) · 1))) |
32 | | remul01 39872 |
. . . . . . . 8
⊢ ((𝐴 · 𝐵) ∈ ℝ → ((𝐴 · 𝐵) · 0) = 0) |
33 | | ax-1rid 10630 |
. . . . . . . 8
⊢ ((𝐴 · 𝐵) ∈ ℝ → ((𝐴 · 𝐵) · 1) = (𝐴 · 𝐵)) |
34 | 32, 33 | oveq12d 7161 |
. . . . . . 7
⊢ ((𝐴 · 𝐵) ∈ ℝ → (((𝐴 · 𝐵) · 0) −ℝ
((𝐴 · 𝐵) · 1)) = (0
−ℝ (𝐴 · 𝐵))) |
35 | 25, 34 | syl 17 |
. . . . . 6
⊢ (𝜑 → (((𝐴 · 𝐵) · 0) −ℝ
((𝐴 · 𝐵) · 1)) = (0
−ℝ (𝐴 · 𝐵))) |
36 | 31, 35 | eqtrd 2794 |
. . . . 5
⊢ (𝜑 → ((𝐴 · 𝐵) · (0 −ℝ 1))
= (0 −ℝ (𝐴 · 𝐵))) |
37 | 36 | breq1d 5035 |
. . . 4
⊢ (𝜑 → (((𝐴 · 𝐵) · (0 −ℝ 1))
< 0 ↔ (0 −ℝ (𝐴 · 𝐵)) < 0)) |
38 | 27, 37 | bitr4d 285 |
. . 3
⊢ (𝜑 → (0 < (𝐴 · 𝐵) ↔ ((𝐴 · 𝐵) · (0 −ℝ 1))
< 0)) |
39 | | relt0neg2 39908 |
. . . . 5
⊢ (𝐵 ∈ ℝ → (0 <
𝐵 ↔ (0
−ℝ 𝐵) < 0)) |
40 | 3, 39 | syl 17 |
. . . 4
⊢ (𝜑 → (0 < 𝐵 ↔ (0 −ℝ 𝐵) < 0)) |
41 | | resubdi 39861 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 0 ∈
ℝ ∧ 1 ∈ ℝ) → (𝐵 · (0 −ℝ 1)) =
((𝐵 · 0)
−ℝ (𝐵 · 1))) |
42 | 3, 28, 29, 41 | syl3anc 1369 |
. . . . . 6
⊢ (𝜑 → (𝐵 · (0 −ℝ 1)) =
((𝐵 · 0)
−ℝ (𝐵 · 1))) |
43 | | remul01 39872 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → (𝐵 · 0) =
0) |
44 | | ax-1rid 10630 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → (𝐵 · 1) = 𝐵) |
45 | 43, 44 | oveq12d 7161 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ → ((𝐵 · 0)
−ℝ (𝐵 · 1)) = (0 −ℝ
𝐵)) |
46 | 3, 45 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝐵 · 0) −ℝ
(𝐵 · 1)) = (0
−ℝ 𝐵)) |
47 | 42, 46 | eqtrd 2794 |
. . . . 5
⊢ (𝜑 → (𝐵 · (0 −ℝ 1)) =
(0 −ℝ 𝐵)) |
48 | 47 | breq1d 5035 |
. . . 4
⊢ (𝜑 → ((𝐵 · (0 −ℝ 1))
< 0 ↔ (0 −ℝ 𝐵) < 0)) |
49 | 40, 48 | bitr4d 285 |
. . 3
⊢ (𝜑 → (0 < 𝐵 ↔ (𝐵 · (0 −ℝ 1))
< 0)) |
50 | 24, 38, 49 | 3imtr4d 298 |
. 2
⊢ (𝜑 → (0 < (𝐴 · 𝐵) → 0 < 𝐵)) |
51 | 9, 50 | impbid 215 |
1
⊢ (𝜑 → (0 < 𝐵 ↔ 0 < (𝐴 · 𝐵))) |