Metamath Proof Explorer

Theorem crre

Description: The real part of a complex number representation. Definition 10-3.1 of Gleason p. 132. (Contributed by NM, 12-May-2005) (Revised by Mario Carneiro, 7-Nov-2013)

Ref Expression
Assertion crre ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2 ax-icn ⊢ i ∈ ℂ
3 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
4 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · 𝐵 ) ∈ ℂ )
5 2 3 4 sylancr ⊢ ( 𝐵 ∈ ℝ → ( i · 𝐵 ) ∈ ℂ )
6 addcl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( i · 𝐵 ) ∈ ℂ ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ )
7 1 5 6 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ )
8 reval ⊢ ( ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ → ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) )
9 7 8 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) )
10 cjcl ⊢ ( ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ → ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℂ )
11 7 10 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℂ )
12 7 11 addcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ∈ ℂ )
13 12 halfcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) ∈ ℂ )
14 1 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℂ )
15 recl ⊢ ( ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ → ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℝ )
16 7 15 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℝ )
17 9 16 eqeltrrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) ∈ ℝ )
18 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
19 17 18 resubcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) − 𝐴 ) ∈ ℝ )
20 2 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → i ∈ ℂ )
21 3 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℂ )
22 2 21 4 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( i · 𝐵 ) ∈ ℂ )
23 7 11 subcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ∈ ℂ )
24 23 halfcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) ∈ ℂ )
25 20 22 24 subdid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( i · ( ( i · 𝐵 ) − ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) ) ) = ( ( i · ( i · 𝐵 ) ) − ( i · ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) ) ) )
26 14 22 14 pnpcand ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + ( i · 𝐵 ) ) − ( 𝐴 + 𝐴 ) ) = ( ( i · 𝐵 ) − 𝐴 ) )
27 22 14 22 pnpcan2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( i · 𝐵 ) + ( i · 𝐵 ) ) − ( 𝐴 + ( i · 𝐵 ) ) ) = ( ( i · 𝐵 ) − 𝐴 ) )
28 26 27 eqtr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + ( i · 𝐵 ) ) − ( 𝐴 + 𝐴 ) ) = ( ( ( i · 𝐵 ) + ( i · 𝐵 ) ) − ( 𝐴 + ( i · 𝐵 ) ) ) )
29 28 oveq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( 𝐴 + 𝐴 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) = ( ( ( ( i · 𝐵 ) + ( i · 𝐵 ) ) − ( 𝐴 + ( i · 𝐵 ) ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) )
30 14 14 addcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐴 ) ∈ ℂ )
31 7 11 30 addsubd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) − ( 𝐴 + 𝐴 ) ) = ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( 𝐴 + 𝐴 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) )
32 22 22 addcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( i · 𝐵 ) + ( i · 𝐵 ) ) ∈ ℂ )
33 32 7 11 subsubd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( i · 𝐵 ) + ( i · 𝐵 ) ) − ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ) = ( ( ( ( i · 𝐵 ) + ( i · 𝐵 ) ) − ( 𝐴 + ( i · 𝐵 ) ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) )
34 29 31 33 3eqtr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) − ( 𝐴 + 𝐴 ) ) = ( ( ( i · 𝐵 ) + ( i · 𝐵 ) ) − ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ) )
35 14 2timesd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
36 35 oveq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) − ( 2 · 𝐴 ) ) = ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) − ( 𝐴 + 𝐴 ) ) )
37 22 2timesd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 2 · ( i · 𝐵 ) ) = ( ( i · 𝐵 ) + ( i · 𝐵 ) ) )
38 37 oveq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 2 · ( i · 𝐵 ) ) − ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ) = ( ( ( i · 𝐵 ) + ( i · 𝐵 ) ) − ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ) )
39 34 36 38 3eqtr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) − ( 2 · 𝐴 ) ) = ( ( 2 · ( i · 𝐵 ) ) − ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ) )
40 39 oveq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) − ( 2 · 𝐴 ) ) / 2 ) = ( ( ( 2 · ( i · 𝐵 ) ) − ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ) / 2 ) )
41 2cn ⊢ 2 ∈ ℂ
42 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 2 · 𝐴 ) ∈ ℂ )
43 41 14 42 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 2 · 𝐴 ) ∈ ℂ )
44 41 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 2 ∈ ℂ )
45 2ne0 ⊢ 2 ≠ 0
46 45 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 2 ≠ 0 )
47 12 43 44 46 divsubdird ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) − ( 2 · 𝐴 ) ) / 2 ) = ( ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) − ( ( 2 · 𝐴 ) / 2 ) ) )
48 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( i · 𝐵 ) ∈ ℂ ) → ( 2 · ( i · 𝐵 ) ) ∈ ℂ )
49 41 22 48 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 2 · ( i · 𝐵 ) ) ∈ ℂ )
50 49 23 44 46 divsubdird ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 2 · ( i · 𝐵 ) ) − ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ) / 2 ) = ( ( ( 2 · ( i · 𝐵 ) ) / 2 ) − ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) ) )
51 40 47 50 3eqtr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) − ( ( 2 · 𝐴 ) / 2 ) ) = ( ( ( 2 · ( i · 𝐵 ) ) / 2 ) − ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) ) )
52 14 44 46 divcan3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 2 · 𝐴 ) / 2 ) = 𝐴 )
53 52 oveq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) − ( ( 2 · 𝐴 ) / 2 ) ) = ( ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) − 𝐴 ) )
54 22 44 46 divcan3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 2 · ( i · 𝐵 ) ) / 2 ) = ( i · 𝐵 ) )
55 54 oveq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 2 · ( i · 𝐵 ) ) / 2 ) − ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) ) = ( ( i · 𝐵 ) − ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) ) )
56 51 53 55 3eqtr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) − 𝐴 ) = ( ( i · 𝐵 ) − ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) ) )
57 56 oveq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( i · ( ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) − 𝐴 ) ) = ( i · ( ( i · 𝐵 ) − ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) ) ) )
58 20 20 21 mulassd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( i · i ) · 𝐵 ) = ( i · ( i · 𝐵 ) ) )
59 20 23 44 46 divassd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( i · ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ) / 2 ) = ( i · ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) ) )
60 58 59 oveq12d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( i · i ) · 𝐵 ) − ( ( i · ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ) / 2 ) ) = ( ( i · ( i · 𝐵 ) ) − ( i · ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) ) ) )
61 25 57 60 3eqtr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( i · ( ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) − 𝐴 ) ) = ( ( ( i · i ) · 𝐵 ) − ( ( i · ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ) / 2 ) ) )
62 ixi ⊢ ( i · i ) = - 1
63 neg1rr ⊢ - 1 ∈ ℝ
64 62 63 eqeltri ⊢ ( i · i ) ∈ ℝ
65 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
66 remulcl ⊢ ( ( ( i · i ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( i · i ) · 𝐵 ) ∈ ℝ )
67 64 65 66 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( i · i ) · 𝐵 ) ∈ ℝ )
68 cjth ⊢ ( ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ → ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ∈ ℝ ∧ ( i · ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ) ∈ ℝ ) )
69 68 simprd ⊢ ( ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ → ( i · ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ) ∈ ℝ )
70 7 69 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( i · ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ) ∈ ℝ )
71 70 rehalfcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( i · ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ) / 2 ) ∈ ℝ )
72 67 71 resubcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( i · i ) · 𝐵 ) − ( ( i · ( ( 𝐴 + ( i · 𝐵 ) ) − ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) ) / 2 ) ) ∈ ℝ )
73 61 72 eqeltrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( i · ( ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) − 𝐴 ) ) ∈ ℝ )
74 rimul ⊢ ( ( ( ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) − 𝐴 ) ∈ ℝ ∧ ( i · ( ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) − 𝐴 ) ) ∈ ℝ ) → ( ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) − 𝐴 ) = 0 )
75 19 73 74 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) − 𝐴 ) = 0 )
76 13 14 75 subeq0d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + ( i · 𝐵 ) ) + ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) / 2 ) = 𝐴 )
77 9 76 eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐴 )