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 ) |