Step |
Hyp |
Ref |
Expression |
1 |
|
iccssxr |
⊢ ( 0 [,] +∞ ) ⊆ ℝ* |
2 |
|
simpl1 |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ 𝐵 = +∞ ) → 𝐴 ∈ ( 0 [,] +∞ ) ) |
3 |
1 2
|
sselid |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ 𝐵 = +∞ ) → 𝐴 ∈ ℝ* ) |
4 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ 𝐵 = +∞ ) → 𝐵 = +∞ ) |
5 |
|
simpl3 |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ 𝐵 = +∞ ) → 𝐵 ≤ 𝐴 ) |
6 |
4 5
|
eqbrtrrd |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ 𝐵 = +∞ ) → +∞ ≤ 𝐴 ) |
7 |
|
xgepnf |
⊢ ( 𝐴 ∈ ℝ* → ( +∞ ≤ 𝐴 ↔ 𝐴 = +∞ ) ) |
8 |
7
|
biimpa |
⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ≤ 𝐴 ) → 𝐴 = +∞ ) |
9 |
3 6 8
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ 𝐵 = +∞ ) → 𝐴 = +∞ ) |
10 |
|
xnegeq |
⊢ ( 𝐵 = +∞ → -𝑒 𝐵 = -𝑒 +∞ ) |
11 |
4 10
|
syl |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ 𝐵 = +∞ ) → -𝑒 𝐵 = -𝑒 +∞ ) |
12 |
9 11
|
oveq12d |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ 𝐵 = +∞ ) → ( 𝐴 +𝑒 -𝑒 𝐵 ) = ( +∞ +𝑒 -𝑒 +∞ ) ) |
13 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
14 |
|
xnegid |
⊢ ( +∞ ∈ ℝ* → ( +∞ +𝑒 -𝑒 +∞ ) = 0 ) |
15 |
13 14
|
ax-mp |
⊢ ( +∞ +𝑒 -𝑒 +∞ ) = 0 |
16 |
12 15
|
eqtrdi |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ 𝐵 = +∞ ) → ( 𝐴 +𝑒 -𝑒 𝐵 ) = 0 ) |
17 |
16
|
oveq1d |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ 𝐵 = +∞ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = ( 0 +𝑒 𝐵 ) ) |
18 |
4
|
oveq2d |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ 𝐵 = +∞ ) → ( 0 +𝑒 𝐵 ) = ( 0 +𝑒 +∞ ) ) |
19 |
|
xaddid2 |
⊢ ( +∞ ∈ ℝ* → ( 0 +𝑒 +∞ ) = +∞ ) |
20 |
13 19
|
mp1i |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ 𝐵 = +∞ ) → ( 0 +𝑒 +∞ ) = +∞ ) |
21 |
17 18 20
|
3eqtrd |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ 𝐵 = +∞ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = +∞ ) |
22 |
21 9
|
eqtr4d |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ 𝐵 = +∞ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = 𝐴 ) |
23 |
|
simpl1 |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ ¬ 𝐵 = +∞ ) → 𝐴 ∈ ( 0 [,] +∞ ) ) |
24 |
1 23
|
sselid |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ ¬ 𝐵 = +∞ ) → 𝐴 ∈ ℝ* ) |
25 |
|
xrge0neqmnf |
⊢ ( 𝐴 ∈ ( 0 [,] +∞ ) → 𝐴 ≠ -∞ ) |
26 |
23 25
|
syl |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ ¬ 𝐵 = +∞ ) → 𝐴 ≠ -∞ ) |
27 |
|
simpl2 |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ ¬ 𝐵 = +∞ ) → 𝐵 ∈ ( 0 [,] +∞ ) ) |
28 |
1 27
|
sselid |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ ¬ 𝐵 = +∞ ) → 𝐵 ∈ ℝ* ) |
29 |
28
|
xnegcld |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ ¬ 𝐵 = +∞ ) → -𝑒 𝐵 ∈ ℝ* ) |
30 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ ¬ 𝐵 = +∞ ) → ¬ 𝐵 = +∞ ) |
31 |
|
xnegneg |
⊢ ( 𝐵 ∈ ℝ* → -𝑒 -𝑒 𝐵 = 𝐵 ) |
32 |
|
xnegeq |
⊢ ( -𝑒 𝐵 = -∞ → -𝑒 -𝑒 𝐵 = -𝑒 -∞ ) |
33 |
31 32
|
sylan9req |
⊢ ( ( 𝐵 ∈ ℝ* ∧ -𝑒 𝐵 = -∞ ) → 𝐵 = -𝑒 -∞ ) |
34 |
|
xnegmnf |
⊢ -𝑒 -∞ = +∞ |
35 |
33 34
|
eqtrdi |
⊢ ( ( 𝐵 ∈ ℝ* ∧ -𝑒 𝐵 = -∞ ) → 𝐵 = +∞ ) |
36 |
35
|
stoic1a |
⊢ ( ( 𝐵 ∈ ℝ* ∧ ¬ 𝐵 = +∞ ) → ¬ -𝑒 𝐵 = -∞ ) |
37 |
36
|
neqned |
⊢ ( ( 𝐵 ∈ ℝ* ∧ ¬ 𝐵 = +∞ ) → -𝑒 𝐵 ≠ -∞ ) |
38 |
28 30 37
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ ¬ 𝐵 = +∞ ) → -𝑒 𝐵 ≠ -∞ ) |
39 |
|
xrge0neqmnf |
⊢ ( 𝐵 ∈ ( 0 [,] +∞ ) → 𝐵 ≠ -∞ ) |
40 |
27 39
|
syl |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ ¬ 𝐵 = +∞ ) → 𝐵 ≠ -∞ ) |
41 |
|
xaddass |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) ∧ ( -𝑒 𝐵 ∈ ℝ* ∧ -𝑒 𝐵 ≠ -∞ ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ -∞ ) ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = ( 𝐴 +𝑒 ( -𝑒 𝐵 +𝑒 𝐵 ) ) ) |
42 |
24 26 29 38 28 40 41
|
syl222anc |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ ¬ 𝐵 = +∞ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = ( 𝐴 +𝑒 ( -𝑒 𝐵 +𝑒 𝐵 ) ) ) |
43 |
|
xnegcl |
⊢ ( 𝐵 ∈ ℝ* → -𝑒 𝐵 ∈ ℝ* ) |
44 |
|
xaddcom |
⊢ ( ( -𝑒 𝐵 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( -𝑒 𝐵 +𝑒 𝐵 ) = ( 𝐵 +𝑒 -𝑒 𝐵 ) ) |
45 |
43 44
|
mpancom |
⊢ ( 𝐵 ∈ ℝ* → ( -𝑒 𝐵 +𝑒 𝐵 ) = ( 𝐵 +𝑒 -𝑒 𝐵 ) ) |
46 |
|
xnegid |
⊢ ( 𝐵 ∈ ℝ* → ( 𝐵 +𝑒 -𝑒 𝐵 ) = 0 ) |
47 |
45 46
|
eqtrd |
⊢ ( 𝐵 ∈ ℝ* → ( -𝑒 𝐵 +𝑒 𝐵 ) = 0 ) |
48 |
47
|
oveq2d |
⊢ ( 𝐵 ∈ ℝ* → ( 𝐴 +𝑒 ( -𝑒 𝐵 +𝑒 𝐵 ) ) = ( 𝐴 +𝑒 0 ) ) |
49 |
|
xaddid1 |
⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 +𝑒 0 ) = 𝐴 ) |
50 |
48 49
|
sylan9eqr |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 +𝑒 ( -𝑒 𝐵 +𝑒 𝐵 ) ) = 𝐴 ) |
51 |
24 28 50
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ ¬ 𝐵 = +∞ ) → ( 𝐴 +𝑒 ( -𝑒 𝐵 +𝑒 𝐵 ) ) = 𝐴 ) |
52 |
42 51
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) ∧ ¬ 𝐵 = +∞ ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = 𝐴 ) |
53 |
22 52
|
pm2.61dan |
⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ≤ 𝐴 ) → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) +𝑒 𝐵 ) = 𝐴 ) |