Proof of Theorem mul2lt0bi
Step | Hyp | Ref
| Expression |
1 | | mul2lt0.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | mul2lt0.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | 1, 2 | remulcld 11005 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ) |
4 | | 0red 10978 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ) |
5 | 3, 4 | ltnled 11122 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 · 𝐵) < 0 ↔ ¬ 0 ≤ (𝐴 · 𝐵))) |
6 | 1 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 𝐴 ∈ ℝ) |
7 | 2 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 𝐵 ∈ ℝ) |
8 | | simprl 768 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ 𝐴) |
9 | | simprr 770 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ 𝐵) |
10 | 6, 7, 8, 9 | mulge0d 11552 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 · 𝐵)) |
11 | 10 | ex 413 |
. . . . . . . 8
⊢ (𝜑 → ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → 0 ≤ (𝐴 · 𝐵))) |
12 | 11 | con3d 152 |
. . . . . . 7
⊢ (𝜑 → (¬ 0 ≤ (𝐴 · 𝐵) → ¬ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵))) |
13 | 5, 12 | sylbid 239 |
. . . . . 6
⊢ (𝜑 → ((𝐴 · 𝐵) < 0 → ¬ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵))) |
14 | | ianor 979 |
. . . . . 6
⊢ (¬ (0
≤ 𝐴 ∧ 0 ≤ 𝐵) ↔ (¬ 0 ≤ 𝐴 ∨ ¬ 0 ≤ 𝐵)) |
15 | 13, 14 | syl6ib 250 |
. . . . 5
⊢ (𝜑 → ((𝐴 · 𝐵) < 0 → (¬ 0 ≤ 𝐴 ∨ ¬ 0 ≤ 𝐵))) |
16 | 1, 4 | ltnled 11122 |
. . . . . 6
⊢ (𝜑 → (𝐴 < 0 ↔ ¬ 0 ≤ 𝐴)) |
17 | 2, 4 | ltnled 11122 |
. . . . . 6
⊢ (𝜑 → (𝐵 < 0 ↔ ¬ 0 ≤ 𝐵)) |
18 | 16, 17 | orbi12d 916 |
. . . . 5
⊢ (𝜑 → ((𝐴 < 0 ∨ 𝐵 < 0) ↔ (¬ 0 ≤ 𝐴 ∨ ¬ 0 ≤ 𝐵))) |
19 | 15, 18 | sylibrd 258 |
. . . 4
⊢ (𝜑 → ((𝐴 · 𝐵) < 0 → (𝐴 < 0 ∨ 𝐵 < 0))) |
20 | 19 | imp 407 |
. . 3
⊢ ((𝜑 ∧ (𝐴 · 𝐵) < 0) → (𝐴 < 0 ∨ 𝐵 < 0)) |
21 | | simpr 485 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 < 0) → 𝐴 < 0) |
22 | 1 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 · 𝐵) < 0) → 𝐴 ∈ ℝ) |
23 | 2 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 · 𝐵) < 0) → 𝐵 ∈ ℝ) |
24 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴 · 𝐵) < 0) → (𝐴 · 𝐵) < 0) |
25 | 22, 23, 24 | mul2lt0llt0 12834 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 < 0) → 0 < 𝐵) |
26 | 21, 25 | jca 512 |
. . . . 5
⊢ (((𝜑 ∧ (𝐴 · 𝐵) < 0) ∧ 𝐴 < 0) → (𝐴 < 0 ∧ 0 < 𝐵)) |
27 | 26 | ex 413 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 · 𝐵) < 0) → (𝐴 < 0 → (𝐴 < 0 ∧ 0 < 𝐵))) |
28 | 22, 23, 24 | mul2lt0rlt0 12832 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐴 · 𝐵) < 0) ∧ 𝐵 < 0) → 0 < 𝐴) |
29 | | simpr 485 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐴 · 𝐵) < 0) ∧ 𝐵 < 0) → 𝐵 < 0) |
30 | 28, 29 | jca 512 |
. . . . 5
⊢ (((𝜑 ∧ (𝐴 · 𝐵) < 0) ∧ 𝐵 < 0) → (0 < 𝐴 ∧ 𝐵 < 0)) |
31 | 30 | ex 413 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 · 𝐵) < 0) → (𝐵 < 0 → (0 < 𝐴 ∧ 𝐵 < 0))) |
32 | 27, 31 | orim12d 962 |
. . 3
⊢ ((𝜑 ∧ (𝐴 · 𝐵) < 0) → ((𝐴 < 0 ∨ 𝐵 < 0) → ((𝐴 < 0 ∧ 0 < 𝐵) ∨ (0 < 𝐴 ∧ 𝐵 < 0)))) |
33 | 20, 32 | mpd 15 |
. 2
⊢ ((𝜑 ∧ (𝐴 · 𝐵) < 0) → ((𝐴 < 0 ∧ 0 < 𝐵) ∨ (0 < 𝐴 ∧ 𝐵 < 0))) |
34 | 1 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 < 0 ∧ 0 < 𝐵)) → 𝐴 ∈ ℝ) |
35 | | 0red 10978 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 < 0 ∧ 0 < 𝐵)) → 0 ∈ ℝ) |
36 | 2 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 < 0 ∧ 0 < 𝐵)) → 𝐵 ∈ ℝ) |
37 | | simprr 770 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐴 < 0 ∧ 0 < 𝐵)) → 0 < 𝐵) |
38 | 36, 37 | elrpd 12769 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 < 0 ∧ 0 < 𝐵)) → 𝐵 ∈
ℝ+) |
39 | | simprl 768 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 < 0 ∧ 0 < 𝐵)) → 𝐴 < 0) |
40 | 34, 35, 38, 39 | ltmul1dd 12827 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 < 0 ∧ 0 < 𝐵)) → (𝐴 · 𝐵) < (0 · 𝐵)) |
41 | 36 | recnd 11003 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 < 0 ∧ 0 < 𝐵)) → 𝐵 ∈ ℂ) |
42 | 41 | mul02d 11173 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 < 0 ∧ 0 < 𝐵)) → (0 · 𝐵) = 0) |
43 | 40, 42 | breqtrd 5100 |
. . 3
⊢ ((𝜑 ∧ (𝐴 < 0 ∧ 0 < 𝐵)) → (𝐴 · 𝐵) < 0) |
44 | 2 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (0 < 𝐴 ∧ 𝐵 < 0)) → 𝐵 ∈ ℝ) |
45 | | 0red 10978 |
. . . . 5
⊢ ((𝜑 ∧ (0 < 𝐴 ∧ 𝐵 < 0)) → 0 ∈
ℝ) |
46 | 1 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (0 < 𝐴 ∧ 𝐵 < 0)) → 𝐴 ∈ ℝ) |
47 | | simprl 768 |
. . . . . 6
⊢ ((𝜑 ∧ (0 < 𝐴 ∧ 𝐵 < 0)) → 0 < 𝐴) |
48 | 46, 47 | elrpd 12769 |
. . . . 5
⊢ ((𝜑 ∧ (0 < 𝐴 ∧ 𝐵 < 0)) → 𝐴 ∈
ℝ+) |
49 | | simprr 770 |
. . . . 5
⊢ ((𝜑 ∧ (0 < 𝐴 ∧ 𝐵 < 0)) → 𝐵 < 0) |
50 | 44, 45, 48, 49 | ltmul2dd 12828 |
. . . 4
⊢ ((𝜑 ∧ (0 < 𝐴 ∧ 𝐵 < 0)) → (𝐴 · 𝐵) < (𝐴 · 0)) |
51 | 46 | recnd 11003 |
. . . . 5
⊢ ((𝜑 ∧ (0 < 𝐴 ∧ 𝐵 < 0)) → 𝐴 ∈ ℂ) |
52 | 51 | mul01d 11174 |
. . . 4
⊢ ((𝜑 ∧ (0 < 𝐴 ∧ 𝐵 < 0)) → (𝐴 · 0) = 0) |
53 | 50, 52 | breqtrd 5100 |
. . 3
⊢ ((𝜑 ∧ (0 < 𝐴 ∧ 𝐵 < 0)) → (𝐴 · 𝐵) < 0) |
54 | 43, 53 | jaodan 955 |
. 2
⊢ ((𝜑 ∧ ((𝐴 < 0 ∧ 0 < 𝐵) ∨ (0 < 𝐴 ∧ 𝐵 < 0))) → (𝐴 · 𝐵) < 0) |
55 | 33, 54 | impbida 798 |
1
⊢ (𝜑 → ((𝐴 · 𝐵) < 0 ↔ ((𝐴 < 0 ∧ 0 < 𝐵) ∨ (0 < 𝐴 ∧ 𝐵 < 0)))) |