Metamath Proof Explorer

Theorem divsub1dir

Description: Distribution of division over subtraction by 1. (Contributed by AV, 6-Jun-2020)

Ref Expression
Assertion divsub1dir ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B − 1 = A − B B

Proof

Step Hyp Ref Expression
1 3simpc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ∈ ℂ ∧ B ≠ 0
2 divid ⊢ B ∈ ℂ ∧ B ≠ 0 → B B = 1
3 1 2 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B B = 1
4 3 eqcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → 1 = B B
5 4 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B − 1 = A B − B B
6 divsubdir ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A − B B = A B − B B
7 1 6 syld3an3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A − B B = A B − B B
8 5 7 eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B − 1 = A − B B