Metamath Proof Explorer

Theorem vdwlem5

Description: Lemma for vdw . (Contributed by Mario Carneiro, 12-Sep-2014)

Ref Expression
Hypotheses vdwlem3.v 
|- ( ph -> V e. NN )
vdwlem3.w 
|- ( ph -> W e. NN )
vdwlem4.r 
|- ( ph -> R e. Fin )
vdwlem4.h 
|- ( ph -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )
vdwlem4.f 
|- F = ( x e. ( 1 ... V ) |-> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) )
vdwlem7.m 
|- ( ph -> M e. NN )
vdwlem7.g 
|- ( ph -> G : ( 1 ... W ) --> R )
vdwlem7.k 
|- ( ph -> K e. ( ZZ>= ` 2 ) )
vdwlem7.a 
|- ( ph -> A e. NN )
vdwlem7.d 
|- ( ph -> D e. NN )
vdwlem7.s 
|- ( ph -> ( A ( AP ` K ) D ) C_ ( `' F " { G } ) )
vdwlem6.b 
|- ( ph -> B e. NN )
vdwlem6.e 
|- ( ph -> E : ( 1 ... M ) --> NN )
vdwlem6.s 
|- ( ph -> A. i e. ( 1 ... M ) ( ( B + ( E ` i ) ) ( AP ` K ) ( E ` i ) ) C_ ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) )
vdwlem6.j 
|- J = ( i e. ( 1 ... M ) |-> ( G ` ( B + ( E ` i ) ) ) )
vdwlem6.r 
|- ( ph -> ( # ` ran J ) = M )
vdwlem6.t 
|- T = ( B + ( W x. ( ( A + ( V - D ) ) - 1 ) ) )
vdwlem6.p 
|- P = ( j e. ( 1 ... ( M + 1 ) ) |-> ( if ( j = ( M + 1 ) , 0 , ( E ` j ) ) + ( W x. D ) ) )
Assertion vdwlem5 
|- ( ph -> T e. NN )

Proof

Step Hyp Ref Expression
1 vdwlem3.v 
 |-  ( ph -> V e. NN )
2 vdwlem3.w 
 |-  ( ph -> W e. NN )
3 vdwlem4.r 
 |-  ( ph -> R e. Fin )
4 vdwlem4.h 
 |-  ( ph -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )
5 vdwlem4.f 
 |-  F = ( x e. ( 1 ... V ) |-> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) )
6 vdwlem7.m 
 |-  ( ph -> M e. NN )
7 vdwlem7.g 
 |-  ( ph -> G : ( 1 ... W ) --> R )
8 vdwlem7.k 
 |-  ( ph -> K e. ( ZZ>= ` 2 ) )
9 vdwlem7.a 
 |-  ( ph -> A e. NN )
10 vdwlem7.d 
 |-  ( ph -> D e. NN )
11 vdwlem7.s 
 |-  ( ph -> ( A ( AP ` K ) D ) C_ ( `' F " { G } ) )
12 vdwlem6.b 
 |-  ( ph -> B e. NN )
13 vdwlem6.e 
 |-  ( ph -> E : ( 1 ... M ) --> NN )
14 vdwlem6.s 
 |-  ( ph -> A. i e. ( 1 ... M ) ( ( B + ( E ` i ) ) ( AP ` K ) ( E ` i ) ) C_ ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) )
15 vdwlem6.j 
 |-  J = ( i e. ( 1 ... M ) |-> ( G ` ( B + ( E ` i ) ) ) )
16 vdwlem6.r 
 |-  ( ph -> ( # ` ran J ) = M )
17 vdwlem6.t 
 |-  T = ( B + ( W x. ( ( A + ( V - D ) ) - 1 ) ) )
18 vdwlem6.p 
 |-  P = ( j e. ( 1 ... ( M + 1 ) ) |-> ( if ( j = ( M + 1 ) , 0 , ( E ` j ) ) + ( W x. D ) ) )
19 2 nnnn0d 
 |-  ( ph -> W e. NN0 )
20 1 nncnd 
 |-  ( ph -> V e. CC )
21 10 nncnd 
 |-  ( ph -> D e. CC )
22 20 21 subcld 
 |-  ( ph -> ( V - D ) e. CC )
23 9 nncnd 
 |-  ( ph -> A e. CC )
24 22 23 npcand 
 |-  ( ph -> ( ( ( V - D ) - A ) + A ) = ( V - D ) )
25 20 21 23 subsub4d 
 |-  ( ph -> ( ( V - D ) - A ) = ( V - ( D + A ) ) )
26 21 23 addcomd 
 |-  ( ph -> ( D + A ) = ( A + D ) )
27 26 oveq2d 
 |-  ( ph -> ( V - ( D + A ) ) = ( V - ( A + D ) ) )
28 25 27 eqtrd 
 |-  ( ph -> ( ( V - D ) - A ) = ( V - ( A + D ) ) )
29 cnvimass 
 |-  ( `' F " { G } ) C_ dom F
30 1 2 3 4 5 vdwlem4 
 |-  ( ph -> F : ( 1 ... V ) --> ( R ^m ( 1 ... W ) ) )
31 29 30 fssdm 
 |-  ( ph -> ( `' F " { G } ) C_ ( 1 ... V ) )
32 ssun2 
 |-  ( ( A + D ) ( AP ` ( K - 1 ) ) D ) C_ ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) )
33 uz2m1nn 
 |-  ( K e. ( ZZ>= ` 2 ) -> ( K - 1 ) e. NN )
34 8 33 syl 
 |-  ( ph -> ( K - 1 ) e. NN )
35 9 10 nnaddcld 
 |-  ( ph -> ( A + D ) e. NN )
36 vdwapid1 
 |-  ( ( ( K - 1 ) e. NN /\ ( A + D ) e. NN /\ D e. NN ) -> ( A + D ) e. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) )
37 34 35 10 36 syl3anc 
 |-  ( ph -> ( A + D ) e. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) )
38 32 37 sseldi 
 |-  ( ph -> ( A + D ) e. ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) ) )
39 eluz2nn 
 |-  ( K e. ( ZZ>= ` 2 ) -> K e. NN )
40 8 39 syl 
 |-  ( ph -> K e. NN )
41 40 nncnd 
 |-  ( ph -> K e. CC )
42 ax-1cn 
 |-  1 e. CC
43 npcan 
 |-  ( ( K e. CC /\ 1 e. CC ) -> ( ( K - 1 ) + 1 ) = K )
44 41 42 43 sylancl 
 |-  ( ph -> ( ( K - 1 ) + 1 ) = K )
45 44 fveq2d 
 |-  ( ph -> ( AP ` ( ( K - 1 ) + 1 ) ) = ( AP ` K ) )
46 45 oveqd 
 |-  ( ph -> ( A ( AP ` ( ( K - 1 ) + 1 ) ) D ) = ( A ( AP ` K ) D ) )
47 nnm1nn0 
 |-  ( K e. NN -> ( K - 1 ) e. NN0 )
48 40 47 syl 
 |-  ( ph -> ( K - 1 ) e. NN0 )
49 vdwapun 
 |-  ( ( ( K - 1 ) e. NN0 /\ A e. NN /\ D e. NN ) -> ( A ( AP ` ( ( K - 1 ) + 1 ) ) D ) = ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) ) )
50 48 9 10 49 syl3anc 
 |-  ( ph -> ( A ( AP ` ( ( K - 1 ) + 1 ) ) D ) = ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) ) )
51 46 50 eqtr3d 
 |-  ( ph -> ( A ( AP ` K ) D ) = ( { A } u. ( ( A + D ) ( AP ` ( K - 1 ) ) D ) ) )
52 38 51 eleqtrrd 
 |-  ( ph -> ( A + D ) e. ( A ( AP ` K ) D ) )
53 11 52 sseldd 
 |-  ( ph -> ( A + D ) e. ( `' F " { G } ) )
54 31 53 sseldd 
 |-  ( ph -> ( A + D ) e. ( 1 ... V ) )
55 elfzuz3 
 |-  ( ( A + D ) e. ( 1 ... V ) -> V e. ( ZZ>= ` ( A + D ) ) )
56 54 55 syl 
 |-  ( ph -> V e. ( ZZ>= ` ( A + D ) ) )
57 uznn0sub 
 |-  ( V e. ( ZZ>= ` ( A + D ) ) -> ( V - ( A + D ) ) e. NN0 )
58 56 57 syl 
 |-  ( ph -> ( V - ( A + D ) ) e. NN0 )
59 28 58 eqeltrd 
 |-  ( ph -> ( ( V - D ) - A ) e. NN0 )
60 nn0nnaddcl 
 |-  ( ( ( ( V - D ) - A ) e. NN0 /\ A e. NN ) -> ( ( ( V - D ) - A ) + A ) e. NN )
61 59 9 60 syl2anc 
 |-  ( ph -> ( ( ( V - D ) - A ) + A ) e. NN )
62 24 61 eqeltrrd 
 |-  ( ph -> ( V - D ) e. NN )
63 9 62 nnaddcld 
 |-  ( ph -> ( A + ( V - D ) ) e. NN )
64 nnm1nn0 
 |-  ( ( A + ( V - D ) ) e. NN -> ( ( A + ( V - D ) ) - 1 ) e. NN0 )
65 63 64 syl 
 |-  ( ph -> ( ( A + ( V - D ) ) - 1 ) e. NN0 )
66 19 65 nn0mulcld 
 |-  ( ph -> ( W x. ( ( A + ( V - D ) ) - 1 ) ) e. NN0 )
67 nnnn0addcl 
 |-  ( ( B e. NN /\ ( W x. ( ( A + ( V - D ) ) - 1 ) ) e. NN0 ) -> ( B + ( W x. ( ( A + ( V - D ) ) - 1 ) ) ) e. NN )
68 12 66 67 syl2anc 
 |-  ( ph -> ( B + ( W x. ( ( A + ( V - D ) ) - 1 ) ) ) e. NN )
69 17 68 eqeltrid 
 |-  ( ph -> T e. NN )