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