Step | Hyp | Ref
| Expression |
1 | | 0cn 10656 |
. 2
⊢ 0 ∈
ℂ |
2 | | cnre 10661 |
. 2
⊢ (0 ∈
ℂ → ∃𝑎
∈ ℝ ∃𝑏
∈ ℝ 0 = (𝑎 + (i
· 𝑏))) |
3 | | oveq2 7151 |
. . . 4
⊢ (0 =
(𝑎 + (i · 𝑏)) → ((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) |
4 | | ax-icn 10619 |
. . . . . . . . . 10
⊢ i ∈
ℂ |
5 | 4 | a1i 11 |
. . . . . . . . 9
⊢ (𝑏 ∈ ℝ → i ∈
ℂ) |
6 | | recn 10650 |
. . . . . . . . 9
⊢ (𝑏 ∈ ℝ → 𝑏 ∈
ℂ) |
7 | | 0cnd 10657 |
. . . . . . . . 9
⊢ (𝑏 ∈ ℝ → 0 ∈
ℂ) |
8 | 5, 6, 7 | mulassd 10687 |
. . . . . . . 8
⊢ (𝑏 ∈ ℝ → ((i
· 𝑏) · 0) =
(i · (𝑏 ·
0))) |
9 | | remul01 39872 |
. . . . . . . . 9
⊢ (𝑏 ∈ ℝ → (𝑏 · 0) =
0) |
10 | 9 | oveq2d 7159 |
. . . . . . . 8
⊢ (𝑏 ∈ ℝ → (i
· (𝑏 · 0)) =
(i · 0)) |
11 | 8, 10 | eqtrd 2794 |
. . . . . . 7
⊢ (𝑏 ∈ ℝ → ((i
· 𝑏) · 0) =
(i · 0)) |
12 | 11 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) → ((i · 𝑏) · 0) = (i ·
0)) |
13 | | rernegcl 39836 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℝ → (0
−ℝ 𝑎) ∈ ℝ) |
14 | 13 | recnd 10692 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℝ → (0
−ℝ 𝑎) ∈ ℂ) |
15 | 14 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (0
−ℝ 𝑎) ∈ ℂ) |
16 | | recn 10650 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℝ → 𝑎 ∈
ℂ) |
17 | 16 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → 𝑎 ∈
ℂ) |
18 | 5, 6 | mulcld 10684 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ ℝ → (i
· 𝑏) ∈
ℂ) |
19 | 18 | adantl 486 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (i
· 𝑏) ∈
ℂ) |
20 | 15, 17, 19 | addassd 10686 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (((0
−ℝ 𝑎) + 𝑎) + (i · 𝑏)) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) |
21 | | renegid2 39878 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℝ → ((0
−ℝ 𝑎) + 𝑎) = 0) |
22 | 21 | oveq1d 7158 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℝ → (((0
−ℝ 𝑎) + 𝑎) + (i · 𝑏)) = (0 + (i · 𝑏))) |
23 | | sn-addid2 39869 |
. . . . . . . . . . . . 13
⊢ ((i
· 𝑏) ∈ ℂ
→ (0 + (i · 𝑏))
= (i · 𝑏)) |
24 | 18, 23 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ℝ → (0 + (i
· 𝑏)) = (i ·
𝑏)) |
25 | 22, 24 | sylan9eq 2814 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (((0
−ℝ 𝑎) + 𝑎) + (i · 𝑏)) = (i · 𝑏)) |
26 | 20, 25 | eqtr3d 2796 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((0
−ℝ 𝑎) + (𝑎 + (i · 𝑏))) = (i · 𝑏)) |
27 | 26 | eqeq2d 2770 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))) ↔ ((0 −ℝ
𝑎) + 0) = (i · 𝑏))) |
28 | 27 | biimpa 481 |
. . . . . . . 8
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) → ((0 −ℝ
𝑎) + 0) = (i · 𝑏)) |
29 | 28 | oveq1d 7158 |
. . . . . . 7
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) → (((0 −ℝ
𝑎) + 0) · 0) = ((i
· 𝑏) ·
0)) |
30 | | elre0re 39778 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℝ → 0 ∈
ℝ) |
31 | 13, 30 | readdcld 10693 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℝ → ((0
−ℝ 𝑎) + 0) ∈ ℝ) |
32 | 31 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) → ((0 −ℝ
𝑎) + 0) ∈
ℝ) |
33 | | remul01 39872 |
. . . . . . . 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 2796 |
. . . . . 6
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) → ((i · 𝑏) · 0) = 0) |
36 | 12, 35 | eqtr3d 2796 |
. . . . 5
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) → (i · 0) =
0) |
37 | 36 | ex 417 |
. . . 4
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (((0
−ℝ 𝑎) + 0) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))) → (i · 0) =
0)) |
38 | 3, 37 | syl5 34 |
. . 3
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (0 =
(𝑎 + (i · 𝑏)) → (i · 0) =
0)) |
39 | 38 | rexlimivv 3214 |
. 2
⊢
(∃𝑎 ∈
ℝ ∃𝑏 ∈
ℝ 0 = (𝑎 + (i
· 𝑏)) → (i
· 0) = 0) |
40 | 1, 2, 39 | mp2b 10 |
1
⊢ (i
· 0) = 0 |