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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recn | |
|
2 | ax-icn | |
|
3 | recn | |
|
4 | mulcl | |
|
5 | 2 3 4 | sylancr | |
6 | addcl | |
|
7 | 1 5 6 | syl2an | |
8 | abscl | |
|
9 | 7 8 | syl | |
10 | absge0 | |
|
11 | 7 10 | syl | |
12 | sqrtsq | |
|
13 | 9 11 12 | syl2anc | |
14 | absreimsq | |
|
15 | 14 | fveq2d | |
16 | 13 15 | eqtr3d | |