Step | Hyp | Ref
| Expression |
1 | | ax-rnegex 7895 |
. . . 4
⊢ (𝐴 ∈ ℝ →
∃𝑥 ∈ ℝ
(𝐴 + 𝑥) = 0) |
2 | 1 | 3ad2ant1 1018 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) →
∃𝑥 ∈ ℝ
(𝐴 + 𝑥) = 0) |
3 | | recn 7919 |
. . . 4
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
4 | | recn 7919 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
5 | | oveq2 5873 |
. . . . . . . . . . 11
⊢ ((𝐴 + 𝐵) = (𝐴 + 𝐶) → (𝑥 + (𝐴 + 𝐵)) = (𝑥 + (𝐴 + 𝐶))) |
6 | | simpr 110 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → 𝑥 ∈
ℂ) |
7 | | simpll 527 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → 𝐴 ∈
ℂ) |
8 | | simplrl 535 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → 𝐵 ∈
ℂ) |
9 | 6, 7, 8 | addassd 7954 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → ((𝑥 + 𝐴) + 𝐵) = (𝑥 + (𝐴 + 𝐵))) |
10 | | simplrr 536 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → 𝐶 ∈
ℂ) |
11 | 6, 7, 10 | addassd 7954 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → ((𝑥 + 𝐴) + 𝐶) = (𝑥 + (𝐴 + 𝐶))) |
12 | 9, 11 | eqeq12d 2190 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → (((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶) ↔ (𝑥 + (𝐴 + 𝐵)) = (𝑥 + (𝐴 + 𝐶)))) |
13 | 5, 12 | syl5ibr 156 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → ((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶))) |
14 | 13 | adantr 276 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) ∧ (𝐴 + 𝑥) = 0) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → ((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶))) |
15 | | addcom 8068 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴 + 𝑥) = (𝑥 + 𝐴)) |
16 | 15 | eqeq1d 2184 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝐴 + 𝑥) = 0 ↔ (𝑥 + 𝐴) = 0)) |
17 | 16 | adantlr 477 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → ((𝐴 + 𝑥) = 0 ↔ (𝑥 + 𝐴) = 0)) |
18 | | oveq1 5872 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 + 𝐴) = 0 → ((𝑥 + 𝐴) + 𝐵) = (0 + 𝐵)) |
19 | | oveq1 5872 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 + 𝐴) = 0 → ((𝑥 + 𝐴) + 𝐶) = (0 + 𝐶)) |
20 | 18, 19 | eqeq12d 2190 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 + 𝐴) = 0 → (((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶) ↔ (0 + 𝐵) = (0 + 𝐶))) |
21 | 20 | adantl 277 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) ∧ (𝑥 + 𝐴) = 0) → (((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶) ↔ (0 + 𝐵) = (0 + 𝐶))) |
22 | | addid2 8070 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ ℂ → (0 +
𝐵) = 𝐵) |
23 | | addid2 8070 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 ∈ ℂ → (0 +
𝐶) = 𝐶) |
24 | 22, 23 | eqeqan12d 2191 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((0 +
𝐵) = (0 + 𝐶) ↔ 𝐵 = 𝐶)) |
25 | 24 | adantl 277 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) → ((0 +
𝐵) = (0 + 𝐶) ↔ 𝐵 = 𝐶)) |
26 | 25 | ad2antrr 488 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) ∧ (𝑥 + 𝐴) = 0) → ((0 + 𝐵) = (0 + 𝐶) ↔ 𝐵 = 𝐶)) |
27 | 21, 26 | bitrd 188 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) ∧ (𝑥 + 𝐴) = 0) → (((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶) ↔ 𝐵 = 𝐶)) |
28 | 27 | ex 115 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → ((𝑥 + 𝐴) = 0 → (((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶) ↔ 𝐵 = 𝐶))) |
29 | 17, 28 | sylbid 150 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → ((𝐴 + 𝑥) = 0 → (((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶) ↔ 𝐵 = 𝐶))) |
30 | 29 | imp 124 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) ∧ (𝐴 + 𝑥) = 0) → (((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶) ↔ 𝐵 = 𝐶)) |
31 | 14, 30 | sylibd 149 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) ∧ (𝐴 + 𝑥) = 0) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → 𝐵 = 𝐶)) |
32 | 31 | ex 115 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → ((𝐴 + 𝑥) = 0 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → 𝐵 = 𝐶))) |
33 | 4, 32 | sylan2 286 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℝ) → ((𝐴 + 𝑥) = 0 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → 𝐵 = 𝐶))) |
34 | 33 | rexlimdva 2592 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) →
(∃𝑥 ∈ ℝ
(𝐴 + 𝑥) = 0 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → 𝐵 = 𝐶))) |
35 | 34 | 3impb 1199 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) →
(∃𝑥 ∈ ℝ
(𝐴 + 𝑥) = 0 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → 𝐵 = 𝐶))) |
36 | 3, 35 | syl3an1 1271 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) →
(∃𝑥 ∈ ℝ
(𝐴 + 𝑥) = 0 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → 𝐵 = 𝐶))) |
37 | 2, 36 | mpd 13 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → 𝐵 = 𝐶)) |
38 | | oveq2 5873 |
. 2
⊢ (𝐵 = 𝐶 → (𝐴 + 𝐵) = (𝐴 + 𝐶)) |
39 | 37, 38 | impbid1 142 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶)) |