Metamath Proof Explorer

Theorem mccllem

Description: * Induction step for mccl . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses mccllem.a 
|- ( ph -> A e. Fin )
mccllem.c 
|- ( ph -> C C_ A )
mccllem.d 
|- ( ph -> D e. ( A \ C ) )
mccllem.b 
|- ( ph -> B e. ( NN0 ^m ( C u. { D } ) ) )
mccllem.6 
|- ( ph -> A. b e. ( NN0 ^m C ) ( ( ! ` sum_ k e. C ( b ` k ) ) / prod_ k e. C ( ! ` ( b ` k ) ) ) e. NN )
Assertion mccllem 
|- ( ph -> ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / prod_ k e. ( C u. { D } ) ( ! ` ( B ` k ) ) ) e. NN )

Proof

Step Hyp Ref Expression
1 mccllem.a 
 |-  ( ph -> A e. Fin )
2 mccllem.c 
 |-  ( ph -> C C_ A )
3 mccllem.d 
 |-  ( ph -> D e. ( A \ C ) )
4 mccllem.b 
 |-  ( ph -> B e. ( NN0 ^m ( C u. { D } ) ) )
5 mccllem.6 
 |-  ( ph -> A. b e. ( NN0 ^m C ) ( ( ! ` sum_ k e. C ( b ` k ) ) / prod_ k e. C ( ! ` ( b ` k ) ) ) e. NN )
6 nfv 
 |-  F/ k ph
7 nfcv 
 |-  F/_ k ( ! ` ( B ` D ) )
8 ssfi 
 |-  ( ( A e. Fin /\ C C_ A ) -> C e. Fin )
9 1 2 8 syl2anc 
 |-  ( ph -> C e. Fin )
10 eldifn 
 |-  ( D e. ( A \ C ) -> -. D e. C )
11 3 10 syl 
 |-  ( ph -> -. D e. C )
12 elmapi 
 |-  ( B e. ( NN0 ^m ( C u. { D } ) ) -> B : ( C u. { D } ) --> NN0 )
13 4 12 syl 
 |-  ( ph -> B : ( C u. { D } ) --> NN0 )
14 13 adantr 
 |-  ( ( ph /\ k e. C ) -> B : ( C u. { D } ) --> NN0 )
15 elun1 
 |-  ( k e. C -> k e. ( C u. { D } ) )
16 15 adantl 
 |-  ( ( ph /\ k e. C ) -> k e. ( C u. { D } ) )
17 14 16 ffvelrnd 
 |-  ( ( ph /\ k e. C ) -> ( B ` k ) e. NN0 )
18 17 faccld 
 |-  ( ( ph /\ k e. C ) -> ( ! ` ( B ` k ) ) e. NN )
19 18 nncnd 
 |-  ( ( ph /\ k e. C ) -> ( ! ` ( B ` k ) ) e. CC )
20 2fveq3 
 |-  ( k = D -> ( ! ` ( B ` k ) ) = ( ! ` ( B ` D ) ) )
21 snidg 
 |-  ( D e. ( A \ C ) -> D e. { D } )
22 3 21 syl 
 |-  ( ph -> D e. { D } )
23 elun2 
 |-  ( D e. { D } -> D e. ( C u. { D } ) )
24 22 23 syl 
 |-  ( ph -> D e. ( C u. { D } ) )
25 13 24 ffvelrnd 
 |-  ( ph -> ( B ` D ) e. NN0 )
26 25 faccld 
 |-  ( ph -> ( ! ` ( B ` D ) ) e. NN )
27 26 nncnd 
 |-  ( ph -> ( ! ` ( B ` D ) ) e. CC )
28 6 7 9 3 11 19 20 27 fprodsplitsn 
 |-  ( ph -> prod_ k e. ( C u. { D } ) ( ! ` ( B ` k ) ) = ( prod_ k e. C ( ! ` ( B ` k ) ) x. ( ! ` ( B ` D ) ) ) )
29 28 oveq2d 
 |-  ( ph -> ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / prod_ k e. ( C u. { D } ) ( ! ` ( B ` k ) ) ) = ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( prod_ k e. C ( ! ` ( B ` k ) ) x. ( ! ` ( B ` D ) ) ) ) )
30 3 eldifad 
 |-  ( ph -> D e. A )
31 snssi 
 |-  ( D e. A -> { D } C_ A )
32 30 31 syl 
 |-  ( ph -> { D } C_ A )
33 2 32 unssd 
 |-  ( ph -> ( C u. { D } ) C_ A )
34 ssfi 
 |-  ( ( A e. Fin /\ ( C u. { D } ) C_ A ) -> ( C u. { D } ) e. Fin )
35 1 33 34 syl2anc 
 |-  ( ph -> ( C u. { D } ) e. Fin )
36 13 ffvelrnda 
 |-  ( ( ph /\ k e. ( C u. { D } ) ) -> ( B ` k ) e. NN0 )
37 35 36 fsumnn0cl 
 |-  ( ph -> sum_ k e. ( C u. { D } ) ( B ` k ) e. NN0 )
38 37 faccld 
 |-  ( ph -> ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) e. NN )
39 38 nncnd 
 |-  ( ph -> ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) e. CC )
40 6 9 19 fprodclf 
 |-  ( ph -> prod_ k e. C ( ! ` ( B ` k ) ) e. CC )
41 40 27 mulcld 
 |-  ( ph -> ( prod_ k e. C ( ! ` ( B ` k ) ) x. ( ! ` ( B ` D ) ) ) e. CC )
42 18 nnne0d 
 |-  ( ( ph /\ k e. C ) -> ( ! ` ( B ` k ) ) =/= 0 )
43 9 19 42 fprodn0 
 |-  ( ph -> prod_ k e. C ( ! ` ( B ` k ) ) =/= 0 )
44 26 nnne0d 
 |-  ( ph -> ( ! ` ( B ` D ) ) =/= 0 )
45 40 27 43 44 mulne0d 
 |-  ( ph -> ( prod_ k e. C ( ! ` ( B ` k ) ) x. ( ! ` ( B ` D ) ) ) =/= 0 )
46 39 41 45 divcld 
 |-  ( ph -> ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( prod_ k e. C ( ! ` ( B ` k ) ) x. ( ! ` ( B ` D ) ) ) ) e. CC )
47 46 mulid2d 
 |-  ( ph -> ( 1 x. ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( prod_ k e. C ( ! ` ( B ` k ) ) x. ( ! ` ( B ` D ) ) ) ) ) = ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( prod_ k e. C ( ! ` ( B ` k ) ) x. ( ! ` ( B ` D ) ) ) ) )
48 47 eqcomd 
 |-  ( ph -> ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( prod_ k e. C ( ! ` ( B ` k ) ) x. ( ! ` ( B ` D ) ) ) ) = ( 1 x. ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( prod_ k e. C ( ! ` ( B ` k ) ) x. ( ! ` ( B ` D ) ) ) ) ) )
49 9 17 fsumnn0cl 
 |-  ( ph -> sum_ k e. C ( B ` k ) e. NN0 )
50 49 faccld 
 |-  ( ph -> ( ! ` sum_ k e. C ( B ` k ) ) e. NN )
51 50 nncnd 
 |-  ( ph -> ( ! ` sum_ k e. C ( B ` k ) ) e. CC )
52 nnne0 
 |-  ( ( ! ` sum_ k e. C ( B ` k ) ) e. NN -> ( ! ` sum_ k e. C ( B ` k ) ) =/= 0 )
53 50 52 syl 
 |-  ( ph -> ( ! ` sum_ k e. C ( B ` k ) ) =/= 0 )
54 51 53 dividd 
 |-  ( ph -> ( ( ! ` sum_ k e. C ( B ` k ) ) / ( ! ` sum_ k e. C ( B ` k ) ) ) = 1 )
55 54 eqcomd 
 |-  ( ph -> 1 = ( ( ! ` sum_ k e. C ( B ` k ) ) / ( ! ` sum_ k e. C ( B ` k ) ) ) )
56 40 27 mulcomd 
 |-  ( ph -> ( prod_ k e. C ( ! ` ( B ` k ) ) x. ( ! ` ( B ` D ) ) ) = ( ( ! ` ( B ` D ) ) x. prod_ k e. C ( ! ` ( B ` k ) ) ) )
57 56 oveq2d 
 |-  ( ph -> ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( prod_ k e. C ( ! ` ( B ` k ) ) x. ( ! ` ( B ` D ) ) ) ) = ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ( ! ` ( B ` D ) ) x. prod_ k e. C ( ! ` ( B ` k ) ) ) ) )
58 39 27 40 44 43 divdiv1d 
 |-  ( ph -> ( ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ! ` ( B ` D ) ) ) / prod_ k e. C ( ! ` ( B ` k ) ) ) = ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ( ! ` ( B ` D ) ) x. prod_ k e. C ( ! ` ( B ` k ) ) ) ) )
59 58 eqcomd 
 |-  ( ph -> ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ( ! ` ( B ` D ) ) x. prod_ k e. C ( ! ` ( B ` k ) ) ) ) = ( ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ! ` ( B ` D ) ) ) / prod_ k e. C ( ! ` ( B ` k ) ) ) )
60 57 59 eqtrd 
 |-  ( ph -> ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( prod_ k e. C ( ! ` ( B ` k ) ) x. ( ! ` ( B ` D ) ) ) ) = ( ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ! ` ( B ` D ) ) ) / prod_ k e. C ( ! ` ( B ` k ) ) ) )
61 55 60 oveq12d 
 |-  ( ph -> ( 1 x. ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( prod_ k e. C ( ! ` ( B ` k ) ) x. ( ! ` ( B ` D ) ) ) ) ) = ( ( ( ! ` sum_ k e. C ( B ` k ) ) / ( ! ` sum_ k e. C ( B ` k ) ) ) x. ( ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ! ` ( B ` D ) ) ) / prod_ k e. C ( ! ` ( B ` k ) ) ) ) )
62 39 27 44 divcld 
 |-  ( ph -> ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ! ` ( B ` D ) ) ) e. CC )
63 51 51 62 40 53 43 divmul13d 
 |-  ( ph -> ( ( ( ! ` sum_ k e. C ( B ` k ) ) / ( ! ` sum_ k e. C ( B ` k ) ) ) x. ( ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ! ` ( B ` D ) ) ) / prod_ k e. C ( ! ` ( B ` k ) ) ) ) = ( ( ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ! ` ( B ` D ) ) ) / ( ! ` sum_ k e. C ( B ` k ) ) ) x. ( ( ! ` sum_ k e. C ( B ` k ) ) / prod_ k e. C ( ! ` ( B ` k ) ) ) ) )
64 61 63 eqtrd 
 |-  ( ph -> ( 1 x. ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( prod_ k e. C ( ! ` ( B ` k ) ) x. ( ! ` ( B ` D ) ) ) ) ) = ( ( ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ! ` ( B ` D ) ) ) / ( ! ` sum_ k e. C ( B ` k ) ) ) x. ( ( ! ` sum_ k e. C ( B ` k ) ) / prod_ k e. C ( ! ` ( B ` k ) ) ) ) )
65 29 48 64 3eqtrd 
 |-  ( ph -> ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / prod_ k e. ( C u. { D } ) ( ! ` ( B ` k ) ) ) = ( ( ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ! ` ( B ` D ) ) ) / ( ! ` sum_ k e. C ( B ` k ) ) ) x. ( ( ! ` sum_ k e. C ( B ` k ) ) / prod_ k e. C ( ! ` ( B ` k ) ) ) ) )
66 39 27 51 44 53 divdiv1d 
 |-  ( ph -> ( ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ! ` ( B ` D ) ) ) / ( ! ` sum_ k e. C ( B ` k ) ) ) = ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ( ! ` ( B ` D ) ) x. ( ! ` sum_ k e. C ( B ` k ) ) ) ) )
67 nfcsb1v 
 |-  F/_ k [_ D / k ]_ ( B ` k )
68 17 nn0cnd 
 |-  ( ( ph /\ k e. C ) -> ( B ` k ) e. CC )
69 csbeq1a 
 |-  ( k = D -> ( B ` k ) = [_ D / k ]_ ( B ` k ) )
70 csbfv 
 |-  [_ D / k ]_ ( B ` k ) = ( B ` D )
71 70 a1i 
 |-  ( ph -> [_ D / k ]_ ( B ` k ) = ( B ` D ) )
72 25 nn0cnd 
 |-  ( ph -> ( B ` D ) e. CC )
73 71 72 eqeltrd 
 |-  ( ph -> [_ D / k ]_ ( B ` k ) e. CC )
74 6 67 9 30 11 68 69 73 fsumsplitsn 
 |-  ( ph -> sum_ k e. ( C u. { D } ) ( B ` k ) = ( sum_ k e. C ( B ` k ) + [_ D / k ]_ ( B ` k ) ) )
75 74 oveq1d 
 |-  ( ph -> ( sum_ k e. ( C u. { D } ) ( B ` k ) - sum_ k e. C ( B ` k ) ) = ( ( sum_ k e. C ( B ` k ) + [_ D / k ]_ ( B ` k ) ) - sum_ k e. C ( B ` k ) ) )
76 49 nn0cnd 
 |-  ( ph -> sum_ k e. C ( B ` k ) e. CC )
77 76 73 pncan2d 
 |-  ( ph -> ( ( sum_ k e. C ( B ` k ) + [_ D / k ]_ ( B ` k ) ) - sum_ k e. C ( B ` k ) ) = [_ D / k ]_ ( B ` k ) )
78 75 77 71 3eqtrrd 
 |-  ( ph -> ( B ` D ) = ( sum_ k e. ( C u. { D } ) ( B ` k ) - sum_ k e. C ( B ` k ) ) )
79 78 fveq2d 
 |-  ( ph -> ( ! ` ( B ` D ) ) = ( ! ` ( sum_ k e. ( C u. { D } ) ( B ` k ) - sum_ k e. C ( B ` k ) ) ) )
80 79 oveq1d 
 |-  ( ph -> ( ( ! ` ( B ` D ) ) x. ( ! ` sum_ k e. C ( B ` k ) ) ) = ( ( ! ` ( sum_ k e. ( C u. { D } ) ( B ` k ) - sum_ k e. C ( B ` k ) ) ) x. ( ! ` sum_ k e. C ( B ` k ) ) ) )
81 80 oveq2d 
 |-  ( ph -> ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ( ! ` ( B ` D ) ) x. ( ! ` sum_ k e. C ( B ` k ) ) ) ) = ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ( ! ` ( sum_ k e. ( C u. { D } ) ( B ` k ) - sum_ k e. C ( B ` k ) ) ) x. ( ! ` sum_ k e. C ( B ` k ) ) ) ) )
82 0zd 
 |-  ( ph -> 0 e. ZZ )
83 37 nn0zd 
 |-  ( ph -> sum_ k e. ( C u. { D } ) ( B ` k ) e. ZZ )
84 49 nn0zd 
 |-  ( ph -> sum_ k e. C ( B ` k ) e. ZZ )
85 82 83 84 3jca 
 |-  ( ph -> ( 0 e. ZZ /\ sum_ k e. ( C u. { D } ) ( B ` k ) e. ZZ /\ sum_ k e. C ( B ` k ) e. ZZ ) )
86 49 nn0ge0d 
 |-  ( ph -> 0 <_ sum_ k e. C ( B ` k ) )
87 25 nn0ge0d 
 |-  ( ph -> 0 <_ ( B ` D ) )
88 71 eqcomd 
 |-  ( ph -> ( B ` D ) = [_ D / k ]_ ( B ` k ) )
89 87 88 breqtrd 
 |-  ( ph -> 0 <_ [_ D / k ]_ ( B ` k ) )
90 49 nn0red 
 |-  ( ph -> sum_ k e. C ( B ` k ) e. RR )
91 25 nn0red 
 |-  ( ph -> ( B ` D ) e. RR )
92 71 91 eqeltrd 
 |-  ( ph -> [_ D / k ]_ ( B ` k ) e. RR )
93 90 92 addge01d 
 |-  ( ph -> ( 0 <_ [_ D / k ]_ ( B ` k ) <-> sum_ k e. C ( B ` k ) <_ ( sum_ k e. C ( B ` k ) + [_ D / k ]_ ( B ` k ) ) ) )
94 89 93 mpbid 
 |-  ( ph -> sum_ k e. C ( B ` k ) <_ ( sum_ k e. C ( B ` k ) + [_ D / k ]_ ( B ` k ) ) )
95 74 eqcomd 
 |-  ( ph -> ( sum_ k e. C ( B ` k ) + [_ D / k ]_ ( B ` k ) ) = sum_ k e. ( C u. { D } ) ( B ` k ) )
96 94 95 breqtrd 
 |-  ( ph -> sum_ k e. C ( B ` k ) <_ sum_ k e. ( C u. { D } ) ( B ` k ) )
97 85 86 96 jca32 
 |-  ( ph -> ( ( 0 e. ZZ /\ sum_ k e. ( C u. { D } ) ( B ` k ) e. ZZ /\ sum_ k e. C ( B ` k ) e. ZZ ) /\ ( 0 <_ sum_ k e. C ( B ` k ) /\ sum_ k e. C ( B ` k ) <_ sum_ k e. ( C u. { D } ) ( B ` k ) ) ) )
98 elfz2 
 |-  ( sum_ k e. C ( B ` k ) e. ( 0 ... sum_ k e. ( C u. { D } ) ( B ` k ) ) <-> ( ( 0 e. ZZ /\ sum_ k e. ( C u. { D } ) ( B ` k ) e. ZZ /\ sum_ k e. C ( B ` k ) e. ZZ ) /\ ( 0 <_ sum_ k e. C ( B ` k ) /\ sum_ k e. C ( B ` k ) <_ sum_ k e. ( C u. { D } ) ( B ` k ) ) ) )
99 97 98 sylibr 
 |-  ( ph -> sum_ k e. C ( B ` k ) e. ( 0 ... sum_ k e. ( C u. { D } ) ( B ` k ) ) )
100 bcval2 
 |-  ( sum_ k e. C ( B ` k ) e. ( 0 ... sum_ k e. ( C u. { D } ) ( B ` k ) ) -> ( sum_ k e. ( C u. { D } ) ( B ` k ) _C sum_ k e. C ( B ` k ) ) = ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ( ! ` ( sum_ k e. ( C u. { D } ) ( B ` k ) - sum_ k e. C ( B ` k ) ) ) x. ( ! ` sum_ k e. C ( B ` k ) ) ) ) )
101 99 100 syl 
 |-  ( ph -> ( sum_ k e. ( C u. { D } ) ( B ` k ) _C sum_ k e. C ( B ` k ) ) = ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ( ! ` ( sum_ k e. ( C u. { D } ) ( B ` k ) - sum_ k e. C ( B ` k ) ) ) x. ( ! ` sum_ k e. C ( B ` k ) ) ) ) )
102 101 eqcomd 
 |-  ( ph -> ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ( ! ` ( sum_ k e. ( C u. { D } ) ( B ` k ) - sum_ k e. C ( B ` k ) ) ) x. ( ! ` sum_ k e. C ( B ` k ) ) ) ) = ( sum_ k e. ( C u. { D } ) ( B ` k ) _C sum_ k e. C ( B ` k ) ) )
103 66 81 102 3eqtrd 
 |-  ( ph -> ( ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ! ` ( B ` D ) ) ) / ( ! ` sum_ k e. C ( B ` k ) ) ) = ( sum_ k e. ( C u. { D } ) ( B ` k ) _C sum_ k e. C ( B ` k ) ) )
104 bccl2 
 |-  ( sum_ k e. C ( B ` k ) e. ( 0 ... sum_ k e. ( C u. { D } ) ( B ` k ) ) -> ( sum_ k e. ( C u. { D } ) ( B ` k ) _C sum_ k e. C ( B ` k ) ) e. NN )
105 99 104 syl 
 |-  ( ph -> ( sum_ k e. ( C u. { D } ) ( B ` k ) _C sum_ k e. C ( B ` k ) ) e. NN )
106 103 105 eqeltrd 
 |-  ( ph -> ( ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ! ` ( B ` D ) ) ) / ( ! ` sum_ k e. C ( B ` k ) ) ) e. NN )
107 ssun1 
 |-  C C_ ( C u. { D } )
108 107 a1i 
 |-  ( ph -> C C_ ( C u. { D } ) )
109 elmapssres 
 |-  ( ( B e. ( NN0 ^m ( C u. { D } ) ) /\ C C_ ( C u. { D } ) ) -> ( B |` C ) e. ( NN0 ^m C ) )
110 4 108 109 syl2anc 
 |-  ( ph -> ( B |` C ) e. ( NN0 ^m C ) )
111 fveq1 
 |-  ( b = ( B |` C ) -> ( b ` k ) = ( ( B |` C ) ` k ) )
112 111 adantr 
 |-  ( ( b = ( B |` C ) /\ k e. C ) -> ( b ` k ) = ( ( B |` C ) ` k ) )
113 fvres 
 |-  ( k e. C -> ( ( B |` C ) ` k ) = ( B ` k ) )
114 113 adantl 
 |-  ( ( b = ( B |` C ) /\ k e. C ) -> ( ( B |` C ) ` k ) = ( B ` k ) )
115 112 114 eqtrd 
 |-  ( ( b = ( B |` C ) /\ k e. C ) -> ( b ` k ) = ( B ` k ) )
116 115 sumeq2dv 
 |-  ( b = ( B |` C ) -> sum_ k e. C ( b ` k ) = sum_ k e. C ( B ` k ) )
117 116 fveq2d 
 |-  ( b = ( B |` C ) -> ( ! ` sum_ k e. C ( b ` k ) ) = ( ! ` sum_ k e. C ( B ` k ) ) )
118 115 fveq2d 
 |-  ( ( b = ( B |` C ) /\ k e. C ) -> ( ! ` ( b ` k ) ) = ( ! ` ( B ` k ) ) )
119 118 prodeq2dv 
 |-  ( b = ( B |` C ) -> prod_ k e. C ( ! ` ( b ` k ) ) = prod_ k e. C ( ! ` ( B ` k ) ) )
120 117 119 oveq12d 
 |-  ( b = ( B |` C ) -> ( ( ! ` sum_ k e. C ( b ` k ) ) / prod_ k e. C ( ! ` ( b ` k ) ) ) = ( ( ! ` sum_ k e. C ( B ` k ) ) / prod_ k e. C ( ! ` ( B ` k ) ) ) )
121 120 eleq1d 
 |-  ( b = ( B |` C ) -> ( ( ( ! ` sum_ k e. C ( b ` k ) ) / prod_ k e. C ( ! ` ( b ` k ) ) ) e. NN <-> ( ( ! ` sum_ k e. C ( B ` k ) ) / prod_ k e. C ( ! ` ( B ` k ) ) ) e. NN ) )
122 121 rspccva 
 |-  ( ( A. b e. ( NN0 ^m C ) ( ( ! ` sum_ k e. C ( b ` k ) ) / prod_ k e. C ( ! ` ( b ` k ) ) ) e. NN /\ ( B |` C ) e. ( NN0 ^m C ) ) -> ( ( ! ` sum_ k e. C ( B ` k ) ) / prod_ k e. C ( ! ` ( B ` k ) ) ) e. NN )
123 5 110 122 syl2anc 
 |-  ( ph -> ( ( ! ` sum_ k e. C ( B ` k ) ) / prod_ k e. C ( ! ` ( B ` k ) ) ) e. NN )
124 106 123 nnmulcld 
 |-  ( ph -> ( ( ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ! ` ( B ` D ) ) ) / ( ! ` sum_ k e. C ( B ` k ) ) ) x. ( ( ! ` sum_ k e. C ( B ` k ) ) / prod_ k e. C ( ! ` ( B ` k ) ) ) ) e. NN )
125 65 124 eqeltrd 
 |-  ( ph -> ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / prod_ k e. ( C u. { D } ) ( ! ` ( B ` k ) ) ) e. NN )