# Metamath Proof Explorer

## Theorem xlemul1a

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

Ref Expression
Assertion xlemul1a ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge \left({C}\in {ℝ}^{*}\wedge 0\le {C}\right)\right)\wedge {A}\le {B}\right)\to {A}{\cdot }_{𝑒}{C}\le {B}{\cdot }_{𝑒}{C}$

### Proof

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