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

Metamath Proof Explorer

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 )