xlemul1a

Description: Extended real version of lemul1a . (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	xlemul1a	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land (C \in ℝ^{*} \land 0 \leq C)) \land A \leq B) \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C$

Proof

Step	Hyp	Ref	Expression
1		0xr	$⊢ 0 \in ℝ^{*}$
2		simpr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{}) \to C \in ℝ^{}$
3		xrleloe	$⊢ (0 \in ℝ^{} \land C \in ℝ^{}) \to (0 \leq C \leftrightarrow (0 < C \lor 0 = C))$
4	1 2 3	sylancr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \to (0 \leq C \leftrightarrow (0 < C \lor 0 = C))$
5		simpllr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to C \in ℝ^{}$
6		elxr	$⊢ C \in ℝ^{*} \leftrightarrow (C \in ℝ \lor C = +∞ \lor C = −∞)$
7	5 6	sylib	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to (C \in ℝ \lor C = +∞ \lor C = −∞)$
8		simplrr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land C \in ℝ)) \to A \leq B$
9		simprll	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land C \in ℝ)) \to A \in ℝ$
10		simprlr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land C \in ℝ)) \to B \in ℝ$
11		simprr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land C \in ℝ)) \to C \in ℝ$
12		simplrl	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land C \in ℝ)) \to 0 < C$
13		lemul1	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A \leq B \leftrightarrow A C \leq B C)$
14	9 10 11 12 13	syl112anc	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land C \in ℝ)) \to (A \leq B \leftrightarrow A C \leq B C)$
15	8 14	mpbid	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land C \in ℝ)) \to A C \leq B C$
16		rexmul	$⊢ (A \in ℝ \land C \in ℝ) \to A \cdot_{𝑒} C = A C$
17	9 11 16	syl2anc	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land C \in ℝ)) \to A \cdot_{𝑒} C = A C$
18		rexmul	$⊢ (B \in ℝ \land C \in ℝ) \to B \cdot_{𝑒} C = B C$
19	10 11 18	syl2anc	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land C \in ℝ)) \to B \cdot_{𝑒} C = B C$
20	15 17 19	3brtr4d	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land C \in ℝ)) \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C$
21	20	expr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to (C \in ℝ \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C)$
22		simprl	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to A \in ℝ$
23		0re	$⊢ 0 \in ℝ$
24		lttri4	$⊢ (A \in ℝ \land 0 \in ℝ) \to (A < 0 \lor A = 0 \lor 0 < A)$
25	22 23 24	sylancl	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to (A < 0 \lor A = 0 \lor 0 < A)$
26		simplll	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{}) \land (0 < C \land A \leq B)) \to A \in ℝ^{}$
27	26	adantr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to A \in ℝ^{}$
28		xmulpnf1n	$⊢ (A \in ℝ^{*} \land A < 0) \to A \cdot_{𝑒} +∞ = −∞$
29	27 28	sylan	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \land A < 0) \to A \cdot_{𝑒} +∞ = −∞$
30		simpllr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{}) \land (0 < C \land A \leq B)) \to B \in ℝ^{}$
31	30	adantr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to B \in ℝ^{}$
32	31	adantr	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \land A < 0) \to B \in ℝ^{}$
33		pnfxr	$⊢ +∞ \in ℝ^{*}$
34		xmulcl	$⊢ (B \in ℝ^{} \land +∞ \in ℝ^{}) \to B \cdot_{𝑒} +∞ \in ℝ^{*}$
35	32 33 34	sylancl	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \land A < 0) \to B \cdot_{𝑒} +∞ \in ℝ^{}$
36		mnfle	$⊢ B \cdot_{𝑒} +∞ \in ℝ^{*} \to −∞ \leq B \cdot_{𝑒} +∞$
37	35 36	syl	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \land A < 0) \to −∞ \leq B \cdot_{𝑒} +∞$
38	29 37	eqbrtrd	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \land A < 0) \to A \cdot_{𝑒} +∞ \leq B \cdot_{𝑒} +∞$
39	38	ex	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to (A < 0 \to A \cdot_{𝑒} +∞ \leq B \cdot_{𝑒} +∞)$
40		oveq1	$⊢ A = 0 \to A \cdot_{𝑒} +∞ = 0 \cdot_{𝑒} +∞$
41		xmul02	$⊢ +∞ \in ℝ^{*} \to 0 \cdot_{𝑒} +∞ = 0$
42	33 41	ax-mp	$⊢ 0 \cdot_{𝑒} +∞ = 0$
43	40 42	eqtrdi	$⊢ A = 0 \to A \cdot_{𝑒} +∞ = 0$
44	43	adantl	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \land A = 0) \to A \cdot_{𝑒} +∞ = 0$
45		simplrr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to A \leq B$
46		breq1	$⊢ A = 0 \to (A \leq B \leftrightarrow 0 \leq B)$
47	45 46	syl5ibcom	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to (A = 0 \to 0 \leq B)$
48		simprr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to B \in ℝ$
49		leloe	$⊢ (0 \in ℝ \land B \in ℝ) \to (0 \leq B \leftrightarrow (0 < B \lor 0 = B))$
50	23 48 49	sylancr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to (0 \leq B \leftrightarrow (0 < B \lor 0 = B))$
51	47 50	sylibd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to (A = 0 \to (0 < B \lor 0 = B))$
52	51	imp	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \land A = 0) \to (0 < B \lor 0 = B)$
53		pnfge	$⊢ 0 \in ℝ^{*} \to 0 \leq +∞$
54	1 53	ax-mp	$⊢ 0 \leq +∞$
55		xmulpnf1	$⊢ (B \in ℝ^{*} \land 0 < B) \to B \cdot_{𝑒} +∞ = +∞$
56	31 55	sylan	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \land 0 < B) \to B \cdot_{𝑒} +∞ = +∞$
57	54 56	breqtrrid	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \land 0 < B) \to 0 \leq B \cdot_{𝑒} +∞$
58		xrleid	$⊢ 0 \in ℝ^{*} \to 0 \leq 0$
59	1 58	ax-mp	$⊢ 0 \leq 0$
60	59 42	breqtrri	$⊢ 0 \leq 0 \cdot_{𝑒} +∞$
61		simpr	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \land 0 = B) \to 0 = B$
62	61	oveq1d	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \land 0 = B) \to 0 \cdot_{𝑒} +∞ = B \cdot_{𝑒} +∞$
63	60 62	breqtrid	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \land 0 = B) \to 0 \leq B \cdot_{𝑒} +∞$
64	57 63	jaodan	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \land (0 < B \lor 0 = B)) \to 0 \leq B \cdot_{𝑒} +∞$
65	52 64	syldan	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \land A = 0) \to 0 \leq B \cdot_{𝑒} +∞$
66	44 65	eqbrtrd	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \land A = 0) \to A \cdot_{𝑒} +∞ \leq B \cdot_{𝑒} +∞$
67	66	ex	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to (A = 0 \to A \cdot_{𝑒} +∞ \leq B \cdot_{𝑒} +∞)$
68		pnfge	$⊢ +∞ \in ℝ^{*} \to +∞ \leq +∞$
69	33 68	ax-mp	$⊢ +∞ \leq +∞$
70	26	adantr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land 0 < A)) \to A \in ℝ^{}$
71		simprr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land 0 < A)) \to 0 < A$
72		xmulpnf1	$⊢ (A \in ℝ^{*} \land 0 < A) \to A \cdot_{𝑒} +∞ = +∞$
73	70 71 72	syl2anc	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land 0 < A)) \to A \cdot_{𝑒} +∞ = +∞$
74	30	adantr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land 0 < A)) \to B \in ℝ^{}$
75		ltletr	$⊢ (0 \in ℝ \land A \in ℝ \land B \in ℝ) \to ((0 < A \land A \leq B) \to 0 < B)$
76	23 75	mp3an1	$⊢ (A \in ℝ \land B \in ℝ) \to ((0 < A \land A \leq B) \to 0 < B)$
77	76	adantl	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to ((0 < A \land A \leq B) \to 0 < B)$
78	45 77	mpan2d	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to (0 < A \to 0 < B)$
79	78	impr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land 0 < A)) \to 0 < B$
80	74 79 55	syl2anc	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land 0 < A)) \to B \cdot_{𝑒} +∞ = +∞$
81	73 80	breq12d	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land 0 < A)) \to (A \cdot_{𝑒} +∞ \leq B \cdot_{𝑒} +∞ \leftrightarrow +∞ \leq +∞)$
82	69 81	mpbiri	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land ((A \in ℝ \land B \in ℝ) \land 0 < A)) \to A \cdot_{𝑒} +∞ \leq B \cdot_{𝑒} +∞$
83	82	expr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to (0 < A \to A \cdot_{𝑒} +∞ \leq B \cdot_{𝑒} +∞)$
84	39 67 83	3jaod	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to ((A < 0 \lor A = 0 \lor 0 < A) \to A \cdot_{𝑒} +∞ \leq B \cdot_{𝑒} +∞)$
85	25 84	mpd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to A \cdot_{𝑒} +∞ \leq B \cdot_{𝑒} +∞$
86		oveq2	$⊢ C = +∞ \to A \cdot_{𝑒} C = A \cdot_{𝑒} +∞$
87		oveq2	$⊢ C = +∞ \to B \cdot_{𝑒} C = B \cdot_{𝑒} +∞$
88	86 87	breq12d	$⊢ C = +∞ \to (A \cdot_{𝑒} C \leq B \cdot_{𝑒} C \leftrightarrow A \cdot_{𝑒} +∞ \leq B \cdot_{𝑒} +∞)$
89	85 88	syl5ibrcom	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to (C = +∞ \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C)$
90		nltmnf	$⊢ 0 \in ℝ^{*} \to \neg 0 < −∞$
91	1 90	ax-mp	$⊢ \neg 0 < −∞$
92		breq2	$⊢ C = −∞ \to (0 < C \leftrightarrow 0 < −∞)$
93	91 92	mtbiri	$⊢ C = −∞ \to \neg 0 < C$
94	93	con2i	$⊢ 0 < C \to \neg C = −∞$
95	94	ad2antrl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \to \neg C = −∞$
96	95	adantr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to \neg C = −∞$
97	96	pm2.21d	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to (C = −∞ \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C)$
98	21 89 97	3jaod	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to ((C \in ℝ \lor C = +∞ \lor C = −∞) \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C)$
99	7 98	mpd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land (A \in ℝ \land B \in ℝ)) \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C$
100	99	anassrs	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land A \in ℝ) \land B \in ℝ) \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C$
101		xmulcl	$⊢ (A \in ℝ^{} \land C \in ℝ^{}) \to A \cdot_{𝑒} C \in ℝ^{*}$
102	101	adantlr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{}) \to A \cdot_{𝑒} C \in ℝ^{}$
103	102	ad2antrr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{}) \land (0 < C \land A \leq B)) \land B = +∞) \to A \cdot_{𝑒} C \in ℝ^{}$
104		pnfge	$⊢ A \cdot_{𝑒} C \in ℝ^{*} \to A \cdot_{𝑒} C \leq +∞$
105	103 104	syl	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land B = +∞) \to A \cdot_{𝑒} C \leq +∞$
106		oveq1	$⊢ B = +∞ \to B \cdot_{𝑒} C = +∞ \cdot_{𝑒} C$
107		xmulpnf2	$⊢ (C \in ℝ^{*} \land 0 < C) \to +∞ \cdot_{𝑒} C = +∞$
108	107	ad2ant2lr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \to +∞ \cdot_{𝑒} C = +∞$
109	106 108	sylan9eqr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land B = +∞) \to B \cdot_{𝑒} C = +∞$
110	105 109	breqtrrd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land B = +∞) \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C$
111	110	adantlr	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land A \in ℝ) \land B = +∞) \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C$
112		simplrr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land B = −∞) \to A \leq B$
113		simpr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land B = −∞) \to B = −∞$
114	26	adantr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{}) \land (0 < C \land A \leq B)) \land B = −∞) \to A \in ℝ^{}$
115		mnfle	$⊢ A \in ℝ^{*} \to −∞ \leq A$
116	114 115	syl	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land B = −∞) \to −∞ \leq A$
117	113 116	eqbrtrd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land B = −∞) \to B \leq A$
118		xrletri3	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A = B \leftrightarrow (A \leq B \land B \leq A))$
119	118	ad3antrrr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land B = −∞) \to (A = B \leftrightarrow (A \leq B \land B \leq A))$
120	112 117 119	mpbir2and	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land B = −∞) \to A = B$
121	120	oveq1d	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land B = −∞) \to A \cdot_{𝑒} C = B \cdot_{𝑒} C$
122		xmulcl	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to B \cdot_{𝑒} C \in ℝ^{*}$
123	122	adantll	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{}) \to B \cdot_{𝑒} C \in ℝ^{}$
124	123	ad2antrr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{}) \land (0 < C \land A \leq B)) \land B = −∞) \to B \cdot_{𝑒} C \in ℝ^{}$
125		xrleid	$⊢ B \cdot_{𝑒} C \in ℝ^{*} \to B \cdot_{𝑒} C \leq B \cdot_{𝑒} C$
126	124 125	syl	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land B = −∞) \to B \cdot_{𝑒} C \leq B \cdot_{𝑒} C$
127	121 126	eqbrtrd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land B = −∞) \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C$
128	127	adantlr	$⊢ (((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land A \in ℝ) \land B = −∞) \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C$
129		elxr	$⊢ B \in ℝ^{*} \leftrightarrow (B \in ℝ \lor B = +∞ \lor B = −∞)$
130	30 129	sylib	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \to (B \in ℝ \lor B = +∞ \lor B = −∞)$
131	130	adantr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land A \in ℝ) \to (B \in ℝ \lor B = +∞ \lor B = −∞)$
132	100 111 128 131	mpjao3dan	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land A \in ℝ) \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C$
133		simplrr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land A = +∞) \to A \leq B$
134	30	adantr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{}) \land (0 < C \land A \leq B)) \land A = +∞) \to B \in ℝ^{}$
135		pnfge	$⊢ B \in ℝ^{*} \to B \leq +∞$
136	134 135	syl	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land A = +∞) \to B \leq +∞$
137		simpr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land A = +∞) \to A = +∞$
138	136 137	breqtrrd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land A = +∞) \to B \leq A$
139	118	ad3antrrr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land A = +∞) \to (A = B \leftrightarrow (A \leq B \land B \leq A))$
140	133 138 139	mpbir2and	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land A = +∞) \to A = B$
141	140	oveq1d	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land A = +∞) \to A \cdot_{𝑒} C = B \cdot_{𝑒} C$
142	123 125	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \to B \cdot_{𝑒} C \leq B \cdot_{𝑒} C$
143	142	ad2antrr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land A = +∞) \to B \cdot_{𝑒} C \leq B \cdot_{𝑒} C$
144	141 143	eqbrtrd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land A = +∞) \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C$
145		oveq1	$⊢ A = −∞ \to A \cdot_{𝑒} C = −∞ \cdot_{𝑒} C$
146		xmulmnf2	$⊢ (C \in ℝ^{*} \land 0 < C) \to −∞ \cdot_{𝑒} C = −∞$
147	146	ad2ant2lr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \to −∞ \cdot_{𝑒} C = −∞$
148	145 147	sylan9eqr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land A = −∞) \to A \cdot_{𝑒} C = −∞$
149	123	ad2antrr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{}) \land (0 < C \land A \leq B)) \land A = −∞) \to B \cdot_{𝑒} C \in ℝ^{}$
150		mnfle	$⊢ B \cdot_{𝑒} C \in ℝ^{*} \to −∞ \leq B \cdot_{𝑒} C$
151	149 150	syl	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land A = −∞) \to −∞ \leq B \cdot_{𝑒} C$
152	148 151	eqbrtrd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \land A = −∞) \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C$
153		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
154	26 153	sylib	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \to (A \in ℝ \lor A = +∞ \lor A = −∞)$
155	132 144 152 154	mpjao3dan	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \land (0 < C \land A \leq B)) \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C$
156	155	exp32	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \to (0 < C \to (A \leq B \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C))$
157		xmul01	$⊢ A \in ℝ^{*} \to A \cdot_{𝑒} 0 = 0$
158	157	ad2antrr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \to A \cdot_{𝑒} 0 = 0$
159		xmul01	$⊢ B \in ℝ^{*} \to B \cdot_{𝑒} 0 = 0$
160	159	ad2antlr	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \to B \cdot_{𝑒} 0 = 0$
161	158 160	breq12d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \to (A \cdot_{𝑒} 0 \leq B \cdot_{𝑒} 0 \leftrightarrow 0 \leq 0)$
162	59 161	mpbiri	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \to A \cdot_{𝑒} 0 \leq B \cdot_{𝑒} 0$
163		oveq2	$⊢ 0 = C \to A \cdot_{𝑒} 0 = A \cdot_{𝑒} C$
164		oveq2	$⊢ 0 = C \to B \cdot_{𝑒} 0 = B \cdot_{𝑒} C$
165	163 164	breq12d	$⊢ 0 = C \to (A \cdot_{𝑒} 0 \leq B \cdot_{𝑒} 0 \leftrightarrow A \cdot_{𝑒} C \leq B \cdot_{𝑒} C)$
166	162 165	syl5ibcom	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \to (0 = C \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C)$
167	166	a1dd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \to (0 = C \to (A \leq B \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C))$
168	156 167	jaod	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \to ((0 < C \lor 0 = C) \to (A \leq B \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C))$
169	4 168	sylbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land C \in ℝ^{*}) \to (0 \leq C \to (A \leq B \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C))$
170	169	expimpd	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((C \in ℝ^{*} \land 0 \leq C) \to (A \leq B \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C))$
171	170	3impia	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land (C \in ℝ^{*} \land 0 \leq C)) \to (A \leq B \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C)$
172	171	imp	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land (C \in ℝ^{*} \land 0 \leq C)) \land A \leq B) \to A \cdot_{𝑒} C \leq B \cdot_{𝑒} C$

Metamath Proof Explorer

Theorem xlemul1a

Proof