Proof of Theorem readd
Step | Hyp | Ref
| Expression |
1 | | recl 10804 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(ℜ‘𝐴) ∈
ℝ) |
2 | 1 | adantr 274 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘𝐴) ∈
ℝ) |
3 | 2 | recnd 7935 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘𝐴) ∈
ℂ) |
4 | | ax-icn 7856 |
. . . . . 6
⊢ i ∈
ℂ |
5 | | imcl 10805 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
(ℑ‘𝐴) ∈
ℝ) |
6 | 5 | adantr 274 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘𝐴) ∈
ℝ) |
7 | 6 | recnd 7935 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘𝐴) ∈
ℂ) |
8 | | mulcl 7888 |
. . . . . 6
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → (i ·
(ℑ‘𝐴)) ∈
ℂ) |
9 | 4, 7, 8 | sylancr 412 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (ℑ‘𝐴))
∈ ℂ) |
10 | | recl 10804 |
. . . . . . 7
⊢ (𝐵 ∈ ℂ →
(ℜ‘𝐵) ∈
ℝ) |
11 | 10 | adantl 275 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘𝐵) ∈
ℝ) |
12 | 11 | recnd 7935 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘𝐵) ∈
ℂ) |
13 | | imcl 10805 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ →
(ℑ‘𝐵) ∈
ℝ) |
14 | 13 | adantl 275 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘𝐵) ∈
ℝ) |
15 | 14 | recnd 7935 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℑ‘𝐵) ∈
ℂ) |
16 | | mulcl 7888 |
. . . . . 6
⊢ ((i
∈ ℂ ∧ (ℑ‘𝐵) ∈ ℂ) → (i ·
(ℑ‘𝐵)) ∈
ℂ) |
17 | 4, 15, 16 | sylancr 412 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· (ℑ‘𝐵))
∈ ℂ) |
18 | 3, 9, 12, 17 | add4d 8075 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((ℜ‘𝐴) + (i
· (ℑ‘𝐴))) + ((ℜ‘𝐵) + (i · (ℑ‘𝐵)))) = (((ℜ‘𝐴) + (ℜ‘𝐵)) + ((i ·
(ℑ‘𝐴)) + (i
· (ℑ‘𝐵))))) |
19 | | replim 10810 |
. . . . 5
⊢ (𝐴 ∈ ℂ → 𝐴 = ((ℜ‘𝐴) + (i ·
(ℑ‘𝐴)))) |
20 | | replim 10810 |
. . . . 5
⊢ (𝐵 ∈ ℂ → 𝐵 = ((ℜ‘𝐵) + (i ·
(ℑ‘𝐵)))) |
21 | 19, 20 | oveqan12d 5869 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (((ℜ‘𝐴) + (i · (ℑ‘𝐴))) + ((ℜ‘𝐵) + (i ·
(ℑ‘𝐵))))) |
22 | 4 | a1i 9 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → i ∈
ℂ) |
23 | 22, 7, 15 | adddid 7931 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i
· ((ℑ‘𝐴)
+ (ℑ‘𝐵))) = ((i
· (ℑ‘𝐴))
+ (i · (ℑ‘𝐵)))) |
24 | 23 | oveq2d 5866 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(((ℜ‘𝐴) +
(ℜ‘𝐵)) + (i
· ((ℑ‘𝐴)
+ (ℑ‘𝐵)))) =
(((ℜ‘𝐴) +
(ℜ‘𝐵)) + ((i
· (ℑ‘𝐴))
+ (i · (ℑ‘𝐵))))) |
25 | 18, 21, 24 | 3eqtr4d 2213 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (((ℜ‘𝐴) + (ℜ‘𝐵)) + (i · ((ℑ‘𝐴) + (ℑ‘𝐵))))) |
26 | 25 | fveq2d 5498 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘(𝐴 + 𝐵)) =
(ℜ‘(((ℜ‘𝐴) + (ℜ‘𝐵)) + (i · ((ℑ‘𝐴) + (ℑ‘𝐵)))))) |
27 | | readdcl 7887 |
. . . 4
⊢
(((ℜ‘𝐴)
∈ ℝ ∧ (ℜ‘𝐵) ∈ ℝ) →
((ℜ‘𝐴) +
(ℜ‘𝐵)) ∈
ℝ) |
28 | 1, 10, 27 | syl2an 287 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℜ‘𝐴) +
(ℜ‘𝐵)) ∈
ℝ) |
29 | | readdcl 7887 |
. . . 4
⊢
(((ℑ‘𝐴)
∈ ℝ ∧ (ℑ‘𝐵) ∈ ℝ) →
((ℑ‘𝐴) +
(ℑ‘𝐵)) ∈
ℝ) |
30 | 5, 13, 29 | syl2an 287 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
((ℑ‘𝐴) +
(ℑ‘𝐵)) ∈
ℝ) |
31 | | crre 10808 |
. . 3
⊢
((((ℜ‘𝐴)
+ (ℜ‘𝐵)) ∈
ℝ ∧ ((ℑ‘𝐴) + (ℑ‘𝐵)) ∈ ℝ) →
(ℜ‘(((ℜ‘𝐴) + (ℜ‘𝐵)) + (i · ((ℑ‘𝐴) + (ℑ‘𝐵))))) = ((ℜ‘𝐴) + (ℜ‘𝐵))) |
32 | 28, 30, 31 | syl2anc 409 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘(((ℜ‘𝐴) + (ℜ‘𝐵)) + (i · ((ℑ‘𝐴) + (ℑ‘𝐵))))) = ((ℜ‘𝐴) + (ℜ‘𝐵))) |
33 | 26, 32 | eqtrd 2203 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))) |