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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = ( √ ‘ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2		ax-icn	⊢ i ∈ ℂ
3		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
4		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · 𝐵 ) ∈ ℂ )
5	2 3 4	sylancr	⊢ ( 𝐵 ∈ ℝ → ( i · 𝐵 ) ∈ ℂ )
6		addcl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( i · 𝐵 ) ∈ ℂ ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ )
7	1 5 6	syl2an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ )
8		abscl	⊢ ( ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ → ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℝ )
9	7 8	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℝ )
10		absge0	⊢ ( ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ → 0 ≤ ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) )
11	7 10	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 0 ≤ ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) )
12		sqrtsq	⊢ ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) → ( √ ‘ ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) = ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) )
13	9 11 12	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( √ ‘ ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) = ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) )
14		absreimsq	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
15	14	fveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( √ ‘ ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) = ( √ ‘ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )
16	13 15	eqtr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = ( √ ‘ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )