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	|- ( ( A e. RR /\ B e. RR ) -> ( Re ` ( A + ( _i x. B ) ) ) = A )

Proof

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