Metamath Proof Explorer

Theorem recval

Description: Reciprocal expressed with a real denominator. (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion recval 
|- ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) = ( ( * ` A ) / ( ( abs ` A ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
2 1 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( * ` A ) e. CC )
3 simpl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> A e. CC )
4 2 3 mulcomd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( * ` A ) x. A ) = ( A x. ( * ` A ) ) )
5 absvalsq 
 |-  ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
6 5 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
7 4 6 eqtr4d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( * ` A ) x. A ) = ( ( abs ` A ) ^ 2 ) )
8 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
9 8 adantr 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR )
10 9 recnd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. CC )
11 10 sqcld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` A ) ^ 2 ) e. CC )
12 cjne0 
 |-  ( A e. CC -> ( A =/= 0 <-> ( * ` A ) =/= 0 ) )
13 12 biimpa 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( * ` A ) =/= 0 )
14 11 2 3 13 divmuld 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( ( ( abs ` A ) ^ 2 ) / ( * ` A ) ) = A <-> ( ( * ` A ) x. A ) = ( ( abs ` A ) ^ 2 ) ) )
15 7 14 mpbird 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( ( abs ` A ) ^ 2 ) / ( * ` A ) ) = A )
16 15 oveq2d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / ( ( ( abs ` A ) ^ 2 ) / ( * ` A ) ) ) = ( 1 / A ) )
17 abs00 
 |-  ( A e. CC -> ( ( abs ` A ) = 0 <-> A = 0 ) )
18 17 necon3bid 
 |-  ( A e. CC -> ( ( abs ` A ) =/= 0 <-> A =/= 0 ) )
19 18 biimpar 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) =/= 0 )
20 sqne0 
 |-  ( ( abs ` A ) e. CC -> ( ( ( abs ` A ) ^ 2 ) =/= 0 <-> ( abs ` A ) =/= 0 ) )
21 10 20 syl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( ( abs ` A ) ^ 2 ) =/= 0 <-> ( abs ` A ) =/= 0 ) )
22 19 21 mpbird 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( abs ` A ) ^ 2 ) =/= 0 )
23 11 2 22 13 recdivd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / ( ( ( abs ` A ) ^ 2 ) / ( * ` A ) ) ) = ( ( * ` A ) / ( ( abs ` A ) ^ 2 ) ) )
24 16 23 eqtr3d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) = ( ( * ` A ) / ( ( abs ` A ) ^ 2 ) ) )