Theorem vdwlem9 15693

Description: Lemma for vdw 15698. (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 15688	. . . 4 |- ( ph -> F : ( 1 ... V ) --> ( R ^m ( 1 ... W ) ) )
7		ovex 6678	. . . . 5 |- ( R ^m ( 1 ... W ) ) e. _V
8		ovex 6678	. . . . 5 |- ( 1 ... V ) e. _V
9	7, 8	elmap 7886	. . . 4 |- ( F e. ( ( R ^m ( 1 ... W ) ) ^m ( 1 ... V ) ) <-> F : ( 1 ... V ) --> ( R ^m ( 1 ... W ) ) )
10	6, 9	sylibr 224	. . 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 4657	. . . 4 |- ( f = F -> ( K MonoAP f <-> K MonoAP F ) )
13	12	rspcv 3305	. . 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 65	. 2 |- ( ph -> K MonoAP F )
15		vdwlem9.k	. . . . . 6 |- ( ph -> K e. ( ZZ>= ` 2 ) )
16		eluz2nn 11726	. . . . . 6 |- ( K e. ( ZZ>= ` 2 ) -> K e. NN )
17	15, 16	syl 17	. . . . 5 |- ( ph -> K e. NN )
18	17	nnnn0d 11351	. . . 4 |- ( ph -> K e. NN0 )
19	8, 18, 6	vdwmc 15682	. . 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 481	. . . . . . . 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 796	. . . . . . . . . . . 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 481	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> K e. NN )
24		simprll 802	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. NN )
25		simprlr 803	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> d e. NN )
26		vdwapid1 15679	. . . . . . . . . . . . 13 |- ( ( K e. NN /\ a e. NN /\ d e. NN ) -> a e. ( a (AP ` K ) d ) )
27	23, 24, 25, 26	syl3anc 1326	. . . . . . . . . . . 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 3604	. . . . . . . . . . 11 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. ( `' F " { g } ) )
29		ffn 6045	. . . . . . . . . . . . . 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 481	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> F Fn ( 1 ... V ) )
32		fniniseg 6338	. . . . . . . . . . . 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 222	. . . . . . . . . 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 479	. . . . . . . . 9 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( F ` a ) = g )
36	6	adantr 481	. . . . . . . . . 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 475	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. ( 1 ... V ) )
38	36, 37	ffvelrnd 6360	. . . . . . . . 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 2702	. . . . . . . 8 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> g e. ( R ^m ( 1 ... W ) ) )
40		rsp 2929	. . . . . . . 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 65	. . . . . . 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 481	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> V e. NN )
43	2	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> W e. NN )
44	3	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> R e. Fin )
45	4	adantr 481	. . . . . . . . . 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 481	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> M e. NN )
48		ovex 6678	. . . . . . . . . . . 12 |- ( 1 ... W ) e. _V
49		elmapg 7870	. . . . . . . . . . . 12 |- ( ( R e. Fin /\ ( 1 ... W ) e. _V ) -> ( g e. ( R ^m ( 1 ... W ) ) <-> g : ( 1 ... W ) --> R ) )
50	44, 48, 49	sylancl 694	. . . . . . . . . . 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 222	. . . . . . . . . 10 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> g : ( 1 ... W ) --> R )
52	15	adantr 481	. . . . . . . . . 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 15691	. . . . . . . . 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 399	. . . . . . . . . 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 395	. . . . . . . 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 6657	. . . . . . . . . . . . . . . . . . 19 |- ( x = a -> ( x - 1 ) = ( a - 1 ) )
58	57	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 |- ( x = a -> ( ( x - 1 ) + V ) = ( ( a - 1 ) + V ) )
59	58	oveq2d 6666	. . . . . . . . . . . . . . . . 17 |- ( x = a -> ( W x. ( ( x - 1 ) + V ) ) = ( W x. ( ( a - 1 ) + V ) ) )
60	59	oveq2d 6666	. . . . . . . . . . . . . . . 16 |- ( x = a -> ( y + ( W x. ( ( x - 1 ) + V ) ) ) = ( y + ( W x. ( ( a - 1 ) + V ) ) ) )
61	60	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( x = a -> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) = ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) )
62	61	mpteq2dv 4745	. . . . . . . . . . . . . 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 6486	. . . . . . . . . . . . . 14 |- ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) ) e. _V
64	62, 5, 63	fvmpt 6282	. . . . . . . . . . . . 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 2658	. . . . . . . . . . 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 4665	. . . . . . . . . 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 481	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> K e. NN0 )
69		peano2nn0 11333	. . . . . . . . . . . 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 11334	. . . . . . . . . . . . . 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 11324	. . . . . . . . . . . . 13 |- ( ( ( a - 1 ) e. NN0 /\ V e. NN ) -> ( ( a - 1 ) + V ) e. NN )
74	72, 42, 73	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( ( a - 1 ) + V ) e. NN )
75	43, 74	nnmulcld 11068	. . . . . . . . . . 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 11067	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a + V ) e. NN )
77	43, 76	nnmulcld 11068	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( a + V ) ) e. NN )
78	77	nnzd 11481	. . . . . . . . . . . . 13 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. ( a + V ) ) e. ZZ )
79		2nn 11185	. . . . . . . . . . . . . . . . 17 |- 2 e. NN
80		nnmulcl 11043	. . . . . . . . . . . . . . . . 17 |- ( ( 2 e. NN /\ V e. NN ) -> ( 2 x. V ) e. NN )
81	79, 1, 80	sylancr 695	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 2 x. V ) e. NN )
82	2, 81	nnmulcld 11068	. . . . . . . . . . . . . . 15 |- ( ph -> ( W x. ( 2 x. V ) ) e. NN )
83	82	nnzd 11481	. . . . . . . . . . . . . 14 |- ( ph -> ( W x. ( 2 x. V ) ) e. ZZ )
84	83	adantr 481	. . . . . . . . . . . . 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 11035	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. RR )
86	42	nnred 11035	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> V e. RR )
87		elfzle2 12345	. . . . . . . . . . . . . . . . 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 10641	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a + V ) <_ ( V + V ) )
90	42	nncnd 11036	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> V e. CC )
91	90	2timesd 11275	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( 2 x. V ) = ( V + V ) )
92	89, 91	breqtrrd 4681	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a + V ) <_ ( 2 x. V ) )
93	76	nnred 11035	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a + V ) e. RR )
94	81	nnred 11035	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 2 x. V ) e. RR )
95	94	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( 2 x. V ) e. RR )
96	43	nnred 11035	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> W e. RR )
97	43	nngt0d 11064	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> 0 < W )
98		lemul2 10876	. . . . . . . . . . . . . . 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 1330	. . . . . . . . . . . . . 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 222	. . . . . . . . . . . . 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 11693	. . . . . . . . . . . . 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 1246	. . . . . . . . . . . 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 11036	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> W e. CC )
104		1cnd 10056	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> 1 e. CC )
105	72	nn0cnd 11353	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( a - 1 ) e. CC )
106	105, 90	addcld 10059	. . . . . . . . . . . . . . 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 10064	. . . . . . . . . . . . . 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 10062	. . . . . . . . . . . . . . . 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 9994	. . . . . . . . . . . . . . . . . 18 |- 1 e. CC
110	24	nncnd 11036	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> a e. CC )
111		pncan3 10289	. . . . . . . . . . . . . . . . . 18 |- ( ( 1 e. CC /\ a e. CC ) -> ( 1 + ( a - 1 ) ) = a )
112	109, 110, 111	sylancr 695	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( 1 + ( a - 1 ) ) = a )
113	112	oveq1d 6665	. . . . . . . . . . . . . . . 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 2658	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( 1 + ( ( a - 1 ) + V ) ) = ( a + V ) )
115	114	oveq2d 6666	. . . . . . . . . . . . . 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 10057	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( ( a e. NN /\ d e. NN ) /\ ( a (AP ` K ) d ) C_ ( `' F " { g } ) ) ) -> ( W x. 1 ) = W )
117	116	oveq1d 6665	. . . . . . . . . . . . . 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 2664	. . . . . . . . . . . . 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 6195	. . . . . . . . . . . 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 2703	. . . . . . . . . . 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 6657	. . . . . . . . . . . . 13 |- ( y = z -> ( y + ( W x. ( ( a - 1 ) + V ) ) ) = ( z + ( W x. ( ( a - 1 ) + V ) ) ) )
122	121	fveq2d 6195	. . . . . . . . . . . 12 |- ( y = z -> ( H ` ( y + ( W x. ( ( a - 1 ) + V ) ) ) ) = ( H ` ( z + ( W x. ( ( a - 1 ) + V ) ) ) ) )
123	122	cbvmptv 4750	. . . . . . . . . . 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 15686	. . . . . . . . . 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 250	. . . . . . . . 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 885	. . . . . . . 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 47	. . . . . . 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 643	. . . . 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 3038	. . . 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 1861	. . 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 230	. 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 196   \/ wo 383   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   C_ wss 3574   {csn 4177   <.cop 4183   class class class wbr 4653   |-> cmpt 4729   `'ccnv 5113   "cima 5117   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   ^m cmap 7857   Fincfn 7955   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   < clt 10074   <_ cle 10075   - cmin 10266   NNcn 11020   2c2 11070   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   ...cfz 12326  APcvdwa 15669   MonoAP cvdwm 15670   PolyAP cvdwp 15671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-n0 11293  df-z 11378  df-uz 11688  df-rp 11833  df-fz 12327  df-hash 13118  df-vdwap 15672  df-vdwmc 15673  df-vdwpc 15674

This theorem is referenced by:  vdwlem10  15694