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	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left|A+\mathrm{i}B\right|=\sqrt{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		abscl	$$⊢A+\mathrm{i}B\in ℂ\to \left|A+\mathrm{i}B\right|\in ℝ$$
9	7 8	syl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left|A+\mathrm{i}B\right|\in ℝ$$
10		absge0	$$⊢A+\mathrm{i}B\in ℂ\to 0\le \left|A+\mathrm{i}B\right|$$
11	7 10	syl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to 0\le \left|A+\mathrm{i}B\right|$$
12		sqrtsq	$$⊢\left(\left|A+\mathrm{i}B\right|\in ℝ\wedge 0\le \left|A+\mathrm{i}B\right|\right)\to \sqrt{{\left|A+\mathrm{i}B\right|}^2}=\left|A+\mathrm{i}B\right|$$
13	9 11 12	syl2anc	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \sqrt{{\left|A+\mathrm{i}B\right|}^2}=\left|A+\mathrm{i}B\right|$$
14		absreimsq	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to {\left|A+\mathrm{i}B\right|}^2=A^2+B^2$$
15	14	fveq2d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \sqrt{{\left|A+\mathrm{i}B\right|}^2}=\sqrt{A^2+B^2}$$
16	13 15	eqtr3d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left|A+\mathrm{i}B\right|=\sqrt{A^2+B^2}$$