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 ) ) ) )