Step |
Hyp |
Ref |
Expression |
1 |
|
simpl1 |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → 𝐴 ∈ ℝ* ) |
2 |
|
simpl2 |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → 𝐵 ∈ ℝ* ) |
3 |
|
xnegcl |
⊢ ( 𝐵 ∈ ℝ* → -𝑒 𝐵 ∈ ℝ* ) |
4 |
2 3
|
syl |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → -𝑒 𝐵 ∈ ℝ* ) |
5 |
|
xaddcl |
⊢ ( ( 𝐴 ∈ ℝ* ∧ -𝑒 𝐵 ∈ ℝ* ) → ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ* ) |
6 |
1 4 5
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ* ) |
7 |
6
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐵 ∈ ℝ ) → ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ* ) |
8 |
|
simpll3 |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐵 ∈ ℝ ) → 𝐶 ∈ ℝ* ) |
9 |
|
simpr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ ) |
10 |
|
xleadd1 |
⊢ ( ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶 ↔ ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) ≤ ( 𝐶 +𝑒 𝐵 ) ) ) |
11 |
7 8 9 10
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶 ↔ ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) ≤ ( 𝐶 +𝑒 𝐵 ) ) ) |
12 |
|
xnpcan |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = 𝐴 ) |
13 |
1 12
|
sylan |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = 𝐴 ) |
14 |
13
|
breq1d |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) ≤ ( 𝐶 +𝑒 𝐵 ) ↔ 𝐴 ≤ ( 𝐶 +𝑒 𝐵 ) ) ) |
15 |
11 14
|
bitrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐶 +𝑒 𝐵 ) ) ) |
16 |
|
simpr3 |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → 0 ≤ 𝐶 ) |
17 |
|
oveq1 |
⊢ ( 𝐴 = +∞ → ( 𝐴 +𝑒 -∞ ) = ( +∞ +𝑒 -∞ ) ) |
18 |
|
pnfaddmnf |
⊢ ( +∞ +𝑒 -∞ ) = 0 |
19 |
17 18
|
eqtrdi |
⊢ ( 𝐴 = +∞ → ( 𝐴 +𝑒 -∞ ) = 0 ) |
20 |
19
|
breq1d |
⊢ ( 𝐴 = +∞ → ( ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 ↔ 0 ≤ 𝐶 ) ) |
21 |
16 20
|
syl5ibrcom |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 = +∞ → ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 ) ) |
22 |
|
xaddmnf1 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) → ( 𝐴 +𝑒 -∞ ) = -∞ ) |
23 |
22
|
ex |
⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ≠ +∞ → ( 𝐴 +𝑒 -∞ ) = -∞ ) ) |
24 |
1 23
|
syl |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 ≠ +∞ → ( 𝐴 +𝑒 -∞ ) = -∞ ) ) |
25 |
|
simpl3 |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → 𝐶 ∈ ℝ* ) |
26 |
|
mnfle |
⊢ ( 𝐶 ∈ ℝ* → -∞ ≤ 𝐶 ) |
27 |
25 26
|
syl |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → -∞ ≤ 𝐶 ) |
28 |
|
breq1 |
⊢ ( ( 𝐴 +𝑒 -∞ ) = -∞ → ( ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 ↔ -∞ ≤ 𝐶 ) ) |
29 |
27 28
|
syl5ibrcom |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( ( 𝐴 +𝑒 -∞ ) = -∞ → ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 ) ) |
30 |
24 29
|
syld |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 ≠ +∞ → ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 ) ) |
31 |
21 30
|
pm2.61dne |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 ) |
32 |
|
pnfge |
⊢ ( 𝐴 ∈ ℝ* → 𝐴 ≤ +∞ ) |
33 |
1 32
|
syl |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → 𝐴 ≤ +∞ ) |
34 |
|
ge0nemnf |
⊢ ( ( 𝐶 ∈ ℝ* ∧ 0 ≤ 𝐶 ) → 𝐶 ≠ -∞ ) |
35 |
25 16 34
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → 𝐶 ≠ -∞ ) |
36 |
|
xaddpnf1 |
⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞ ) → ( 𝐶 +𝑒 +∞ ) = +∞ ) |
37 |
25 35 36
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐶 +𝑒 +∞ ) = +∞ ) |
38 |
33 37
|
breqtrrd |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → 𝐴 ≤ ( 𝐶 +𝑒 +∞ ) ) |
39 |
31 38
|
2thd |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐶 +𝑒 +∞ ) ) ) |
40 |
|
xnegeq |
⊢ ( 𝐵 = +∞ → -𝑒 𝐵 = -𝑒 +∞ ) |
41 |
|
xnegpnf |
⊢ -𝑒 +∞ = -∞ |
42 |
40 41
|
eqtrdi |
⊢ ( 𝐵 = +∞ → -𝑒 𝐵 = -∞ ) |
43 |
42
|
oveq2d |
⊢ ( 𝐵 = +∞ → ( 𝐴 +𝑒 -𝑒 𝐵 ) = ( 𝐴 +𝑒 -∞ ) ) |
44 |
43
|
breq1d |
⊢ ( 𝐵 = +∞ → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶 ↔ ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 ) ) |
45 |
|
oveq2 |
⊢ ( 𝐵 = +∞ → ( 𝐶 +𝑒 𝐵 ) = ( 𝐶 +𝑒 +∞ ) ) |
46 |
45
|
breq2d |
⊢ ( 𝐵 = +∞ → ( 𝐴 ≤ ( 𝐶 +𝑒 𝐵 ) ↔ 𝐴 ≤ ( 𝐶 +𝑒 +∞ ) ) ) |
47 |
44 46
|
bibi12d |
⊢ ( 𝐵 = +∞ → ( ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐶 +𝑒 𝐵 ) ) ↔ ( ( 𝐴 +𝑒 -∞ ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐶 +𝑒 +∞ ) ) ) ) |
48 |
39 47
|
syl5ibrcom |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐵 = +∞ → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐶 +𝑒 𝐵 ) ) ) ) |
49 |
48
|
imp |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐵 = +∞ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐶 +𝑒 𝐵 ) ) ) |
50 |
|
simpr2 |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → 𝐵 ≠ -∞ ) |
51 |
2 50
|
jca |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ) |
52 |
|
xrnemnf |
⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ↔ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) ) |
53 |
51 52
|
sylib |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ) ) |
54 |
15 49 53
|
mpjaodan |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 0 ≤ 𝐴 ∧ 𝐵 ≠ -∞ ∧ 0 ≤ 𝐶 ) ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ≤ 𝐶 ↔ 𝐴 ≤ ( 𝐶 +𝑒 𝐵 ) ) ) |