| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mulcxp.1 |
|- ( ph -> A e. CC ) |
| 2 |
|
mulcxp.2 |
|- ( ph -> C e. CC ) |
| 3 |
|
oveq2 |
|- ( C = 0 -> ( 0 ^c C ) = ( 0 ^c 0 ) ) |
| 4 |
|
0cn |
|- 0 e. CC |
| 5 |
|
cxp0 |
|- ( 0 e. CC -> ( 0 ^c 0 ) = 1 ) |
| 6 |
4 5
|
ax-mp |
|- ( 0 ^c 0 ) = 1 |
| 7 |
3 6
|
eqtrdi |
|- ( C = 0 -> ( 0 ^c C ) = 1 ) |
| 8 |
|
oveq2 |
|- ( C = 0 -> ( A ^c C ) = ( A ^c 0 ) ) |
| 9 |
8 7
|
oveq12d |
|- ( C = 0 -> ( ( A ^c C ) x. ( 0 ^c C ) ) = ( ( A ^c 0 ) x. 1 ) ) |
| 10 |
7 9
|
eqeq12d |
|- ( C = 0 -> ( ( 0 ^c C ) = ( ( A ^c C ) x. ( 0 ^c C ) ) <-> 1 = ( ( A ^c 0 ) x. 1 ) ) ) |
| 11 |
|
cxpcl |
|- ( ( A e. CC /\ C e. CC ) -> ( A ^c C ) e. CC ) |
| 12 |
1 2 11
|
syl2anc |
|- ( ph -> ( A ^c C ) e. CC ) |
| 13 |
12
|
adantr |
|- ( ( ph /\ C =/= 0 ) -> ( A ^c C ) e. CC ) |
| 14 |
13
|
mul01d |
|- ( ( ph /\ C =/= 0 ) -> ( ( A ^c C ) x. 0 ) = 0 ) |
| 15 |
|
0cxp |
|- ( ( C e. CC /\ C =/= 0 ) -> ( 0 ^c C ) = 0 ) |
| 16 |
2 15
|
sylan |
|- ( ( ph /\ C =/= 0 ) -> ( 0 ^c C ) = 0 ) |
| 17 |
16
|
oveq2d |
|- ( ( ph /\ C =/= 0 ) -> ( ( A ^c C ) x. ( 0 ^c C ) ) = ( ( A ^c C ) x. 0 ) ) |
| 18 |
14 17 16
|
3eqtr4rd |
|- ( ( ph /\ C =/= 0 ) -> ( 0 ^c C ) = ( ( A ^c C ) x. ( 0 ^c C ) ) ) |
| 19 |
|
cxp0 |
|- ( A e. CC -> ( A ^c 0 ) = 1 ) |
| 20 |
1 19
|
syl |
|- ( ph -> ( A ^c 0 ) = 1 ) |
| 21 |
20
|
oveq1d |
|- ( ph -> ( ( A ^c 0 ) x. 1 ) = ( 1 x. 1 ) ) |
| 22 |
|
1t1e1 |
|- ( 1 x. 1 ) = 1 |
| 23 |
21 22
|
eqtr2di |
|- ( ph -> 1 = ( ( A ^c 0 ) x. 1 ) ) |
| 24 |
10 18 23
|
pm2.61ne |
|- ( ph -> ( 0 ^c C ) = ( ( A ^c C ) x. ( 0 ^c C ) ) ) |