Metamath Proof Explorer

Theorem mulge0b

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

Ref Expression
Assertion mulge0b ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ ( 𝐴 · 𝐵 ) ↔ ( ( 𝐴 ≤ 0 ∧ 𝐵 ≤ 0 ) ∨ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) ) )

Proof

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