Step | Hyp | Ref
| Expression |
1 | | renegcl.1 |
. 2
⊢ 𝐴 ∈ ℝ |
2 | | ax-rnegex 10951 |
. 2
⊢ (𝐴 ∈ ℝ →
∃𝑥 ∈ ℝ
(𝐴 + 𝑥) = 0) |
3 | | recn 10970 |
. . . . 5
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
4 | | df-neg 11217 |
. . . . . . 7
⊢ -𝐴 = (0 − 𝐴) |
5 | 4 | eqeq1i 2744 |
. . . . . 6
⊢ (-𝐴 = 𝑥 ↔ (0 − 𝐴) = 𝑥) |
6 | | 0cn 10976 |
. . . . . . 7
⊢ 0 ∈
ℂ |
7 | 1 | recni 10998 |
. . . . . . 7
⊢ 𝐴 ∈ ℂ |
8 | | subadd 11233 |
. . . . . . 7
⊢ ((0
∈ ℂ ∧ 𝐴
∈ ℂ ∧ 𝑥
∈ ℂ) → ((0 − 𝐴) = 𝑥 ↔ (𝐴 + 𝑥) = 0)) |
9 | 6, 7, 8 | mp3an12 1450 |
. . . . . 6
⊢ (𝑥 ∈ ℂ → ((0
− 𝐴) = 𝑥 ↔ (𝐴 + 𝑥) = 0)) |
10 | 5, 9 | bitrid 282 |
. . . . 5
⊢ (𝑥 ∈ ℂ → (-𝐴 = 𝑥 ↔ (𝐴 + 𝑥) = 0)) |
11 | 3, 10 | syl 17 |
. . . 4
⊢ (𝑥 ∈ ℝ → (-𝐴 = 𝑥 ↔ (𝐴 + 𝑥) = 0)) |
12 | | eleq1a 2835 |
. . . 4
⊢ (𝑥 ∈ ℝ → (-𝐴 = 𝑥 → -𝐴 ∈ ℝ)) |
13 | 11, 12 | sylbird 259 |
. . 3
⊢ (𝑥 ∈ ℝ → ((𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ)) |
14 | 13 | rexlimiv 3210 |
. 2
⊢
(∃𝑥 ∈
ℝ (𝐴 + 𝑥) = 0 → -𝐴 ∈ ℝ) |
15 | 1, 2, 14 | mp2b 10 |
1
⊢ -𝐴 ∈ ℝ |