Metamath Proof Explorer


Theorem 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 𝐶 ) )