Step | Hyp | Ref
| Expression |
1 | | readdcl 6805 |
. . . . . 6
⊢ ((𝑏 ∈ ℝ ∧
x ∈
ℝ) → (𝑏 + x) ∈
ℝ) |
2 | | ax-rnegex 6792 |
. . . . . 6
⊢ ((𝑏 + x) ∈ ℝ
→ ∃𝑐 ∈ ℝ
((𝑏 + x) + 𝑐) = 0) |
3 | 1, 2 | syl 14 |
. . . . 5
⊢ ((𝑏 ∈ ℝ ∧
x ∈
ℝ) → ∃𝑐 ∈ ℝ
((𝑏 + x) + 𝑐) = 0) |
4 | 3 | adantlr 446 |
. . . 4
⊢ (((𝑏 ∈ ℝ ∧
y ∈
ℝ) ∧ x ∈ ℝ)
→ ∃𝑐 ∈ ℝ
((𝑏 + x) + 𝑐) = 0) |
5 | 4 | adantr 261 |
. . 3
⊢ ((((𝑏 ∈ ℝ ∧
y ∈
ℝ) ∧ x ∈ ℝ) ∧ (y + x) = 0) → ∃𝑐 ∈ ℝ
((𝑏 + x) + 𝑐) = 0) |
6 | | recn 6812 |
. . . . . . . 8
⊢ (𝑏 ∈ ℝ → 𝑏 ∈
ℂ) |
7 | | recn 6812 |
. . . . . . . 8
⊢ (y ∈ ℝ →
y ∈
ℂ) |
8 | 6, 7 | anim12i 321 |
. . . . . . 7
⊢ ((𝑏 ∈ ℝ ∧
y ∈
ℝ) → (𝑏 ∈ ℂ ∧
y ∈
ℂ)) |
9 | 8 | anim1i 323 |
. . . . . 6
⊢ (((𝑏 ∈ ℝ ∧
y ∈
ℝ) ∧ x ∈ ℝ)
→ ((𝑏 ∈ ℂ ∧
y ∈
ℂ) ∧ x ∈
ℝ)) |
10 | 9 | anim1i 323 |
. . . . 5
⊢ ((((𝑏 ∈ ℝ ∧
y ∈
ℝ) ∧ x ∈ ℝ) ∧ (y + x) = 0) → (((𝑏 ∈ ℂ
∧ y ∈ ℂ) ∧
x ∈
ℝ) ∧ (y + x) =
0)) |
11 | | recn 6812 |
. . . . 5
⊢ (𝑐 ∈ ℝ → 𝑐 ∈
ℂ) |
12 | | recn 6812 |
. . . . . . . . . 10
⊢ (x ∈ ℝ →
x ∈
ℂ) |
13 | | add32 6967 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℂ ∧
x ∈
ℂ ∧ 𝑐 ∈ ℂ)
→ ((𝑏 + x) + 𝑐) = ((𝑏 + 𝑐) + x)) |
14 | 13 | 3expa 1103 |
. . . . . . . . . . 11
⊢ (((𝑏 ∈ ℂ ∧
x ∈
ℂ) ∧ 𝑐 ∈ ℂ)
→ ((𝑏 + x) + 𝑐) = ((𝑏 + 𝑐) + x)) |
15 | | addcl 6804 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) → (𝑏 + 𝑐) ∈
ℂ) |
16 | | addcom 6947 |
. . . . . . . . . . . . 13
⊢ (((𝑏 + 𝑐) ∈ ℂ
∧ x ∈ ℂ) → ((𝑏 + 𝑐) + x) =
(x + (𝑏 + 𝑐))) |
17 | 15, 16 | sylan 267 |
. . . . . . . . . . . 12
⊢ (((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) ∧
x ∈
ℂ) → ((𝑏 + 𝑐) + x) = (x + (𝑏 + 𝑐))) |
18 | 17 | an32s 502 |
. . . . . . . . . . 11
⊢ (((𝑏 ∈ ℂ ∧
x ∈
ℂ) ∧ 𝑐 ∈ ℂ)
→ ((𝑏 + 𝑐) + x) =
(x + (𝑏 + 𝑐))) |
19 | 14, 18 | eqtr2d 2070 |
. . . . . . . . . 10
⊢ (((𝑏 ∈ ℂ ∧
x ∈
ℂ) ∧ 𝑐 ∈ ℂ)
→ (x + (𝑏 + 𝑐)) = ((𝑏 + x) +
𝑐)) |
20 | 12, 19 | sylanl2 383 |
. . . . . . . . 9
⊢ (((𝑏 ∈ ℂ ∧
x ∈
ℝ) ∧ 𝑐 ∈ ℂ)
→ (x + (𝑏 + 𝑐)) = ((𝑏 + x) +
𝑐)) |
21 | 20 | adantllr 450 |
. . . . . . . 8
⊢ ((((𝑏 ∈ ℂ ∧
y ∈
ℂ) ∧ x ∈ ℝ) ∧ 𝑐
∈ ℂ) → (x + (𝑏 + 𝑐)) = ((𝑏 + x) +
𝑐)) |
22 | 21 | adantlr 446 |
. . . . . . 7
⊢
(((((𝑏 ∈ ℂ ∧
y ∈
ℂ) ∧ x ∈ ℝ) ∧ (y + x) = 0) ∧ 𝑐 ∈ ℂ) → (x + (𝑏 + 𝑐)) = ((𝑏 + x) +
𝑐)) |
23 | | addcom 6947 |
. . . . . . . . . . . 12
⊢
((x ∈ ℂ ∧
y ∈
ℂ) → (x + y) = (y +
x)) |
24 | 23 | ancoms 255 |
. . . . . . . . . . 11
⊢
((y ∈ ℂ ∧
x ∈
ℂ) → (x + y) = (y +
x)) |
25 | 12, 24 | sylan2 270 |
. . . . . . . . . 10
⊢
((y ∈ ℂ ∧
x ∈
ℝ) → (x + y) = (y +
x)) |
26 | | id 19 |
. . . . . . . . . 10
⊢
((y + x) = 0 → (y
+ x) = 0) |
27 | 25, 26 | sylan9eq 2089 |
. . . . . . . . 9
⊢
(((y ∈ ℂ ∧
x ∈
ℝ) ∧ (y + x) = 0)
→ (x + y) = 0) |
28 | 27 | adantlll 449 |
. . . . . . . 8
⊢ ((((𝑏 ∈ ℂ ∧
y ∈
ℂ) ∧ x ∈ ℝ) ∧ (y + x) = 0) → (x + y) =
0) |
29 | 28 | adantr 261 |
. . . . . . 7
⊢
(((((𝑏 ∈ ℂ ∧
y ∈
ℂ) ∧ x ∈ ℝ) ∧ (y + x) = 0) ∧ 𝑐 ∈ ℂ) → (x + y) =
0) |
30 | 22, 29 | eqeq12d 2051 |
. . . . . 6
⊢
(((((𝑏 ∈ ℂ ∧
y ∈
ℂ) ∧ x ∈ ℝ) ∧ (y + x) = 0) ∧ 𝑐 ∈ ℂ) → ((x + (𝑏 + 𝑐)) = (x +
y) ↔ ((𝑏 + x) +
𝑐) = 0)) |
31 | | simplr 482 |
. . . . . . . 8
⊢ ((((𝑏 ∈ ℂ ∧
y ∈
ℂ) ∧ x ∈ ℝ) ∧ 𝑐
∈ ℂ) → x ∈
ℝ) |
32 | 15 | adantlr 446 |
. . . . . . . . 9
⊢ (((𝑏 ∈ ℂ ∧
y ∈
ℂ) ∧ 𝑐 ∈ ℂ)
→ (𝑏 + 𝑐) ∈
ℂ) |
33 | 32 | adantlr 446 |
. . . . . . . 8
⊢ ((((𝑏 ∈ ℂ ∧
y ∈
ℂ) ∧ x ∈ ℝ) ∧ 𝑐
∈ ℂ) → (𝑏 + 𝑐) ∈
ℂ) |
34 | | simpllr 486 |
. . . . . . . 8
⊢ ((((𝑏 ∈ ℂ ∧
y ∈
ℂ) ∧ x ∈ ℝ) ∧ 𝑐
∈ ℂ) → y ∈
ℂ) |
35 | | cnegexlem1 6983 |
. . . . . . . 8
⊢
((x ∈ ℝ ∧ (𝑏 + 𝑐) ∈ ℂ
∧ y ∈ ℂ) → ((x + (𝑏 + 𝑐)) = (x +
y) ↔ (𝑏 + 𝑐) = y)) |
36 | 31, 33, 34, 35 | syl3anc 1134 |
. . . . . . 7
⊢ ((((𝑏 ∈ ℂ ∧
y ∈
ℂ) ∧ x ∈ ℝ) ∧ 𝑐
∈ ℂ) → ((x + (𝑏 + 𝑐)) = (x +
y) ↔ (𝑏 + 𝑐) = y)) |
37 | 36 | adantlr 446 |
. . . . . 6
⊢
(((((𝑏 ∈ ℂ ∧
y ∈
ℂ) ∧ x ∈ ℝ) ∧ (y + x) = 0) ∧ 𝑐 ∈ ℂ) → ((x + (𝑏 + 𝑐)) = (x +
y) ↔ (𝑏 + 𝑐) = y)) |
38 | 30, 37 | bitr3d 179 |
. . . . 5
⊢
(((((𝑏 ∈ ℂ ∧
y ∈
ℂ) ∧ x ∈ ℝ) ∧ (y + x) = 0) ∧ 𝑐 ∈ ℂ) → (((𝑏 + x) +
𝑐) = 0 ↔ (𝑏 + 𝑐) = y)) |
39 | 10, 11, 38 | syl2an 273 |
. . . 4
⊢
(((((𝑏 ∈ ℝ ∧
y ∈
ℝ) ∧ x ∈ ℝ) ∧ (y + x) = 0) ∧ 𝑐 ∈ ℝ) → (((𝑏 + x) +
𝑐) = 0 ↔ (𝑏 + 𝑐) = y)) |
40 | 39 | rexbidva 2317 |
. . 3
⊢ ((((𝑏 ∈ ℝ ∧
y ∈
ℝ) ∧ x ∈ ℝ) ∧ (y + x) = 0) → (∃𝑐 ∈ ℝ
((𝑏 + x) + 𝑐) = 0 ↔ ∃𝑐 ∈ ℝ
(𝑏 + 𝑐) = y)) |
41 | 5, 40 | mpbid 135 |
. 2
⊢ ((((𝑏 ∈ ℝ ∧
y ∈
ℝ) ∧ x ∈ ℝ) ∧ (y + x) = 0) → ∃𝑐 ∈ ℝ
(𝑏 + 𝑐) = y) |
42 | | ax-rnegex 6792 |
. . 3
⊢ (y ∈ ℝ →
∃x ∈ ℝ (y +
x) = 0) |
43 | 42 | adantl 262 |
. 2
⊢ ((𝑏 ∈ ℝ ∧
y ∈
ℝ) → ∃x ∈ ℝ
(y + x)
= 0) |
44 | 41, 43 | r19.29a 2448 |
1
⊢ ((𝑏 ∈ ℝ ∧
y ∈
ℝ) → ∃𝑐 ∈ ℝ
(𝑏 + 𝑐) = y) |