Theorem divsub1dir

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

	Ref	Expression
Assertion	divsub1dir	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) - 1 ) = ( ( A - B ) / B ) )

Proof

Step	Hyp	Ref	Expression
1		3simpc	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B e. CC /\ B =/= 0 ) )
2		divid	|- ( ( B e. CC /\ B =/= 0 ) -> ( B / B ) = 1 )
3	1 2	syl	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B / B ) = 1 )
4	3	eqcomd	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> 1 = ( B / B ) )
5	4	oveq2d	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) - 1 ) = ( ( A / B ) - ( B / B ) ) )
6		divsubdir	|- ( ( A e. CC /\ B e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A - B ) / B ) = ( ( A / B ) - ( B / B ) ) )
7	1 6	syld3an3	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A - B ) / B ) = ( ( A / B ) - ( B / B ) ) )
8	5 7	eqtr4d	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) - 1 ) = ( ( A - B ) / B ) )