Theorem vdwlem9 14518

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

Hypotheses

Ref	Expression
vdw.r	|- ( ph -> R e. Fin )
vdwlem9.k	|- ( ph -> K e. ( ZZ>= ` 2 ) )
vdwlem9.s	|- ( ph -> A. s e. Fin E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f )
vdwlem9.m	|- ( ph -> M e. NN )
vdwlem9.w	|- ( ph -> W e. NN )
vdwlem9.g	|- ( ph -> A. g e. ( R ^m ( 1 ... W ) ) ( <. M , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) )
vdwlem9.v	|- ( ph -> V e. NN )
vdwlem9.a	|- ( ph -> A. f e. ( ( R ^m ( 1 ... W ) ) ^m ( 1 ... V ) ) K MonoAP f )
vdwlem9.h	|- ( ph -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )
vdwlem9.f	|- F = ( x e. ( 1 ... V ) |-> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) )

Assertion

Ref	Expression
vdwlem9	|- ( ph -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) )

Distinct variable groups:   g, n, x, y, ph   x, f, y, V   f, W, x, y   f, g, F, x, y   f, n, s, K, g, x, y   f, M, g, n, x, y   R, f, g, n, s, x, y   g, H, x, y

Allowed substitution hints:   ph( f, s)   F( n, s)   H( f, n, s)   M( s)   V( g, n, s)   W( g, n, s)

Proof of Theorem vdwlem9

Dummy variables a d z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vdwlem9.v	. . . . 5 |- ( ph -> V e. NN )
2		vdwlem9.w	. . . . 5 |- ( ph -> W e. NN )
3		vdw.r	. . . . 5 |- ( ph -> R e. Fin )
4		vdwlem9.h	. . . . 5 |- ( ph -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )
5		vdwlem9.f	. . . . 5 |- F = ( x e. ( 1 ... V ) |-> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) )
6	1, 2, 3, 4, 5	vdwlem4 14513	. . . 4 |- ( ph -> F : ( 1 ... V ) --> ( R ^m ( 1 ... W ) ) )
7		ovex 6324	. . . . 5 |- ( R ^m ( 1 ... W ) ) e. _V
8		ovex 6324	. . . . 5 |- ( 1 ... V ) e. _V
9	7, 8	elmap 7466	. . . 4 |- ( F e. ( ( R ^m ( 1 ... W ) ) ^m ( 1 ... V ) ) <-> F : ( 1 ... V ) --> ( R ^m ( 1 ... W ) ) )
10	6, 9	sylibr 212	. . 3 |- ( ph -> F e. ( ( R ^m ( 1 ... W ) ) ^m ( 1 ... V ) ) )
11		vdwlem9.a	. . 3 |- ( ph -> A. f e. ( ( R ^m ( 1 ... W ) ) ^m ( 1 ... V ) ) K MonoAP f )
12		breq2 4460	. . . 4 |- ( f = F -> ( K MonoAP f <-> K MonoAP F ) )
13	12	rspcv 3206	. . 3 |- ( F e. ( ( R ^m ( 1 ... W ) ) ^m ( 1 ... V ) ) -> ( A. f e. ( ( R ^m ( 1 ... W ) ) ^m ( 1 ... V ) ) K MonoAP f -> K MonoAP F ) )
14	10, 11, 13	sylc 60	. 2 |- ( ph -> K MonoAP F )
15		vdwlem9.k	. . . . . 6 |- ( ph -> K e. ( ZZ>= ` 2 ) )
16		eluz2nn 11144	. . . . . 6 |- ( K e. ( ZZ>= ` 2 ) -> K e. NN )
17	15, 16	syl 16	. . . . 5 |- ( ph -> K e. NN )
18	17	nnnn0d 10873	. . . 4 |- ( ph -> K e. NN0 )
19	8, 18, 6	vdwmc 14507	. . 3 |- ( ph -> ( K MonoAP F <-> E. g E. a e. NN E. d e. NN ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) )
20		vdwlem9.g	. . . . . . . . 9 |- ( ph -> A. g e. ( R ^m ( 1 ... W ) ) ( <. M , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) )
21	20	adantr 465	. . . . . . . 8 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> A. g e. ( R ^m ( 1 ... W ) ) ( <. M , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) )
22		simprr 757	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a (AP ` K ) d ) C_ ( `' F " { g } ) )
23	17	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> K e. NN )
24		simprll 763	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. NN )
25		simprlr 764	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> d e. NN )
26		vdwapid1 14504	. . . . . . . . . . . . 13 |- ( ( K e. NN /\ a e. NN /\ d e. NN ) -> a e. ( a (AP ` K ) d ) )
27	23, 24, 25, 26	syl3anc 1228	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. ( a (AP ` K ) d ) )
28	22, 27	sseldd 3500	. . . . . . . . . . 11 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. ( `' F " { g } ) )
29		ffn 5737	. . . . . . . . . . . . . 14 |- ( F : ( 1 ... V ) --> ( R ^m ( 1 ... W ) ) -> F Fn ( 1 ... V ) )
30	6, 29	syl 16	. . . . . . . . . . . . 13 |- ( ph -> F Fn ( 1 ... V ) )
31	30	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> F Fn ( 1 ... V ) )
32		fniniseg 6009	. . . . . . . . . . . 12 |- ( F Fn ( 1 ... V ) -> ( a e. ( `' F " { g } ) <-> ( a e. ( 1 ... V ) /\ ( F ` a ) = g ) ) )
33	31, 32	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a e. ( `' F " { g } ) <-> ( a e. ( 1 ... V ) /\ ( F ` a ) = g ) ) )
34	28, 33	mpbid 210	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a e. ( 1 ... V ) /\ ( F ` a ) = g ) )
35	34	simprd 463	. . . . . . . . 9 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( F ` a ) = g )
36	6	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> F : ( 1 ... V ) --> ( R ^m ( 1 ... W ) ) )
37	34	simpld 459	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. ( 1 ... V ) )
38	36, 37	ffvelrnd 6033	. . . . . . . . 9 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( F ` a ) e. ( R ^m ( 1 ... W ) ) )
39	35, 38	eqeltrrd 2546	. . . . . . . 8 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> g e. ( R ^m ( 1 ... W ) ) )
40		rsp 2823	. . . . . . . 8 |- ( A. g e. ( R ^m ( 1 ... W ) ) ( <. M , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) -> ( g e. ( R ^m ( 1 ... W ) ) -> ( <. M , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) ) )
41	21, 39, 40	sylc 60	. . . . . . 7 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( <. M , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) )
42	1	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> V e. NN )
43	2	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> W e. NN )
44	3	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> R e. Fin )
45	4	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )
46		vdwlem9.m	. . . . . . . . . . 11 |- ( ph -> M e. NN )
47	46	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> M e. NN )
48		ovex 6324	. . . . . . . . . . . 12 |- ( 1 ... W ) e. _V
49		elmapg 7451	. . . . . . . . . . . 12 |- ( ( R e. Fin /\ ( 1 ... W ) e. _V ) -> ( g e. ( R ^m ( 1 ... W ) ) <-> g : ( 1 ... W ) --> R ) )
50	44, 48, 49	sylancl 662	. . . . . . . . . . 11 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( g e. ( R ^m ( 1 ... W ) ) <-> g : ( 1 ... W ) --> R ) )
51	39, 50	mpbid 210	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> g : ( 1 ... W ) --> R )
52	15	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> K e. ( ZZ>= ` 2 ) )
53	42, 43, 44, 45, 5, 47, 51, 52, 24, 25, 22	vdwlem7 14516	. . . . . . . . 9 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( <. M , K >. PolyAP g -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP g ) ) )
54		olc 384	. . . . . . . . . 10 |- ( ( K + 1 ) MonoAP g -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP g ) )
55	54	a1i 11	. . . . . . . . 9 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( K + 1 ) MonoAP g -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP g ) ) )
56	53, 55	jaod 380	. . . . . . . 8 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( <. M , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP g ) ) )
57		oveq1 6303	. . . . . . . . . . . . . . . . . . 19 |- ( x = a -> ( x - 1 ) = ( a - 1 ) )
58	57	oveq1d 6311	. . . . . . . . . . . . . . . . . 18 |- ( x = a -> ( ( x - 1 ) + V ) = ( ( a - 1 ) + V ) )
59	58	oveq2d 6312	. . . . . . . . . . . . . . . . 17 |- ( x = a -> ( W x. ( ( x - 1 ) + V ) ) = ( W x. ( ( a - 1 ) + V ) ) )
60	59	oveq2d 6312	. . . . . . . . . . . . . . . 16 |- ( x = a -> ( y + ( W x. ( ( x - 1 ) + V ) ) ) = ( y + ( W x. ( ( a - 1 ) + V ) ) ) )
61	60	fveq2d 5876	. . . . . . . . . . . . . . 15 |- ( x = a -> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) = ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) )
62	61	mpteq2dv 4544	. . . . . . . . . . . . . 14 |- ( x = a -> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) )
63	48	mptex 6144	. . . . . . . . . . . . . 14 |- ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) e. _V
64	62, 5, 63	fvmpt 5956	. . . . . . . . . . . . 13 |- ( a e. ( 1 ... V ) -> ( F ` a ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) )
65	37, 64	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( F ` a ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) )
66	65, 35	eqtr3d 2500	. . . . . . . . . . 11 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) = g )
67	66	breq2d 4468	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( K + 1 ) MonoAP ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) <-> ( K + 1 ) MonoAP g ) )
68	18	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> K e. NN0 )
69		peano2nn0 10857	. . . . . . . . . . . 12 |- ( K e. NN0 -> ( K + 1 ) e. NN0 )
70	68, 69	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( K + 1 ) e. NN0 )
71		nnm1nn0 10858	. . . . . . . . . . . . . 14 |- ( a e. NN -> ( a - 1 ) e. NN0 )
72	24, 71	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a - 1 ) e. NN0 )
73		nn0nnaddcl 10848	. . . . . . . . . . . . 13 |- ( ( ( a - 1 ) e. NN0 /\ V e. NN ) -> ( ( a - 1 ) + V ) e. NN )
74	72, 42, 73	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( a - 1 ) + V ) e. NN )
75	43, 74	nnmulcld 10604	. . . . . . . . . . 11 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( ( a - 1 ) + V ) ) e. NN )
76	24, 42	nnaddcld 10603	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a + V ) e. NN )
77	43, 76	nnmulcld 10604	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( a + V ) ) e. NN )
78	77	nnzd 10989	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( a + V ) ) e. ZZ )
79		2nn 10714	. . . . . . . . . . . . . . . . 17 |- 2 e. NN
80		nnmulcl 10579	. . . . . . . . . . . . . . . . 17 |- ( ( 2 e. NN /\ V e. NN ) -> ( 2 x. V ) e. NN )
81	79, 1, 80	sylancr 663	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 2 x. V ) e. NN )
82	2, 81	nnmulcld 10604	. . . . . . . . . . . . . . 15 |- ( ph -> ( W x. ( 2 x. V ) ) e. NN )
83	82	nnzd 10989	. . . . . . . . . . . . . 14 |- ( ph -> ( W x. ( 2 x. V ) ) e. ZZ )
84	83	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( 2 x. V ) ) e. ZZ )
85	24	nnred 10571	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. RR )
86	42	nnred 10571	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> V e. RR )
87		elfzle2 11715	. . . . . . . . . . . . . . . . 17 |- ( a e. ( 1 ... V ) -> a <_ V )
88	37, 87	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a <_ V )
89	85, 86, 86, 88	leadd1dd 10187	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a + V ) <_ ( V + V ) )
90	42	nncnd 10572	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> V e. CC )
91	90	2timesd 10802	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( 2 x. V ) = ( V + V ) )
92	89, 91	breqtrrd 4482	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a + V ) <_ ( 2 x. V ) )
93	76	nnred 10571	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a + V ) e. RR )
94	81	nnred 10571	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 2 x. V ) e. RR )
95	94	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( 2 x. V ) e. RR )
96	43	nnred 10571	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> W e. RR )
97	43	nngt0d 10600	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> 0 < W )
98		lemul2 10416	. . . . . . . . . . . . . . 15 |- ( ( ( a + V ) e. RR /\ ( 2 x. V ) e. RR /\ ( W e. RR /\ 0 < W ) ) -> ( ( a + V ) <_ ( 2 x. V ) <-> ( W x. ( a + V ) ) <_ ( W x. ( 2 x. V ) ) ) )
99	93, 95, 96, 97, 98	syl112anc 1232	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( a + V ) <_ ( 2 x. V ) <-> ( W x. ( a + V ) ) <_ ( W x. ( 2 x. V ) ) ) )
100	92, 99	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( a + V ) ) <_ ( W x. ( 2 x. V ) ) )
101		eluz2 11112	. . . . . . . . . . . . 13 |- ( ( W x. ( 2 x. V ) ) e. ( ZZ>= ` ( W x. ( a + V ) ) ) <-> ( ( W x. ( a + V ) ) e. ZZ /\ ( W x. ( 2 x. V ) ) e. ZZ /\ ( W x. ( a + V ) ) <_ ( W x. ( 2 x. V ) ) ) )
102	78, 84, 100, 101	syl3anbrc 1180	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( 2 x. V ) ) e. ( ZZ>= ` ( W x. ( a + V ) ) ) )
103	43	nncnd 10572	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> W e. CC )
104		1cnd 9629	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> 1 e. CC )
105	72	nn0cnd 10875	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a - 1 ) e. CC )
106	105, 90	addcld 9632	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( a - 1 ) + V ) e. CC )
107	103, 104, 106	adddid 9637	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( 1 + ( ( a - 1 ) + V ) ) ) = ( ( W x. 1 ) + ( W x. ( ( a - 1 ) + V ) ) ) )
108	104, 105, 90	addassd 9635	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( 1 + ( a - 1 ) ) + V ) = ( 1 + ( ( a - 1 ) + V ) ) )
109		ax-1cn 9567	. . . . . . . . . . . . . . . . . 18 |- 1 e. CC
110	24	nncnd 10572	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. CC )
111		pncan3 9847	. . . . . . . . . . . . . . . . . 18 |- ( ( 1 e. CC /\ a e. CC ) -> ( 1 + ( a - 1 ) ) = a )
112	109, 110, 111	sylancr 663	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( 1 + ( a - 1 ) ) = a )
113	112	oveq1d 6311	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( 1 + ( a - 1 ) ) + V ) = ( a + V ) )
114	108, 113	eqtr3d 2500	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( 1 + ( ( a - 1 ) + V ) ) = ( a + V ) )
115	114	oveq2d 6312	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( 1 + ( ( a - 1 ) + V ) ) ) = ( W x. ( a + V ) ) )
116	103	mulid1d 9630	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. 1 ) = W )
117	116	oveq1d 6311	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( W x. 1 ) + ( W x. ( ( a - 1 ) + V ) ) ) = ( W + ( W x. ( ( a - 1 ) + V ) ) ) )
118	107, 115, 117	3eqtr3d 2506	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( a + V ) ) = ( W + ( W x. ( ( a - 1 ) + V ) ) ) )
119	118	fveq2d 5876	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ZZ>= ` ( W x. ( a + V ) ) ) = ( ZZ>= ` ( W + ( W x. ( ( a - 1 ) + V ) ) ) ) )
120	102, 119	eleqtrd 2547	. . . . . . . . . . 11 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( 2 x. V ) ) e. ( ZZ>= ` ( W + ( W x. ( ( a - 1 ) + V ) ) ) ) )
121		oveq1 6303	. . . . . . . . . . . . 13 |- ( y = z -> ( y + ( W x. ( ( a - 1 ) + V ) ) ) = ( z + ( W x. ( ( a - 1 ) + V ) ) ) )
122	121	fveq2d 5876	. . . . . . . . . . . 12 |- ( y = z -> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) = ( H ` ( z + ( W x. ( ( a - 1 ) + V ) ) ) ) )
123	122	cbvmptv 4548	. . . . . . . . . . 11 |- ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) = ( z e. ( 1 ... W ) |-> ( H ` ( z + ( W x. ( ( a - 1 ) + V ) ) ) ) )
124	44, 70, 43, 75, 45, 120, 123	vdwlem2 14511	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( K + 1 ) MonoAP ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) -> ( K + 1 ) MonoAP H ) )
125	67, 124	sylbird 235	. . . . . . . . 9 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( K + 1 ) MonoAP g -> ( K + 1 ) MonoAP H ) )
126	125	orim2d 840	. . . . . . . 8 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP g ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) ) )
127	56, 126	syld 44	. . . . . . 7 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( <. M , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) ) )
128	41, 127	mpd 15	. . . . . 6 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) )
129	128	expr 615	. . . . 5 |- ( ( ph /\ ( a e. NN /\ d e. NN ) ) -> ( ( a (AP ` K ) d ) C_ ( `' F " { g } ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) ) )
130	129	rexlimdvva 2956	. . . 4 |- ( ph -> ( E. a e. NN E. d e. NN ( a (AP ` K ) d ) C_ ( `' F " { g } ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) ) )
131	130	exlimdv 1725	. . 3 |- ( ph -> ( E. g E. a e. NN E. d e. NN ( a (AP ` K ) d ) C_ ( `' F " { g } ) -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) ) )
132	19, 131	sylbid 215	. 2 |- ( ph -> ( K MonoAP F -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) ) )
133	14, 132	mpd 15	1 |- ( ph -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) )

Syntax hints:   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   = wceq 1395   E.wex 1613   e. wcel 1819   A.wral 2807   E.wrex 2808   _Vcvv 3109   C_ wss 3471   {csn 4032   <.cop 4038   class class class wbr 4456   |-> cmpt 4515   `'ccnv 5007   "cima 5011   Fn wfn 5589   -->wf 5590   ` cfv 5594  (class class class)co 6296   ^m cmap 7438   Fincfn 7535   CCcc 9507   RRcr 9508   0cc0 9509   1c1 9510   + caddc 9512   x. cmul 9514   < clt 9645   <_ cle 9646   - cmin 9824   NNcn 10556   2c2 10606   NN0cn0 10816   ZZcz 10885   ZZ>=cuz 11106   ...cfz 11697  APcvdwa 14494   MonoAP cvdwm 14495   PolyAP cvdwp 14496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6700  df-1st 6799  df-2nd 6800  df-recs 7060  df-rdg 7094  df-1o 7148  df-oadd 7152  df-er 7329  df-map 7440  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-card 8337  df-cda 8565  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-nn 10557  df-2 10615  df-n0 10817  df-z 10886  df-uz 11107  df-rp 11246  df-fz 11698  df-hash 12408  df-vdwap 14497  df-vdwmc 14498  df-vdwpc 14499

This theorem is referenced by:  vdwlem10  14519