Description: Expand the square of a subtraction. (Contributed by Scott Fenton, 13-Jun-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | binom2subi.1 | โข ๐ด โ โ | |
binom2subi.2 | โข ๐ต โ โ | ||
Assertion | binom2subi | โข ( ( ๐ด โ ๐ต ) โ 2 ) = ( ( ( ๐ด โ 2 ) โ ( 2 ยท ( ๐ด ยท ๐ต ) ) ) + ( ๐ต โ 2 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | binom2subi.1 | โข ๐ด โ โ | |
2 | binom2subi.2 | โข ๐ต โ โ | |
3 | binom2sub | โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ( ๐ด โ ๐ต ) โ 2 ) = ( ( ( ๐ด โ 2 ) โ ( 2 ยท ( ๐ด ยท ๐ต ) ) ) + ( ๐ต โ 2 ) ) ) | |
4 | 1 2 3 | mp2an | โข ( ( ๐ด โ ๐ต ) โ 2 ) = ( ( ( ๐ด โ 2 ) โ ( 2 ยท ( ๐ด ยท ๐ต ) ) ) + ( ๐ต โ 2 ) ) |