Proof of Theorem cjadd
Step | Hyp | Ref
| Expression |
1 | | readd 14578 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))) |
2 | | imadd 14586 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))) |
3 | 2 | oveq2d 7189 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (ℑ‘(𝐴
+ 𝐵))) = (i ·
((ℑ‘𝐴) +
(ℑ‘𝐵)))) |
4 | | ax-icn 10677 |
. . . . . . 7
⊢ i ∈
ℂ |
5 | 4 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → i ∈
ℂ) |
6 | | imcl 14563 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) |
7 | 6 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘𝐴) ∈
ℝ) |
8 | 7 | recnd 10750 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘𝐴) ∈
ℂ) |
9 | | imcl 14563 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ →
(ℑ‘𝐵) ∈
ℝ) |
10 | 9 | adantl 485 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘𝐵) ∈
ℝ) |
11 | 10 | recnd 10750 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘𝐵) ∈
ℂ) |
12 | 5, 8, 11 | adddid 10746 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· ((ℑ‘𝐴)
+ (ℑ‘𝐵))) = ((i
· (ℑ‘𝐴))
+ (i · (ℑ‘𝐵)))) |
13 | 3, 12 | eqtrd 2774 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (ℑ‘(𝐴
+ 𝐵))) = ((i ·
(ℑ‘𝐴)) + (i
· (ℑ‘𝐵)))) |
14 | 1, 13 | oveq12d 7191 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℜ‘(𝐴 + 𝐵)) − (i ·
(ℑ‘(𝐴 + 𝐵)))) = (((ℜ‘𝐴) + (ℜ‘𝐵)) − ((i ·
(ℑ‘𝐴)) + (i
· (ℑ‘𝐵))))) |
15 | | recl 14562 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) |
16 | 15 | adantr 484 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘𝐴) ∈
ℝ) |
17 | 16 | recnd 10750 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘𝐴) ∈
ℂ) |
18 | | recl 14562 |
. . . . . 6
⊢ (𝐵 ∈ ℂ →
(ℜ‘𝐵) ∈
ℝ) |
19 | 18 | adantl 485 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘𝐵) ∈
ℝ) |
20 | 19 | recnd 10750 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘𝐵) ∈
ℂ) |
21 | | mulcl 10702 |
. . . . 5
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → (i ·
(ℑ‘𝐴)) ∈
ℂ) |
22 | 4, 8, 21 | sylancr 590 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (ℑ‘𝐴))
∈ ℂ) |
23 | | mulcl 10702 |
. . . . 5
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐵) ∈ ℂ) → (i ·
(ℑ‘𝐵)) ∈
ℂ) |
24 | 4, 11, 23 | sylancr 590 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (ℑ‘𝐵))
∈ ℂ) |
25 | 17, 20, 22, 24 | addsub4d 11125 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((ℜ‘𝐴) +
(ℜ‘𝐵)) −
((i · (ℑ‘𝐴)) + (i · (ℑ‘𝐵)))) = (((ℜ‘𝐴) − (i ·
(ℑ‘𝐴))) +
((ℜ‘𝐵) −
(i · (ℑ‘𝐵))))) |
26 | 14, 25 | eqtrd 2774 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℜ‘(𝐴 + 𝐵)) − (i ·
(ℑ‘(𝐴 + 𝐵)))) = (((ℜ‘𝐴) − (i ·
(ℑ‘𝐴))) +
((ℜ‘𝐵) −
(i · (ℑ‘𝐵))))) |
27 | | addcl 10700 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) |
28 | | remim 14569 |
. . 3
⊢ ((𝐴 + 𝐵) ∈ ℂ →
(∗‘(𝐴 + 𝐵)) = ((ℜ‘(𝐴 + 𝐵)) − (i · (ℑ‘(𝐴 + 𝐵))))) |
29 | 27, 28 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(∗‘(𝐴 + 𝐵)) = ((ℜ‘(𝐴 + 𝐵)) − (i · (ℑ‘(𝐴 + 𝐵))))) |
30 | | remim 14569 |
. . 3
⊢ (𝐴 ∈ ℂ →
(∗‘𝐴) =
((ℜ‘𝐴) −
(i · (ℑ‘𝐴)))) |
31 | | remim 14569 |
. . 3
⊢ (𝐵 ∈ ℂ →
(∗‘𝐵) =
((ℜ‘𝐵) −
(i · (ℑ‘𝐵)))) |
32 | 30, 31 | oveqan12d 7192 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((∗‘𝐴) +
(∗‘𝐵)) =
(((ℜ‘𝐴) −
(i · (ℑ‘𝐴))) + ((ℜ‘𝐵) − (i · (ℑ‘𝐵))))) |
33 | 26, 29, 32 | 3eqtr4d 2784 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵))) |