Metamath Proof Explorer


Theorem absreim

Description: Absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 14-Jan-2006)

Ref Expression
Assertion absreim
|- ( ( A e. RR /\ B e. RR ) -> ( abs ` ( A + ( _i x. B ) ) ) = ( sqrt ` ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )

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 abscl
 |-  ( ( A + ( _i x. B ) ) e. CC -> ( abs ` ( A + ( _i x. B ) ) ) e. RR )
9 7 8 syl
 |-  ( ( A e. RR /\ B e. RR ) -> ( abs ` ( A + ( _i x. B ) ) ) e. RR )
10 absge0
 |-  ( ( A + ( _i x. B ) ) e. CC -> 0 <_ ( abs ` ( A + ( _i x. B ) ) ) )
11 7 10 syl
 |-  ( ( A e. RR /\ B e. RR ) -> 0 <_ ( abs ` ( A + ( _i x. B ) ) ) )
12 sqrtsq
 |-  ( ( ( abs ` ( A + ( _i x. B ) ) ) e. RR /\ 0 <_ ( abs ` ( A + ( _i x. B ) ) ) ) -> ( sqrt ` ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) ) = ( abs ` ( A + ( _i x. B ) ) ) )
13 9 11 12 syl2anc
 |-  ( ( A e. RR /\ B e. RR ) -> ( sqrt ` ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) ) = ( abs ` ( A + ( _i x. B ) ) ) )
14 absreimsq
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
15 14 fveq2d
 |-  ( ( A e. RR /\ B e. RR ) -> ( sqrt ` ( ( abs ` ( A + ( _i x. B ) ) ) ^ 2 ) ) = ( sqrt ` ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
16 13 15 eqtr3d
 |-  ( ( A e. RR /\ B e. RR ) -> ( abs ` ( A + ( _i x. B ) ) ) = ( sqrt ` ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )