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

Metamath Proof Explorer

Theorem abslem2

Description: Lemma involving absolute values. (Contributed by NM, 11-Oct-1999) (Revised by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion abslem2 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ( ∗ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) · 𝐴 ) + ( ( 𝐴 / ( abs ‘ 𝐴 ) ) · ( ∗ ‘ 𝐴 ) ) ) = ( 2 · ( abs ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 absvalsq ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
2 1 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
3 abscl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
4 3 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
5 4 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℂ )
6 5 sqvald ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐴 ) ) )
7 2 6 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) = ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐴 ) ) )
8 7 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) / ( abs ‘ 𝐴 ) ) = ( ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐴 ) ) / ( abs ‘ 𝐴 ) ) )
9 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
10 9 cjcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
11 abs00 ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )
12 11 necon3bid ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )
13 12 biimpar ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ≠ 0 )
14 9 10 5 13 div23d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) / ( abs ‘ 𝐴 ) ) = ( ( 𝐴 / ( abs ‘ 𝐴 ) ) · ( ∗ ‘ 𝐴 ) ) )
15 5 5 13 divcan3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ( abs ‘ 𝐴 ) · ( abs ‘ 𝐴 ) ) / ( abs ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
16 8 14 15 3eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 / ( abs ‘ 𝐴 ) ) · ( ∗ ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
17 16 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ ( ( 𝐴 / ( abs ‘ 𝐴 ) ) · ( ∗ ‘ 𝐴 ) ) ) = ( ∗ ‘ ( abs ‘ 𝐴 ) ) )
18 9 5 13 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴 / ( abs ‘ 𝐴 ) ) ∈ ℂ )
19 18 10 cjmuld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ ( ( 𝐴 / ( abs ‘ 𝐴 ) ) · ( ∗ ‘ 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) · ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) ) )
20 9 cjcjd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) = 𝐴 )
21 20 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ∗ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) · ( ∗ ‘ ( ∗ ‘ 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) · 𝐴 ) )
22 19 21 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ ( ( 𝐴 / ( abs ‘ 𝐴 ) ) · ( ∗ ‘ 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) · 𝐴 ) )
23 4 cjred ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ ( abs ‘ 𝐴 ) ) = ( abs ‘ 𝐴 ) )
24 17 22 23 3eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ∗ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) · 𝐴 ) = ( abs ‘ 𝐴 ) )
25 24 16 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ( ∗ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) · 𝐴 ) + ( ( 𝐴 / ( abs ‘ 𝐴 ) ) · ( ∗ ‘ 𝐴 ) ) ) = ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐴 ) ) )
26 5 2timesd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 2 · ( abs ‘ 𝐴 ) ) = ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐴 ) ) )
27 25 26 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ( ∗ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) · 𝐴 ) + ( ( 𝐴 / ( abs ‘ 𝐴 ) ) · ( ∗ ‘ 𝐴 ) ) ) = ( 2 · ( abs ‘ 𝐴 ) ) )