Step |
Hyp |
Ref |
Expression |
1 |
|
mulneg2 |
|- ( ( B e. CC /\ C e. CC ) -> ( B x. -u C ) = -u ( B x. C ) ) |
2 |
1
|
adantl |
|- ( ( A e. CC /\ ( B e. CC /\ C e. CC ) ) -> ( B x. -u C ) = -u ( B x. C ) ) |
3 |
2
|
oveq2d |
|- ( ( A e. CC /\ ( B e. CC /\ C e. CC ) ) -> ( A + ( B x. -u C ) ) = ( A + -u ( B x. C ) ) ) |
4 |
|
mulcl |
|- ( ( B e. CC /\ C e. CC ) -> ( B x. C ) e. CC ) |
5 |
|
negsub |
|- ( ( A e. CC /\ ( B x. C ) e. CC ) -> ( A + -u ( B x. C ) ) = ( A - ( B x. C ) ) ) |
6 |
4 5
|
sylan2 |
|- ( ( A e. CC /\ ( B e. CC /\ C e. CC ) ) -> ( A + -u ( B x. C ) ) = ( A - ( B x. C ) ) ) |
7 |
3 6
|
eqtr2d |
|- ( ( A e. CC /\ ( B e. CC /\ C e. CC ) ) -> ( A - ( B x. C ) ) = ( A + ( B x. -u C ) ) ) |
8 |
7
|
3impb |
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B x. C ) ) = ( A + ( B x. -u C ) ) ) |