Theorem absreimsq

Description: Square of the absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 1-Feb-2007)

	Ref	Expression
Assertion	absreimsq	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to {\left|A+\mathrm{i}B\right|}^2=A^2+B^2$$

Proof

Step	Hyp	Ref	Expression
1		recn	$$⊢A\in ℝ\to A\in ℂ$$
2		ax-icn	$$⊢\mathrm{i}\in ℂ$$
3		recn	$$⊢B\in ℝ\to B\in ℂ$$
4		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge B\in ℂ\right)\to \mathrm{i}B\in ℂ$$
5	2 3 4	sylancr	$$⊢B\in ℝ\to \mathrm{i}B\in ℂ$$
6		addcl	$$⊢\left(A\in ℂ\wedge \mathrm{i}B\in ℂ\right)\to A+\mathrm{i}B\in ℂ$$
7	1 5 6	syl2an	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A+\mathrm{i}B\in ℂ$$
8		absvalsq2	$$⊢A+\mathrm{i}B\in ℂ\to {\left|A+\mathrm{i}B\right|}^2={\Re \left(A+\mathrm{i}B\right)}^2+{\Im \left(A+\mathrm{i}B\right)}^2$$
9	7 8	syl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to {\left|A+\mathrm{i}B\right|}^2={\Re \left(A+\mathrm{i}B\right)}^2+{\Im \left(A+\mathrm{i}B\right)}^2$$
10		crre	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \Re \left(A+\mathrm{i}B\right)=A$$
11	10	oveq1d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to {\Re \left(A+\mathrm{i}B\right)}^2=A^2$$
12		crim	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \Im \left(A+\mathrm{i}B\right)=B$$
13	12	oveq1d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to {\Im \left(A+\mathrm{i}B\right)}^2=B^2$$
14	11 13	oveq12d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to {\Re \left(A+\mathrm{i}B\right)}^2+{\Im \left(A+\mathrm{i}B\right)}^2=A^2+B^2$$
15	9 14	eqtrd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to {\left|A+\mathrm{i}B\right|}^2=A^2+B^2$$