Step | Hyp | Ref
| Expression |
1 | | 0cn 10656 |
. . 3
⊢ 0 ∈
ℂ |
2 | | ax-icn 10619 |
. . 3
⊢ i ∈
ℂ |
3 | 1, 2 | mulcli 10671 |
. 2
⊢ (0
· i) ∈ ℂ |
4 | | cnre 10661 |
. 2
⊢ ((0
· i) ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (0 · i) = (𝑎 + (i · 𝑏))) |
5 | | simplr 769 |
. . . . . . 7
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · i) = (𝑎 + (i · 𝑏))) |
6 | | neqne 2957 |
. . . . . . . . . . . 12
⊢ (¬ (0
· i) = 0 → (0 · i) ≠ 0) |
7 | 6 | adantl 486 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · i) ≠ 0) |
8 | | simplll 775 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → 𝑎 ∈ ℝ) |
9 | | rernegcl 39836 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ ℝ → (0
−ℝ 𝑎) ∈ ℝ) |
10 | 8, 9 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 −ℝ 𝑎) ∈ ℝ) |
11 | | 1red 10665 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → 1 ∈ ℝ) |
12 | 10, 11 | readdcld 10693 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 −ℝ 𝑎) + 1) ∈ ℝ) |
13 | | ax-rrecex 10632 |
. . . . . . . . . . . . . . 15
⊢ ((((0
−ℝ 𝑎) + 1) ∈ ℝ ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) → ∃𝑥 ∈ ℝ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1) |
14 | 12, 13 | sylan 584 |
. . . . . . . . . . . . . 14
⊢
(((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) → ∃𝑥 ∈ ℝ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1) |
15 | 2 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → i ∈ ℂ) |
16 | 10 | recnd 10692 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 −ℝ 𝑎) ∈ ℂ) |
17 | | 1cnd 10659 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → 1 ∈ ℂ) |
18 | 15, 16, 17 | adddid 10688 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (i · ((0 −ℝ 𝑎) + 1)) = ((i · (0
−ℝ 𝑎)) + (i · 1))) |
19 | | it1ei 39900 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (i
· 1) = i |
20 | 19 | oveq2i 7154 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((i
· (0 −ℝ 𝑎)) + (i · 1)) = ((i · (0
−ℝ 𝑎)) + i) |
21 | 18, 20 | eqtrdi 2810 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (i · ((0 −ℝ 𝑎) + 1)) = ((i · (0
−ℝ 𝑎)) + i)) |
22 | 21 | oveq2d 7159 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · (i · ((0
−ℝ 𝑎) + 1))) = (0 · ((i · (0
−ℝ 𝑎)) + i))) |
23 | | 0cnd 10657 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → 0 ∈ ℂ) |
24 | 15, 16 | mulcld 10684 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (i · (0 −ℝ 𝑎)) ∈
ℂ) |
25 | 23, 24, 15 | adddid 10688 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · ((i · (0
−ℝ 𝑎)) + i)) = ((0 · (i · (0
−ℝ 𝑎))) + (0 · i))) |
26 | 22, 25 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · (i · ((0
−ℝ 𝑎) + 1))) = ((0 · (i · (0
−ℝ 𝑎))) + (0 · i))) |
27 | 5 | oveq2d 7159 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 −ℝ 𝑎) + (0 · i)) = ((0
−ℝ 𝑎) + (𝑎 + (i · 𝑏)))) |
28 | | renegid2 39878 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 ∈ ℝ → ((0
−ℝ 𝑎) + 𝑎) = 0) |
29 | 28 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 −ℝ 𝑎) + 𝑎) = 0) |
30 | 29 | oveq1d 7158 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (((0 −ℝ 𝑎) + 𝑎) + (i · 𝑏)) = (0 + (i · 𝑏))) |
31 | 8 | recnd 10692 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → 𝑎 ∈ ℂ) |
32 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → 𝑏 ∈ ℝ) |
33 | 32 | recnd 10692 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → 𝑏 ∈ ℂ) |
34 | 15, 33 | mulcld 10684 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (i · 𝑏) ∈ ℂ) |
35 | 16, 31, 34 | addassd 10686 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (((0 −ℝ 𝑎) + 𝑎) + (i · 𝑏)) = ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏)))) |
36 | | sn-addid2 39869 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((i
· 𝑏) ∈ ℂ
→ (0 + (i · 𝑏))
= (i · 𝑏)) |
37 | 34, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 + (i · 𝑏)) = (i · 𝑏)) |
38 | 30, 35, 37 | 3eqtr3d 2802 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 −ℝ 𝑎) + (𝑎 + (i · 𝑏))) = (i · 𝑏)) |
39 | 27, 38 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 −ℝ 𝑎) + (0 · i)) = (i · 𝑏)) |
40 | 39 | oveq2d 7159 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 · i) · ((0
−ℝ 𝑎) + (0 · i))) = ((0 · i)
· (i · 𝑏))) |
41 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · i) ∈ ℂ) |
42 | 41, 16, 41 | adddid 10688 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 · i) · ((0
−ℝ 𝑎) + (0 · i))) = (((0 · i)
· (0 −ℝ 𝑎)) + ((0 · i) · (0 ·
i)))) |
43 | 23, 15, 16 | mulassd 10687 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 · i) · (0
−ℝ 𝑎)) = (0 · (i · (0
−ℝ 𝑎)))) |
44 | 41, 23, 15 | mulassd 10687 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (((0 · i) · 0) · i) = ((0
· i) · (0 · i))) |
45 | | sn-mul01 39889 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((0
· i) ∈ ℂ → ((0 · i) · 0) =
0) |
46 | 41, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 · i) · 0) = 0) |
47 | 46 | oveq1d 7158 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (((0 · i) · 0) · i) = (0
· i)) |
48 | 44, 47 | eqtr3d 2796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 · i) · (0 · i)) = (0
· i)) |
49 | 43, 48 | oveq12d 7161 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (((0 · i) · (0
−ℝ 𝑎)) + ((0 · i) · (0 ·
i))) = ((0 · (i · (0 −ℝ 𝑎))) + (0 · i))) |
50 | 42, 49 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 · i) · ((0
−ℝ 𝑎) + (0 · i))) = ((0 · (i
· (0 −ℝ 𝑎))) + (0 · i))) |
51 | 23, 15, 34 | mulassd 10687 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 · i) · (i · 𝑏)) = (0 · (i · (i
· 𝑏)))) |
52 | 15, 15, 33 | mulassd 10687 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((i · i) · 𝑏) = (i · (i · 𝑏))) |
53 | | reixi 39886 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (i
· i) = (0 −ℝ 1) |
54 | | 1re 10664 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ∈
ℝ |
55 | | rernegcl 39836 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (1 ∈
ℝ → (0 −ℝ 1) ∈ ℝ) |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0
−ℝ 1) ∈ ℝ |
57 | 53, 56 | eqeltri 2847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (i
· i) ∈ ℝ |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (i · i) ∈ ℝ) |
59 | 58, 32 | remulcld 10694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((i · i) · 𝑏) ∈ ℝ) |
60 | 52, 59 | eqeltrrd 2852 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (i · (i · 𝑏)) ∈ ℝ) |
61 | | remul02 39870 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((i
· (i · 𝑏))
∈ ℝ → (0 · (i · (i · 𝑏))) = 0) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · (i · (i · 𝑏))) = 0) |
63 | 51, 62 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 · i) · (i · 𝑏)) = 0) |
64 | 40, 50, 63 | 3eqtr3d 2802 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 · (i · (0
−ℝ 𝑎))) + (0 · i)) = 0) |
65 | 26, 64 | eqtrd 2794 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · (i · ((0
−ℝ 𝑎) + 1))) = 0) |
66 | 65 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 · (i · ((0
−ℝ 𝑎) + 1))) = 0) |
67 | 66 | oveq1d 7158 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0
−ℝ 𝑎) + 1))) · 𝑥) = (0 · 𝑥)) |
68 | | 0cnd 10657 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → 0 ∈
ℂ) |
69 | 2 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → i ∈
ℂ) |
70 | 10 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 −ℝ
𝑎) ∈
ℝ) |
71 | 70 | recnd 10692 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 −ℝ
𝑎) ∈
ℂ) |
72 | | 1cnd 10659 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → 1 ∈
ℂ) |
73 | 71, 72 | addcld 10683 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → ((0 −ℝ
𝑎) + 1) ∈
ℂ) |
74 | 69, 73 | mulcld 10684 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → (i · ((0
−ℝ 𝑎) + 1)) ∈ ℂ) |
75 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → 𝑥 ∈ ℝ) |
76 | 75 | recnd 10692 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → 𝑥 ∈ ℂ) |
77 | 68, 74, 76 | mulassd 10687 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0
−ℝ 𝑎) + 1))) · 𝑥) = (0 · ((i · ((0
−ℝ 𝑎) + 1)) · 𝑥))) |
78 | 69, 73, 76 | mulassd 10687 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → ((i · ((0
−ℝ 𝑎) + 1)) · 𝑥) = (i · (((0
−ℝ 𝑎) + 1) · 𝑥))) |
79 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → (((0 −ℝ
𝑎) + 1) · 𝑥) = 1) |
80 | 79 | oveq2d 7159 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → (i · (((0
−ℝ 𝑎) + 1) · 𝑥)) = (i · 1)) |
81 | 80, 19 | eqtrdi 2810 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → (i · (((0
−ℝ 𝑎) + 1) · 𝑥)) = i) |
82 | 78, 81 | eqtrd 2794 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → ((i · ((0
−ℝ 𝑎) + 1)) · 𝑥) = i) |
83 | 82 | oveq2d 7159 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 · ((i · ((0
−ℝ 𝑎) + 1)) · 𝑥)) = (0 · i)) |
84 | 77, 83 | eqtrd 2794 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → ((0 · (i · ((0
−ℝ 𝑎) + 1))) · 𝑥) = (0 · i)) |
85 | | remul02 39870 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ → (0
· 𝑥) =
0) |
86 | 75, 85 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 · 𝑥) = 0) |
87 | 67, 84, 86 | 3eqtr3d 2802 |
. . . . . . . . . . . . . 14
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) ∧ (𝑥 ∈ ℝ ∧ (((0
−ℝ 𝑎) + 1) · 𝑥) = 1)) → (0 · i) =
0) |
88 | 14, 87 | rexlimddv 3213 |
. . . . . . . . . . . . 13
⊢
(((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ ((0
−ℝ 𝑎) + 1) ≠ 0) → (0 · i) =
0) |
89 | 88 | ex 417 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (((0 −ℝ 𝑎) + 1) ≠ 0 → (0 · i) =
0)) |
90 | 89 | necon1d 2971 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 · i) ≠ 0 → ((0
−ℝ 𝑎) + 1) = 0)) |
91 | 7, 90 | mpd 15 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 −ℝ 𝑎) + 1) = 0) |
92 | 91 | oveq2d 7159 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (𝑎 + ((0 −ℝ 𝑎) + 1)) = (𝑎 + 0)) |
93 | 31, 16, 17 | addassd 10686 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((𝑎 + (0 −ℝ 𝑎)) + 1) = (𝑎 + ((0 −ℝ 𝑎) + 1))) |
94 | | renegid 39838 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℝ → (𝑎 + (0 −ℝ
𝑎)) = 0) |
95 | 8, 94 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (𝑎 + (0 −ℝ 𝑎)) = 0) |
96 | 95 | oveq1d 7158 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((𝑎 + (0 −ℝ 𝑎)) + 1) = (0 +
1)) |
97 | | readdid2 39868 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℝ → (0 + 1) = 1) |
98 | 54, 97 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (0 + 1) =
1 |
99 | 96, 98 | eqtrdi 2810 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((𝑎 + (0 −ℝ 𝑎)) + 1) = 1) |
100 | 93, 99 | eqtr3d 2796 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (𝑎 + ((0 −ℝ 𝑎) + 1)) = 1) |
101 | | readdid1 39874 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℝ → (𝑎 + 0) = 𝑎) |
102 | 8, 101 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (𝑎 + 0) = 𝑎) |
103 | 92, 100, 102 | 3eqtr3rd 2803 |
. . . . . . . 8
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → 𝑎 = 1) |
104 | | rernegcl 39836 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ ℝ → (0
−ℝ 𝑏) ∈ ℝ) |
105 | 32, 104 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 −ℝ 𝑏) ∈ ℝ) |
106 | 11, 105 | readdcld 10693 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (1 + (0 −ℝ 𝑏)) ∈ ℝ) |
107 | | ax-rrecex 10632 |
. . . . . . . . . . . . . . . 16
⊢ (((1 + (0
−ℝ 𝑏)) ∈ ℝ ∧ (1 + (0
−ℝ 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1) |
108 | 106, 107 | sylan 584 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1) |
109 | 105 | recnd 10692 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 −ℝ 𝑏) ∈ ℂ) |
110 | 15, 109 | mulcld 10684 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (i · (0 −ℝ 𝑏)) ∈
ℂ) |
111 | 23, 15, 110 | adddid 10688 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · (i + (i · (0
−ℝ 𝑏)))) = ((0 · i) + (0 · (i
· (0 −ℝ 𝑏))))) |
112 | | 0re 10666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ∈
ℝ |
113 | | remul02 39870 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (0 ∈
ℝ → (0 · 0) = 0) |
114 | 112, 113 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0
· 0) = 0 |
115 | 114 | oveq1i 7153 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((0
· 0) · i) = (0 · i) |
116 | 1, 1, 2 | mulassi 10675 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((0
· 0) · i) = (0 · (0 · i)) |
117 | 115, 116 | eqtr3i 2784 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0
· i) = (0 · (0 · i)) |
118 | 117 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · i) = (0 · (0 ·
i))) |
119 | 118 | oveq1d 7158 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 · i) + (0 · (i · (0
−ℝ 𝑏)))) = ((0 · (0 · i)) + (0
· (i · (0 −ℝ 𝑏))))) |
120 | 111, 119 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · (i + (i · (0
−ℝ 𝑏)))) = ((0 · (0 · i)) + (0
· (i · (0 −ℝ 𝑏))))) |
121 | 15, 17, 109 | adddid 10688 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (i · (1 + (0 −ℝ 𝑏))) = ((i · 1) + (i
· (0 −ℝ 𝑏)))) |
122 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (i · 1) = i) |
123 | 122 | oveq1d 7158 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((i · 1) + (i · (0
−ℝ 𝑏))) = (i + (i · (0
−ℝ 𝑏)))) |
124 | 121, 123 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (i · (1 + (0 −ℝ 𝑏))) = (i + (i · (0
−ℝ 𝑏)))) |
125 | 124 | oveq2d 7159 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · (i · (1 + (0
−ℝ 𝑏)))) = (0 · (i + (i · (0
−ℝ 𝑏))))) |
126 | 23, 41, 110 | adddid 10688 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · ((0 · i) + (i · (0
−ℝ 𝑏)))) = ((0 · (0 · i)) + (0
· (i · (0 −ℝ 𝑏))))) |
127 | 120, 125,
126 | 3eqtr4d 2804 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · (i · (1 + (0
−ℝ 𝑏)))) = (0 · ((0 · i) + (i
· (0 −ℝ 𝑏))))) |
128 | 103 | oveq1d 7158 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (𝑎 + (i · 𝑏)) = (1 + (i · 𝑏))) |
129 | 5, 128 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · i) = (1 + (i · 𝑏))) |
130 | 129 | oveq1d 7158 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 · i) + (i · (0
−ℝ 𝑏))) = ((1 + (i · 𝑏)) + (i · (0 −ℝ
𝑏)))) |
131 | 17, 34, 110 | addassd 10686 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((1 + (i · 𝑏)) + (i · (0 −ℝ
𝑏))) = (1 + ((i ·
𝑏) + (i · (0
−ℝ 𝑏))))) |
132 | | renegid 39838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑏 ∈ ℝ → (𝑏 + (0 −ℝ
𝑏)) = 0) |
133 | 32, 132 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (𝑏 + (0 −ℝ 𝑏)) = 0) |
134 | 133 | oveq2d 7159 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (i · (𝑏 + (0 −ℝ 𝑏))) = (i ·
0)) |
135 | 15, 33, 109 | adddid 10688 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (i · (𝑏 + (0 −ℝ 𝑏))) = ((i · 𝑏) + (i · (0
−ℝ 𝑏)))) |
136 | | sn-mul01 39889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (i ∈
ℂ → (i · 0) = 0) |
137 | 2, 136 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (i · 0) = 0) |
138 | 134, 135,
137 | 3eqtr3d 2802 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((i · 𝑏) + (i · (0 −ℝ
𝑏))) = 0) |
139 | 138 | oveq2d 7159 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (1 + ((i · 𝑏) + (i · (0 −ℝ
𝑏)))) = (1 +
0)) |
140 | | readdid1 39874 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (1 ∈
ℝ → (1 + 0) = 1) |
141 | 54, 140 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 + 0) =
1 |
142 | 139, 141 | eqtrdi 2810 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (1 + ((i · 𝑏) + (i · (0 −ℝ
𝑏)))) = 1) |
143 | 131, 142 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((1 + (i · 𝑏)) + (i · (0 −ℝ
𝑏))) = 1) |
144 | 130, 143 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 · i) + (i · (0
−ℝ 𝑏))) = 1) |
145 | 144 | oveq2d 7159 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · ((0 · i) + (i · (0
−ℝ 𝑏)))) = (0 · 1)) |
146 | 127, 145 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · (i · (1 + (0
−ℝ 𝑏)))) = (0 · 1)) |
147 | | ax-1rid 10630 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 ∈
ℝ → (0 · 1) = 0) |
148 | 112, 147 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0
· 1) = 0 |
149 | 146, 148 | eqtrdi 2810 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · (i · (1 + (0
−ℝ 𝑏)))) = 0) |
150 | 149 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → (0 · (i · (1 +
(0 −ℝ 𝑏)))) = 0) |
151 | 150 | oveq1d 7158 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 +
(0 −ℝ 𝑏)))) · 𝑦) = (0 · 𝑦)) |
152 | | 0cnd 10657 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → 0 ∈
ℂ) |
153 | 2 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → i ∈
ℂ) |
154 | | 1cnd 10659 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → 1 ∈
ℂ) |
155 | 109 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → (0 −ℝ
𝑏) ∈
ℂ) |
156 | 154, 155 | addcld 10683 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → (1 + (0
−ℝ 𝑏)) ∈ ℂ) |
157 | 153, 156 | mulcld 10684 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → (i · (1 + (0
−ℝ 𝑏))) ∈ ℂ) |
158 | | simprl 771 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → 𝑦 ∈ ℝ) |
159 | 158 | recnd 10692 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → 𝑦 ∈ ℂ) |
160 | 152, 157,
159 | mulassd 10687 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 +
(0 −ℝ 𝑏)))) · 𝑦) = (0 · ((i · (1 + (0
−ℝ 𝑏))) · 𝑦))) |
161 | 153, 156,
159 | mulassd 10687 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → ((i · (1 + (0
−ℝ 𝑏))) · 𝑦) = (i · ((1 + (0
−ℝ 𝑏)) · 𝑦))) |
162 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1) |
163 | 162 | oveq2d 7159 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → (i · ((1 + (0
−ℝ 𝑏)) · 𝑦)) = (i · 1)) |
164 | 163, 19 | eqtrdi 2810 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → (i · ((1 + (0
−ℝ 𝑏)) · 𝑦)) = i) |
165 | 161, 164 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → ((i · (1 + (0
−ℝ 𝑏))) · 𝑦) = i) |
166 | 165 | oveq2d 7159 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → (0 · ((i · (1 +
(0 −ℝ 𝑏))) · 𝑦)) = (0 · i)) |
167 | 160, 166 | eqtrd 2794 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → ((0 · (i · (1 +
(0 −ℝ 𝑏)))) · 𝑦) = (0 · i)) |
168 | | remul02 39870 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ → (0
· 𝑦) =
0) |
169 | 158, 168 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → (0 · 𝑦) = 0) |
170 | 151, 167,
169 | 3eqtr3d 2802 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) ∧ (𝑦 ∈ ℝ ∧ ((1 + (0
−ℝ 𝑏)) · 𝑦) = 1)) → (0 · i) =
0) |
171 | 108, 170 | rexlimddv 3213 |
. . . . . . . . . . . . . 14
⊢
(((((𝑎 ∈
ℝ ∧ 𝑏 ∈
ℝ) ∧ (0 · i) = (𝑎 + (i · 𝑏))) ∧ ¬ (0 · i) = 0) ∧ (1
+ (0 −ℝ 𝑏)) ≠ 0) → (0 · i) =
0) |
172 | 171 | ex 417 |
. . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) ≠ 0 → (0 · i)
= 0)) |
173 | 172 | necon1d 2971 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 · i) ≠ 0 → (1 + (0
−ℝ 𝑏)) = 0)) |
174 | 7, 173 | mpd 15 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (1 + (0 −ℝ 𝑏)) = 0) |
175 | 174 | oveq1d 7158 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) + 𝑏) = (0 + 𝑏)) |
176 | 17, 109, 33 | addassd 10686 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) + 𝑏) = (1 + ((0 −ℝ 𝑏) + 𝑏))) |
177 | | renegid2 39878 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ ℝ → ((0
−ℝ 𝑏) + 𝑏) = 0) |
178 | 32, 177 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((0 −ℝ 𝑏) + 𝑏) = 0) |
179 | 178 | oveq2d 7159 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (1 + ((0 −ℝ 𝑏) + 𝑏)) = (1 + 0)) |
180 | 179, 141 | eqtrdi 2810 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (1 + ((0 −ℝ 𝑏) + 𝑏)) = 1) |
181 | 176, 180 | eqtrd 2794 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → ((1 + (0 −ℝ 𝑏)) + 𝑏) = 1) |
182 | | readdid2 39868 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ℝ → (0 +
𝑏) = 𝑏) |
183 | 32, 182 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 + 𝑏) = 𝑏) |
184 | 175, 181,
183 | 3eqtr3rd 2803 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → 𝑏 = 1) |
185 | 184 | oveq2d 7159 |
. . . . . . . 8
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (i · 𝑏) = (i · 1)) |
186 | 103, 185 | oveq12d 7161 |
. . . . . . 7
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (𝑎 + (i · 𝑏)) = (1 + (i · 1))) |
187 | 5, 186 | eqtrd 2794 |
. . . . . 6
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · i) = (1 + (i ·
1))) |
188 | 19 | oveq2i 7154 |
. . . . . . . . 9
⊢ (1 + (i
· 1)) = (1 + i) |
189 | 188 | eqeq2i 2772 |
. . . . . . . 8
⊢ ((0
· i) = (1 + (i · 1)) ↔ (0 · i) = (1 +
i)) |
190 | | oveq2 7151 |
. . . . . . . . . 10
⊢ ((0
· i) = (1 + i) → (((i · i) · i) · (0 ·
i)) = (((i · i) · i) · (1 + i))) |
191 | 2, 2 | mulcli 10671 |
. . . . . . . . . . . . 13
⊢ (i
· i) ∈ ℂ |
192 | 191, 2 | mulcli 10671 |
. . . . . . . . . . . 12
⊢ ((i
· i) · i) ∈ ℂ |
193 | 192, 1, 2 | mulassi 10675 |
. . . . . . . . . . 11
⊢ ((((i
· i) · i) · 0) · i) = (((i · i) · i)
· (0 · i)) |
194 | | sn-mul01 39889 |
. . . . . . . . . . . . 13
⊢ (((i
· i) · i) ∈ ℂ → (((i · i) · i)
· 0) = 0) |
195 | 192, 194 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (((i
· i) · i) · 0) = 0 |
196 | 195 | oveq1i 7153 |
. . . . . . . . . . 11
⊢ ((((i
· i) · i) · 0) · i) = (0 ·
i) |
197 | 193, 196 | eqtr3i 2784 |
. . . . . . . . . 10
⊢ (((i
· i) · i) · (0 · i)) = (0 ·
i) |
198 | | ax-1cn 10618 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
199 | 192, 198,
2 | adddii 10676 |
. . . . . . . . . . 11
⊢ (((i
· i) · i) · (1 + i)) = ((((i · i) · i)
· 1) + (((i · i) · i) · i)) |
200 | 191, 2, 198 | mulassi 10675 |
. . . . . . . . . . . . 13
⊢ (((i
· i) · i) · 1) = ((i · i) · (i ·
1)) |
201 | 19 | oveq2i 7154 |
. . . . . . . . . . . . 13
⊢ ((i
· i) · (i · 1)) = ((i · i) ·
i) |
202 | 200, 201 | eqtri 2782 |
. . . . . . . . . . . 12
⊢ (((i
· i) · i) · 1) = ((i · i) ·
i) |
203 | 191, 2, 2 | mulassi 10675 |
. . . . . . . . . . . . 13
⊢ (((i
· i) · i) · i) = ((i · i) · (i ·
i)) |
204 | | rei4 39887 |
. . . . . . . . . . . . 13
⊢ ((i
· i) · (i · i)) = 1 |
205 | 203, 204 | eqtri 2782 |
. . . . . . . . . . . 12
⊢ (((i
· i) · i) · i) = 1 |
206 | 202, 205 | oveq12i 7155 |
. . . . . . . . . . 11
⊢ ((((i
· i) · i) · 1) + (((i · i) · i) · i))
= (((i · i) · i) + 1) |
207 | 199, 206 | eqtri 2782 |
. . . . . . . . . 10
⊢ (((i
· i) · i) · (1 + i)) = (((i · i) · i) +
1) |
208 | 190, 197,
207 | 3eqtr3g 2817 |
. . . . . . . . 9
⊢ ((0
· i) = (1 + i) → (0 · i) = (((i · i) · i) +
1)) |
209 | 54, 54 | readdcli 10679 |
. . . . . . . . . . 11
⊢ (1 + 1)
∈ ℝ |
210 | | df-2 11722 |
. . . . . . . . . . . 12
⊢ 2 = (1 +
1) |
211 | | sn-0ne2 39871 |
. . . . . . . . . . . . 13
⊢ 0 ≠
2 |
212 | 211 | necomi 3003 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
213 | 210, 212 | eqnetrri 3020 |
. . . . . . . . . . 11
⊢ (1 + 1)
≠ 0 |
214 | | ax-rrecex 10632 |
. . . . . . . . . . 11
⊢ (((1 + 1)
∈ ℝ ∧ (1 + 1) ≠ 0) → ∃𝑧 ∈ ℝ ((1 + 1) · 𝑧) = 1) |
215 | 209, 213,
214 | mp2an 692 |
. . . . . . . . . 10
⊢
∃𝑧 ∈
ℝ ((1 + 1) · 𝑧) = 1 |
216 | 192, 198 | addcli 10670 |
. . . . . . . . . . . . . . . . . 18
⊢ (((i
· i) · i) + 1) ∈ ℂ |
217 | 198, 2, 216 | addassi 10674 |
. . . . . . . . . . . . . . . . 17
⊢ ((1 + i)
+ (((i · i) · i) + 1)) = (1 + (i + (((i · i) · i) +
1))) |
218 | 2, 192, 198 | addassi 10674 |
. . . . . . . . . . . . . . . . . 18
⊢ ((i + ((i
· i) · i)) + 1) = (i + (((i · i) · i) +
1)) |
219 | 218 | oveq2i 7154 |
. . . . . . . . . . . . . . . . 17
⊢ (1 + ((i
+ ((i · i) · i)) + 1)) = (1 + (i + (((i · i) · i) +
1))) |
220 | 2, 2, 2 | mulassi 10675 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((i
· i) · i) = (i · (i · i)) |
221 | 220 | oveq2i 7154 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (i + ((i
· i) · i)) = (i + (i · (i · i))) |
222 | | ipiiie0 39901 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (i + (i
· (i · i))) = 0 |
223 | 221, 222 | eqtri 2782 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (i + ((i
· i) · i)) = 0 |
224 | 223 | oveq1i 7153 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((i + ((i
· i) · i)) + 1) = (0 + 1) |
225 | 224, 98 | eqtri 2782 |
. . . . . . . . . . . . . . . . . 18
⊢ ((i + ((i
· i) · i)) + 1) = 1 |
226 | 225 | oveq2i 7154 |
. . . . . . . . . . . . . . . . 17
⊢ (1 + ((i
+ ((i · i) · i)) + 1)) = (1 + 1) |
227 | 217, 219,
226 | 3eqtr2i 2788 |
. . . . . . . . . . . . . . . 16
⊢ ((1 + i)
+ (((i · i) · i) + 1)) = (1 + 1) |
228 | 227 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
→ ((1 + i) + (((i · i) · i) + 1)) = (1 +
1)) |
229 | 3, 198, 198 | adddii 10676 |
. . . . . . . . . . . . . . . 16
⊢ ((0
· i) · (1 + 1)) = (((0 · i) · 1) + ((0 · i)
· 1)) |
230 | 1, 2, 198 | mulassi 10675 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0
· i) · 1) = (0 · (i · 1)) |
231 | 19 | oveq2i 7154 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0
· (i · 1)) = (0 · i) |
232 | 230, 231 | eqtri 2782 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
· i) · 1) = (0 · i) |
233 | | simpl 487 |
. . . . . . . . . . . . . . . . . 18
⊢ (((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
→ (0 · i) = (1 + i)) |
234 | 232, 233 | syl5eq 2806 |
. . . . . . . . . . . . . . . . 17
⊢ (((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
→ ((0 · i) · 1) = (1 + i)) |
235 | | simpr 489 |
. . . . . . . . . . . . . . . . . 18
⊢ (((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
→ (0 · i) = (((i · i) · i) + 1)) |
236 | 232, 235 | syl5eq 2806 |
. . . . . . . . . . . . . . . . 17
⊢ (((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
→ ((0 · i) · 1) = (((i · i) · i) +
1)) |
237 | 234, 236 | oveq12d 7161 |
. . . . . . . . . . . . . . . 16
⊢ (((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
→ (((0 · i) · 1) + ((0 · i) · 1)) = ((1 + i) +
(((i · i) · i) + 1))) |
238 | 229, 237 | syl5eq 2806 |
. . . . . . . . . . . . . . 15
⊢ (((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
→ ((0 · i) · (1 + 1)) = ((1 + i) + (((i · i) ·
i) + 1))) |
239 | | remulid2 39897 |
. . . . . . . . . . . . . . . 16
⊢ ((1 + 1)
∈ ℝ → (1 · (1 + 1)) = (1 + 1)) |
240 | 209, 239 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ (((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
→ (1 · (1 + 1)) = (1 + 1)) |
241 | 228, 238,
240 | 3eqtr4d 2804 |
. . . . . . . . . . . . . 14
⊢ (((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
→ ((0 · i) · (1 + 1)) = (1 · (1 +
1))) |
242 | 241 | oveq1d 7158 |
. . . . . . . . . . . . 13
⊢ (((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
→ (((0 · i) · (1 + 1)) · 𝑧) = ((1 · (1 + 1)) · 𝑧)) |
243 | 242 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
∧ (𝑧 ∈ ℝ
∧ ((1 + 1) · 𝑧)
= 1)) → (((0 · i) · (1 + 1)) · 𝑧) = ((1 · (1 + 1)) · 𝑧)) |
244 | 3 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
∧ (𝑧 ∈ ℝ
∧ ((1 + 1) · 𝑧)
= 1)) → (0 · i) ∈ ℂ) |
245 | | 1cnd 10659 |
. . . . . . . . . . . . . . 15
⊢ ((((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
∧ (𝑧 ∈ ℝ
∧ ((1 + 1) · 𝑧)
= 1)) → 1 ∈ ℂ) |
246 | 245, 245 | addcld 10683 |
. . . . . . . . . . . . . 14
⊢ ((((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
∧ (𝑧 ∈ ℝ
∧ ((1 + 1) · 𝑧)
= 1)) → (1 + 1) ∈ ℂ) |
247 | | simprl 771 |
. . . . . . . . . . . . . . 15
⊢ ((((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
∧ (𝑧 ∈ ℝ
∧ ((1 + 1) · 𝑧)
= 1)) → 𝑧 ∈
ℝ) |
248 | 247 | recnd 10692 |
. . . . . . . . . . . . . 14
⊢ ((((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
∧ (𝑧 ∈ ℝ
∧ ((1 + 1) · 𝑧)
= 1)) → 𝑧 ∈
ℂ) |
249 | 244, 246,
248 | mulassd 10687 |
. . . . . . . . . . . . 13
⊢ ((((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
∧ (𝑧 ∈ ℝ
∧ ((1 + 1) · 𝑧)
= 1)) → (((0 · i) · (1 + 1)) · 𝑧) = ((0 · i) · ((1 + 1)
· 𝑧))) |
250 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢ ((((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
∧ (𝑧 ∈ ℝ
∧ ((1 + 1) · 𝑧)
= 1)) → ((1 + 1) · 𝑧) = 1) |
251 | 250 | oveq2d 7159 |
. . . . . . . . . . . . . 14
⊢ ((((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
∧ (𝑧 ∈ ℝ
∧ ((1 + 1) · 𝑧)
= 1)) → ((0 · i) · ((1 + 1) · 𝑧)) = ((0 · i) ·
1)) |
252 | 251, 232 | eqtrdi 2810 |
. . . . . . . . . . . . 13
⊢ ((((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
∧ (𝑧 ∈ ℝ
∧ ((1 + 1) · 𝑧)
= 1)) → ((0 · i) · ((1 + 1) · 𝑧)) = (0 · i)) |
253 | 249, 252 | eqtrd 2794 |
. . . . . . . . . . . 12
⊢ ((((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
∧ (𝑧 ∈ ℝ
∧ ((1 + 1) · 𝑧)
= 1)) → (((0 · i) · (1 + 1)) · 𝑧) = (0 · i)) |
254 | 245, 246,
248 | mulassd 10687 |
. . . . . . . . . . . . 13
⊢ ((((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
∧ (𝑧 ∈ ℝ
∧ ((1 + 1) · 𝑧)
= 1)) → ((1 · (1 + 1)) · 𝑧) = (1 · ((1 + 1) · 𝑧))) |
255 | 250 | oveq2d 7159 |
. . . . . . . . . . . . . 14
⊢ ((((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
∧ (𝑧 ∈ ℝ
∧ ((1 + 1) · 𝑧)
= 1)) → (1 · ((1 + 1) · 𝑧)) = (1 · 1)) |
256 | | 1t1e1ALT 39779 |
. . . . . . . . . . . . . 14
⊢ (1
· 1) = 1 |
257 | 255, 256 | eqtrdi 2810 |
. . . . . . . . . . . . 13
⊢ ((((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
∧ (𝑧 ∈ ℝ
∧ ((1 + 1) · 𝑧)
= 1)) → (1 · ((1 + 1) · 𝑧)) = 1) |
258 | 254, 257 | eqtrd 2794 |
. . . . . . . . . . . 12
⊢ ((((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
∧ (𝑧 ∈ ℝ
∧ ((1 + 1) · 𝑧)
= 1)) → ((1 · (1 + 1)) · 𝑧) = 1) |
259 | 243, 253,
258 | 3eqtr3d 2802 |
. . . . . . . . . . 11
⊢ ((((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
∧ (𝑧 ∈ ℝ
∧ ((1 + 1) · 𝑧)
= 1)) → (0 · i) = 1) |
260 | 259 | rexlimdvaa 3207 |
. . . . . . . . . 10
⊢ (((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
→ (∃𝑧 ∈
ℝ ((1 + 1) · 𝑧) = 1 → (0 · i) =
1)) |
261 | 215, 260 | mpi 20 |
. . . . . . . . 9
⊢ (((0
· i) = (1 + i) ∧ (0 · i) = (((i · i) · i) + 1))
→ (0 · i) = 1) |
262 | 208, 261 | mpdan 687 |
. . . . . . . 8
⊢ ((0
· i) = (1 + i) → (0 · i) = 1) |
263 | 189, 262 | sylbi 220 |
. . . . . . 7
⊢ ((0
· i) = (1 + (i · 1)) → (0 · i) = 1) |
264 | | oveq2 7151 |
. . . . . . . 8
⊢ ((0
· i) = 1 → (0 · (0 · i)) = (0 ·
1)) |
265 | 116, 115 | eqtr3i 2784 |
. . . . . . . 8
⊢ (0
· (0 · i)) = (0 · i) |
266 | 264, 265,
148 | 3eqtr3g 2817 |
. . . . . . 7
⊢ ((0
· i) = 1 → (0 · i) = 0) |
267 | 263, 266 | syl 17 |
. . . . . 6
⊢ ((0
· i) = (1 + (i · 1)) → (0 · i) = 0) |
268 | 187, 267 | syl 17 |
. . . . 5
⊢ ((((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) ∧ ¬
(0 · i) = 0) → (0 · i) = 0) |
269 | 268 | pm2.18da 800 |
. . . 4
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (0
· i) = (𝑎 + (i
· 𝑏))) → (0
· i) = 0) |
270 | 269 | ex 417 |
. . 3
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((0
· i) = (𝑎 + (i
· 𝑏)) → (0
· i) = 0)) |
271 | 270 | rexlimivv 3214 |
. 2
⊢
(∃𝑎 ∈
ℝ ∃𝑏 ∈
ℝ (0 · i) = (𝑎
+ (i · 𝑏)) → (0
· i) = 0) |
272 | 3, 4, 271 | mp2b 10 |
1
⊢ (0
· i) = 0 |