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 
|- ( ( A e. CC /\ A =/= 0 ) -> ( ( ( * ` ( A / ( abs ` A ) ) ) x. A ) + ( ( A / ( abs ` A ) ) x. ( * ` A ) ) ) = ( 2 x. ( abs ` A ) ) )

Proof

Step Hyp Ref Expression
1 absvalsq 
 |-  ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
2 1 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
3 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
4 3 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR )
5 4 recnd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. CC )
6 5 sqvald 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` A ) ^ 2 ) = ( ( abs ` A ) x. ( abs ` A ) ) )
7 2 6 eqtr3d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( A x. ( * ` A ) ) = ( ( abs ` A ) x. ( abs ` A ) ) )
8 7 oveq1d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( A x. ( * ` A ) ) / ( abs ` A ) ) = ( ( ( abs ` A ) x. ( abs ` A ) ) / ( abs ` A ) ) )
9 simpl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> A e. CC )
10 9 cjcld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( * ` A ) e. CC )
11 abs00 
 |-  ( A e. CC -> ( ( abs ` A ) = 0 <-> A = 0 ) )
12 11 necon3bid 
 |-  ( A e. CC -> ( ( abs ` A ) =/= 0 <-> A =/= 0 ) )
13 12 biimpar 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) =/= 0 )
14 9 10 5 13 div23d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( A x. ( * ` A ) ) / ( abs ` A ) ) = ( ( A / ( abs ` A ) ) x. ( * ` A ) ) )
15 5 5 13 divcan3d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( ( abs ` A ) x. ( abs ` A ) ) / ( abs ` A ) ) = ( abs ` A ) )
16 8 14 15 3eqtr3d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( A / ( abs ` A ) ) x. ( * ` A ) ) = ( abs ` A ) )
17 16 fveq2d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( * ` ( ( A / ( abs ` A ) ) x. ( * ` A ) ) ) = ( * ` ( abs ` A ) ) )
18 9 5 13 divcld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( A / ( abs ` A ) ) e. CC )
19 18 10 cjmuld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( * ` ( ( A / ( abs ` A ) ) x. ( * ` A ) ) ) = ( ( * ` ( A / ( abs ` A ) ) ) x. ( * ` ( * ` A ) ) ) )
20 9 cjcjd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( * ` ( * ` A ) ) = A )
21 20 oveq2d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( * ` ( A / ( abs ` A ) ) ) x. ( * ` ( * ` A ) ) ) = ( ( * ` ( A / ( abs ` A ) ) ) x. A ) )
22 19 21 eqtrd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( * ` ( ( A / ( abs ` A ) ) x. ( * ` A ) ) ) = ( ( * ` ( A / ( abs ` A ) ) ) x. A ) )
23 4 cjred 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( * ` ( abs ` A ) ) = ( abs ` A ) )
24 17 22 23 3eqtr3d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( * ` ( A / ( abs ` A ) ) ) x. A ) = ( abs ` A ) )
25 24 16 oveq12d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( ( * ` ( A / ( abs ` A ) ) ) x. A ) + ( ( A / ( abs ` A ) ) x. ( * ` A ) ) ) = ( ( abs ` A ) + ( abs ` A ) ) )
26 5 2timesd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 2 x. ( abs ` A ) ) = ( ( abs ` A ) + ( abs ` A ) ) )
27 25 26 eqtr4d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( ( * ` ( A / ( abs ` A ) ) ) x. A ) + ( ( A / ( abs ` A ) ) x. ( * ` A ) ) ) = ( 2 x. ( abs ` A ) ) )