Theorem divsub1dir

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

	Ref	Expression
Assertion	divsub1dir	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left(\frac{A}{B}\right)-1=\frac{A-B}{B}$$

Proof

Step	Hyp	Ref	Expression
1		3simpc	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left(B\in ℂ\wedge B\ne 0\right)$$
2		divid	$$⊢\left(B\in ℂ\wedge B\ne 0\right)\to \frac{B}{B}=1$$
3	1 2	syl	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \frac{B}{B}=1$$
4	3	eqcomd	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to 1=\frac{B}{B}$$
5	4	oveq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left(\frac{A}{B}\right)-1=\left(\frac{A}{B}\right)-\left(\frac{B}{B}\right)$$
6		divsubdir	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge \left(B\in ℂ\wedge B\ne 0\right)\right)\to \frac{A-B}{B}=\left(\frac{A}{B}\right)-\left(\frac{B}{B}\right)$$
7	1 6	syld3an3	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \frac{A-B}{B}=\left(\frac{A}{B}\right)-\left(\frac{B}{B}\right)$$
8	5 7	eqtr4d	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left(\frac{A}{B}\right)-1=\frac{A-B}{B}$$