| Step |
Hyp |
Ref |
Expression |
| 1 |
|
recn |
|- ( B e. RR -> B e. CC ) |
| 2 |
|
recn |
|- ( C e. RR -> C e. CC ) |
| 3 |
|
mulcom |
|- ( ( B e. CC /\ C e. CC ) -> ( B x. C ) = ( C x. B ) ) |
| 4 |
1 2 3
|
syl2an |
|- ( ( B e. RR /\ C e. RR ) -> ( B x. C ) = ( C x. B ) ) |
| 5 |
4
|
3adant1 |
|- ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> ( B x. C ) = ( C x. B ) ) |
| 6 |
5
|
oveq2d |
|- ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> ( A ^c ( B x. C ) ) = ( A ^c ( C x. B ) ) ) |
| 7 |
|
cxpmul |
|- ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^c C ) ) |
| 8 |
2 7
|
syl3an3 |
|- ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^c C ) ) |
| 9 |
|
simp1 |
|- ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> A e. RR+ ) |
| 10 |
|
simp3 |
|- ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> C e. RR ) |
| 11 |
1
|
3ad2ant2 |
|- ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> B e. CC ) |
| 12 |
9 10 11
|
cxpmuld |
|- ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> ( A ^c ( C x. B ) ) = ( ( A ^c C ) ^c B ) ) |
| 13 |
6 8 12
|
3eqtr3d |
|- ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> ( ( A ^c B ) ^c C ) = ( ( A ^c C ) ^c B ) ) |