Metamath Proof Explorer

Theorem divcan6

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

Ref Expression
Assertion divcan6 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A B ⁢ B A = 1

Proof

Step Hyp Ref Expression
1 recdiv ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → 1 A B = B A
2 1 oveq2d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A B ⁢ 1 A B = A B ⁢ B A
3 divcl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B ∈ ℂ
4 3 3expb ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B ∈ ℂ
5 4 adantlr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A B ∈ ℂ
6 divne0 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A B ≠ 0
7 recid ⊢ A B ∈ ℂ ∧ A B ≠ 0 → A B ⁢ 1 A B = 1
8 5 6 7 syl2anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A B ⁢ 1 A B = 1
9 2 8 eqtr3d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A B ⁢ B A = 1