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 ABA+iB=A2+B2

Proof

Step Hyp Ref Expression
1 recn AA
2 ax-icn i
3 recn BB
4 mulcl iBiB
5 2 3 4 sylancr BiB
6 addcl AiBA+iB
7 1 5 6 syl2an ABA+iB
8 abscl A+iBA+iB
9 7 8 syl ABA+iB
10 absge0 A+iB0A+iB
11 7 10 syl AB0A+iB
12 sqrtsq A+iB0A+iBA+iB2=A+iB
13 9 11 12 syl2anc ABA+iB2=A+iB
14 absreimsq ABA+iB2=A2+B2
15 14 fveq2d ABA+iB2=A2+B2
16 13 15 eqtr3d ABA+iB=A2+B2