# 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 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \Re \left({A}+\mathrm{i}{B}\right)={A}$

### Proof

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