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