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 ) ) )