xlemul1a

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

		Ref	Expression
	Assertion	xlemul1a	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ ( 𝐶 ∈ ℝ^* ∧ 0 ≤ 𝐶 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 ·_e 𝐶 ) ≤ ( 𝐵 ·_e 𝐶 ) )

Proof

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

Metamath Proof Explorer

Theorem xlemul1a

Proof