| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cnre 11258 | . 2
⊢ (𝐴 ∈ ℂ →
∃𝑎 ∈ ℝ
∃𝑏 ∈ ℝ
𝐴 = (𝑎 + (i · 𝑏))) | 
| 2 |  | ax-rnegex 11226 | . . . . . . 7
⊢ (𝑎 ∈ ℝ →
∃𝑐 ∈ ℝ
(𝑎 + 𝑐) = 0) | 
| 3 |  | ax-rnegex 11226 | . . . . . . 7
⊢ (𝑏 ∈ ℝ →
∃𝑑 ∈ ℝ
(𝑏 + 𝑑) = 0) | 
| 4 | 2, 3 | anim12i 613 | . . . . . 6
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) →
(∃𝑐 ∈ ℝ
(𝑎 + 𝑐) = 0 ∧ ∃𝑑 ∈ ℝ (𝑏 + 𝑑) = 0)) | 
| 5 |  | reeanv 3229 | . . . . . 6
⊢
(∃𝑐 ∈
ℝ ∃𝑑 ∈
ℝ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0) ↔ (∃𝑐 ∈ ℝ (𝑎 + 𝑐) = 0 ∧ ∃𝑑 ∈ ℝ (𝑏 + 𝑑) = 0)) | 
| 6 | 4, 5 | sylibr 234 | . . . . 5
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) →
∃𝑐 ∈ ℝ
∃𝑑 ∈ ℝ
((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) | 
| 7 |  | ax-icn 11214 | . . . . . . . . . . 11
⊢ i ∈
ℂ | 
| 8 | 7 | a1i 11 | . . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → i ∈
ℂ) | 
| 9 |  | simplrr 778 | . . . . . . . . . . 11
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → 𝑑 ∈ ℝ) | 
| 10 | 9 | recnd 11289 | . . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → 𝑑 ∈ ℂ) | 
| 11 | 8, 10 | mulcld 11281 | . . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → (i · 𝑑) ∈ ℂ) | 
| 12 |  | simplrl 777 | . . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → 𝑐 ∈ ℝ) | 
| 13 | 12 | recnd 11289 | . . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → 𝑐 ∈ ℂ) | 
| 14 | 11, 13 | addcld 11280 | . . . . . . . 8
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → ((i · 𝑑) + 𝑐) ∈ ℂ) | 
| 15 |  | simplll 775 | . . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → 𝑎 ∈ ℝ) | 
| 16 | 15 | recnd 11289 | . . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → 𝑎 ∈ ℂ) | 
| 17 |  | simpllr 776 | . . . . . . . . . . . . . . 15
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → 𝑏 ∈ ℝ) | 
| 18 | 17 | recnd 11289 | . . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → 𝑏 ∈ ℂ) | 
| 19 | 8, 18 | mulcld 11281 | . . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → (i · 𝑏) ∈ ℂ) | 
| 20 | 16, 19, 11 | addassd 11283 | . . . . . . . . . . . 12
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → ((𝑎 + (i · 𝑏)) + (i · 𝑑)) = (𝑎 + ((i · 𝑏) + (i · 𝑑)))) | 
| 21 | 8, 18, 10 | adddid 11285 | . . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → (i · (𝑏 + 𝑑)) = ((i · 𝑏) + (i · 𝑑))) | 
| 22 |  | simprr 773 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → (𝑏 + 𝑑) = 0) | 
| 23 | 22 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → (i · (𝑏 + 𝑑)) = (i · 0)) | 
| 24 |  | mul01 11440 | . . . . . . . . . . . . . . . 16
⊢ (i ∈
ℂ → (i · 0) = 0) | 
| 25 | 7, 24 | ax-mp 5 | . . . . . . . . . . . . . . 15
⊢ (i
· 0) = 0 | 
| 26 | 23, 25 | eqtrdi 2793 | . . . . . . . . . . . . . 14
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → (i · (𝑏 + 𝑑)) = 0) | 
| 27 | 21, 26 | eqtr3d 2779 | . . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → ((i · 𝑏) + (i · 𝑑)) = 0) | 
| 28 | 27 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → (𝑎 + ((i · 𝑏) + (i · 𝑑))) = (𝑎 + 0)) | 
| 29 |  | addrid 11441 | . . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℂ → (𝑎 + 0) = 𝑎) | 
| 30 | 16, 29 | syl 17 | . . . . . . . . . . . 12
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → (𝑎 + 0) = 𝑎) | 
| 31 | 20, 28, 30 | 3eqtrd 2781 | . . . . . . . . . . 11
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → ((𝑎 + (i · 𝑏)) + (i · 𝑑)) = 𝑎) | 
| 32 | 31 | oveq1d 7446 | . . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → (((𝑎 + (i · 𝑏)) + (i · 𝑑)) + 𝑐) = (𝑎 + 𝑐)) | 
| 33 | 16, 19 | addcld 11280 | . . . . . . . . . . 11
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → (𝑎 + (i · 𝑏)) ∈ ℂ) | 
| 34 | 33, 11, 13 | addassd 11283 | . . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → (((𝑎 + (i · 𝑏)) + (i · 𝑑)) + 𝑐) = ((𝑎 + (i · 𝑏)) + ((i · 𝑑) + 𝑐))) | 
| 35 | 32, 34 | eqtr3d 2779 | . . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → (𝑎 + 𝑐) = ((𝑎 + (i · 𝑏)) + ((i · 𝑑) + 𝑐))) | 
| 36 |  | simprl 771 | . . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → (𝑎 + 𝑐) = 0) | 
| 37 | 35, 36 | eqtr3d 2779 | . . . . . . . 8
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → ((𝑎 + (i · 𝑏)) + ((i · 𝑑) + 𝑐)) = 0) | 
| 38 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑥 = ((i · 𝑑) + 𝑐) → ((𝑎 + (i · 𝑏)) + 𝑥) = ((𝑎 + (i · 𝑏)) + ((i · 𝑑) + 𝑐))) | 
| 39 | 38 | eqeq1d 2739 | . . . . . . . . 9
⊢ (𝑥 = ((i · 𝑑) + 𝑐) → (((𝑎 + (i · 𝑏)) + 𝑥) = 0 ↔ ((𝑎 + (i · 𝑏)) + ((i · 𝑑) + 𝑐)) = 0)) | 
| 40 | 39 | rspcev 3622 | . . . . . . . 8
⊢ ((((i
· 𝑑) + 𝑐) ∈ ℂ ∧ ((𝑎 + (i · 𝑏)) + ((i · 𝑑) + 𝑐)) = 0) → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) + 𝑥) = 0) | 
| 41 | 14, 37, 40 | syl2anc 584 | . . . . . . 7
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0)) → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) + 𝑥) = 0) | 
| 42 | 41 | ex 412 | . . . . . 6
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) →
(((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0) → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) + 𝑥) = 0)) | 
| 43 | 42 | rexlimdvva 3213 | . . . . 5
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) →
(∃𝑐 ∈ ℝ
∃𝑑 ∈ ℝ
((𝑎 + 𝑐) = 0 ∧ (𝑏 + 𝑑) = 0) → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) + 𝑥) = 0)) | 
| 44 | 6, 43 | mpd 15 | . . . 4
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) →
∃𝑥 ∈ ℂ
((𝑎 + (i · 𝑏)) + 𝑥) = 0) | 
| 45 |  | oveq1 7438 | . . . . . 6
⊢ (𝐴 = (𝑎 + (i · 𝑏)) → (𝐴 + 𝑥) = ((𝑎 + (i · 𝑏)) + 𝑥)) | 
| 46 | 45 | eqeq1d 2739 | . . . . 5
⊢ (𝐴 = (𝑎 + (i · 𝑏)) → ((𝐴 + 𝑥) = 0 ↔ ((𝑎 + (i · 𝑏)) + 𝑥) = 0)) | 
| 47 | 46 | rexbidv 3179 | . . . 4
⊢ (𝐴 = (𝑎 + (i · 𝑏)) → (∃𝑥 ∈ ℂ (𝐴 + 𝑥) = 0 ↔ ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) + 𝑥) = 0)) | 
| 48 | 44, 47 | syl5ibrcom 247 | . . 3
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝐴 = (𝑎 + (i · 𝑏)) → ∃𝑥 ∈ ℂ (𝐴 + 𝑥) = 0)) | 
| 49 | 48 | rexlimivv 3201 | . 2
⊢
(∃𝑎 ∈
ℝ ∃𝑏 ∈
ℝ 𝐴 = (𝑎 + (i · 𝑏)) → ∃𝑥 ∈ ℂ (𝐴 + 𝑥) = 0) | 
| 50 | 1, 49 | syl 17 | 1
⊢ (𝐴 ∈ ℂ →
∃𝑥 ∈ ℂ
(𝐴 + 𝑥) = 0) |