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