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 49 nn0ge0d
 |-  ( ph -> 0 <_ sum_ k e. C ( B ` k ) )
86 25 nn0ge0d
 |-  ( ph -> 0 <_ ( B ` D ) )
87 71 eqcomd
 |-  ( ph -> ( B ` D ) = [_ D / k ]_ ( B ` k ) )
88 86 87 breqtrd
 |-  ( ph -> 0 <_ [_ D / k ]_ ( B ` k ) )
89 49 nn0red
 |-  ( ph -> sum_ k e. C ( B ` k ) e. RR )
90 25 nn0red
 |-  ( ph -> ( B ` D ) e. RR )
91 71 90 eqeltrd
 |-  ( ph -> [_ D / k ]_ ( B ` k ) e. RR )
92 89 91 addge01d
 |-  ( ph -> ( 0 <_ [_ D / k ]_ ( B ` k ) <-> sum_ k e. C ( B ` k ) <_ ( sum_ k e. C ( B ` k ) + [_ D / k ]_ ( B ` k ) ) ) )
93 88 92 mpbid
 |-  ( ph -> sum_ k e. C ( B ` k ) <_ ( sum_ k e. C ( B ` k ) + [_ D / k ]_ ( B ` k ) ) )
94 74 eqcomd
 |-  ( ph -> ( sum_ k e. C ( B ` k ) + [_ D / k ]_ ( B ` k ) ) = sum_ k e. ( C u. { D } ) ( B ` k ) )
95 93 94 breqtrd
 |-  ( ph -> sum_ k e. C ( B ` k ) <_ sum_ k e. ( C u. { D } ) ( B ` k ) )
96 82 83 84 85 95 elfzd
 |-  ( ph -> sum_ k e. C ( B ` k ) e. ( 0 ... sum_ k e. ( C u. { D } ) ( B ` k ) ) )
97 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 ) ) ) ) )
98 96 97 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 ) ) ) ) )
99 98 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 ) ) )
100 66 81 99 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 ) ) )
101 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 )
102 96 101 syl
 |-  ( ph -> ( sum_ k e. ( C u. { D } ) ( B ` k ) _C sum_ k e. C ( B ` k ) ) e. NN )
103 100 102 eqeltrd
 |-  ( ph -> ( ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / ( ! ` ( B ` D ) ) ) / ( ! ` sum_ k e. C ( B ` k ) ) ) e. NN )
104 ssun1
 |-  C C_ ( C u. { D } )
105 104 a1i
 |-  ( ph -> C C_ ( C u. { D } ) )
106 elmapssres
 |-  ( ( B e. ( NN0 ^m ( C u. { D } ) ) /\ C C_ ( C u. { D } ) ) -> ( B |` C ) e. ( NN0 ^m C ) )
107 4 105 106 syl2anc
 |-  ( ph -> ( B |` C ) e. ( NN0 ^m C ) )
108 fveq1
 |-  ( b = ( B |` C ) -> ( b ` k ) = ( ( B |` C ) ` k ) )
109 108 adantr
 |-  ( ( b = ( B |` C ) /\ k e. C ) -> ( b ` k ) = ( ( B |` C ) ` k ) )
110 fvres
 |-  ( k e. C -> ( ( B |` C ) ` k ) = ( B ` k ) )
111 110 adantl
 |-  ( ( b = ( B |` C ) /\ k e. C ) -> ( ( B |` C ) ` k ) = ( B ` k ) )
112 109 111 eqtrd
 |-  ( ( b = ( B |` C ) /\ k e. C ) -> ( b ` k ) = ( B ` k ) )
113 112 sumeq2dv
 |-  ( b = ( B |` C ) -> sum_ k e. C ( b ` k ) = sum_ k e. C ( B ` k ) )
114 113 fveq2d
 |-  ( b = ( B |` C ) -> ( ! ` sum_ k e. C ( b ` k ) ) = ( ! ` sum_ k e. C ( B ` k ) ) )
115 112 fveq2d
 |-  ( ( b = ( B |` C ) /\ k e. C ) -> ( ! ` ( b ` k ) ) = ( ! ` ( B ` k ) ) )
116 115 prodeq2dv
 |-  ( b = ( B |` C ) -> prod_ k e. C ( ! ` ( b ` k ) ) = prod_ k e. C ( ! ` ( B ` k ) ) )
117 114 116 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 ) ) ) )
118 117 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 ) )
119 118 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 )
120 5 107 119 syl2anc
 |-  ( ph -> ( ( ! ` sum_ k e. C ( B ` k ) ) / prod_ k e. C ( ! ` ( B ` k ) ) ) e. NN )
121 103 120 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 )
122 65 121 eqeltrd
 |-  ( ph -> ( ( ! ` sum_ k e. ( C u. { D } ) ( B ` k ) ) / prod_ k e. ( C u. { D } ) ( ! ` ( B ` k ) ) ) e. NN )