Proof of Theorem crreczi
Step | Hyp | Ref
| Expression |
1 | | crrecz.1 |
. . . . . . . 8
⊢ 𝐴 ∈ ℝ |
2 | 1 | recni 10678 |
. . . . . . 7
⊢ 𝐴 ∈ ℂ |
3 | 2 | sqcli 13579 |
. . . . . 6
⊢ (𝐴↑2) ∈
ℂ |
4 | | ax-icn 10619 |
. . . . . . . 8
⊢ i ∈
ℂ |
5 | | crrecz.2 |
. . . . . . . . 9
⊢ 𝐵 ∈ ℝ |
6 | 5 | recni 10678 |
. . . . . . . 8
⊢ 𝐵 ∈ ℂ |
7 | 4, 6 | mulcli 10671 |
. . . . . . 7
⊢ (i
· 𝐵) ∈
ℂ |
8 | 7 | sqcli 13579 |
. . . . . 6
⊢ ((i
· 𝐵)↑2) ∈
ℂ |
9 | 3, 8 | negsubi 10987 |
. . . . 5
⊢ ((𝐴↑2) + -((i · 𝐵)↑2)) = ((𝐴↑2) − ((i · 𝐵)↑2)) |
10 | 4, 6 | sqmuli 13582 |
. . . . . . . . 9
⊢ ((i
· 𝐵)↑2) =
((i↑2) · (𝐵↑2)) |
11 | | i2 13600 |
. . . . . . . . . 10
⊢
(i↑2) = -1 |
12 | 11 | oveq1i 7153 |
. . . . . . . . 9
⊢
((i↑2) · (𝐵↑2)) = (-1 · (𝐵↑2)) |
13 | | ax-1cn 10618 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
14 | 6 | sqcli 13579 |
. . . . . . . . . 10
⊢ (𝐵↑2) ∈
ℂ |
15 | 13, 14 | mulneg1i 11109 |
. . . . . . . . 9
⊢ (-1
· (𝐵↑2)) = -(1
· (𝐵↑2)) |
16 | 10, 12, 15 | 3eqtri 2786 |
. . . . . . . 8
⊢ ((i
· 𝐵)↑2) = -(1
· (𝐵↑2)) |
17 | 16 | negeqi 10902 |
. . . . . . 7
⊢ -((i
· 𝐵)↑2) = --(1
· (𝐵↑2)) |
18 | 13, 14 | mulcli 10671 |
. . . . . . . 8
⊢ (1
· (𝐵↑2)) ∈
ℂ |
19 | 18 | negnegi 10979 |
. . . . . . 7
⊢ --(1
· (𝐵↑2)) = (1
· (𝐵↑2)) |
20 | 14 | mulid2i 10669 |
. . . . . . 7
⊢ (1
· (𝐵↑2)) =
(𝐵↑2) |
21 | 17, 19, 20 | 3eqtri 2786 |
. . . . . 6
⊢ -((i
· 𝐵)↑2) =
(𝐵↑2) |
22 | 21 | oveq2i 7154 |
. . . . 5
⊢ ((𝐴↑2) + -((i · 𝐵)↑2)) = ((𝐴↑2) + (𝐵↑2)) |
23 | 2, 7 | subsqi 13610 |
. . . . 5
⊢ ((𝐴↑2) − ((i ·
𝐵)↑2)) = ((𝐴 + (i · 𝐵)) · (𝐴 − (i · 𝐵))) |
24 | 9, 22, 23 | 3eqtr3ri 2791 |
. . . 4
⊢ ((𝐴 + (i · 𝐵)) · (𝐴 − (i · 𝐵))) = ((𝐴↑2) + (𝐵↑2)) |
25 | 24 | oveq1i 7153 |
. . 3
⊢ (((𝐴 + (i · 𝐵)) · (𝐴 − (i · 𝐵))) / ((𝐴↑2) + (𝐵↑2))) = (((𝐴↑2) + (𝐵↑2)) / ((𝐴↑2) + (𝐵↑2))) |
26 | | neorian 3043 |
. . . . 5
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ↔ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) |
27 | | sumsqeq0 13577 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 = 0 ∧ 𝐵 = 0) ↔ ((𝐴↑2) + (𝐵↑2)) = 0)) |
28 | 1, 5, 27 | mp2an 692 |
. . . . . 6
⊢ ((𝐴 = 0 ∧ 𝐵 = 0) ↔ ((𝐴↑2) + (𝐵↑2)) = 0) |
29 | 28 | necon3bbii 2996 |
. . . . 5
⊢ (¬
(𝐴 = 0 ∧ 𝐵 = 0) ↔ ((𝐴↑2) + (𝐵↑2)) ≠ 0) |
30 | 26, 29 | bitri 278 |
. . . 4
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ↔ ((𝐴↑2) + (𝐵↑2)) ≠ 0) |
31 | 2, 7 | addcli 10670 |
. . . . 5
⊢ (𝐴 + (i · 𝐵)) ∈ ℂ |
32 | 2, 7 | subcli 10985 |
. . . . 5
⊢ (𝐴 − (i · 𝐵)) ∈
ℂ |
33 | 3, 14 | addcli 10670 |
. . . . 5
⊢ ((𝐴↑2) + (𝐵↑2)) ∈ ℂ |
34 | 31, 32, 33 | divasszi 11413 |
. . . 4
⊢ (((𝐴↑2) + (𝐵↑2)) ≠ 0 → (((𝐴 + (i · 𝐵)) · (𝐴 − (i · 𝐵))) / ((𝐴↑2) + (𝐵↑2))) = ((𝐴 + (i · 𝐵)) · ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2))))) |
35 | 30, 34 | sylbi 220 |
. . 3
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → (((𝐴 + (i · 𝐵)) · (𝐴 − (i · 𝐵))) / ((𝐴↑2) + (𝐵↑2))) = ((𝐴 + (i · 𝐵)) · ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2))))) |
36 | | divid 11350 |
. . . . 5
⊢ ((((𝐴↑2) + (𝐵↑2)) ∈ ℂ ∧ ((𝐴↑2) + (𝐵↑2)) ≠ 0) → (((𝐴↑2) + (𝐵↑2)) / ((𝐴↑2) + (𝐵↑2))) = 1) |
37 | 33, 36 | mpan 690 |
. . . 4
⊢ (((𝐴↑2) + (𝐵↑2)) ≠ 0 → (((𝐴↑2) + (𝐵↑2)) / ((𝐴↑2) + (𝐵↑2))) = 1) |
38 | 30, 37 | sylbi 220 |
. . 3
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → (((𝐴↑2) + (𝐵↑2)) / ((𝐴↑2) + (𝐵↑2))) = 1) |
39 | 25, 35, 38 | 3eqtr3a 2818 |
. 2
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → ((𝐴 + (i · 𝐵)) · ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2)))) = 1) |
40 | 32, 33 | divclzi 11398 |
. . . 4
⊢ (((𝐴↑2) + (𝐵↑2)) ≠ 0 → ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2))) ∈ ℂ) |
41 | 30, 40 | sylbi 220 |
. . 3
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2))) ∈ ℂ) |
42 | 31 | a1i 11 |
. . 3
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → (𝐴 + (i · 𝐵)) ∈ ℂ) |
43 | | crne0 11652 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ↔ (𝐴 + (i · 𝐵)) ≠ 0)) |
44 | 1, 5, 43 | mp2an 692 |
. . . 4
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ↔ (𝐴 + (i · 𝐵)) ≠ 0) |
45 | 44 | biimpi 219 |
. . 3
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → (𝐴 + (i · 𝐵)) ≠ 0) |
46 | | divmul 11324 |
. . . 4
⊢ ((1
∈ ℂ ∧ ((𝐴
− (i · 𝐵)) /
((𝐴↑2) + (𝐵↑2))) ∈ ℂ ∧
((𝐴 + (i · 𝐵)) ∈ ℂ ∧ (𝐴 + (i · 𝐵)) ≠ 0)) → ((1 / (𝐴 + (i · 𝐵))) = ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2))) ↔ ((𝐴 + (i · 𝐵)) · ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2)))) = 1)) |
47 | 13, 46 | mp3an1 1446 |
. . 3
⊢ ((((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2))) ∈ ℂ ∧ ((𝐴 + (i · 𝐵)) ∈ ℂ ∧ (𝐴 + (i · 𝐵)) ≠ 0)) → ((1 / (𝐴 + (i · 𝐵))) = ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2))) ↔ ((𝐴 + (i · 𝐵)) · ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2)))) = 1)) |
48 | 41, 42, 45, 47 | syl12anc 836 |
. 2
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → ((1 / (𝐴 + (i · 𝐵))) = ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2))) ↔ ((𝐴 + (i · 𝐵)) · ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2)))) = 1)) |
49 | 39, 48 | mpbird 260 |
1
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → (1 / (𝐴 + (i · 𝐵))) = ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2)))) |