This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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