This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + i ⁢ B = A 2 + B 2

Proof

Step Hyp Ref Expression
1 recn ⊢ A ∈ ℝ → A ∈ ℂ
2 ax-icn ⊢ i ∈ ℂ
3 recn ⊢ B ∈ ℝ → B ∈ ℂ
4 mulcl ⊢ i ∈ ℂ ∧ B ∈ ℂ → i ⁢ B ∈ ℂ
5 2 3 4 sylancr ⊢ B ∈ ℝ → i ⁢ B ∈ ℂ
6 addcl ⊢ A ∈ ℂ ∧ i ⁢ B ∈ ℂ → A + i ⁢ B ∈ ℂ
7 1 5 6 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + i ⁢ B ∈ ℂ
8 abscl ⊢ A + i ⁢ B ∈ ℂ → A + i ⁢ B ∈ ℝ
9 7 8 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + i ⁢ B ∈ ℝ
10 absge0 ⊢ A + i ⁢ B ∈ ℂ → 0 ≤ A + i ⁢ B
11 7 10 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ A + i ⁢ B
12 sqrtsq ⊢ A + i ⁢ B ∈ ℝ ∧ 0 ≤ A + i ⁢ B → A + i ⁢ B 2 = A + i ⁢ B
13 9 11 12 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + i ⁢ B 2 = A + i ⁢ B
14 absreimsq ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + i ⁢ B 2 = A 2 + B 2
15 14 fveq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + i ⁢ B 2 = A 2 + B 2
16 13 15 eqtr3d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + i ⁢ B = A 2 + B 2