Metamath Proof Explorer


Theorem recval

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

Ref Expression
Assertion recval ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) = ( ( ∗ ‘ 𝐴 ) / ( ( abs ‘ 𝐴 ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 cjcl ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ )
2 1 adantr ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
3 simpl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
4 2 3 mulcomd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ∗ ‘ 𝐴 ) · 𝐴 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
5 absvalsq ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
6 5 adantr ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
7 4 6 eqtr4d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ∗ ‘ 𝐴 ) · 𝐴 ) = ( ( abs ‘ 𝐴 ) ↑ 2 ) )
8 abscl ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
9 8 adantr ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
10 9 recnd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℂ )
11 10 sqcld ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
12 cjne0 ( 𝐴 ∈ ℂ → ( 𝐴 ≠ 0 ↔ ( ∗ ‘ 𝐴 ) ≠ 0 ) )
13 12 biimpa ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ 𝐴 ) ≠ 0 )
14 11 2 3 13 divmuld ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ( ( abs ‘ 𝐴 ) ↑ 2 ) / ( ∗ ‘ 𝐴 ) ) = 𝐴 ↔ ( ( ∗ ‘ 𝐴 ) · 𝐴 ) = ( ( abs ‘ 𝐴 ) ↑ 2 ) ) )
15 7 14 mpbird ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ( abs ‘ 𝐴 ) ↑ 2 ) / ( ∗ ‘ 𝐴 ) ) = 𝐴 )
16 15 oveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / ( ( ( abs ‘ 𝐴 ) ↑ 2 ) / ( ∗ ‘ 𝐴 ) ) ) = ( 1 / 𝐴 ) )
17 abs00 ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )
18 17 necon3bid ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )
19 18 biimpar ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ≠ 0 )
20 sqne0 ( ( abs ‘ 𝐴 ) ∈ ℂ → ( ( ( abs ‘ 𝐴 ) ↑ 2 ) ≠ 0 ↔ ( abs ‘ 𝐴 ) ≠ 0 ) )
21 10 20 syl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( ( abs ‘ 𝐴 ) ↑ 2 ) ≠ 0 ↔ ( abs ‘ 𝐴 ) ≠ 0 ) )
22 19 21 mpbird ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) ≠ 0 )
23 11 2 22 13 recdivd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / ( ( ( abs ‘ 𝐴 ) ↑ 2 ) / ( ∗ ‘ 𝐴 ) ) ) = ( ( ∗ ‘ 𝐴 ) / ( ( abs ‘ 𝐴 ) ↑ 2 ) ) )
24 16 23 eqtr3d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) = ( ( ∗ ‘ 𝐴 ) / ( ( abs ‘ 𝐴 ) ↑ 2 ) ) )