Step | Hyp | Ref
| Expression |
1 | | readdcl 7887 |
. . . . . 6
⊢ ((𝑏 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑏 + 𝑥) ∈ ℝ) |
2 | | ax-rnegex 7870 |
. . . . . 6
⊢ ((𝑏 + 𝑥) ∈ ℝ → ∃𝑐 ∈ ℝ ((𝑏 + 𝑥) + 𝑐) = 0) |
3 | 1, 2 | syl 14 |
. . . . 5
⊢ ((𝑏 ∈ ℝ ∧ 𝑥 ∈ ℝ) →
∃𝑐 ∈ ℝ
((𝑏 + 𝑥) + 𝑐) = 0) |
4 | 3 | adantlr 474 |
. . . 4
⊢ (((𝑏 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) →
∃𝑐 ∈ ℝ
((𝑏 + 𝑥) + 𝑐) = 0) |
5 | 4 | adantr 274 |
. . 3
⊢ ((((𝑏 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ (𝑦 + 𝑥) = 0) → ∃𝑐 ∈ ℝ ((𝑏 + 𝑥) + 𝑐) = 0) |
6 | | recn 7894 |
. . . . . . . 8
⊢ (𝑏 ∈ ℝ → 𝑏 ∈
ℂ) |
7 | | recn 7894 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
8 | 6, 7 | anim12i 336 |
. . . . . . 7
⊢ ((𝑏 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑏 ∈ ℂ ∧ 𝑦 ∈
ℂ)) |
9 | 8 | anim1i 338 |
. . . . . 6
⊢ (((𝑏 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝑏 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ 𝑥 ∈
ℝ)) |
10 | 9 | anim1i 338 |
. . . . 5
⊢ ((((𝑏 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ (𝑦 + 𝑥) = 0) → (((𝑏 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ 𝑥 ∈ ℝ) ∧ (𝑦 + 𝑥) = 0)) |
11 | | recn 7894 |
. . . . 5
⊢ (𝑐 ∈ ℝ → 𝑐 ∈
ℂ) |
12 | | recn 7894 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
13 | | add32 8065 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ((𝑏 + 𝑥) + 𝑐) = ((𝑏 + 𝑐) + 𝑥)) |
14 | 13 | 3expa 1198 |
. . . . . . . . . . 11
⊢ (((𝑏 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ 𝑐 ∈ ℂ) → ((𝑏 + 𝑥) + 𝑐) = ((𝑏 + 𝑐) + 𝑥)) |
15 | | addcl 7886 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) → (𝑏 + 𝑐) ∈ ℂ) |
16 | | addcom 8043 |
. . . . . . . . . . . . 13
⊢ (((𝑏 + 𝑐) ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝑏 + 𝑐) + 𝑥) = (𝑥 + (𝑏 + 𝑐))) |
17 | 15, 16 | sylan 281 |
. . . . . . . . . . . 12
⊢ (((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) ∧ 𝑥 ∈ ℂ) → ((𝑏 + 𝑐) + 𝑥) = (𝑥 + (𝑏 + 𝑐))) |
18 | 17 | an32s 563 |
. . . . . . . . . . 11
⊢ (((𝑏 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ 𝑐 ∈ ℂ) → ((𝑏 + 𝑐) + 𝑥) = (𝑥 + (𝑏 + 𝑐))) |
19 | 14, 18 | eqtr2d 2204 |
. . . . . . . . . 10
⊢ (((𝑏 ∈ ℂ ∧ 𝑥 ∈ ℂ) ∧ 𝑐 ∈ ℂ) → (𝑥 + (𝑏 + 𝑐)) = ((𝑏 + 𝑥) + 𝑐)) |
20 | 12, 19 | sylanl2 401 |
. . . . . . . . 9
⊢ (((𝑏 ∈ ℂ ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ ℂ) → (𝑥 + (𝑏 + 𝑐)) = ((𝑏 + 𝑥) + 𝑐)) |
21 | 20 | adantllr 478 |
. . . . . . . 8
⊢ ((((𝑏 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ ℂ) → (𝑥 + (𝑏 + 𝑐)) = ((𝑏 + 𝑥) + 𝑐)) |
22 | 21 | adantlr 474 |
. . . . . . 7
⊢
(((((𝑏 ∈
ℂ ∧ 𝑦 ∈
ℂ) ∧ 𝑥 ∈
ℝ) ∧ (𝑦 + 𝑥) = 0) ∧ 𝑐 ∈ ℂ) → (𝑥 + (𝑏 + 𝑐)) = ((𝑏 + 𝑥) + 𝑐)) |
23 | | addcom 8043 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
24 | 23 | ancoms 266 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
25 | 12, 24 | sylan2 284 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℝ) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) |
26 | | id 19 |
. . . . . . . . . 10
⊢ ((𝑦 + 𝑥) = 0 → (𝑦 + 𝑥) = 0) |
27 | 25, 26 | sylan9eq 2223 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℝ) ∧ (𝑦 + 𝑥) = 0) → (𝑥 + 𝑦) = 0) |
28 | 27 | adantlll 477 |
. . . . . . . 8
⊢ ((((𝑏 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ 𝑥 ∈ ℝ) ∧ (𝑦 + 𝑥) = 0) → (𝑥 + 𝑦) = 0) |
29 | 28 | adantr 274 |
. . . . . . 7
⊢
(((((𝑏 ∈
ℂ ∧ 𝑦 ∈
ℂ) ∧ 𝑥 ∈
ℝ) ∧ (𝑦 + 𝑥) = 0) ∧ 𝑐 ∈ ℂ) → (𝑥 + 𝑦) = 0) |
30 | 22, 29 | eqeq12d 2185 |
. . . . . 6
⊢
(((((𝑏 ∈
ℂ ∧ 𝑦 ∈
ℂ) ∧ 𝑥 ∈
ℝ) ∧ (𝑦 + 𝑥) = 0) ∧ 𝑐 ∈ ℂ) → ((𝑥 + (𝑏 + 𝑐)) = (𝑥 + 𝑦) ↔ ((𝑏 + 𝑥) + 𝑐) = 0)) |
31 | | simplr 525 |
. . . . . . . 8
⊢ ((((𝑏 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ ℂ) → 𝑥 ∈
ℝ) |
32 | 15 | adantlr 474 |
. . . . . . . . 9
⊢ (((𝑏 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ 𝑐 ∈ ℂ) → (𝑏 + 𝑐) ∈ ℂ) |
33 | 32 | adantlr 474 |
. . . . . . . 8
⊢ ((((𝑏 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ ℂ) → (𝑏 + 𝑐) ∈ ℂ) |
34 | | simpllr 529 |
. . . . . . . 8
⊢ ((((𝑏 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ ℂ) → 𝑦 ∈
ℂ) |
35 | | cnegexlem1 8081 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ (𝑏 + 𝑐) ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑥 + (𝑏 + 𝑐)) = (𝑥 + 𝑦) ↔ (𝑏 + 𝑐) = 𝑦)) |
36 | 31, 33, 34, 35 | syl3anc 1233 |
. . . . . . 7
⊢ ((((𝑏 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ 𝑥 ∈ ℝ) ∧ 𝑐 ∈ ℂ) → ((𝑥 + (𝑏 + 𝑐)) = (𝑥 + 𝑦) ↔ (𝑏 + 𝑐) = 𝑦)) |
37 | 36 | adantlr 474 |
. . . . . 6
⊢
(((((𝑏 ∈
ℂ ∧ 𝑦 ∈
ℂ) ∧ 𝑥 ∈
ℝ) ∧ (𝑦 + 𝑥) = 0) ∧ 𝑐 ∈ ℂ) → ((𝑥 + (𝑏 + 𝑐)) = (𝑥 + 𝑦) ↔ (𝑏 + 𝑐) = 𝑦)) |
38 | 30, 37 | bitr3d 189 |
. . . . 5
⊢
(((((𝑏 ∈
ℂ ∧ 𝑦 ∈
ℂ) ∧ 𝑥 ∈
ℝ) ∧ (𝑦 + 𝑥) = 0) ∧ 𝑐 ∈ ℂ) → (((𝑏 + 𝑥) + 𝑐) = 0 ↔ (𝑏 + 𝑐) = 𝑦)) |
39 | 10, 11, 38 | syl2an 287 |
. . . 4
⊢
(((((𝑏 ∈
ℝ ∧ 𝑦 ∈
ℝ) ∧ 𝑥 ∈
ℝ) ∧ (𝑦 + 𝑥) = 0) ∧ 𝑐 ∈ ℝ) → (((𝑏 + 𝑥) + 𝑐) = 0 ↔ (𝑏 + 𝑐) = 𝑦)) |
40 | 39 | rexbidva 2467 |
. . 3
⊢ ((((𝑏 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ (𝑦 + 𝑥) = 0) → (∃𝑐 ∈ ℝ ((𝑏 + 𝑥) + 𝑐) = 0 ↔ ∃𝑐 ∈ ℝ (𝑏 + 𝑐) = 𝑦)) |
41 | 5, 40 | mpbid 146 |
. 2
⊢ ((((𝑏 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ (𝑦 + 𝑥) = 0) → ∃𝑐 ∈ ℝ (𝑏 + 𝑐) = 𝑦) |
42 | | ax-rnegex 7870 |
. . 3
⊢ (𝑦 ∈ ℝ →
∃𝑥 ∈ ℝ
(𝑦 + 𝑥) = 0) |
43 | 42 | adantl 275 |
. 2
⊢ ((𝑏 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
∃𝑥 ∈ ℝ
(𝑦 + 𝑥) = 0) |
44 | 41, 43 | r19.29a 2613 |
1
⊢ ((𝑏 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
∃𝑐 ∈ ℝ
(𝑏 + 𝑐) = 𝑦) |