Proof of Theorem xaddass2
| Step | Hyp | Ref
| Expression |
| 1 | | simp1l 1198 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) → 𝐴 ∈
ℝ*) |
| 2 | | xnegcl 13255 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ -𝑒𝐴 ∈
ℝ*) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
-𝑒𝐴
∈ ℝ*) |
| 4 | | simp1r 1199 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) → 𝐴 ≠ +∞) |
| 5 | | pnfxr 11315 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
| 6 | | xneg11 13257 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (-𝑒𝐴 = -𝑒+∞
↔ 𝐴 =
+∞)) |
| 7 | 1, 5, 6 | sylancl 586 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
(-𝑒𝐴 =
-𝑒+∞ ↔ 𝐴 = +∞)) |
| 8 | 7 | necon3bid 2985 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
(-𝑒𝐴
≠ -𝑒+∞ ↔ 𝐴 ≠ +∞)) |
| 9 | 4, 8 | mpbird 257 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
-𝑒𝐴 ≠
-𝑒+∞) |
| 10 | | xnegpnf 13251 |
. . . . . . 7
⊢
-𝑒+∞ = -∞ |
| 11 | 10 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
-𝑒+∞ = -∞) |
| 12 | 9, 11 | neeqtrd 3010 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
-𝑒𝐴 ≠
-∞) |
| 13 | | simp2l 1200 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) → 𝐵 ∈
ℝ*) |
| 14 | | xnegcl 13255 |
. . . . . 6
⊢ (𝐵 ∈ ℝ*
→ -𝑒𝐵 ∈
ℝ*) |
| 15 | 13, 14 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
-𝑒𝐵
∈ ℝ*) |
| 16 | | simp2r 1201 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) → 𝐵 ≠ +∞) |
| 17 | | xneg11 13257 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (-𝑒𝐵 = -𝑒+∞
↔ 𝐵 =
+∞)) |
| 18 | 13, 5, 17 | sylancl 586 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
(-𝑒𝐵 =
-𝑒+∞ ↔ 𝐵 = +∞)) |
| 19 | 18 | necon3bid 2985 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
(-𝑒𝐵
≠ -𝑒+∞ ↔ 𝐵 ≠ +∞)) |
| 20 | 16, 19 | mpbird 257 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
-𝑒𝐵 ≠
-𝑒+∞) |
| 21 | 20, 11 | neeqtrd 3010 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
-𝑒𝐵 ≠
-∞) |
| 22 | | simp3l 1202 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) → 𝐶 ∈
ℝ*) |
| 23 | | xnegcl 13255 |
. . . . . 6
⊢ (𝐶 ∈ ℝ*
→ -𝑒𝐶 ∈
ℝ*) |
| 24 | 22, 23 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
-𝑒𝐶
∈ ℝ*) |
| 25 | | simp3r 1203 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) → 𝐶 ≠ +∞) |
| 26 | | xneg11 13257 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (-𝑒𝐶 = -𝑒+∞
↔ 𝐶 =
+∞)) |
| 27 | 22, 5, 26 | sylancl 586 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
(-𝑒𝐶 =
-𝑒+∞ ↔ 𝐶 = +∞)) |
| 28 | 27 | necon3bid 2985 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
(-𝑒𝐶
≠ -𝑒+∞ ↔ 𝐶 ≠ +∞)) |
| 29 | 25, 28 | mpbird 257 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
-𝑒𝐶 ≠
-𝑒+∞) |
| 30 | 29, 11 | neeqtrd 3010 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
-𝑒𝐶 ≠
-∞) |
| 31 | | xaddass 13291 |
. . . . 5
⊢
(((-𝑒𝐴 ∈ ℝ* ∧
-𝑒𝐴 ≠
-∞) ∧ (-𝑒𝐵 ∈ ℝ* ∧
-𝑒𝐵 ≠
-∞) ∧ (-𝑒𝐶 ∈ ℝ* ∧
-𝑒𝐶 ≠
-∞)) → ((-𝑒𝐴 +𝑒
-𝑒𝐵)
+𝑒 -𝑒𝐶) = (-𝑒𝐴 +𝑒
(-𝑒𝐵
+𝑒 -𝑒𝐶))) |
| 32 | 3, 12, 15, 21, 24, 30, 31 | syl222anc 1388 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
((-𝑒𝐴
+𝑒 -𝑒𝐵) +𝑒
-𝑒𝐶) =
(-𝑒𝐴
+𝑒 (-𝑒𝐵 +𝑒
-𝑒𝐶))) |
| 33 | | xnegdi 13290 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒
-𝑒𝐵)) |
| 34 | 1, 13, 33 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
-𝑒(𝐴
+𝑒 𝐵) =
(-𝑒𝐴
+𝑒 -𝑒𝐵)) |
| 35 | 34 | oveq1d 7446 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
(-𝑒(𝐴
+𝑒 𝐵)
+𝑒 -𝑒𝐶) = ((-𝑒𝐴 +𝑒
-𝑒𝐵)
+𝑒 -𝑒𝐶)) |
| 36 | | xnegdi 13290 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → -𝑒(𝐵 +𝑒 𝐶) = (-𝑒𝐵 +𝑒
-𝑒𝐶)) |
| 37 | 13, 22, 36 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
-𝑒(𝐵
+𝑒 𝐶) =
(-𝑒𝐵
+𝑒 -𝑒𝐶)) |
| 38 | 37 | oveq2d 7447 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
(-𝑒𝐴
+𝑒 -𝑒(𝐵 +𝑒 𝐶)) = (-𝑒𝐴 +𝑒
(-𝑒𝐵
+𝑒 -𝑒𝐶))) |
| 39 | 32, 35, 38 | 3eqtr4d 2787 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
(-𝑒(𝐴
+𝑒 𝐵)
+𝑒 -𝑒𝐶) = (-𝑒𝐴 +𝑒
-𝑒(𝐵
+𝑒 𝐶))) |
| 40 | | xaddcl 13281 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 +𝑒 𝐵) ∈
ℝ*) |
| 41 | 1, 13, 40 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) → (𝐴 +𝑒 𝐵) ∈
ℝ*) |
| 42 | | xnegdi 13290 |
. . . 4
⊢ (((𝐴 +𝑒 𝐵) ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → -𝑒((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (-𝑒(𝐴 +𝑒 𝐵) +𝑒
-𝑒𝐶)) |
| 43 | 41, 22, 42 | syl2anc 584 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
-𝑒((𝐴
+𝑒 𝐵)
+𝑒 𝐶) =
(-𝑒(𝐴
+𝑒 𝐵)
+𝑒 -𝑒𝐶)) |
| 44 | | xaddcl 13281 |
. . . . 5
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
| 45 | 13, 22, 44 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
| 46 | | xnegdi 13290 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵
+𝑒 𝐶)
∈ ℝ*) → -𝑒(𝐴 +𝑒 (𝐵 +𝑒 𝐶)) = (-𝑒𝐴 +𝑒
-𝑒(𝐵
+𝑒 𝐶))) |
| 47 | 1, 45, 46 | syl2anc 584 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
-𝑒(𝐴
+𝑒 (𝐵
+𝑒 𝐶)) =
(-𝑒𝐴
+𝑒 -𝑒(𝐵 +𝑒 𝐶))) |
| 48 | 39, 43, 47 | 3eqtr4d 2787 |
. 2
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
-𝑒((𝐴
+𝑒 𝐵)
+𝑒 𝐶) =
-𝑒(𝐴
+𝑒 (𝐵
+𝑒 𝐶))) |
| 49 | | xaddcl 13281 |
. . . 4
⊢ (((𝐴 +𝑒 𝐵) ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) ∈
ℝ*) |
| 50 | 41, 22, 49 | syl2anc 584 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) ∈
ℝ*) |
| 51 | | xaddcl 13281 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵
+𝑒 𝐶)
∈ ℝ*) → (𝐴 +𝑒 (𝐵 +𝑒 𝐶)) ∈
ℝ*) |
| 52 | 1, 45, 51 | syl2anc 584 |
. . 3
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) → (𝐴 +𝑒 (𝐵 +𝑒 𝐶)) ∈
ℝ*) |
| 53 | | xneg11 13257 |
. . 3
⊢ ((((𝐴 +𝑒 𝐵) +𝑒 𝐶) ∈ ℝ*
∧ (𝐴
+𝑒 (𝐵
+𝑒 𝐶))
∈ ℝ*) → (-𝑒((𝐴 +𝑒 𝐵) +𝑒 𝐶) = -𝑒(𝐴 +𝑒 (𝐵 +𝑒 𝐶)) ↔ ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶)))) |
| 54 | 50, 52, 53 | syl2anc 584 |
. 2
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) →
(-𝑒((𝐴
+𝑒 𝐵)
+𝑒 𝐶) =
-𝑒(𝐴
+𝑒 (𝐵
+𝑒 𝐶))
↔ ((𝐴
+𝑒 𝐵)
+𝑒 𝐶) =
(𝐴 +𝑒
(𝐵 +𝑒
𝐶)))) |
| 55 | 48, 54 | mpbid 232 |
1
⊢ (((𝐴 ∈ ℝ*
∧ 𝐴 ≠ +∞)
∧ (𝐵 ∈
ℝ* ∧ 𝐵
≠ +∞) ∧ (𝐶
∈ ℝ* ∧ 𝐶 ≠ +∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) |