Proof of Theorem crre
Step | Hyp | Ref
| Expression |
1 | | recn 10698 |
. . . 4
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
2 | | ax-icn 10667 |
. . . . 5
⊢ i ∈
ℂ |
3 | | recn 10698 |
. . . . 5
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
4 | | mulcl 10692 |
. . . . 5
⊢ ((i
∈ ℂ ∧ 𝐵
∈ ℂ) → (i · 𝐵) ∈ ℂ) |
5 | 2, 3, 4 | sylancr 590 |
. . . 4
⊢ (𝐵 ∈ ℝ → (i
· 𝐵) ∈
ℂ) |
6 | | addcl 10690 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (i
· 𝐵) ∈ ℂ)
→ (𝐴 + (i ·
𝐵)) ∈
ℂ) |
7 | 1, 5, 6 | syl2an 599 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + (i · 𝐵)) ∈ ℂ) |
8 | | reval 14548 |
. . 3
⊢ ((𝐴 + (i · 𝐵)) ∈ ℂ →
(ℜ‘(𝐴 + (i
· 𝐵))) = (((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) / 2)) |
9 | 7, 8 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(ℜ‘(𝐴 + (i
· 𝐵))) = (((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) / 2)) |
10 | | cjcl 14547 |
. . . . . 6
⊢ ((𝐴 + (i · 𝐵)) ∈ ℂ →
(∗‘(𝐴 + (i
· 𝐵))) ∈
ℂ) |
11 | 7, 10 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(∗‘(𝐴 + (i
· 𝐵))) ∈
ℂ) |
12 | 7, 11 | addcld 10731 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) ∈ ℂ) |
13 | 12 | halfcld 11954 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) / 2) ∈ ℂ) |
14 | 1 | adantr 484 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ∈
ℂ) |
15 | | recl 14552 |
. . . . . . 7
⊢ ((𝐴 + (i · 𝐵)) ∈ ℂ →
(ℜ‘(𝐴 + (i
· 𝐵))) ∈
ℝ) |
16 | 7, 15 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(ℜ‘(𝐴 + (i
· 𝐵))) ∈
ℝ) |
17 | 9, 16 | eqeltrrd 2834 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) / 2) ∈ ℝ) |
18 | | simpl 486 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ∈
ℝ) |
19 | 17, 18 | resubcld 11139 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) / 2) − 𝐴) ∈ ℝ) |
20 | 2 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → i ∈
ℂ) |
21 | 3 | adantl 485 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈
ℂ) |
22 | 2, 21, 4 | sylancr 590 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (i
· 𝐵) ∈
ℂ) |
23 | 7, 11 | subcld 11068 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + (i · 𝐵)) − (∗‘(𝐴 + (i · 𝐵)))) ∈ ℂ) |
24 | 23 | halfcld 11954 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 + (i · 𝐵)) − (∗‘(𝐴 + (i · 𝐵)))) / 2) ∈ ℂ) |
25 | 20, 22, 24 | subdid 11167 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (i
· ((i · 𝐵)
− (((𝐴 + (i ·
𝐵)) −
(∗‘(𝐴 + (i
· 𝐵)))) / 2))) = ((i
· (i · 𝐵))
− (i · (((𝐴 +
(i · 𝐵)) −
(∗‘(𝐴 + (i
· 𝐵)))) /
2)))) |
26 | 14, 22, 14 | pnpcand 11105 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + (i · 𝐵)) − (𝐴 + 𝐴)) = ((i · 𝐵) − 𝐴)) |
27 | 22, 14, 22 | pnpcan2d 11106 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((i
· 𝐵) + (i ·
𝐵)) − (𝐴 + (i · 𝐵))) = ((i · 𝐵) − 𝐴)) |
28 | 26, 27 | eqtr4d 2776 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + (i · 𝐵)) − (𝐴 + 𝐴)) = (((i · 𝐵) + (i · 𝐵)) − (𝐴 + (i · 𝐵)))) |
29 | 28 | oveq1d 7179 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 + (i · 𝐵)) − (𝐴 + 𝐴)) + (∗‘(𝐴 + (i · 𝐵)))) = ((((i · 𝐵) + (i · 𝐵)) − (𝐴 + (i · 𝐵))) + (∗‘(𝐴 + (i · 𝐵))))) |
30 | 14, 14 | addcld 10731 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐴) ∈ ℂ) |
31 | 7, 11, 30 | addsubd 11089 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) − (𝐴 + 𝐴)) = (((𝐴 + (i · 𝐵)) − (𝐴 + 𝐴)) + (∗‘(𝐴 + (i · 𝐵))))) |
32 | 22, 22 | addcld 10731 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((i
· 𝐵) + (i ·
𝐵)) ∈
ℂ) |
33 | 32, 7, 11 | subsubd 11096 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((i
· 𝐵) + (i ·
𝐵)) − ((𝐴 + (i · 𝐵)) − (∗‘(𝐴 + (i · 𝐵))))) = ((((i · 𝐵) + (i · 𝐵)) − (𝐴 + (i · 𝐵))) + (∗‘(𝐴 + (i · 𝐵))))) |
34 | 29, 31, 33 | 3eqtr4d 2783 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) − (𝐴 + 𝐴)) = (((i · 𝐵) + (i · 𝐵)) − ((𝐴 + (i · 𝐵)) − (∗‘(𝐴 + (i · 𝐵)))))) |
35 | 14 | 2timesd 11952 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (2
· 𝐴) = (𝐴 + 𝐴)) |
36 | 35 | oveq2d 7180 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) − (2 · 𝐴)) = (((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) − (𝐴 + 𝐴))) |
37 | 22 | 2timesd 11952 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (2
· (i · 𝐵)) =
((i · 𝐵) + (i
· 𝐵))) |
38 | 37 | oveq1d 7179 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((2
· (i · 𝐵))
− ((𝐴 + (i ·
𝐵)) −
(∗‘(𝐴 + (i
· 𝐵))))) = (((i
· 𝐵) + (i ·
𝐵)) − ((𝐴 + (i · 𝐵)) − (∗‘(𝐴 + (i · 𝐵)))))) |
39 | 34, 36, 38 | 3eqtr4d 2783 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) − (2 · 𝐴)) = ((2 · (i · 𝐵)) − ((𝐴 + (i · 𝐵)) − (∗‘(𝐴 + (i · 𝐵)))))) |
40 | 39 | oveq1d 7179 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) − (2 · 𝐴)) / 2) = (((2 · (i · 𝐵)) − ((𝐴 + (i · 𝐵)) − (∗‘(𝐴 + (i · 𝐵))))) / 2)) |
41 | | 2cn 11784 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
42 | | mulcl 10692 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 𝐴
∈ ℂ) → (2 · 𝐴) ∈ ℂ) |
43 | 41, 14, 42 | sylancr 590 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (2
· 𝐴) ∈
ℂ) |
44 | 41 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 2 ∈
ℂ) |
45 | | 2ne0 11813 |
. . . . . . . . . . 11
⊢ 2 ≠
0 |
46 | 45 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 2 ≠
0) |
47 | 12, 43, 44, 46 | divsubdird 11526 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) − (2 · 𝐴)) / 2) = ((((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) / 2) − ((2 · 𝐴) / 2))) |
48 | | mulcl 10692 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ (i · 𝐵) ∈ ℂ) → (2 · (i
· 𝐵)) ∈
ℂ) |
49 | 41, 22, 48 | sylancr 590 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (2
· (i · 𝐵))
∈ ℂ) |
50 | 49, 23, 44, 46 | divsubdird 11526 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((2
· (i · 𝐵))
− ((𝐴 + (i ·
𝐵)) −
(∗‘(𝐴 + (i
· 𝐵))))) / 2) = (((2
· (i · 𝐵)) /
2) − (((𝐴 + (i
· 𝐵)) −
(∗‘(𝐴 + (i
· 𝐵)))) /
2))) |
51 | 40, 47, 50 | 3eqtr3d 2781 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) / 2) − ((2 · 𝐴) / 2)) = (((2 · (i
· 𝐵)) / 2) −
(((𝐴 + (i · 𝐵)) −
(∗‘(𝐴 + (i
· 𝐵)))) /
2))) |
52 | 14, 44, 46 | divcan3d 11492 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((2
· 𝐴) / 2) = 𝐴) |
53 | 52 | oveq2d 7180 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) / 2) − ((2 · 𝐴) / 2)) = ((((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) / 2) − 𝐴)) |
54 | 22, 44, 46 | divcan3d 11492 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((2
· (i · 𝐵)) /
2) = (i · 𝐵)) |
55 | 54 | oveq1d 7179 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((2
· (i · 𝐵)) /
2) − (((𝐴 + (i
· 𝐵)) −
(∗‘(𝐴 + (i
· 𝐵)))) / 2)) = ((i
· 𝐵) −
(((𝐴 + (i · 𝐵)) −
(∗‘(𝐴 + (i
· 𝐵)))) /
2))) |
56 | 51, 53, 55 | 3eqtr3d 2781 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) / 2) − 𝐴) = ((i · 𝐵) − (((𝐴 + (i · 𝐵)) − (∗‘(𝐴 + (i · 𝐵)))) / 2))) |
57 | 56 | oveq2d 7180 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (i
· ((((𝐴 + (i
· 𝐵)) +
(∗‘(𝐴 + (i
· 𝐵)))) / 2) −
𝐴)) = (i · ((i
· 𝐵) −
(((𝐴 + (i · 𝐵)) −
(∗‘(𝐴 + (i
· 𝐵)))) /
2)))) |
58 | 20, 20, 21 | mulassd 10735 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((i
· i) · 𝐵) =
(i · (i · 𝐵))) |
59 | 20, 23, 44, 46 | divassd 11522 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((i
· ((𝐴 + (i ·
𝐵)) −
(∗‘(𝐴 + (i
· 𝐵))))) / 2) = (i
· (((𝐴 + (i ·
𝐵)) −
(∗‘(𝐴 + (i
· 𝐵)))) /
2))) |
60 | 58, 59 | oveq12d 7182 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((i
· i) · 𝐵)
− ((i · ((𝐴 +
(i · 𝐵)) −
(∗‘(𝐴 + (i
· 𝐵))))) / 2)) = ((i
· (i · 𝐵))
− (i · (((𝐴 +
(i · 𝐵)) −
(∗‘(𝐴 + (i
· 𝐵)))) /
2)))) |
61 | 25, 57, 60 | 3eqtr4d 2783 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (i
· ((((𝐴 + (i
· 𝐵)) +
(∗‘(𝐴 + (i
· 𝐵)))) / 2) −
𝐴)) = (((i · i)
· 𝐵) − ((i
· ((𝐴 + (i ·
𝐵)) −
(∗‘(𝐴 + (i
· 𝐵))))) /
2))) |
62 | | ixi 11340 |
. . . . . . . 8
⊢ (i
· i) = -1 |
63 | | neg1rr 11824 |
. . . . . . . 8
⊢ -1 ∈
ℝ |
64 | 62, 63 | eqeltri 2829 |
. . . . . . 7
⊢ (i
· i) ∈ ℝ |
65 | | simpr 488 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈
ℝ) |
66 | | remulcl 10693 |
. . . . . . 7
⊢ (((i
· i) ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((i · i)
· 𝐵) ∈
ℝ) |
67 | 64, 65, 66 | sylancr 590 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((i
· i) · 𝐵)
∈ ℝ) |
68 | | cjth 14545 |
. . . . . . . . 9
⊢ ((𝐴 + (i · 𝐵)) ∈ ℂ → (((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) ∈ ℝ ∧ (i ·
((𝐴 + (i · 𝐵)) −
(∗‘(𝐴 + (i
· 𝐵))))) ∈
ℝ)) |
69 | 68 | simprd 499 |
. . . . . . . 8
⊢ ((𝐴 + (i · 𝐵)) ∈ ℂ → (i · ((𝐴 + (i · 𝐵)) − (∗‘(𝐴 + (i · 𝐵))))) ∈ ℝ) |
70 | 7, 69 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (i
· ((𝐴 + (i ·
𝐵)) −
(∗‘(𝐴 + (i
· 𝐵))))) ∈
ℝ) |
71 | 70 | rehalfcld 11956 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((i
· ((𝐴 + (i ·
𝐵)) −
(∗‘(𝐴 + (i
· 𝐵))))) / 2) ∈
ℝ) |
72 | 67, 71 | resubcld 11139 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((i
· i) · 𝐵)
− ((i · ((𝐴 +
(i · 𝐵)) −
(∗‘(𝐴 + (i
· 𝐵))))) / 2))
∈ ℝ) |
73 | 61, 72 | eqeltrd 2833 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (i
· ((((𝐴 + (i
· 𝐵)) +
(∗‘(𝐴 + (i
· 𝐵)))) / 2) −
𝐴)) ∈
ℝ) |
74 | | rimul 11700 |
. . . 4
⊢
((((((𝐴 + (i
· 𝐵)) +
(∗‘(𝐴 + (i
· 𝐵)))) / 2) −
𝐴) ∈ ℝ ∧ (i
· ((((𝐴 + (i
· 𝐵)) +
(∗‘(𝐴 + (i
· 𝐵)))) / 2) −
𝐴)) ∈ ℝ) →
((((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) / 2) − 𝐴) = 0) |
75 | 19, 73, 74 | syl2anc 587 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) / 2) − 𝐴) = 0) |
76 | 13, 14, 75 | subeq0d 11076 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 + (i · 𝐵)) + (∗‘(𝐴 + (i · 𝐵)))) / 2) = 𝐴) |
77 | 9, 76 | eqtrd 2773 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(ℜ‘(𝐴 + (i
· 𝐵))) = 𝐴) |