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 ≤ 𝐵 ) ) ) )