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