Step |
Hyp |
Ref |
Expression |
1 |
|
exp0 |
|- ( B e. CC -> ( B ^ 0 ) = 1 ) |
2 |
1
|
eqcomd |
|- ( B e. CC -> 1 = ( B ^ 0 ) ) |
3 |
|
prodeq1 |
|- ( A = (/) -> prod_ k e. A B = prod_ k e. (/) B ) |
4 |
|
prod0 |
|- prod_ k e. (/) B = 1 |
5 |
3 4
|
eqtrdi |
|- ( A = (/) -> prod_ k e. A B = 1 ) |
6 |
|
fveq2 |
|- ( A = (/) -> ( # ` A ) = ( # ` (/) ) ) |
7 |
|
hash0 |
|- ( # ` (/) ) = 0 |
8 |
6 7
|
eqtrdi |
|- ( A = (/) -> ( # ` A ) = 0 ) |
9 |
8
|
oveq2d |
|- ( A = (/) -> ( B ^ ( # ` A ) ) = ( B ^ 0 ) ) |
10 |
5 9
|
eqeq12d |
|- ( A = (/) -> ( prod_ k e. A B = ( B ^ ( # ` A ) ) <-> 1 = ( B ^ 0 ) ) ) |
11 |
2 10
|
syl5ibrcom |
|- ( B e. CC -> ( A = (/) -> prod_ k e. A B = ( B ^ ( # ` A ) ) ) ) |
12 |
11
|
adantl |
|- ( ( A e. Fin /\ B e. CC ) -> ( A = (/) -> prod_ k e. A B = ( B ^ ( # ` A ) ) ) ) |
13 |
|
eqidd |
|- ( k = ( f ` n ) -> B = B ) |
14 |
|
simprl |
|- ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. NN ) |
15 |
|
simprr |
|- ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) |
16 |
|
simpllr |
|- ( ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ k e. A ) -> B e. CC ) |
17 |
|
simpllr |
|- ( ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> B e. CC ) |
18 |
|
elfznn |
|- ( n e. ( 1 ... ( # ` A ) ) -> n e. NN ) |
19 |
18
|
adantl |
|- ( ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> n e. NN ) |
20 |
|
fvconst2g |
|- ( ( B e. CC /\ n e. NN ) -> ( ( NN X. { B } ) ` n ) = B ) |
21 |
17 19 20
|
syl2anc |
|- ( ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( NN X. { B } ) ` n ) = B ) |
22 |
13 14 15 16 21
|
fprod |
|- ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ k e. A B = ( seq 1 ( x. , ( NN X. { B } ) ) ` ( # ` A ) ) ) |
23 |
|
expnnval |
|- ( ( B e. CC /\ ( # ` A ) e. NN ) -> ( B ^ ( # ` A ) ) = ( seq 1 ( x. , ( NN X. { B } ) ) ` ( # ` A ) ) ) |
24 |
23
|
ad2ant2lr |
|- ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( B ^ ( # ` A ) ) = ( seq 1 ( x. , ( NN X. { B } ) ) ` ( # ` A ) ) ) |
25 |
22 24
|
eqtr4d |
|- ( ( ( A e. Fin /\ B e. CC ) /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ k e. A B = ( B ^ ( # ` A ) ) ) |
26 |
25
|
expr |
|- ( ( ( A e. Fin /\ B e. CC ) /\ ( # ` A ) e. NN ) -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> prod_ k e. A B = ( B ^ ( # ` A ) ) ) ) |
27 |
26
|
exlimdv |
|- ( ( ( A e. Fin /\ B e. CC ) /\ ( # ` A ) e. NN ) -> ( E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> prod_ k e. A B = ( B ^ ( # ` A ) ) ) ) |
28 |
27
|
expimpd |
|- ( ( A e. Fin /\ B e. CC ) -> ( ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> prod_ k e. A B = ( B ^ ( # ` A ) ) ) ) |
29 |
|
fz1f1o |
|- ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) ) |
30 |
29
|
adantr |
|- ( ( A e. Fin /\ B e. CC ) -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) ) |
31 |
12 28 30
|
mpjaod |
|- ( ( A e. Fin /\ B e. CC ) -> prod_ k e. A B = ( B ^ ( # ` A ) ) ) |