Theorem vdwlem9 14939

Description: Lemma for vdw 14944. (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 14934	. . . 4 |- ( ph -> F : ( 1 ... V ) --> ( R ^m ( 1 ... W ) ) )
7		ovex 6334	. . . . 5 |- ( R ^m ( 1 ... W ) ) e. _V
8		ovex 6334	. . . . 5 |- ( 1 ... V ) e. _V
9	7, 8	elmap 7512	. . . 4 |- ( F e. ( ( R ^m ( 1 ... W ) ) ^m ( 1 ... V ) ) <-> F : ( 1 ... V ) --> ( R ^m ( 1 ... W ) ) )
10	6, 9	sylibr 215	. . 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 4427	. . . 4 |- ( f = F -> ( K MonoAP f <-> K MonoAP F ) )
13	12	rspcv 3178	. . 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 62	. 2 |- ( ph -> K MonoAP F )
15		vdwlem9.k	. . . . . 6 |- ( ph -> K e. ( ZZ>= ` 2 ) )
16		eluz2nn 11205	. . . . . 6 |- ( K e. ( ZZ>= ` 2 ) -> K e. NN )
17	15, 16	syl 17	. . . . 5 |- ( ph -> K e. NN )
18	17	nnnn0d 10933	. . . 4 |- ( ph -> K e. NN0 )
19	8, 18, 6	vdwmc 14928	. . 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 466	. . . . . . . 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 764	. . . . . . . . . . . 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 466	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> K e. NN )
24		simprll 770	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. NN )
25		simprlr 771	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> d e. NN )
26		vdwapid1 14925	. . . . . . . . . . . . 13 |- ( ( K e. NN /\ a e. NN /\ d e. NN ) -> a e. ( a (AP ` K ) d ) )
27	23, 24, 25, 26	syl3anc 1264	. . . . . . . . . . . 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 3465	. . . . . . . . . . 11 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. ( `' F " { g } ) )
29		ffn 5746	. . . . . . . . . . . . . 14 |- ( F : ( 1 ... V ) --> ( R ^m ( 1 ... W ) ) -> F Fn ( 1 ... V ) )
30	6, 29	syl 17	. . . . . . . . . . . . 13 |- ( ph -> F Fn ( 1 ... V ) )
31	30	adantr 466	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> F Fn ( 1 ... V ) )
32		fniniseg 6019	. . . . . . . . . . . 12 |- ( F Fn ( 1 ... V ) -> ( a e. ( `' F " { g } ) <-> ( a e. ( 1 ... V ) /\ ( F ` a ) = g ) ) )
33	31, 32	syl 17	. . . . . . . . . . 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 213	. . . . . . . . . 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 464	. . . . . . . . 9 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( F ` a ) = g )
36	6	adantr 466	. . . . . . . . . 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 460	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. ( 1 ... V ) )
38	36, 37	ffvelrnd 6039	. . . . . . . . 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 2508	. . . . . . . 8 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> g e. ( R ^m ( 1 ... W ) ) )
40		rsp 2788	. . . . . . . 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 62	. . . . . . 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 466	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> V e. NN )
43	2	adantr 466	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> W e. NN )
44	3	adantr 466	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> R e. Fin )
45	4	adantr 466	. . . . . . . . . 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 466	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> M e. NN )
48		ovex 6334	. . . . . . . . . . . 12 |- ( 1 ... W ) e. _V
49		elmapg 7497	. . . . . . . . . . . 12 |- ( ( R e. Fin /\ ( 1 ... W ) e. _V ) -> ( g e. ( R ^m ( 1 ... W ) ) <-> g : ( 1 ... W ) --> R ) )
50	44, 48, 49	sylancl 666	. . . . . . . . . . 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 213	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> g : ( 1 ... W ) --> R )
52	15	adantr 466	. . . . . . . . . 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 14937	. . . . . . . . 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 385	. . . . . . . . . 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 381	. . . . . . . 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 6313	. . . . . . . . . . . . . . . . . . 19 |- ( x = a -> ( x - 1 ) = ( a - 1 ) )
58	57	oveq1d 6321	. . . . . . . . . . . . . . . . . 18 |- ( x = a -> ( ( x - 1 ) + V ) = ( ( a - 1 ) + V ) )
59	58	oveq2d 6322	. . . . . . . . . . . . . . . . 17 |- ( x = a -> ( W x. ( ( x - 1 ) + V ) ) = ( W x. ( ( a - 1 ) + V ) ) )
60	59	oveq2d 6322	. . . . . . . . . . . . . . . 16 |- ( x = a -> ( y + ( W x. ( ( x - 1 ) + V ) ) ) = ( y + ( W x. ( ( a - 1 ) + V ) ) ) )
61	60	fveq2d 5886	. . . . . . . . . . . . . . 15 |- ( x = a -> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) = ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) )
62	61	mpteq2dv 4511	. . . . . . . . . . . . . 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 6152	. . . . . . . . . . . . . 14 |- ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) e. _V
64	62, 5, 63	fvmpt 5965	. . . . . . . . . . . . 13 |- ( a e. ( 1 ... V ) -> ( F ` a ) = ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) )
65	37, 64	syl 17	. . . . . . . . . . . 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 2465	. . . . . . . . . . 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 4435	. . . . . . . . . 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 466	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> K e. NN0 )
69		peano2nn0 10918	. . . . . . . . . . . 12 |- ( K e. NN0 -> ( K + 1 ) e. NN0 )
70	68, 69	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( K + 1 ) e. NN0 )
71		nnm1nn0 10919	. . . . . . . . . . . . . 14 |- ( a e. NN -> ( a - 1 ) e. NN0 )
72	24, 71	syl 17	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a - 1 ) e. NN0 )
73		nn0nnaddcl 10909	. . . . . . . . . . . . 13 |- ( ( ( a - 1 ) e. NN0 /\ V e. NN ) -> ( ( a - 1 ) + V ) e. NN )
74	72, 42, 73	syl2anc 665	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( a - 1 ) + V ) e. NN )
75	43, 74	nnmulcld 10665	. . . . . . . . . . 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 10664	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a + V ) e. NN )
77	43, 76	nnmulcld 10665	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( a + V ) ) e. NN )
78	77	nnzd 11047	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( a + V ) ) e. ZZ )
79		2nn 10775	. . . . . . . . . . . . . . . . 17 |- 2 e. NN
80		nnmulcl 10640	. . . . . . . . . . . . . . . . 17 |- ( ( 2 e. NN /\ V e. NN ) -> ( 2 x. V ) e. NN )
81	79, 1, 80	sylancr 667	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 2 x. V ) e. NN )
82	2, 81	nnmulcld 10665	. . . . . . . . . . . . . . 15 |- ( ph -> ( W x. ( 2 x. V ) ) e. NN )
83	82	nnzd 11047	. . . . . . . . . . . . . 14 |- ( ph -> ( W x. ( 2 x. V ) ) e. ZZ )
84	83	adantr 466	. . . . . . . . . . . . 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 10632	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. RR )
86	42	nnred 10632	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> V e. RR )
87		elfzle2 11811	. . . . . . . . . . . . . . . . 17 |- ( a e. ( 1 ... V ) -> a <_ V )
88	37, 87	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a <_ V )
89	85, 86, 86, 88	leadd1dd 10235	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a + V ) <_ ( V + V ) )
90	42	nncnd 10633	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> V e. CC )
91	90	2timesd 10863	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( 2 x. V ) = ( V + V ) )
92	89, 91	breqtrrd 4450	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a + V ) <_ ( 2 x. V ) )
93	76	nnred 10632	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a + V ) e. RR )
94	81	nnred 10632	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 2 x. V ) e. RR )
95	94	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( 2 x. V ) e. RR )
96	43	nnred 10632	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> W e. RR )
97	43	nngt0d 10661	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> 0 < W )
98		lemul2 10466	. . . . . . . . . . . . . . 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 1268	. . . . . . . . . . . . . 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 213	. . . . . . . . . . . . 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 11173	. . . . . . . . . . . . 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 1189	. . . . . . . . . . . 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 10633	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> W e. CC )
104		1cnd 9667	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> 1 e. CC )
105	72	nn0cnd 10935	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a - 1 ) e. CC )
106	105, 90	addcld 9670	. . . . . . . . . . . . . . 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 9675	. . . . . . . . . . . . . 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 9673	. . . . . . . . . . . . . . . 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 9605	. . . . . . . . . . . . . . . . . 18 |- 1 e. CC
110	24	nncnd 10633	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. CC )
111		pncan3 9891	. . . . . . . . . . . . . . . . . 18 |- ( ( 1 e. CC /\ a e. CC ) -> ( 1 + ( a - 1 ) ) = a )
112	109, 110, 111	sylancr 667	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( 1 + ( a - 1 ) ) = a )
113	112	oveq1d 6321	. . . . . . . . . . . . . . . 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 2465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( 1 + ( ( a - 1 ) + V ) ) = ( a + V ) )
115	114	oveq2d 6322	. . . . . . . . . . . . . 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 9668	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. 1 ) = W )
117	116	oveq1d 6321	. . . . . . . . . . . . . 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 2471	. . . . . . . . . . . . 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 5886	. . . . . . . . . . . 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 2509	. . . . . . . . . . 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 6313	. . . . . . . . . . . . 13 |- ( y = z -> ( y + ( W x. ( ( a - 1 ) + V ) ) ) = ( z + ( W x. ( ( a - 1 ) + V ) ) ) )
122	121	fveq2d 5886	. . . . . . . . . . . 12 |- ( y = z -> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) = ( H ` ( z + ( W x. ( ( a - 1 ) + V ) ) ) ) )
123	122	cbvmptv 4516	. . . . . . . . . . 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 14932	. . . . . . . . . 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 238	. . . . . . . . 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 848	. . . . . . . 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 45	. . . . . . 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 618	. . . . 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 2921	. . . 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 1772	. . 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 218	. 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 187   \/ wo 369   /\ wa 370   = wceq 1437   E.wex 1657   e. wcel 1872   A.wral 2771   E.wrex 2772   _Vcvv 3080   C_ wss 3436   {csn 3998   <.cop 4004   class class class wbr 4423   |-> cmpt 4482   `'ccnv 4852   "cima 4856   Fn wfn 5596   -->wf 5597   ` cfv 5601  (class class class)co 6306   ^m cmap 7484   Fincfn 7581   CCcc 9545   RRcr 9546   0cc0 9547   1c1 9548   + caddc 9550   x. cmul 9552   < clt 9683   <_ cle 9684   - cmin 9868   NNcn 10617   2c2 10667   NN0cn0 10877   ZZcz 10945   ZZ>=cuz 11167   ...cfz 11792  APcvdwa 14915   MonoAP cvdwm 14916   PolyAP cvdwp 14917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598  ax-cnex 9603  ax-resscn 9604  ax-1cn 9605  ax-icn 9606  ax-addcl 9607  ax-addrcl 9608  ax-mulcl 9609  ax-mulrcl 9610  ax-mulcom 9611  ax-addass 9612  ax-mulass 9613  ax-distr 9614  ax-i2m1 9615  ax-1ne0 9616  ax-1rid 9617  ax-rnegex 9618  ax-rrecex 9619  ax-cnre 9620  ax-pre-lttri 9621  ax-pre-lttrn 9622  ax-pre-ltadd 9623  ax-pre-mulgt0 9624

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6268  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-om 6708  df-1st 6808  df-2nd 6809  df-wrecs 7040  df-recs 7102  df-rdg 7140  df-1o 7194  df-oadd 7198  df-er 7375  df-map 7486  df-en 7582  df-dom 7583  df-sdom 7584  df-fin 7585  df-card 8382  df-cda 8606  df-pnf 9685  df-mnf 9686  df-xr 9687  df-ltxr 9688  df-le 9689  df-sub 9870  df-neg 9871  df-nn 10618  df-2 10676  df-n0 10878  df-z 10946  df-uz 11168  df-rp 11311  df-fz 11793  df-hash 12523  df-vdwap 14918  df-vdwmc 14919  df-vdwpc 14920

This theorem is referenced by:  vdwlem10  14940