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	$⊢ (A \in ℝ \land B \in ℝ) \to ℜ (A + i B) = A$

Proof

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

Metamath Proof Explorer

Theorem crre

Proof