Metamath Proof Explorer

Theorem mccl

Description: A multinomial coefficient, in its standard domain, is a positive integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses mccl.kb 
|- F/_ k B
mccl.a 
|- ( ph -> A e. Fin )
mccl.b 
|- ( ph -> B e. ( NN0 ^m A ) )
Assertion mccl 
|- ( ph -> ( ( ! ` sum_ k e. A ( B ` k ) ) / prod_ k e. A ( ! ` ( B ` k ) ) ) e. NN )

Proof

Step Hyp Ref Expression
1 mccl.kb 
 |-  F/_ k B
2 mccl.a 
 |-  ( ph -> A e. Fin )
3 mccl.b 
 |-  ( ph -> B e. ( NN0 ^m A ) )
4 sumeq1 
 |-  ( a = (/) -> sum_ k e. a ( b ` k ) = sum_ k e. (/) ( b ` k ) )
5 4 fveq2d 
 |-  ( a = (/) -> ( ! ` sum_ k e. a ( b ` k ) ) = ( ! ` sum_ k e. (/) ( b ` k ) ) )
6 prodeq1 
 |-  ( a = (/) -> prod_ k e. a ( ! ` ( b ` k ) ) = prod_ k e. (/) ( ! ` ( b ` k ) ) )
7 5 6 oveq12d 
 |-  ( a = (/) -> ( ( ! ` sum_ k e. a ( b ` k ) ) / prod_ k e. a ( ! ` ( b ` k ) ) ) = ( ( ! ` sum_ k e. (/) ( b ` k ) ) / prod_ k e. (/) ( ! ` ( b ` k ) ) ) )
8 7 eleq1d 
 |-  ( a = (/) -> ( ( ( ! ` sum_ k e. a ( b ` k ) ) / prod_ k e. a ( ! ` ( b ` k ) ) ) e. NN <-> ( ( ! ` sum_ k e. (/) ( b ` k ) ) / prod_ k e. (/) ( ! ` ( b ` k ) ) ) e. NN ) )
9 8 ralbidv 
 |-  ( a = (/) -> ( A. b e. ( NN0 ^m a ) ( ( ! ` sum_ k e. a ( b ` k ) ) / prod_ k e. a ( ! ` ( b ` k ) ) ) e. NN <-> A. b e. ( NN0 ^m a ) ( ( ! ` sum_ k e. (/) ( b ` k ) ) / prod_ k e. (/) ( ! ` ( b ` k ) ) ) e. NN ) )
10 oveq2 
 |-  ( a = (/) -> ( NN0 ^m a ) = ( NN0 ^m (/) ) )
11 10 raleqdv 
 |-  ( a = (/) -> ( A. b e. ( NN0 ^m a ) ( ( ! ` sum_ k e. (/) ( b ` k ) ) / prod_ k e. (/) ( ! ` ( b ` k ) ) ) e. NN <-> A. b e. ( NN0 ^m (/) ) ( ( ! ` sum_ k e. (/) ( b ` k ) ) / prod_ k e. (/) ( ! ` ( b ` k ) ) ) e. NN ) )
12 9 11 bitrd 
 |-  ( a = (/) -> ( A. b e. ( NN0 ^m a ) ( ( ! ` sum_ k e. a ( b ` k ) ) / prod_ k e. a ( ! ` ( b ` k ) ) ) e. NN <-> A. b e. ( NN0 ^m (/) ) ( ( ! ` sum_ k e. (/) ( b ` k ) ) / prod_ k e. (/) ( ! ` ( b ` k ) ) ) e. NN ) )
13 sumeq1 
 |-  ( a = c -> sum_ k e. a ( b ` k ) = sum_ k e. c ( b ` k ) )
14 13 fveq2d 
 |-  ( a = c -> ( ! ` sum_ k e. a ( b ` k ) ) = ( ! ` sum_ k e. c ( b ` k ) ) )
15 prodeq1 
 |-  ( a = c -> prod_ k e. a ( ! ` ( b ` k ) ) = prod_ k e. c ( ! ` ( b ` k ) ) )
16 14 15 oveq12d 
 |-  ( a = c -> ( ( ! ` sum_ k e. a ( b ` k ) ) / prod_ k e. a ( ! ` ( b ` k ) ) ) = ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) )
17 16 eleq1d 
 |-  ( a = c -> ( ( ( ! ` sum_ k e. a ( b ` k ) ) / prod_ k e. a ( ! ` ( b ` k ) ) ) e. NN <-> ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) e. NN ) )
18 17 ralbidv 
 |-  ( a = c -> ( A. b e. ( NN0 ^m a ) ( ( ! ` sum_ k e. a ( b ` k ) ) / prod_ k e. a ( ! ` ( b ` k ) ) ) e. NN <-> A. b e. ( NN0 ^m a ) ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) e. NN ) )
19 oveq2 
 |-  ( a = c -> ( NN0 ^m a ) = ( NN0 ^m c ) )
20 19 raleqdv 
 |-  ( a = c -> ( A. b e. ( NN0 ^m a ) ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) e. NN <-> A. b e. ( NN0 ^m c ) ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) e. NN ) )
21 18 20 bitrd 
 |-  ( a = c -> ( A. b e. ( NN0 ^m a ) ( ( ! ` sum_ k e. a ( b ` k ) ) / prod_ k e. a ( ! ` ( b ` k ) ) ) e. NN <-> A. b e. ( NN0 ^m c ) ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) e. NN ) )
22 sumeq1 
 |-  ( a = ( c u. { d } ) -> sum_ k e. a ( b ` k ) = sum_ k e. ( c u. { d } ) ( b ` k ) )
23 22 fveq2d 
 |-  ( a = ( c u. { d } ) -> ( ! ` sum_ k e. a ( b ` k ) ) = ( ! ` sum_ k e. ( c u. { d } ) ( b ` k ) ) )
24 prodeq1 
 |-  ( a = ( c u. { d } ) -> prod_ k e. a ( ! ` ( b ` k ) ) = prod_ k e. ( c u. { d } ) ( ! ` ( b ` k ) ) )
25 23 24 oveq12d 
 |-  ( a = ( c u. { d } ) -> ( ( ! ` sum_ k e. a ( b ` k ) ) / prod_ k e. a ( ! ` ( b ` k ) ) ) = ( ( ! ` sum_ k e. ( c u. { d } ) ( b ` k ) ) / prod_ k e. ( c u. { d } ) ( ! ` ( b ` k ) ) ) )
26 25 eleq1d 
 |-  ( a = ( c u. { d } ) -> ( ( ( ! ` sum_ k e. a ( b ` k ) ) / prod_ k e. a ( ! ` ( b ` k ) ) ) e. NN <-> ( ( ! ` sum_ k e. ( c u. { d } ) ( b ` k ) ) / prod_ k e. ( c u. { d } ) ( ! ` ( b ` k ) ) ) e. NN ) )
27 26 ralbidv 
 |-  ( a = ( c u. { d } ) -> ( A. b e. ( NN0 ^m a ) ( ( ! ` sum_ k e. a ( b ` k ) ) / prod_ k e. a ( ! ` ( b ` k ) ) ) e. NN <-> A. b e. ( NN0 ^m a ) ( ( ! ` sum_ k e. ( c u. { d } ) ( b ` k ) ) / prod_ k e. ( c u. { d } ) ( ! ` ( b ` k ) ) ) e. NN ) )
28 oveq2 
 |-  ( a = ( c u. { d } ) -> ( NN0 ^m a ) = ( NN0 ^m ( c u. { d } ) ) )
29 28 raleqdv 
 |-  ( a = ( c u. { d } ) -> ( A. b e. ( NN0 ^m a ) ( ( ! ` sum_ k e. ( c u. { d } ) ( b ` k ) ) / prod_ k e. ( c u. { d } ) ( ! ` ( b ` k ) ) ) e. NN <-> A. b e. ( NN0 ^m ( c u. { d } ) ) ( ( ! ` sum_ k e. ( c u. { d } ) ( b ` k ) ) / prod_ k e. ( c u. { d } ) ( ! ` ( b ` k ) ) ) e. NN ) )
30 27 29 bitrd 
 |-  ( a = ( c u. { d } ) -> ( A. b e. ( NN0 ^m a ) ( ( ! ` sum_ k e. a ( b ` k ) ) / prod_ k e. a ( ! ` ( b ` k ) ) ) e. NN <-> A. b e. ( NN0 ^m ( c u. { d } ) ) ( ( ! ` sum_ k e. ( c u. { d } ) ( b ` k ) ) / prod_ k e. ( c u. { d } ) ( ! ` ( b ` k ) ) ) e. NN ) )
31 sumeq1 
 |-  ( a = A -> sum_ k e. a ( b ` k ) = sum_ k e. A ( b ` k ) )
32 31 fveq2d 
 |-  ( a = A -> ( ! ` sum_ k e. a ( b ` k ) ) = ( ! ` sum_ k e. A ( b ` k ) ) )
33 prodeq1 
 |-  ( a = A -> prod_ k e. a ( ! ` ( b ` k ) ) = prod_ k e. A ( ! ` ( b ` k ) ) )
34 32 33 oveq12d 
 |-  ( a = A -> ( ( ! ` sum_ k e. a ( b ` k ) ) / prod_ k e. a ( ! ` ( b ` k ) ) ) = ( ( ! ` sum_ k e. A ( b ` k ) ) / prod_ k e. A ( ! ` ( b ` k ) ) ) )
35 34 eleq1d 
 |-  ( a = A -> ( ( ( ! ` sum_ k e. a ( b ` k ) ) / prod_ k e. a ( ! ` ( b ` k ) ) ) e. NN <-> ( ( ! ` sum_ k e. A ( b ` k ) ) / prod_ k e. A ( ! ` ( b ` k ) ) ) e. NN ) )
36 35 ralbidv 
 |-  ( a = A -> ( A. b e. ( NN0 ^m a ) ( ( ! ` sum_ k e. a ( b ` k ) ) / prod_ k e. a ( ! ` ( b ` k ) ) ) e. NN <-> A. b e. ( NN0 ^m a ) ( ( ! ` sum_ k e. A ( b ` k ) ) / prod_ k e. A ( ! ` ( b ` k ) ) ) e. NN ) )
37 oveq2 
 |-  ( a = A -> ( NN0 ^m a ) = ( NN0 ^m A ) )
38 37 raleqdv 
 |-  ( a = A -> ( A. b e. ( NN0 ^m a ) ( ( ! ` sum_ k e. A ( b ` k ) ) / prod_ k e. A ( ! ` ( b ` k ) ) ) e. NN <-> A. b e. ( NN0 ^m A ) ( ( ! ` sum_ k e. A ( b ` k ) ) / prod_ k e. A ( ! ` ( b ` k ) ) ) e. NN ) )
39 36 38 bitrd 
 |-  ( a = A -> ( A. b e. ( NN0 ^m a ) ( ( ! ` sum_ k e. a ( b ` k ) ) / prod_ k e. a ( ! ` ( b ` k ) ) ) e. NN <-> A. b e. ( NN0 ^m A ) ( ( ! ` sum_ k e. A ( b ` k ) ) / prod_ k e. A ( ! ` ( b ` k ) ) ) e. NN ) )
40 sum0 
 |-  sum_ k e. (/) ( b ` k ) = 0
41 40 fveq2i 
 |-  ( ! ` sum_ k e. (/) ( b ` k ) ) = ( ! ` 0 )
42 fac0 
 |-  ( ! ` 0 ) = 1
43 41 42 eqtri 
 |-  ( ! ` sum_ k e. (/) ( b ` k ) ) = 1
44 prod0 
 |-  prod_ k e. (/) ( ! ` ( b ` k ) ) = 1
45 43 44 oveq12i 
 |-  ( ( ! ` sum_ k e. (/) ( b ` k ) ) / prod_ k e. (/) ( ! ` ( b ` k ) ) ) = ( 1 / 1 )
46 1div1e1 
 |-  ( 1 / 1 ) = 1
47 45 46 eqtri 
 |-  ( ( ! ` sum_ k e. (/) ( b ` k ) ) / prod_ k e. (/) ( ! ` ( b ` k ) ) ) = 1
48 1nn 
 |-  1 e. NN
49 47 48 eqeltri 
 |-  ( ( ! ` sum_ k e. (/) ( b ` k ) ) / prod_ k e. (/) ( ! ` ( b ` k ) ) ) e. NN
50 49 a1i 
 |-  ( ( ph /\ b e. ( NN0 ^m (/) ) ) -> ( ( ! ` sum_ k e. (/) ( b ` k ) ) / prod_ k e. (/) ( ! ` ( b ` k ) ) ) e. NN )
51 50 ralrimiva 
 |-  ( ph -> A. b e. ( NN0 ^m (/) ) ( ( ! ` sum_ k e. (/) ( b ` k ) ) / prod_ k e. (/) ( ! ` ( b ` k ) ) ) e. NN )
52 nfv 
 |-  F/ b ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) )
53 nfra1 
 |-  F/ b A. b e. ( NN0 ^m c ) ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) e. NN
54 52 53 nfan 
 |-  F/ b ( ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) ) /\ A. b e. ( NN0 ^m c ) ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) e. NN )
55 simpll 
 |-  ( ( ( ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) ) /\ A. b e. ( NN0 ^m c ) ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) e. NN ) /\ b e. ( NN0 ^m ( c u. { d } ) ) ) -> ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) ) )
56 fveq2 
 |-  ( k = j -> ( b ` k ) = ( b ` j ) )
57 56 cbvsumv 
 |-  sum_ k e. c ( b ` k ) = sum_ j e. c ( b ` j )
58 57 a1i 
 |-  ( b = e -> sum_ k e. c ( b ` k ) = sum_ j e. c ( b ` j ) )
59 fveq1 
 |-  ( b = e -> ( b ` j ) = ( e ` j ) )
60 59 sumeq2sdv 
 |-  ( b = e -> sum_ j e. c ( b ` j ) = sum_ j e. c ( e ` j ) )
61 58 60 eqtrd 
 |-  ( b = e -> sum_ k e. c ( b ` k ) = sum_ j e. c ( e ` j ) )
62 61 fveq2d 
 |-  ( b = e -> ( ! ` sum_ k e. c ( b ` k ) ) = ( ! ` sum_ j e. c ( e ` j ) ) )
63 2fveq3 
 |-  ( k = j -> ( ! ` ( b ` k ) ) = ( ! ` ( b ` j ) ) )
64 63 cbvprodv 
 |-  prod_ k e. c ( ! ` ( b ` k ) ) = prod_ j e. c ( ! ` ( b ` j ) )
65 64 a1i 
 |-  ( b = e -> prod_ k e. c ( ! ` ( b ` k ) ) = prod_ j e. c ( ! ` ( b ` j ) ) )
66 59 fveq2d 
 |-  ( b = e -> ( ! ` ( b ` j ) ) = ( ! ` ( e ` j ) ) )
67 66 prodeq2ad 
 |-  ( b = e -> prod_ j e. c ( ! ` ( b ` j ) ) = prod_ j e. c ( ! ` ( e ` j ) ) )
68 65 67 eqtrd 
 |-  ( b = e -> prod_ k e. c ( ! ` ( b ` k ) ) = prod_ j e. c ( ! ` ( e ` j ) ) )
69 62 68 oveq12d 
 |-  ( b = e -> ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) = ( ( ! ` sum_ j e. c ( e ` j ) ) / prod_ j e. c ( ! ` ( e ` j ) ) ) )
70 69 eleq1d 
 |-  ( b = e -> ( ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) e. NN <-> ( ( ! ` sum_ j e. c ( e ` j ) ) / prod_ j e. c ( ! ` ( e ` j ) ) ) e. NN ) )
71 70 cbvralvw 
 |-  ( A. b e. ( NN0 ^m c ) ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) e. NN <-> A. e e. ( NN0 ^m c ) ( ( ! ` sum_ j e. c ( e ` j ) ) / prod_ j e. c ( ! ` ( e ` j ) ) ) e. NN )
72 71 biimpi 
 |-  ( A. b e. ( NN0 ^m c ) ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) e. NN -> A. e e. ( NN0 ^m c ) ( ( ! ` sum_ j e. c ( e ` j ) ) / prod_ j e. c ( ! ` ( e ` j ) ) ) e. NN )
73 72 ad2antlr 
 |-  ( ( ( ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) ) /\ A. b e. ( NN0 ^m c ) ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) e. NN ) /\ b e. ( NN0 ^m ( c u. { d } ) ) ) -> A. e e. ( NN0 ^m c ) ( ( ! ` sum_ j e. c ( e ` j ) ) / prod_ j e. c ( ! ` ( e ` j ) ) ) e. NN )
74 simpr 
 |-  ( ( ( ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) ) /\ A. b e. ( NN0 ^m c ) ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) e. NN ) /\ b e. ( NN0 ^m ( c u. { d } ) ) ) -> b e. ( NN0 ^m ( c u. { d } ) ) )
75 2 ad3antrrr 
 |-  ( ( ( ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) ) /\ A. e e. ( NN0 ^m c ) ( ( ! ` sum_ j e. c ( e ` j ) ) / prod_ j e. c ( ! ` ( e ` j ) ) ) e. NN ) /\ b e. ( NN0 ^m ( c u. { d } ) ) ) -> A e. Fin )
76 simprl 
 |-  ( ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) ) -> c C_ A )
77 76 ad2antrr 
 |-  ( ( ( ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) ) /\ A. e e. ( NN0 ^m c ) ( ( ! ` sum_ j e. c ( e ` j ) ) / prod_ j e. c ( ! ` ( e ` j ) ) ) e. NN ) /\ b e. ( NN0 ^m ( c u. { d } ) ) ) -> c C_ A )
78 simprr 
 |-  ( ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) ) -> d e. ( A \ c ) )
79 78 ad2antrr 
 |-  ( ( ( ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) ) /\ A. e e. ( NN0 ^m c ) ( ( ! ` sum_ j e. c ( e ` j ) ) / prod_ j e. c ( ! ` ( e ` j ) ) ) e. NN ) /\ b e. ( NN0 ^m ( c u. { d } ) ) ) -> d e. ( A \ c ) )
80 simpr 
 |-  ( ( ( ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) ) /\ A. e e. ( NN0 ^m c ) ( ( ! ` sum_ j e. c ( e ` j ) ) / prod_ j e. c ( ! ` ( e ` j ) ) ) e. NN ) /\ b e. ( NN0 ^m ( c u. { d } ) ) ) -> b e. ( NN0 ^m ( c u. { d } ) ) )
81 fveq2 
 |-  ( j = k -> ( e ` j ) = ( e ` k ) )
82 81 cbvsumv 
 |-  sum_ j e. c ( e ` j ) = sum_ k e. c ( e ` k )
83 82 fveq2i 
 |-  ( ! ` sum_ j e. c ( e ` j ) ) = ( ! ` sum_ k e. c ( e ` k ) )
84 2fveq3 
 |-  ( j = k -> ( ! ` ( e ` j ) ) = ( ! ` ( e ` k ) ) )
85 84 cbvprodv 
 |-  prod_ j e. c ( ! ` ( e ` j ) ) = prod_ k e. c ( ! ` ( e ` k ) )
86 83 85 oveq12i 
 |-  ( ( ! ` sum_ j e. c ( e ` j ) ) / prod_ j e. c ( ! ` ( e ` j ) ) ) = ( ( ! ` sum_ k e. c ( e ` k ) ) / prod_ k e. c ( ! ` ( e ` k ) ) )
87 86 eleq1i 
 |-  ( ( ( ! ` sum_ j e. c ( e ` j ) ) / prod_ j e. c ( ! ` ( e ` j ) ) ) e. NN <-> ( ( ! ` sum_ k e. c ( e ` k ) ) / prod_ k e. c ( ! ` ( e ` k ) ) ) e. NN )
88 87 ralbii 
 |-  ( A. e e. ( NN0 ^m c ) ( ( ! ` sum_ j e. c ( e ` j ) ) / prod_ j e. c ( ! ` ( e ` j ) ) ) e. NN <-> A. e e. ( NN0 ^m c ) ( ( ! ` sum_ k e. c ( e ` k ) ) / prod_ k e. c ( ! ` ( e ` k ) ) ) e. NN )
89 88 biimpi 
 |-  ( A. e e. ( NN0 ^m c ) ( ( ! ` sum_ j e. c ( e ` j ) ) / prod_ j e. c ( ! ` ( e ` j ) ) ) e. NN -> A. e e. ( NN0 ^m c ) ( ( ! ` sum_ k e. c ( e ` k ) ) / prod_ k e. c ( ! ` ( e ` k ) ) ) e. NN )
90 89 ad2antlr 
 |-  ( ( ( ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) ) /\ A. e e. ( NN0 ^m c ) ( ( ! ` sum_ j e. c ( e ` j ) ) / prod_ j e. c ( ! ` ( e ` j ) ) ) e. NN ) /\ b e. ( NN0 ^m ( c u. { d } ) ) ) -> A. e e. ( NN0 ^m c ) ( ( ! ` sum_ k e. c ( e ` k ) ) / prod_ k e. c ( ! ` ( e ` k ) ) ) e. NN )
91 75 77 79 80 90 mccllem 
 |-  ( ( ( ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) ) /\ A. e e. ( NN0 ^m c ) ( ( ! ` sum_ j e. c ( e ` j ) ) / prod_ j e. c ( ! ` ( e ` j ) ) ) e. NN ) /\ b e. ( NN0 ^m ( c u. { d } ) ) ) -> ( ( ! ` sum_ k e. ( c u. { d } ) ( b ` k ) ) / prod_ k e. ( c u. { d } ) ( ! ` ( b ` k ) ) ) e. NN )
92 55 73 74 91 syl21anc 
 |-  ( ( ( ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) ) /\ A. b e. ( NN0 ^m c ) ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) e. NN ) /\ b e. ( NN0 ^m ( c u. { d } ) ) ) -> ( ( ! ` sum_ k e. ( c u. { d } ) ( b ` k ) ) / prod_ k e. ( c u. { d } ) ( ! ` ( b ` k ) ) ) e. NN )
93 92 ex 
 |-  ( ( ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) ) /\ A. b e. ( NN0 ^m c ) ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) e. NN ) -> ( b e. ( NN0 ^m ( c u. { d } ) ) -> ( ( ! ` sum_ k e. ( c u. { d } ) ( b ` k ) ) / prod_ k e. ( c u. { d } ) ( ! ` ( b ` k ) ) ) e. NN ) )
94 54 93 ralrimi 
 |-  ( ( ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) ) /\ A. b e. ( NN0 ^m c ) ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) e. NN ) -> A. b e. ( NN0 ^m ( c u. { d } ) ) ( ( ! ` sum_ k e. ( c u. { d } ) ( b ` k ) ) / prod_ k e. ( c u. { d } ) ( ! ` ( b ` k ) ) ) e. NN )
95 94 ex 
 |-  ( ( ph /\ ( c C_ A /\ d e. ( A \ c ) ) ) -> ( A. b e. ( NN0 ^m c ) ( ( ! ` sum_ k e. c ( b ` k ) ) / prod_ k e. c ( ! ` ( b ` k ) ) ) e. NN -> A. b e. ( NN0 ^m ( c u. { d } ) ) ( ( ! ` sum_ k e. ( c u. { d } ) ( b ` k ) ) / prod_ k e. ( c u. { d } ) ( ! ` ( b ` k ) ) ) e. NN ) )
96 12 21 30 39 51 95 2 findcard2d 
 |-  ( ph -> A. b e. ( NN0 ^m A ) ( ( ! ` sum_ k e. A ( b ` k ) ) / prod_ k e. A ( ! ` ( b ` k ) ) ) e. NN )
97 nfcv 
 |-  F/_ k b
98 97 1 nfeq 
 |-  F/ k b = B
99 fveq1 
 |-  ( b = B -> ( b ` k ) = ( B ` k ) )
100 99 a1d 
 |-  ( b = B -> ( k e. A -> ( b ` k ) = ( B ` k ) ) )
101 98 100 ralrimi 
 |-  ( b = B -> A. k e. A ( b ` k ) = ( B ` k ) )
102 101 sumeq2d 
 |-  ( b = B -> sum_ k e. A ( b ` k ) = sum_ k e. A ( B ` k ) )
103 102 fveq2d 
 |-  ( b = B -> ( ! ` sum_ k e. A ( b ` k ) ) = ( ! ` sum_ k e. A ( B ` k ) ) )
104 99 fveq2d 
 |-  ( b = B -> ( ! ` ( b ` k ) ) = ( ! ` ( B ` k ) ) )
105 104 a1d 
 |-  ( b = B -> ( k e. A -> ( ! ` ( b ` k ) ) = ( ! ` ( B ` k ) ) ) )
106 98 105 ralrimi 
 |-  ( b = B -> A. k e. A ( ! ` ( b ` k ) ) = ( ! ` ( B ` k ) ) )
107 106 prodeq2d 
 |-  ( b = B -> prod_ k e. A ( ! ` ( b ` k ) ) = prod_ k e. A ( ! ` ( B ` k ) ) )
108 103 107 oveq12d 
 |-  ( b = B -> ( ( ! ` sum_ k e. A ( b ` k ) ) / prod_ k e. A ( ! ` ( b ` k ) ) ) = ( ( ! ` sum_ k e. A ( B ` k ) ) / prod_ k e. A ( ! ` ( B ` k ) ) ) )
109 108 eleq1d 
 |-  ( b = B -> ( ( ( ! ` sum_ k e. A ( b ` k ) ) / prod_ k e. A ( ! ` ( b ` k ) ) ) e. NN <-> ( ( ! ` sum_ k e. A ( B ` k ) ) / prod_ k e. A ( ! ` ( B ` k ) ) ) e. NN ) )
110 109 rspccva 
 |-  ( ( A. b e. ( NN0 ^m A ) ( ( ! ` sum_ k e. A ( b ` k ) ) / prod_ k e. A ( ! ` ( b ` k ) ) ) e. NN /\ B e. ( NN0 ^m A ) ) -> ( ( ! ` sum_ k e. A ( B ` k ) ) / prod_ k e. A ( ! ` ( B ` k ) ) ) e. NN )
111 96 3 110 syl2anc 
 |-  ( ph -> ( ( ! ` sum_ k e. A ( B ` k ) ) / prod_ k e. A ( ! ` ( B ` k ) ) ) e. NN )