Proof of Theorem mulge0b
Step | Hyp | Ref
| Expression |
1 | | ianor 982 |
. . . . 5
⊢ (¬
(𝐴 ≤ 0 ∧ 𝐵 ≤ 0) ↔ (¬ 𝐴 ≤ 0 ∨ ¬ 𝐵 ≤ 0)) |
2 | | 0re 10835 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
3 | | ltnle 10912 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 < 𝐴 ↔ ¬ 𝐴 ≤ 0)) |
4 | 2, 3 | mpan 690 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (0 <
𝐴 ↔ ¬ 𝐴 ≤ 0)) |
5 | 4 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 <
𝐴 ↔ ¬ 𝐴 ≤ 0)) |
6 | | ltnle 10912 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ) → (0 < 𝐵 ↔ ¬ 𝐵 ≤ 0)) |
7 | 2, 6 | mpan 690 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ → (0 <
𝐵 ↔ ¬ 𝐵 ≤ 0)) |
8 | 7 | adantl 485 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 <
𝐵 ↔ ¬ 𝐵 ≤ 0)) |
9 | 5, 8 | orbi12d 919 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <
𝐴 ∨ 0 < 𝐵) ↔ (¬ 𝐴 ≤ 0 ∨ ¬ 𝐵 ≤ 0))) |
10 | 9 | adantr 484 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 ≤
(𝐴 · 𝐵)) → ((0 < 𝐴 ∨ 0 < 𝐵) ↔ (¬ 𝐴 ≤ 0 ∨ ¬ 𝐵 ≤ 0))) |
11 | | ltle 10921 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴)) |
12 | 2, 11 | mpan 690 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → (0 <
𝐴 → 0 ≤ 𝐴)) |
13 | 12 | imp 410 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 0 ≤ 𝐴) |
14 | 13 | ad2ant2rl 749 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐴)) → 0 ≤ 𝐴) |
15 | | remulcl 10814 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) |
16 | 15 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐴)) → (𝐴 · 𝐵) ∈ ℝ) |
17 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐴)) → 0 ≤ (𝐴 · 𝐵)) |
18 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐴)) → 𝐴 ∈ ℝ) |
19 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐴)) → 0 < 𝐴) |
20 | | divge0 11701 |
. . . . . . . . . . 11
⊢ ((((𝐴 · 𝐵) ∈ ℝ ∧ 0 ≤ (𝐴 · 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → 0 ≤ ((𝐴 · 𝐵) / 𝐴)) |
21 | 16, 17, 18, 19, 20 | syl22anc 839 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐴)) → 0 ≤ ((𝐴 · 𝐵) / 𝐴)) |
22 | | recn 10819 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
23 | 22 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐴)) → 𝐵 ∈ ℂ) |
24 | | recn 10819 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
25 | 24 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐴)) → 𝐴 ∈ ℂ) |
26 | | gt0ne0 11297 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 𝐴 ≠ 0) |
27 | 26 | ad2ant2rl 749 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐴)) → 𝐴 ≠ 0) |
28 | 23, 25, 27 | divcan3d 11613 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐴)) → ((𝐴 · 𝐵) / 𝐴) = 𝐵) |
29 | 21, 28 | breqtrd 5079 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐴)) → 0 ≤ 𝐵) |
30 | 14, 29 | jca 515 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐴)) → (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) |
31 | 30 | expr 460 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 ≤
(𝐴 · 𝐵)) → (0 < 𝐴 → (0 ≤ 𝐴 ∧ 0 ≤ 𝐵))) |
32 | 15 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐵)) → (𝐴 · 𝐵) ∈ ℝ) |
33 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐵)) → 0 ≤ (𝐴 · 𝐵)) |
34 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐵)) → 𝐵 ∈ ℝ) |
35 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐵)) → 0 < 𝐵) |
36 | | divge0 11701 |
. . . . . . . . . . 11
⊢ ((((𝐴 · 𝐵) ∈ ℝ ∧ 0 ≤ (𝐴 · 𝐵)) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ ((𝐴 · 𝐵) / 𝐵)) |
37 | 32, 33, 34, 35, 36 | syl22anc 839 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐵)) → 0 ≤ ((𝐴 · 𝐵) / 𝐵)) |
38 | 24 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐵)) → 𝐴 ∈ ℂ) |
39 | 22 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐵)) → 𝐵 ∈ ℂ) |
40 | | gt0ne0 11297 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → 𝐵 ≠ 0) |
41 | 40 | ad2ant2l 746 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐵)) → 𝐵 ≠ 0) |
42 | 38, 39, 41 | divcan4d 11614 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐵)) → ((𝐴 · 𝐵) / 𝐵) = 𝐴) |
43 | 37, 42 | breqtrd 5079 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐵)) → 0 ≤ 𝐴) |
44 | | ltle 10921 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 𝐵
∈ ℝ) → (0 < 𝐵 → 0 ≤ 𝐵)) |
45 | 2, 44 | mpan 690 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ → (0 <
𝐵 → 0 ≤ 𝐵)) |
46 | 45 | imp 410 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 0 <
𝐵) → 0 ≤ 𝐵) |
47 | 46 | ad2ant2l 746 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐵)) → 0 ≤ 𝐵) |
48 | 43, 47 | jca 515 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
(𝐴 · 𝐵) ∧ 0 < 𝐵)) → (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) |
49 | 48 | expr 460 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 ≤
(𝐴 · 𝐵)) → (0 < 𝐵 → (0 ≤ 𝐴 ∧ 0 ≤ 𝐵))) |
50 | 31, 49 | jaod 859 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 ≤
(𝐴 · 𝐵)) → ((0 < 𝐴 ∨ 0 < 𝐵) → (0 ≤ 𝐴 ∧ 0 ≤ 𝐵))) |
51 | 10, 50 | sylbird 263 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 ≤
(𝐴 · 𝐵)) → ((¬ 𝐴 ≤ 0 ∨ ¬ 𝐵 ≤ 0) → (0 ≤ 𝐴 ∧ 0 ≤ 𝐵))) |
52 | 1, 51 | syl5bi 245 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 ≤
(𝐴 · 𝐵)) → (¬ (𝐴 ≤ 0 ∧ 𝐵 ≤ 0) → (0 ≤ 𝐴 ∧ 0 ≤ 𝐵))) |
53 | 52 | orrd 863 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 ≤
(𝐴 · 𝐵)) → ((𝐴 ≤ 0 ∧ 𝐵 ≤ 0) ∨ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵))) |
54 | 53 | ex 416 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤
(𝐴 · 𝐵) → ((𝐴 ≤ 0 ∧ 𝐵 ≤ 0) ∨ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)))) |
55 | | le0neg1 11340 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴)) |
56 | | le0neg1 11340 |
. . . . 5
⊢ (𝐵 ∈ ℝ → (𝐵 ≤ 0 ↔ 0 ≤ -𝐵)) |
57 | 55, 56 | bi2anan9 639 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ≤ 0 ∧ 𝐵 ≤ 0) ↔ (0 ≤ -𝐴 ∧ 0 ≤ -𝐵))) |
58 | | renegcl 11141 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → -𝐴 ∈
ℝ) |
59 | | renegcl 11141 |
. . . . . 6
⊢ (𝐵 ∈ ℝ → -𝐵 ∈
ℝ) |
60 | | mulge0 11350 |
. . . . . . . 8
⊢ (((-𝐴 ∈ ℝ ∧ 0 ≤
-𝐴) ∧ (-𝐵 ∈ ℝ ∧ 0 ≤
-𝐵)) → 0 ≤ (-𝐴 · -𝐵)) |
61 | 60 | an4s 660 |
. . . . . . 7
⊢ (((-𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) ∧ (0 ≤
-𝐴 ∧ 0 ≤ -𝐵)) → 0 ≤ (-𝐴 · -𝐵)) |
62 | 61 | ex 416 |
. . . . . 6
⊢ ((-𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → ((0 ≤
-𝐴 ∧ 0 ≤ -𝐵) → 0 ≤ (-𝐴 · -𝐵))) |
63 | 58, 59, 62 | syl2an 599 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 ≤
-𝐴 ∧ 0 ≤ -𝐵) → 0 ≤ (-𝐴 · -𝐵))) |
64 | | mul2neg 11271 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · -𝐵) = (𝐴 · 𝐵)) |
65 | 24, 22, 64 | syl2an 599 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 · -𝐵) = (𝐴 · 𝐵)) |
66 | 65 | breq2d 5065 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤
(-𝐴 · -𝐵) ↔ 0 ≤ (𝐴 · 𝐵))) |
67 | 63, 66 | sylibd 242 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 ≤
-𝐴 ∧ 0 ≤ -𝐵) → 0 ≤ (𝐴 · 𝐵))) |
68 | 57, 67 | sylbid 243 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ≤ 0 ∧ 𝐵 ≤ 0) → 0 ≤ (𝐴 · 𝐵))) |
69 | | mulge0 11350 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 · 𝐵)) |
70 | 69 | an4s 660 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 · 𝐵)) |
71 | 70 | ex 416 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 ≤
𝐴 ∧ 0 ≤ 𝐵) → 0 ≤ (𝐴 · 𝐵))) |
72 | 68, 71 | jaod 859 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 ≤ 0 ∧ 𝐵 ≤ 0) ∨ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 · 𝐵))) |
73 | 54, 72 | impbid 215 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤
(𝐴 · 𝐵) ↔ ((𝐴 ≤ 0 ∧ 𝐵 ≤ 0) ∨ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)))) |