Proof of Theorem mulreap
Step | Hyp | Ref
| Expression |
1 | | rereb 9091 |
. . 3
⊢ (A ∈ ℂ →
(A ∈
ℝ ↔ (ℜ‘A) = A)) |
2 | 1 | 3ad2ant1 924 |
. 2
⊢
((A ∈ ℂ ∧
B ∈
ℝ ∧ B # 0) → (A
∈ ℝ ↔ (ℜ‘A) = A)) |
3 | | recl 9081 |
. . . . 5
⊢ (A ∈ ℂ →
(ℜ‘A) ∈ ℝ) |
4 | 3 | recnd 6851 |
. . . 4
⊢ (A ∈ ℂ →
(ℜ‘A) ∈ ℂ) |
5 | 4 | 3ad2ant1 924 |
. . 3
⊢
((A ∈ ℂ ∧
B ∈
ℝ ∧ B # 0) → (ℜ‘A) ∈
ℂ) |
6 | | simp1 903 |
. . 3
⊢
((A ∈ ℂ ∧
B ∈
ℝ ∧ B # 0) → A
∈ ℂ) |
7 | | recn 6812 |
. . . . 5
⊢ (B ∈ ℝ →
B ∈
ℂ) |
8 | 7 | anim1i 323 |
. . . 4
⊢
((B ∈ ℝ ∧
B # 0) → (B ∈ ℂ ∧ B #
0)) |
9 | 8 | 3adant1 921 |
. . 3
⊢
((A ∈ ℂ ∧
B ∈
ℝ ∧ B # 0) → (B
∈ ℂ ∧
B # 0)) |
10 | | mulcanap 7428 |
. . 3
⊢
(((ℜ‘A) ∈ ℂ ∧
A ∈
ℂ ∧ (B ∈ ℂ ∧ B # 0)) →
((B · (ℜ‘A)) = (B
· A) ↔ (ℜ‘A) = A)) |
11 | 5, 6, 9, 10 | syl3anc 1134 |
. 2
⊢
((A ∈ ℂ ∧
B ∈
ℝ ∧ B # 0) → ((B · (ℜ‘A)) = (B
· A) ↔ (ℜ‘A) = A)) |
12 | 7 | adantr 261 |
. . . . . . . . . 10
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → B ∈ ℂ) |
13 | 4 | adantl 262 |
. . . . . . . . . 10
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → (ℜ‘A) ∈ ℂ) |
14 | | ax-icn 6778 |
. . . . . . . . . . . 12
⊢ i ∈ ℂ |
15 | | imcl 9082 |
. . . . . . . . . . . . 13
⊢ (A ∈ ℂ →
(ℑ‘A) ∈ ℝ) |
16 | 15 | recnd 6851 |
. . . . . . . . . . . 12
⊢ (A ∈ ℂ →
(ℑ‘A) ∈ ℂ) |
17 | | mulcl 6806 |
. . . . . . . . . . . 12
⊢ ((i ∈ ℂ ∧
(ℑ‘A) ∈ ℂ) → (i ·
(ℑ‘A)) ∈ ℂ) |
18 | 14, 16, 17 | sylancr 393 |
. . . . . . . . . . 11
⊢ (A ∈ ℂ →
(i · (ℑ‘A)) ∈ ℂ) |
19 | 18 | adantl 262 |
. . . . . . . . . 10
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → (i · (ℑ‘A)) ∈
ℂ) |
20 | 12, 13, 19 | adddid 6849 |
. . . . . . . . 9
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → (B ·
((ℜ‘A) + (i ·
(ℑ‘A)))) = ((B · (ℜ‘A)) + (B
· (i · (ℑ‘A))))) |
21 | | replim 9087 |
. . . . . . . . . . 11
⊢ (A ∈ ℂ →
A = ((ℜ‘A) + (i · (ℑ‘A)))) |
22 | 21 | adantl 262 |
. . . . . . . . . 10
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → A = ((ℜ‘A) + (i · (ℑ‘A)))) |
23 | 22 | oveq2d 5471 |
. . . . . . . . 9
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → (B · A) = (B ·
((ℜ‘A) + (i ·
(ℑ‘A))))) |
24 | | mul12 6939 |
. . . . . . . . . . . 12
⊢ ((i ∈ ℂ ∧
B ∈
ℂ ∧ (ℑ‘A) ∈ ℂ)
→ (i · (B ·
(ℑ‘A))) = (B · (i · (ℑ‘A)))) |
25 | 14, 24 | mp3an1 1218 |
. . . . . . . . . . 11
⊢
((B ∈ ℂ ∧
(ℑ‘A) ∈ ℂ) → (i · (B · (ℑ‘A))) = (B
· (i · (ℑ‘A)))) |
26 | 7, 16, 25 | syl2an 273 |
. . . . . . . . . 10
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → (i · (B ·
(ℑ‘A))) = (B · (i · (ℑ‘A)))) |
27 | 26 | oveq2d 5471 |
. . . . . . . . 9
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → ((B ·
(ℜ‘A)) + (i · (B · (ℑ‘A)))) = ((B
· (ℜ‘A)) + (B · (i · (ℑ‘A))))) |
28 | 20, 23, 27 | 3eqtr4d 2079 |
. . . . . . . 8
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → (B · A) = ((B
· (ℜ‘A)) + (i ·
(B · (ℑ‘A))))) |
29 | 28 | fveq2d 5125 |
. . . . . . 7
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → (ℜ‘(B ·
A)) = (ℜ‘((B · (ℜ‘A)) + (i · (B · (ℑ‘A)))))) |
30 | | remulcl 6807 |
. . . . . . . . 9
⊢
((B ∈ ℝ ∧
(ℜ‘A) ∈ ℝ) → (B · (ℜ‘A)) ∈
ℝ) |
31 | 3, 30 | sylan2 270 |
. . . . . . . 8
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → (B ·
(ℜ‘A)) ∈ ℝ) |
32 | | remulcl 6807 |
. . . . . . . . 9
⊢
((B ∈ ℝ ∧
(ℑ‘A) ∈ ℝ) → (B · (ℑ‘A)) ∈
ℝ) |
33 | 15, 32 | sylan2 270 |
. . . . . . . 8
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → (B ·
(ℑ‘A)) ∈ ℝ) |
34 | | crre 9085 |
. . . . . . . 8
⊢
(((B · (ℜ‘A)) ∈ ℝ
∧ (B
· (ℑ‘A)) ∈ ℝ) → (ℜ‘((B · (ℜ‘A)) + (i · (B · (ℑ‘A))))) = (B
· (ℜ‘A))) |
35 | 31, 33, 34 | syl2anc 391 |
. . . . . . 7
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → (ℜ‘((B ·
(ℜ‘A)) + (i · (B · (ℑ‘A))))) = (B
· (ℜ‘A))) |
36 | 29, 35 | eqtr2d 2070 |
. . . . . 6
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → (B ·
(ℜ‘A)) = (ℜ‘(B · A))) |
37 | 36 | eqeq1d 2045 |
. . . . 5
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → ((B ·
(ℜ‘A)) = (B · A)
↔ (ℜ‘(B · A)) = (B
· A))) |
38 | | mulcl 6806 |
. . . . . . 7
⊢
((B ∈ ℂ ∧
A ∈
ℂ) → (B · A) ∈
ℂ) |
39 | 7, 38 | sylan 267 |
. . . . . 6
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → (B · A) ∈
ℂ) |
40 | | rereb 9091 |
. . . . . 6
⊢
((B · A) ∈ ℂ
→ ((B · A) ∈ ℝ
↔ (ℜ‘(B · A)) = (B
· A))) |
41 | 39, 40 | syl 14 |
. . . . 5
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → ((B · A) ∈ ℝ
↔ (ℜ‘(B · A)) = (B
· A))) |
42 | 37, 41 | bitr4d 180 |
. . . 4
⊢
((B ∈ ℝ ∧
A ∈
ℂ) → ((B ·
(ℜ‘A)) = (B · A)
↔ (B · A) ∈
ℝ)) |
43 | 42 | ancoms 255 |
. . 3
⊢
((A ∈ ℂ ∧
B ∈
ℝ) → ((B ·
(ℜ‘A)) = (B · A)
↔ (B · A) ∈
ℝ)) |
44 | 43 | 3adant3 923 |
. 2
⊢
((A ∈ ℂ ∧
B ∈
ℝ ∧ B # 0) → ((B · (ℜ‘A)) = (B
· A) ↔ (B · A)
∈ ℝ)) |
45 | 2, 11, 44 | 3bitr2d 205 |
1
⊢
((A ∈ ℂ ∧
B ∈
ℝ ∧ B # 0) → (A
∈ ℝ ↔ (B · A)
∈ ℝ)) |