Theorem absval2

Description: Value of absolute value function. Definition 10.36 of Gleason p. 133. (Contributed by NM, 17-Mar-2005)

	Ref	Expression
Assertion	absval2	|- ( A e. CC -> ( abs ` A ) = ( sqrt ` ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		absval	|- ( A e. CC -> ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) ) )
2		cjmulval	|- ( A e. CC -> ( A x. ( * ` A ) ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
3	2	fveq2d	|- ( A e. CC -> ( sqrt ` ( A x. ( * ` A ) ) ) = ( sqrt ` ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) )
4	1 3	eqtrd	|- ( A e. CC -> ( abs ` A ) = ( sqrt ` ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) )