Proof of Theorem crreczi
| Step | Hyp | Ref
| Expression |
| 1 | | crrecz.1 |
. . . . . . . 8
⊢ 𝐴 ∈ ℝ |
| 2 | 1 | recni 11275 |
. . . . . . 7
⊢ 𝐴 ∈ ℂ |
| 3 | 2 | sqcli 14220 |
. . . . . 6
⊢ (𝐴↑2) ∈
ℂ |
| 4 | | ax-icn 11214 |
. . . . . . . 8
⊢ i ∈
ℂ |
| 5 | | crrecz.2 |
. . . . . . . . 9
⊢ 𝐵 ∈ ℝ |
| 6 | 5 | recni 11275 |
. . . . . . . 8
⊢ 𝐵 ∈ ℂ |
| 7 | 4, 6 | mulcli 11268 |
. . . . . . 7
⊢ (i
· 𝐵) ∈
ℂ |
| 8 | 7 | sqcli 14220 |
. . . . . 6
⊢ ((i
· 𝐵)↑2) ∈
ℂ |
| 9 | 3, 8 | negsubi 11587 |
. . . . 5
⊢ ((𝐴↑2) + -((i · 𝐵)↑2)) = ((𝐴↑2) − ((i · 𝐵)↑2)) |
| 10 | 4, 6 | sqmuli 14223 |
. . . . . . . . 9
⊢ ((i
· 𝐵)↑2) =
((i↑2) · (𝐵↑2)) |
| 11 | | i2 14241 |
. . . . . . . . . 10
⊢
(i↑2) = -1 |
| 12 | 11 | oveq1i 7441 |
. . . . . . . . 9
⊢
((i↑2) · (𝐵↑2)) = (-1 · (𝐵↑2)) |
| 13 | | ax-1cn 11213 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
| 14 | 6 | sqcli 14220 |
. . . . . . . . . 10
⊢ (𝐵↑2) ∈
ℂ |
| 15 | 13, 14 | mulneg1i 11709 |
. . . . . . . . 9
⊢ (-1
· (𝐵↑2)) = -(1
· (𝐵↑2)) |
| 16 | 10, 12, 15 | 3eqtri 2769 |
. . . . . . . 8
⊢ ((i
· 𝐵)↑2) = -(1
· (𝐵↑2)) |
| 17 | 16 | negeqi 11501 |
. . . . . . 7
⊢ -((i
· 𝐵)↑2) = --(1
· (𝐵↑2)) |
| 18 | 13, 14 | mulcli 11268 |
. . . . . . . 8
⊢ (1
· (𝐵↑2)) ∈
ℂ |
| 19 | 18 | negnegi 11579 |
. . . . . . 7
⊢ --(1
· (𝐵↑2)) = (1
· (𝐵↑2)) |
| 20 | 14 | mullidi 11266 |
. . . . . . 7
⊢ (1
· (𝐵↑2)) =
(𝐵↑2) |
| 21 | 17, 19, 20 | 3eqtri 2769 |
. . . . . 6
⊢ -((i
· 𝐵)↑2) =
(𝐵↑2) |
| 22 | 21 | oveq2i 7442 |
. . . . 5
⊢ ((𝐴↑2) + -((i · 𝐵)↑2)) = ((𝐴↑2) + (𝐵↑2)) |
| 23 | 2, 7 | subsqi 14252 |
. . . . 5
⊢ ((𝐴↑2) − ((i ·
𝐵)↑2)) = ((𝐴 + (i · 𝐵)) · (𝐴 − (i · 𝐵))) |
| 24 | 9, 22, 23 | 3eqtr3ri 2774 |
. . . 4
⊢ ((𝐴 + (i · 𝐵)) · (𝐴 − (i · 𝐵))) = ((𝐴↑2) + (𝐵↑2)) |
| 25 | 24 | oveq1i 7441 |
. . 3
⊢ (((𝐴 + (i · 𝐵)) · (𝐴 − (i · 𝐵))) / ((𝐴↑2) + (𝐵↑2))) = (((𝐴↑2) + (𝐵↑2)) / ((𝐴↑2) + (𝐵↑2))) |
| 26 | | neorian 3037 |
. . . . 5
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ↔ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) |
| 27 | | sumsqeq0 14218 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 = 0 ∧ 𝐵 = 0) ↔ ((𝐴↑2) + (𝐵↑2)) = 0)) |
| 28 | 1, 5, 27 | mp2an 692 |
. . . . . 6
⊢ ((𝐴 = 0 ∧ 𝐵 = 0) ↔ ((𝐴↑2) + (𝐵↑2)) = 0) |
| 29 | 28 | necon3bbii 2988 |
. . . . 5
⊢ (¬
(𝐴 = 0 ∧ 𝐵 = 0) ↔ ((𝐴↑2) + (𝐵↑2)) ≠ 0) |
| 30 | 26, 29 | bitri 275 |
. . . 4
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ↔ ((𝐴↑2) + (𝐵↑2)) ≠ 0) |
| 31 | 2, 7 | addcli 11267 |
. . . . 5
⊢ (𝐴 + (i · 𝐵)) ∈ ℂ |
| 32 | 2, 7 | subcli 11585 |
. . . . 5
⊢ (𝐴 − (i · 𝐵)) ∈
ℂ |
| 33 | 3, 14 | addcli 11267 |
. . . . 5
⊢ ((𝐴↑2) + (𝐵↑2)) ∈ ℂ |
| 34 | 31, 32, 33 | divasszi 12017 |
. . . 4
⊢ (((𝐴↑2) + (𝐵↑2)) ≠ 0 → (((𝐴 + (i · 𝐵)) · (𝐴 − (i · 𝐵))) / ((𝐴↑2) + (𝐵↑2))) = ((𝐴 + (i · 𝐵)) · ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2))))) |
| 35 | 30, 34 | sylbi 217 |
. . 3
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → (((𝐴 + (i · 𝐵)) · (𝐴 − (i · 𝐵))) / ((𝐴↑2) + (𝐵↑2))) = ((𝐴 + (i · 𝐵)) · ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2))))) |
| 36 | | divid 11953 |
. . . . 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 217 |
. . 3
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → (((𝐴↑2) + (𝐵↑2)) / ((𝐴↑2) + (𝐵↑2))) = 1) |
| 39 | 25, 35, 38 | 3eqtr3a 2801 |
. 2
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → ((𝐴 + (i · 𝐵)) · ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2)))) = 1) |
| 40 | 32, 33 | divclzi 12002 |
. . . 4
⊢ (((𝐴↑2) + (𝐵↑2)) ≠ 0 → ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2))) ∈ ℂ) |
| 41 | 30, 40 | sylbi 217 |
. . 3
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2))) ∈ ℂ) |
| 42 | 31 | a1i 11 |
. . 3
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → (𝐴 + (i · 𝐵)) ∈ ℂ) |
| 43 | | crne0 12259 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ↔ (𝐴 + (i · 𝐵)) ≠ 0)) |
| 44 | 1, 5, 43 | mp2an 692 |
. . . 4
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ↔ (𝐴 + (i · 𝐵)) ≠ 0) |
| 45 | 44 | biimpi 216 |
. . 3
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → (𝐴 + (i · 𝐵)) ≠ 0) |
| 46 | | divmul 11925 |
. . . 4
⊢ ((1
∈ ℂ ∧ ((𝐴
− (i · 𝐵)) /
((𝐴↑2) + (𝐵↑2))) ∈ ℂ ∧
((𝐴 + (i · 𝐵)) ∈ ℂ ∧ (𝐴 + (i · 𝐵)) ≠ 0)) → ((1 / (𝐴 + (i · 𝐵))) = ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2))) ↔ ((𝐴 + (i · 𝐵)) · ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2)))) = 1)) |
| 47 | 13, 46 | mp3an1 1450 |
. . 3
⊢ ((((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2))) ∈ ℂ ∧ ((𝐴 + (i · 𝐵)) ∈ ℂ ∧ (𝐴 + (i · 𝐵)) ≠ 0)) → ((1 / (𝐴 + (i · 𝐵))) = ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2))) ↔ ((𝐴 + (i · 𝐵)) · ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2)))) = 1)) |
| 48 | 41, 42, 45, 47 | syl12anc 837 |
. 2
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → ((1 / (𝐴 + (i · 𝐵))) = ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2))) ↔ ((𝐴 + (i · 𝐵)) · ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2)))) = 1)) |
| 49 | 39, 48 | mpbird 257 |
1
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → (1 / (𝐴 + (i · 𝐵))) = ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2)))) |