| Step | Hyp | Ref
| Expression |
| 1 | | 0cn 11253 |
. 2
⊢ 0 ∈
ℂ |
| 2 | | cnre 11258 |
. 2
⊢ (0 ∈
ℂ → ∃𝑎
∈ ℝ ∃𝑏
∈ ℝ 0 = (𝑎 + (i
· 𝑏))) |
| 3 | | oveq2 7439 |
. . . 4
⊢ (0 =
(𝑎 + (i · 𝑏)) → ((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) |
| 4 | | ax-icn 11214 |
. . . . . . . . . 10
⊢ i ∈
ℂ |
| 5 | 4 | a1i 11 |
. . . . . . . . 9
⊢ (𝑏 ∈ ℝ → i ∈
ℂ) |
| 6 | | recn 11245 |
. . . . . . . . 9
⊢ (𝑏 ∈ ℝ → 𝑏 ∈
ℂ) |
| 7 | | 0cnd 11254 |
. . . . . . . . 9
⊢ (𝑏 ∈ ℝ → 0 ∈
ℂ) |
| 8 | 5, 6, 7 | mulassd 11284 |
. . . . . . . 8
⊢ (𝑏 ∈ ℝ → ((i
· 𝑏) · 0) =
(i · (𝑏 ·
0))) |
| 9 | | remul01 42437 |
. . . . . . . . 9
⊢ (𝑏 ∈ ℝ → (𝑏 · 0) =
0) |
| 10 | 9 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑏 ∈ ℝ → (i
· (𝑏 · 0)) =
(i · 0)) |
| 11 | 8, 10 | eqtrd 2777 |
. . . . . . 7
⊢ (𝑏 ∈ ℝ → ((i
· 𝑏) · 0) =
(i · 0)) |
| 12 | 11 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) → ((i · 𝑏) · 0) = (i ·
0)) |
| 13 | | rernegcl 42401 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℝ → (0
−ℝ 𝑎) ∈ ℝ) |
| 14 | 13 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℝ → (0
−ℝ 𝑎) ∈ ℂ) |
| 15 | 14 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (0
−ℝ 𝑎) ∈ ℂ) |
| 16 | | recn 11245 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℝ → 𝑎 ∈
ℂ) |
| 17 | 16 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → 𝑎 ∈
ℂ) |
| 18 | 5, 6 | mulcld 11281 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ ℝ → (i
· 𝑏) ∈
ℂ) |
| 19 | 18 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (i
· 𝑏) ∈
ℂ) |
| 20 | 15, 17, 19 | addassd 11283 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (((0
−ℝ 𝑎) + 𝑎) + (i · 𝑏)) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) |
| 21 | | renegid2 42443 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℝ → ((0
−ℝ 𝑎) + 𝑎) = 0) |
| 22 | 21 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℝ → (((0
−ℝ 𝑎) + 𝑎) + (i · 𝑏)) = (0 + (i · 𝑏))) |
| 23 | | sn-addlid 42434 |
. . . . . . . . . . . . 13
⊢ ((i
· 𝑏) ∈ ℂ
→ (0 + (i · 𝑏))
= (i · 𝑏)) |
| 24 | 18, 23 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ℝ → (0 + (i
· 𝑏)) = (i ·
𝑏)) |
| 25 | 22, 24 | sylan9eq 2797 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (((0
−ℝ 𝑎) + 𝑎) + (i · 𝑏)) = (i · 𝑏)) |
| 26 | 20, 25 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((0
−ℝ 𝑎) + (𝑎 + (i · 𝑏))) = (i · 𝑏)) |
| 27 | 26 | eqeq2d 2748 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))) ↔ ((0 −ℝ
𝑎) + 0) = (i · 𝑏))) |
| 28 | 27 | biimpa 476 |
. . . . . . . 8
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) → ((0 −ℝ
𝑎) + 0) = (i · 𝑏)) |
| 29 | 28 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) → (((0 −ℝ
𝑎) + 0) · 0) = ((i
· 𝑏) ·
0)) |
| 30 | | elre0re 42295 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℝ → 0 ∈
ℝ) |
| 31 | 13, 30 | readdcld 11290 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℝ → ((0
−ℝ 𝑎) + 0) ∈ ℝ) |
| 32 | 31 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) → ((0 −ℝ
𝑎) + 0) ∈
ℝ) |
| 33 | | remul01 42437 |
. . . . . . . 8
⊢ (((0
−ℝ 𝑎) + 0) ∈ ℝ → (((0
−ℝ 𝑎) + 0) · 0) = 0) |
| 34 | 32, 33 | syl 17 |
. . . . . . 7
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) → (((0 −ℝ
𝑎) + 0) · 0) =
0) |
| 35 | 29, 34 | eqtr3d 2779 |
. . . . . 6
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) → ((i · 𝑏) · 0) = 0) |
| 36 | 12, 35 | eqtr3d 2779 |
. . . . 5
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) → (i · 0) =
0) |
| 37 | 36 | ex 412 |
. . . 4
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))) → (i · 0) =
0)) |
| 38 | 3, 37 | syl5 34 |
. . 3
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (0 =
(𝑎 + (i · 𝑏)) → (i · 0) =
0)) |
| 39 | 38 | rexlimivv 3201 |
. 2
⊢
(∃𝑎 ∈
ℝ ∃𝑏 ∈
ℝ 0 = (𝑎 + (i
· 𝑏)) → (i
· 0) = 0) |
| 40 | 1, 2, 39 | mp2b 10 |
1
⊢ (i
· 0) = 0 |