Proof of Theorem cjadd
| Step | Hyp | Ref
| Expression |
| 1 | | readd 15165 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))) |
| 2 | | imadd 15173 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))) |
| 3 | 2 | oveq2d 7447 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (ℑ‘(𝐴
+ 𝐵))) = (i ·
((ℑ‘𝐴) +
(ℑ‘𝐵)))) |
| 4 | | ax-icn 11214 |
. . . . . . 7
⊢ i ∈
ℂ |
| 5 | 4 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → i ∈
ℂ) |
| 6 | | imcl 15150 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) |
| 7 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘𝐴) ∈
ℝ) |
| 8 | 7 | recnd 11289 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘𝐴) ∈
ℂ) |
| 9 | | imcl 15150 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ →
(ℑ‘𝐵) ∈
ℝ) |
| 10 | 9 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘𝐵) ∈
ℝ) |
| 11 | 10 | recnd 11289 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘𝐵) ∈
ℂ) |
| 12 | 5, 8, 11 | adddid 11285 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· ((ℑ‘𝐴)
+ (ℑ‘𝐵))) = ((i
· (ℑ‘𝐴))
+ (i · (ℑ‘𝐵)))) |
| 13 | 3, 12 | eqtrd 2777 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (ℑ‘(𝐴
+ 𝐵))) = ((i ·
(ℑ‘𝐴)) + (i
· (ℑ‘𝐵)))) |
| 14 | 1, 13 | oveq12d 7449 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℜ‘(𝐴 + 𝐵)) − (i ·
(ℑ‘(𝐴 + 𝐵)))) = (((ℜ‘𝐴) + (ℜ‘𝐵)) − ((i ·
(ℑ‘𝐴)) + (i
· (ℑ‘𝐵))))) |
| 15 | | recl 15149 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) |
| 16 | 15 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘𝐴) ∈
ℝ) |
| 17 | 16 | recnd 11289 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘𝐴) ∈
ℂ) |
| 18 | | recl 15149 |
. . . . . 6
⊢ (𝐵 ∈ ℂ →
(ℜ‘𝐵) ∈
ℝ) |
| 19 | 18 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘𝐵) ∈
ℝ) |
| 20 | 19 | recnd 11289 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘𝐵) ∈
ℂ) |
| 21 | | mulcl 11239 |
. . . . 5
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → (i ·
(ℑ‘𝐴)) ∈
ℂ) |
| 22 | 4, 8, 21 | sylancr 587 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (ℑ‘𝐴))
∈ ℂ) |
| 23 | | mulcl 11239 |
. . . . 5
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐵) ∈ ℂ) → (i ·
(ℑ‘𝐵)) ∈
ℂ) |
| 24 | 4, 11, 23 | sylancr 587 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (ℑ‘𝐵))
∈ ℂ) |
| 25 | 17, 20, 22, 24 | addsub4d 11667 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((ℜ‘𝐴) +
(ℜ‘𝐵)) −
((i · (ℑ‘𝐴)) + (i · (ℑ‘𝐵)))) = (((ℜ‘𝐴) − (i ·
(ℑ‘𝐴))) +
((ℜ‘𝐵) −
(i · (ℑ‘𝐵))))) |
| 26 | 14, 25 | eqtrd 2777 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℜ‘(𝐴 + 𝐵)) − (i ·
(ℑ‘(𝐴 + 𝐵)))) = (((ℜ‘𝐴) − (i ·
(ℑ‘𝐴))) +
((ℜ‘𝐵) −
(i · (ℑ‘𝐵))))) |
| 27 | | addcl 11237 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
| 28 | | remim 15156 |
. . 3
⊢ ((𝐴 + 𝐵) ∈ ℂ →
(∗‘(𝐴 + 𝐵)) = ((ℜ‘(𝐴 + 𝐵)) − (i · (ℑ‘(𝐴 + 𝐵))))) |
| 29 | 27, 28 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(∗‘(𝐴 + 𝐵)) = ((ℜ‘(𝐴 + 𝐵)) − (i · (ℑ‘(𝐴 + 𝐵))))) |
| 30 | | remim 15156 |
. . 3
⊢ (𝐴 ∈ ℂ →
(∗‘𝐴) =
((ℜ‘𝐴) −
(i · (ℑ‘𝐴)))) |
| 31 | | remim 15156 |
. . 3
⊢ (𝐵 ∈ ℂ →
(∗‘𝐵) =
((ℜ‘𝐵) −
(i · (ℑ‘𝐵)))) |
| 32 | 30, 31 | oveqan12d 7450 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((∗‘𝐴) +
(∗‘𝐵)) =
(((ℜ‘𝐴) −
(i · (ℑ‘𝐴))) + ((ℜ‘𝐵) − (i · (ℑ‘𝐵))))) |
| 33 | 26, 29, 32 | 3eqtr4d 2787 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵))) |