| Step | Hyp | Ref
| Expression |
| 1 | | cnegex 11442 |
. 2
⊢ (𝐴 ∈ ℂ →
∃𝑥 ∈ ℂ
(𝐴 + 𝑥) = 0) |
| 2 | | cnegex 11442 |
. . . 4
⊢ (𝑥 ∈ ℂ →
∃𝑦 ∈ ℂ
(𝑥 + 𝑦) = 0) |
| 3 | 2 | ad2antrl 728 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0)) → ∃𝑦 ∈ ℂ (𝑥 + 𝑦) = 0) |
| 4 | | 0cn 11253 |
. . . . . . . . . 10
⊢ 0 ∈
ℂ |
| 5 | | addass 11242 |
. . . . . . . . . 10
⊢ ((0
∈ ℂ ∧ 0 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((0 + 0) + 𝑦) = (0 + (0 + 𝑦))) |
| 6 | 4, 4, 5 | mp3an12 1453 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℂ → ((0 + 0)
+ 𝑦) = (0 + (0 + 𝑦))) |
| 7 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0) → ((0 + 0) + 𝑦) = (0 + (0 + 𝑦))) |
| 8 | 7 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → ((0 + 0) + 𝑦) = (0 + (0 + 𝑦))) |
| 9 | | 00id 11436 |
. . . . . . . . 9
⊢ (0 + 0) =
0 |
| 10 | 9 | oveq1i 7441 |
. . . . . . . 8
⊢ ((0 + 0)
+ 𝑦) = (0 + 𝑦) |
| 11 | | simp1 1137 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → 𝐴 ∈ ℂ) |
| 12 | | simp2l 1200 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → 𝑥 ∈ ℂ) |
| 13 | | simp3l 1202 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → 𝑦 ∈ ℂ) |
| 14 | 11, 12, 13 | addassd 11283 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → ((𝐴 + 𝑥) + 𝑦) = (𝐴 + (𝑥 + 𝑦))) |
| 15 | | simp2r 1201 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → (𝐴 + 𝑥) = 0) |
| 16 | 15 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → ((𝐴 + 𝑥) + 𝑦) = (0 + 𝑦)) |
| 17 | | simp3r 1203 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → (𝑥 + 𝑦) = 0) |
| 18 | 17 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → (𝐴 + (𝑥 + 𝑦)) = (𝐴 + 0)) |
| 19 | 14, 16, 18 | 3eqtr3rd 2786 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → (𝐴 + 0) = (0 + 𝑦)) |
| 20 | | addrid 11441 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) |
| 21 | 20 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → (𝐴 + 0) = 𝐴) |
| 22 | 19, 21 | eqtr3d 2779 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → (0 + 𝑦) = 𝐴) |
| 23 | 10, 22 | eqtrid 2789 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → ((0 + 0) + 𝑦) = 𝐴) |
| 24 | 22 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → (0 + (0 + 𝑦)) = (0 + 𝐴)) |
| 25 | 8, 23, 24 | 3eqtr3rd 2786 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0) ∧ (𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0)) → (0 + 𝐴) = 𝐴) |
| 26 | 25 | 3expia 1122 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0)) → ((𝑦 ∈ ℂ ∧ (𝑥 + 𝑦) = 0) → (0 + 𝐴) = 𝐴)) |
| 27 | 26 | expd 415 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0)) → (𝑦 ∈ ℂ → ((𝑥 + 𝑦) = 0 → (0 + 𝐴) = 𝐴))) |
| 28 | 27 | rexlimdv 3153 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0)) → (∃𝑦 ∈ ℂ (𝑥 + 𝑦) = 0 → (0 + 𝐴) = 𝐴)) |
| 29 | 3, 28 | mpd 15 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ (𝐴 + 𝑥) = 0)) → (0 + 𝐴) = 𝐴) |
| 30 | 1, 29 | rexlimddv 3161 |
1
⊢ (𝐴 ∈ ℂ → (0 +
𝐴) = 𝐴) |