Theorem divcan6

Description: Cancellation of inverted fractions. (Contributed by NM, 28-Dec-2007)

	Ref	Expression
Assertion	divcan6	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 / 𝐵 ) · ( 𝐵 / 𝐴 ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		recdiv	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 1 / ( 𝐴 / 𝐵 ) ) = ( 𝐵 / 𝐴 ) )
2	1	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 / 𝐵 ) · ( 1 / ( 𝐴 / 𝐵 ) ) ) = ( ( 𝐴 / 𝐵 ) · ( 𝐵 / 𝐴 ) ) )
3		divcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℂ )
4	3	3expb	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) ∈ ℂ )
5	4	adantlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) ∈ ℂ )
6		divne0	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) ≠ 0 )
7		recid	⊢ ( ( ( 𝐴 / 𝐵 ) ∈ ℂ ∧ ( 𝐴 / 𝐵 ) ≠ 0 ) → ( ( 𝐴 / 𝐵 ) · ( 1 / ( 𝐴 / 𝐵 ) ) ) = 1 )
8	5 6 7	syl2anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 / 𝐵 ) · ( 1 / ( 𝐴 / 𝐵 ) ) ) = 1 )
9	2 8	eqtr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 / 𝐵 ) · ( 𝐵 / 𝐴 ) ) = 1 )