mulge0b - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mulge0b		Structured version Visualization version GIF version

Theorem mulge0b 11358

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

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

**Proof of Theorem mulge0b**
Step	Hyp	Ref	Expression
1		ianor 976	. . . . 5 ⊢ (¬ (𝐴 ≤ 0 ∧ 𝐵 ≤ 0) ↔ (¬ 𝐴 ≤ 0 ∨ ¬ 𝐵 ≤ 0))
2		0re 10489	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
3		ltnle 10567	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 < 𝐴 ↔ ¬ 𝐴 ≤ 0))
4	2, 3	mpan 686	. . . . . . . . 9 ⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ ¬ 𝐴 ≤ 0))
5	4	adantr 481	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ ¬ 𝐴 ≤ 0))
6		ltnle 10567	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐵 ↔ ¬ 𝐵 ≤ 0))
7	2, 6	mpan 686	. . . . . . . . 9 ⊢ (𝐵 ∈ ℝ → (0 < 𝐵 ↔ ¬ 𝐵 ≤ 0))
8	7	adantl 482	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐵 ↔ ¬ 𝐵 ≤ 0))
9	5, 8	orbi12d 913	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∨ 0 < 𝐵) ↔ (¬ 𝐴 ≤ 0 ∨ ¬ 𝐵 ≤ 0)))
10	9	adantr 481	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 ≤ (𝐴 · 𝐵)) → ((0 < 𝐴 ∨ 0 < 𝐵) ↔ (¬ 𝐴 ≤ 0 ∨ ¬ 𝐵 ≤ 0)))
11		ltle 10576	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴))
12	2, 11	mpan 686	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → (0 < 𝐴 → 0 ≤ 𝐴))
13	12	imp 407	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 0 ≤ 𝐴)
14	13	ad2ant2rl 745	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐴)) → 0 ≤ 𝐴)
15		remulcl 10468	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
16	15	adantr 481	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐴)) → (𝐴 · 𝐵) ∈ ℝ)
17		simprl 767	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐴)) → 0 ≤ (𝐴 · 𝐵))
18		simpll 763	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐴)) → 𝐴 ∈ ℝ)
19		simprr 769	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐴)) → 0 < 𝐴)
20		divge0 11357	. . . . . . . . . . 11 ⊢ ((((𝐴 · 𝐵) ∈ ℝ ∧ 0 ≤ (𝐴 · 𝐵)) ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → 0 ≤ ((𝐴 · 𝐵) / 𝐴))
21	16, 17, 18, 19, 20	syl22anc 835	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐴)) → 0 ≤ ((𝐴 · 𝐵) / 𝐴))
22		recn 10473	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
23	22	ad2antlr 723	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐴)) → 𝐵 ∈ ℂ)
24		recn 10473	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
25	24	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐴)) → 𝐴 ∈ ℂ)
26		gt0ne0 10953	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 ≠ 0)
27	26	ad2ant2rl 745	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐴)) → 𝐴 ≠ 0)
28	23, 25, 27	divcan3d 11269	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐴)) → ((𝐴 · 𝐵) / 𝐴) = 𝐵)
29	21, 28	breqtrd 4988	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐴)) → 0 ≤ 𝐵)
30	14, 29	jca 512	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐴)) → (0 ≤ 𝐴 ∧ 0 ≤ 𝐵))
31	30	expr 457	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 ≤ (𝐴 · 𝐵)) → (0 < 𝐴 → (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)))
32	15	adantr 481	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐵)) → (𝐴 · 𝐵) ∈ ℝ)
33		simprl 767	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐵)) → 0 ≤ (𝐴 · 𝐵))
34		simplr 765	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐵)) → 𝐵 ∈ ℝ)
35		simprr 769	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐵)) → 0 < 𝐵)
36		divge0 11357	. . . . . . . . . . 11 ⊢ ((((𝐴 · 𝐵) ∈ ℝ ∧ 0 ≤ (𝐴 · 𝐵)) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ ((𝐴 · 𝐵) / 𝐵))
37	32, 33, 34, 35, 36	syl22anc 835	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐵)) → 0 ≤ ((𝐴 · 𝐵) / 𝐵))
38	24	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐵)) → 𝐴 ∈ ℂ)
39	22	ad2antlr 723	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐵)) → 𝐵 ∈ ℂ)
40		gt0ne0 10953	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ ∧ 0 < 𝐵) → 𝐵 ≠ 0)
41	40	ad2ant2l 742	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐵)) → 𝐵 ≠ 0)
42	38, 39, 41	divcan4d 11270	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐵)) → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
43	37, 42	breqtrd 4988	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐵)) → 0 ≤ 𝐴)
44		ltle 10576	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐵 → 0 ≤ 𝐵))
45	2, 44	mpan 686	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ → (0 < 𝐵 → 0 ≤ 𝐵))
46	45	imp 407	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ 0 < 𝐵) → 0 ≤ 𝐵)
47	46	ad2ant2l 742	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐵)) → 0 ≤ 𝐵)
48	43, 47	jca 512	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐵) ∧ 0 < 𝐵)) → (0 ≤ 𝐴 ∧ 0 ≤ 𝐵))
49	48	expr 457	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 ≤ (𝐴 · 𝐵)) → (0 < 𝐵 → (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)))
50	31, 49	jaod 854	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 ≤ (𝐴 · 𝐵)) → ((0 < 𝐴 ∨ 0 < 𝐵) → (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)))
51	10, 50	sylbird 261	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 ≤ (𝐴 · 𝐵)) → ((¬ 𝐴 ≤ 0 ∨ ¬ 𝐵 ≤ 0) → (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)))
52	1, 51	syl5bi 243	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 ≤ (𝐴 · 𝐵)) → (¬ (𝐴 ≤ 0 ∧ 𝐵 ≤ 0) → (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)))
53	52	orrd 858	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 0 ≤ (𝐴 · 𝐵)) → ((𝐴 ≤ 0 ∧ 𝐵 ≤ 0) ∨ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)))
54	53	ex 413	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 · 𝐵) → ((𝐴 ≤ 0 ∧ 𝐵 ≤ 0) ∨ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵))))
55		le0neg1 10996	. . . . 5 ⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴))
56		le0neg1 10996	. . . . 5 ⊢ (𝐵 ∈ ℝ → (𝐵 ≤ 0 ↔ 0 ≤ -𝐵))
57	55, 56	bi2anan9 635	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ≤ 0 ∧ 𝐵 ≤ 0) ↔ (0 ≤ -𝐴 ∧ 0 ≤ -𝐵)))
58		renegcl 10797	. . . . . 6 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
59		renegcl 10797	. . . . . 6 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
60		mulge0 11006	. . . . . . . 8 ⊢ (((-𝐴 ∈ ℝ ∧ 0 ≤ -𝐴) ∧ (-𝐵 ∈ ℝ ∧ 0 ≤ -𝐵)) → 0 ≤ (-𝐴 · -𝐵))
61	60	an4s 656	. . . . . . 7 ⊢ (((-𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) ∧ (0 ≤ -𝐴 ∧ 0 ≤ -𝐵)) → 0 ≤ (-𝐴 · -𝐵))
62	61	ex 413	. . . . . 6 ⊢ ((-𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → ((0 ≤ -𝐴 ∧ 0 ≤ -𝐵) → 0 ≤ (-𝐴 · -𝐵)))
63	58, 59, 62	syl2an 595	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 ≤ -𝐴 ∧ 0 ≤ -𝐵) → 0 ≤ (-𝐴 · -𝐵)))
64		mul2neg 10927	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · -𝐵) = (𝐴 · 𝐵))
65	24, 22, 64	syl2an 595	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 · -𝐵) = (𝐴 · 𝐵))
66	65	breq2d 4974	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ (-𝐴 · -𝐵) ↔ 0 ≤ (𝐴 · 𝐵)))
67	63, 66	sylibd 240	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 ≤ -𝐴 ∧ 0 ≤ -𝐵) → 0 ≤ (𝐴 · 𝐵)))
68	57, 67	sylbid 241	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ≤ 0 ∧ 𝐵 ≤ 0) → 0 ≤ (𝐴 · 𝐵)))
69		mulge0 11006	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 · 𝐵))
70	69	an4s 656	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 · 𝐵))
71	70	ex 413	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → 0 ≤ (𝐴 · 𝐵)))
72	68, 71	jaod 854	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 ≤ 0 ∧ 𝐵 ≤ 0) ∨ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 · 𝐵)))
73	54, 72	impbid 213	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 · 𝐵) ↔ ((𝐴 ≤ 0 ∧ 𝐵 ≤ 0) ∨ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∨ wo 842 = wceq 1522 ∈ wcel 2081 ≠ wne 2984 class class class wbr 4962 (class class class)co 7016 ℂcc 10381 ℝcr 10382 0cc0 10383 · cmul 10388 < clt 10521 ≤ cle 10522 -cneg 10718 / cdiv 11145

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 ax-resscn 10440 ax-1cn 10441 ax-icn 10442 ax-addcl 10443 ax-addrcl 10444 ax-mulcl 10445 ax-mulrcl 10446 ax-mulcom 10447 ax-addass 10448 ax-mulass 10449 ax-distr 10450 ax-i2m1 10451 ax-1ne0 10452 ax-1rid 10453 ax-rnegex 10454 ax-rrecex 10455 ax-cnre 10456 ax-pre-lttri 10457 ax-pre-lttrn 10458 ax-pre-ltadd 10459 ax-pre-mulgt0 10460

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-nel 3091 df-ral 3110 df-rex 3111 df-reu 3112 df-rmo 3113 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-opab 5025 df-mpt 5042 df-id 5348 df-po 5362 df-so 5363 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-riota 6977 df-ov 7019 df-oprab 7020 df-mpo 7021 df-er 8139 df-en 8358 df-dom 8359 df-sdom 8360 df-pnf 10523 df-mnf 10524 df-xr 10525 df-ltxr 10526 df-le 10527 df-sub 10719 df-neg 10720 df-div 11146

This theorem is referenced by: mulle0b 11359

W3C validator