Description: Distribution of multiplication over subtraction. Theorem I.5 of Apostol p. 18. (Contributed by NM, 30-Dec-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | subdir | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subdi | |
|
2 | 1 | 3coml | |
3 | subcl | |
|
4 | mulcom | |
|
5 | 3 4 | stoic3 | |
6 | mulcom | |
|
7 | 6 | 3adant2 | |
8 | mulcom | |
|
9 | 8 | 3adant1 | |
10 | 7 9 | oveq12d | |
11 | 2 5 10 | 3eqtr4d | |