Metamath Proof Explorer


Theorem divsub1dir

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

Ref Expression
Assertion divsub1dir ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 / 𝐵 ) − 1 ) = ( ( 𝐴𝐵 ) / 𝐵 ) )

Proof

Step Hyp Ref Expression
1 3simpc ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
2 divid ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐵 / 𝐵 ) = 1 )
3 1 2 syl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐵 / 𝐵 ) = 1 )
4 3 eqcomd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → 1 = ( 𝐵 / 𝐵 ) )
5 4 oveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 / 𝐵 ) − 1 ) = ( ( 𝐴 / 𝐵 ) − ( 𝐵 / 𝐵 ) ) )
6 divsubdir ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴𝐵 ) / 𝐵 ) = ( ( 𝐴 / 𝐵 ) − ( 𝐵 / 𝐵 ) ) )
7 1 6 syld3an3 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝐴𝐵 ) / 𝐵 ) = ( ( 𝐴 / 𝐵 ) − ( 𝐵 / 𝐵 ) ) )
8 5 7 eqtr4d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 / 𝐵 ) − 1 ) = ( ( 𝐴𝐵 ) / 𝐵 ) )