Metamath Proof Explorer

Theorem mulge0b

Description: A condition for multiplication to be nonnegative. (Contributed by Scott Fenton, 25-Jun-2013)

Ref Expression
Assertion mulge0b ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ A ⁢ B ↔ A ≤ 0 ∧ B ≤ 0 ∨ 0 ≤ A ∧ 0 ≤ B

Proof

Step Hyp Ref Expression
1 ianor ⊢ ¬ A ≤ 0 ∧ B ≤ 0 ↔ ¬ A ≤ 0 ∨ ¬ B ≤ 0
2 0re ⊢ 0 ∈ ℝ
3 ltnle ⊢ 0 ∈ ℝ ∧ A ∈ ℝ → 0 < A ↔ ¬ A ≤ 0
4 2 3 mpan ⊢ A ∈ ℝ → 0 < A ↔ ¬ A ≤ 0
5 4 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ↔ ¬ A ≤ 0
6 ltnle ⊢ 0 ∈ ℝ ∧ B ∈ ℝ → 0 < B ↔ ¬ B ≤ 0
7 2 6 mpan ⊢ B ∈ ℝ → 0 < B ↔ ¬ B ≤ 0
8 7 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < B ↔ ¬ B ≤ 0
9 5 8 orbi12d ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ∨ 0 < B ↔ ¬ A ≤ 0 ∨ ¬ B ≤ 0
10 9 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B → 0 < A ∨ 0 < B ↔ ¬ A ≤ 0 ∨ ¬ B ≤ 0
11 ltle ⊢ 0 ∈ ℝ ∧ A ∈ ℝ → 0 < A → 0 ≤ A
12 2 11 mpan ⊢ A ∈ ℝ → 0 < A → 0 ≤ A
13 12 imp ⊢ A ∈ ℝ ∧ 0 < A → 0 ≤ A
14 13 ad2ant2rl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < A → 0 ≤ A
15 remulcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ⁢ B ∈ ℝ
16 15 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < A → A ⁢ B ∈ ℝ
17 simprl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < A → 0 ≤ A ⁢ B
18 simpll ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < A → A ∈ ℝ
19 simprr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < A → 0 < A
20 divge0 ⊢ A ⁢ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ A ∈ ℝ ∧ 0 < A → 0 ≤ A ⁢ B A
21 16 17 18 19 20 syl22anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < A → 0 ≤ A ⁢ B A
22 recn ⊢ B ∈ ℝ → B ∈ ℂ
23 22 ad2antlr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < A → B ∈ ℂ
24 recn ⊢ A ∈ ℝ → A ∈ ℂ
25 24 ad2antrr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < A → A ∈ ℂ
26 gt0ne0 ⊢ A ∈ ℝ ∧ 0 < A → A ≠ 0
27 26 ad2ant2rl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < A → A ≠ 0
28 23 25 27 divcan3d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < A → A ⁢ B A = B
29 21 28 breqtrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < A → 0 ≤ B
30 14 29 jca ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < A → 0 ≤ A ∧ 0 ≤ B
31 30 expr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B → 0 < A → 0 ≤ A ∧ 0 ≤ B
32 15 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < B → A ⁢ B ∈ ℝ
33 simprl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < B → 0 ≤ A ⁢ B
34 simplr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < B → B ∈ ℝ
35 simprr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < B → 0 < B
36 divge0 ⊢ A ⁢ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ B ∈ ℝ ∧ 0 < B → 0 ≤ A ⁢ B B
37 32 33 34 35 36 syl22anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < B → 0 ≤ A ⁢ B B
38 24 ad2antrr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < B → A ∈ ℂ
39 22 ad2antlr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < B → B ∈ ℂ
40 gt0ne0 ⊢ B ∈ ℝ ∧ 0 < B → B ≠ 0
41 40 ad2ant2l ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < B → B ≠ 0
42 38 39 41 divcan4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < B → A ⁢ B B = A
43 37 42 breqtrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < B → 0 ≤ A
44 ltle ⊢ 0 ∈ ℝ ∧ B ∈ ℝ → 0 < B → 0 ≤ B
45 2 44 mpan ⊢ B ∈ ℝ → 0 < B → 0 ≤ B
46 45 imp ⊢ B ∈ ℝ ∧ 0 < B → 0 ≤ B
47 46 ad2ant2l ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < B → 0 ≤ B
48 43 47 jca ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B ∧ 0 < B → 0 ≤ A ∧ 0 ≤ B
49 48 expr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B → 0 < B → 0 ≤ A ∧ 0 ≤ B
50 31 49 jaod ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B → 0 < A ∨ 0 < B → 0 ≤ A ∧ 0 ≤ B
51 10 50 sylbird ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B → ¬ A ≤ 0 ∨ ¬ B ≤ 0 → 0 ≤ A ∧ 0 ≤ B
52 1 51 syl5bi ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B → ¬ A ≤ 0 ∧ B ≤ 0 → 0 ≤ A ∧ 0 ≤ B
53 52 orrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ⁢ B → A ≤ 0 ∧ B ≤ 0 ∨ 0 ≤ A ∧ 0 ≤ B
54 53 ex ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ A ⁢ B → A ≤ 0 ∧ B ≤ 0 ∨ 0 ≤ A ∧ 0 ≤ B
55 le0neg1 ⊢ A ∈ ℝ → A ≤ 0 ↔ 0 ≤ − A
56 le0neg1 ⊢ B ∈ ℝ → B ≤ 0 ↔ 0 ≤ − B
57 55 56 bi2anan9 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ 0 ∧ B ≤ 0 ↔ 0 ≤ − A ∧ 0 ≤ − B
58 renegcl ⊢ A ∈ ℝ → − A ∈ ℝ
59 renegcl ⊢ B ∈ ℝ → − B ∈ ℝ
60 mulge0 ⊢ − A ∈ ℝ ∧ 0 ≤ − A ∧ − B ∈ ℝ ∧ 0 ≤ − B → 0 ≤ − A ⁢ − B
61 60 an4s ⊢ − A ∈ ℝ ∧ − B ∈ ℝ ∧ 0 ≤ − A ∧ 0 ≤ − B → 0 ≤ − A ⁢ − B
62 61 ex ⊢ − A ∈ ℝ ∧ − B ∈ ℝ → 0 ≤ − A ∧ 0 ≤ − B → 0 ≤ − A ⁢ − B
63 58 59 62 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ − A ∧ 0 ≤ − B → 0 ≤ − A ⁢ − B
64 mul2neg ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A ⁢ − B = A ⁢ B
65 24 22 64 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → − A ⁢ − B = A ⁢ B
66 65 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ − A ⁢ − B ↔ 0 ≤ A ⁢ B
67 63 66 sylibd ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ − A ∧ 0 ≤ − B → 0 ≤ A ⁢ B
68 57 67 sylbid ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ 0 ∧ B ≤ 0 → 0 ≤ A ⁢ B
69 mulge0 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → 0 ≤ A ⁢ B
70 69 an4s ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ∧ 0 ≤ B → 0 ≤ A ⁢ B
71 70 ex ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ A ∧ 0 ≤ B → 0 ≤ A ⁢ B
72 68 71 jaod ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ 0 ∧ B ≤ 0 ∨ 0 ≤ A ∧ 0 ≤ B → 0 ≤ A ⁢ B
73 54 72 impbid ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ A ⁢ B ↔ A ≤ 0 ∧ B ≤ 0 ∨ 0 ≤ A ∧ 0 ≤ B