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

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