Step |
Hyp |
Ref |
Expression |
1 |
|
fprodmul.1 |
|- ( ph -> A e. Fin ) |
2 |
|
fprodmul.2 |
|- ( ( ph /\ k e. A ) -> B e. CC ) |
3 |
|
fprodmul.3 |
|- ( ( ph /\ k e. A ) -> C e. CC ) |
4 |
|
fproddiv.4 |
|- ( ( ph /\ k e. A ) -> C =/= 0 ) |
5 |
|
1div1e1 |
|- ( 1 / 1 ) = 1 |
6 |
5
|
eqcomi |
|- 1 = ( 1 / 1 ) |
7 |
|
prodeq1 |
|- ( A = (/) -> prod_ k e. A ( B / C ) = prod_ k e. (/) ( B / C ) ) |
8 |
|
prod0 |
|- prod_ k e. (/) ( B / C ) = 1 |
9 |
7 8
|
eqtrdi |
|- ( A = (/) -> prod_ k e. A ( B / C ) = 1 ) |
10 |
|
prodeq1 |
|- ( A = (/) -> prod_ k e. A B = prod_ k e. (/) B ) |
11 |
|
prod0 |
|- prod_ k e. (/) B = 1 |
12 |
10 11
|
eqtrdi |
|- ( A = (/) -> prod_ k e. A B = 1 ) |
13 |
|
prodeq1 |
|- ( A = (/) -> prod_ k e. A C = prod_ k e. (/) C ) |
14 |
|
prod0 |
|- prod_ k e. (/) C = 1 |
15 |
13 14
|
eqtrdi |
|- ( A = (/) -> prod_ k e. A C = 1 ) |
16 |
12 15
|
oveq12d |
|- ( A = (/) -> ( prod_ k e. A B / prod_ k e. A C ) = ( 1 / 1 ) ) |
17 |
6 9 16
|
3eqtr4a |
|- ( A = (/) -> prod_ k e. A ( B / C ) = ( prod_ k e. A B / prod_ k e. A C ) ) |
18 |
17
|
a1i |
|- ( ph -> ( A = (/) -> prod_ k e. A ( B / C ) = ( prod_ k e. A B / prod_ k e. A C ) ) ) |
19 |
|
simprl |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. NN ) |
20 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
21 |
19 20
|
eleqtrdi |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. ( ZZ>= ` 1 ) ) |
22 |
2
|
fmpttd |
|- ( ph -> ( k e. A |-> B ) : A --> CC ) |
23 |
|
f1of |
|- ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : ( 1 ... ( # ` A ) ) --> A ) |
24 |
23
|
adantl |
|- ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> f : ( 1 ... ( # ` A ) ) --> A ) |
25 |
|
fco |
|- ( ( ( k e. A |-> B ) : A --> CC /\ f : ( 1 ... ( # ` A ) ) --> A ) -> ( ( k e. A |-> B ) o. f ) : ( 1 ... ( # ` A ) ) --> CC ) |
26 |
22 24 25
|
syl2an |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( k e. A |-> B ) o. f ) : ( 1 ... ( # ` A ) ) --> CC ) |
27 |
26
|
ffvelrnda |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` n ) e. CC ) |
28 |
3
|
fmpttd |
|- ( ph -> ( k e. A |-> C ) : A --> CC ) |
29 |
|
fco |
|- ( ( ( k e. A |-> C ) : A --> CC /\ f : ( 1 ... ( # ` A ) ) --> A ) -> ( ( k e. A |-> C ) o. f ) : ( 1 ... ( # ` A ) ) --> CC ) |
30 |
28 24 29
|
syl2an |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( k e. A |-> C ) o. f ) : ( 1 ... ( # ` A ) ) --> CC ) |
31 |
30
|
ffvelrnda |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> C ) o. f ) ` n ) e. CC ) |
32 |
|
simprr |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) |
33 |
32 23
|
syl |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) --> A ) |
34 |
|
fvco3 |
|- ( ( f : ( 1 ... ( # ` A ) ) --> A /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> C ) o. f ) ` n ) = ( ( k e. A |-> C ) ` ( f ` n ) ) ) |
35 |
33 34
|
sylan |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> C ) o. f ) ` n ) = ( ( k e. A |-> C ) ` ( f ` n ) ) ) |
36 |
33
|
ffvelrnda |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( f ` n ) e. A ) |
37 |
|
simpr |
|- ( ( ph /\ k e. A ) -> k e. A ) |
38 |
|
eqid |
|- ( k e. A |-> C ) = ( k e. A |-> C ) |
39 |
38
|
fvmpt2 |
|- ( ( k e. A /\ C e. CC ) -> ( ( k e. A |-> C ) ` k ) = C ) |
40 |
37 3 39
|
syl2anc |
|- ( ( ph /\ k e. A ) -> ( ( k e. A |-> C ) ` k ) = C ) |
41 |
40 4
|
eqnetrd |
|- ( ( ph /\ k e. A ) -> ( ( k e. A |-> C ) ` k ) =/= 0 ) |
42 |
41
|
ralrimiva |
|- ( ph -> A. k e. A ( ( k e. A |-> C ) ` k ) =/= 0 ) |
43 |
42
|
ad2antrr |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> A. k e. A ( ( k e. A |-> C ) ` k ) =/= 0 ) |
44 |
|
nffvmpt1 |
|- F/_ k ( ( k e. A |-> C ) ` ( f ` n ) ) |
45 |
|
nfcv |
|- F/_ k 0 |
46 |
44 45
|
nfne |
|- F/ k ( ( k e. A |-> C ) ` ( f ` n ) ) =/= 0 |
47 |
|
fveq2 |
|- ( k = ( f ` n ) -> ( ( k e. A |-> C ) ` k ) = ( ( k e. A |-> C ) ` ( f ` n ) ) ) |
48 |
47
|
neeq1d |
|- ( k = ( f ` n ) -> ( ( ( k e. A |-> C ) ` k ) =/= 0 <-> ( ( k e. A |-> C ) ` ( f ` n ) ) =/= 0 ) ) |
49 |
46 48
|
rspc |
|- ( ( f ` n ) e. A -> ( A. k e. A ( ( k e. A |-> C ) ` k ) =/= 0 -> ( ( k e. A |-> C ) ` ( f ` n ) ) =/= 0 ) ) |
50 |
36 43 49
|
sylc |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( k e. A |-> C ) ` ( f ` n ) ) =/= 0 ) |
51 |
35 50
|
eqnetrd |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> C ) o. f ) ` n ) =/= 0 ) |
52 |
2 3 4
|
divcld |
|- ( ( ph /\ k e. A ) -> ( B / C ) e. CC ) |
53 |
|
eqid |
|- ( k e. A |-> ( B / C ) ) = ( k e. A |-> ( B / C ) ) |
54 |
53
|
fvmpt2 |
|- ( ( k e. A /\ ( B / C ) e. CC ) -> ( ( k e. A |-> ( B / C ) ) ` k ) = ( B / C ) ) |
55 |
37 52 54
|
syl2anc |
|- ( ( ph /\ k e. A ) -> ( ( k e. A |-> ( B / C ) ) ` k ) = ( B / C ) ) |
56 |
|
eqid |
|- ( k e. A |-> B ) = ( k e. A |-> B ) |
57 |
56
|
fvmpt2 |
|- ( ( k e. A /\ B e. CC ) -> ( ( k e. A |-> B ) ` k ) = B ) |
58 |
37 2 57
|
syl2anc |
|- ( ( ph /\ k e. A ) -> ( ( k e. A |-> B ) ` k ) = B ) |
59 |
58 40
|
oveq12d |
|- ( ( ph /\ k e. A ) -> ( ( ( k e. A |-> B ) ` k ) / ( ( k e. A |-> C ) ` k ) ) = ( B / C ) ) |
60 |
55 59
|
eqtr4d |
|- ( ( ph /\ k e. A ) -> ( ( k e. A |-> ( B / C ) ) ` k ) = ( ( ( k e. A |-> B ) ` k ) / ( ( k e. A |-> C ) ` k ) ) ) |
61 |
60
|
ralrimiva |
|- ( ph -> A. k e. A ( ( k e. A |-> ( B / C ) ) ` k ) = ( ( ( k e. A |-> B ) ` k ) / ( ( k e. A |-> C ) ` k ) ) ) |
62 |
61
|
ad2antrr |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> A. k e. A ( ( k e. A |-> ( B / C ) ) ` k ) = ( ( ( k e. A |-> B ) ` k ) / ( ( k e. A |-> C ) ` k ) ) ) |
63 |
|
nffvmpt1 |
|- F/_ k ( ( k e. A |-> ( B / C ) ) ` ( f ` n ) ) |
64 |
|
nffvmpt1 |
|- F/_ k ( ( k e. A |-> B ) ` ( f ` n ) ) |
65 |
|
nfcv |
|- F/_ k / |
66 |
64 65 44
|
nfov |
|- F/_ k ( ( ( k e. A |-> B ) ` ( f ` n ) ) / ( ( k e. A |-> C ) ` ( f ` n ) ) ) |
67 |
63 66
|
nfeq |
|- F/ k ( ( k e. A |-> ( B / C ) ) ` ( f ` n ) ) = ( ( ( k e. A |-> B ) ` ( f ` n ) ) / ( ( k e. A |-> C ) ` ( f ` n ) ) ) |
68 |
|
fveq2 |
|- ( k = ( f ` n ) -> ( ( k e. A |-> ( B / C ) ) ` k ) = ( ( k e. A |-> ( B / C ) ) ` ( f ` n ) ) ) |
69 |
|
fveq2 |
|- ( k = ( f ` n ) -> ( ( k e. A |-> B ) ` k ) = ( ( k e. A |-> B ) ` ( f ` n ) ) ) |
70 |
69 47
|
oveq12d |
|- ( k = ( f ` n ) -> ( ( ( k e. A |-> B ) ` k ) / ( ( k e. A |-> C ) ` k ) ) = ( ( ( k e. A |-> B ) ` ( f ` n ) ) / ( ( k e. A |-> C ) ` ( f ` n ) ) ) ) |
71 |
68 70
|
eqeq12d |
|- ( k = ( f ` n ) -> ( ( ( k e. A |-> ( B / C ) ) ` k ) = ( ( ( k e. A |-> B ) ` k ) / ( ( k e. A |-> C ) ` k ) ) <-> ( ( k e. A |-> ( B / C ) ) ` ( f ` n ) ) = ( ( ( k e. A |-> B ) ` ( f ` n ) ) / ( ( k e. A |-> C ) ` ( f ` n ) ) ) ) ) |
72 |
67 71
|
rspc |
|- ( ( f ` n ) e. A -> ( A. k e. A ( ( k e. A |-> ( B / C ) ) ` k ) = ( ( ( k e. A |-> B ) ` k ) / ( ( k e. A |-> C ) ` k ) ) -> ( ( k e. A |-> ( B / C ) ) ` ( f ` n ) ) = ( ( ( k e. A |-> B ) ` ( f ` n ) ) / ( ( k e. A |-> C ) ` ( f ` n ) ) ) ) ) |
73 |
36 62 72
|
sylc |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( k e. A |-> ( B / C ) ) ` ( f ` n ) ) = ( ( ( k e. A |-> B ) ` ( f ` n ) ) / ( ( k e. A |-> C ) ` ( f ` n ) ) ) ) |
74 |
|
fvco3 |
|- ( ( f : ( 1 ... ( # ` A ) ) --> A /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> ( B / C ) ) o. f ) ` n ) = ( ( k e. A |-> ( B / C ) ) ` ( f ` n ) ) ) |
75 |
33 74
|
sylan |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> ( B / C ) ) o. f ) ` n ) = ( ( k e. A |-> ( B / C ) ) ` ( f ` n ) ) ) |
76 |
|
fvco3 |
|- ( ( f : ( 1 ... ( # ` A ) ) --> A /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` n ) = ( ( k e. A |-> B ) ` ( f ` n ) ) ) |
77 |
33 76
|
sylan |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` n ) = ( ( k e. A |-> B ) ` ( f ` n ) ) ) |
78 |
77 35
|
oveq12d |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( ( k e. A |-> B ) o. f ) ` n ) / ( ( ( k e. A |-> C ) o. f ) ` n ) ) = ( ( ( k e. A |-> B ) ` ( f ` n ) ) / ( ( k e. A |-> C ) ` ( f ` n ) ) ) ) |
79 |
73 75 78
|
3eqtr4d |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> ( B / C ) ) o. f ) ` n ) = ( ( ( ( k e. A |-> B ) o. f ) ` n ) / ( ( ( k e. A |-> C ) o. f ) ` n ) ) ) |
80 |
21 27 31 51 79
|
prodfdiv |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( seq 1 ( x. , ( ( k e. A |-> ( B / C ) ) o. f ) ) ` ( # ` A ) ) = ( ( seq 1 ( x. , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) / ( seq 1 ( x. , ( ( k e. A |-> C ) o. f ) ) ` ( # ` A ) ) ) ) |
81 |
|
fveq2 |
|- ( m = ( f ` n ) -> ( ( k e. A |-> ( B / C ) ) ` m ) = ( ( k e. A |-> ( B / C ) ) ` ( f ` n ) ) ) |
82 |
52
|
fmpttd |
|- ( ph -> ( k e. A |-> ( B / C ) ) : A --> CC ) |
83 |
82
|
adantr |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( k e. A |-> ( B / C ) ) : A --> CC ) |
84 |
83
|
ffvelrnda |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. A ) -> ( ( k e. A |-> ( B / C ) ) ` m ) e. CC ) |
85 |
81 19 32 84 75
|
fprod |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ m e. A ( ( k e. A |-> ( B / C ) ) ` m ) = ( seq 1 ( x. , ( ( k e. A |-> ( B / C ) ) o. f ) ) ` ( # ` A ) ) ) |
86 |
|
fveq2 |
|- ( m = ( f ` n ) -> ( ( k e. A |-> B ) ` m ) = ( ( k e. A |-> B ) ` ( f ` n ) ) ) |
87 |
22
|
adantr |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( k e. A |-> B ) : A --> CC ) |
88 |
87
|
ffvelrnda |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. A ) -> ( ( k e. A |-> B ) ` m ) e. CC ) |
89 |
86 19 32 88 77
|
fprod |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ m e. A ( ( k e. A |-> B ) ` m ) = ( seq 1 ( x. , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) ) |
90 |
|
fveq2 |
|- ( m = ( f ` n ) -> ( ( k e. A |-> C ) ` m ) = ( ( k e. A |-> C ) ` ( f ` n ) ) ) |
91 |
28
|
adantr |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( k e. A |-> C ) : A --> CC ) |
92 |
91
|
ffvelrnda |
|- ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. A ) -> ( ( k e. A |-> C ) ` m ) e. CC ) |
93 |
90 19 32 92 35
|
fprod |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ m e. A ( ( k e. A |-> C ) ` m ) = ( seq 1 ( x. , ( ( k e. A |-> C ) o. f ) ) ` ( # ` A ) ) ) |
94 |
89 93
|
oveq12d |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( prod_ m e. A ( ( k e. A |-> B ) ` m ) / prod_ m e. A ( ( k e. A |-> C ) ` m ) ) = ( ( seq 1 ( x. , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) / ( seq 1 ( x. , ( ( k e. A |-> C ) o. f ) ) ` ( # ` A ) ) ) ) |
95 |
80 85 94
|
3eqtr4d |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ m e. A ( ( k e. A |-> ( B / C ) ) ` m ) = ( prod_ m e. A ( ( k e. A |-> B ) ` m ) / prod_ m e. A ( ( k e. A |-> C ) ` m ) ) ) |
96 |
|
prodfc |
|- prod_ m e. A ( ( k e. A |-> ( B / C ) ) ` m ) = prod_ k e. A ( B / C ) |
97 |
|
prodfc |
|- prod_ m e. A ( ( k e. A |-> B ) ` m ) = prod_ k e. A B |
98 |
|
prodfc |
|- prod_ m e. A ( ( k e. A |-> C ) ` m ) = prod_ k e. A C |
99 |
97 98
|
oveq12i |
|- ( prod_ m e. A ( ( k e. A |-> B ) ` m ) / prod_ m e. A ( ( k e. A |-> C ) ` m ) ) = ( prod_ k e. A B / prod_ k e. A C ) |
100 |
95 96 99
|
3eqtr3g |
|- ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ k e. A ( B / C ) = ( prod_ k e. A B / prod_ k e. A C ) ) |
101 |
100
|
expr |
|- ( ( ph /\ ( # ` A ) e. NN ) -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> prod_ k e. A ( B / C ) = ( prod_ k e. A B / prod_ k e. A C ) ) ) |
102 |
101
|
exlimdv |
|- ( ( ph /\ ( # ` A ) e. NN ) -> ( E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> prod_ k e. A ( B / C ) = ( prod_ k e. A B / prod_ k e. A C ) ) ) |
103 |
102
|
expimpd |
|- ( ph -> ( ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> prod_ k e. A ( B / C ) = ( prod_ k e. A B / prod_ k e. A C ) ) ) |
104 |
|
fz1f1o |
|- ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) ) |
105 |
1 104
|
syl |
|- ( ph -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) ) |
106 |
18 103 105
|
mpjaod |
|- ( ph -> prod_ k e. A ( B / C ) = ( prod_ k e. A B / prod_ k e. A C ) ) |