Theorem cjth

Description: The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013)

	Ref	Expression
Assertion	cjth	|- ( A e. CC -> ( ( A + ( * ` A ) ) e. RR /\ ( _i x. ( A - ( * ` A ) ) ) e. RR ) )

Proof

Step	Hyp	Ref	Expression
1		cju	|- ( A e. CC -> E! x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) )
2		riotasbc	|- ( E! x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) -> [. ( iota_ x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) / x ]. ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) )
3	1 2	syl	|- ( A e. CC -> [. ( iota_ x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) / x ]. ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) )
4		cjval	|- ( A e. CC -> ( * ` A ) = ( iota_ x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) )
5	4	sbceq1d	|- ( A e. CC -> ( [. ( * ` A ) / x ]. ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) <-> [. ( iota_ x e. CC ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) / x ]. ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) ) )
6	3 5	mpbird	|- ( A e. CC -> [. ( * ` A ) / x ]. ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) )
7		fvex	|- ( * ` A ) e. _V
8		oveq2	|- ( x = ( * ` A ) -> ( A + x ) = ( A + ( * ` A ) ) )
9	8	eleq1d	|- ( x = ( * ` A ) -> ( ( A + x ) e. RR <-> ( A + ( * ` A ) ) e. RR ) )
10		oveq2	|- ( x = ( * ` A ) -> ( A - x ) = ( A - ( * ` A ) ) )
11	10	oveq2d	|- ( x = ( * ` A ) -> ( _i x. ( A - x ) ) = ( _i x. ( A - ( * ` A ) ) ) )
12	11	eleq1d	|- ( x = ( * ` A ) -> ( ( _i x. ( A - x ) ) e. RR <-> ( _i x. ( A - ( * ` A ) ) ) e. RR ) )
13	9 12	anbi12d	|- ( x = ( * ` A ) -> ( ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) <-> ( ( A + ( * ` A ) ) e. RR /\ ( _i x. ( A - ( * ` A ) ) ) e. RR ) ) )
14	7 13	sbcie	|- ( [. ( * ` A ) / x ]. ( ( A + x ) e. RR /\ ( _i x. ( A - x ) ) e. RR ) <-> ( ( A + ( * ` A ) ) e. RR /\ ( _i x. ( A - ( * ` A ) ) ) e. RR ) )
15	6 14	sylib	|- ( A e. CC -> ( ( A + ( * ` A ) ) e. RR /\ ( _i x. ( A - ( * ` A ) ) ) e. RR ) )