Theorem vdwlem8 15692

Description: Lemma for vdw 15698. (Contributed by Mario Carneiro, 18-Aug-2014.)

Hypotheses

Ref	Expression
vdwlem8.r	|- ( ph -> R e. Fin )
vdwlem8.k	|- ( ph -> K e. ( ZZ>= ` 2 ) )
vdwlem8.w	|- ( ph -> W e. NN )
vdwlem8.f	|- ( ph -> F : ( 1 ... ( 2 x. W ) ) --> R )
vdwlem8.c	|- C e. _V
vdwlem8.a	|- ( ph -> A e. NN )
vdwlem8.d	|- ( ph -> D e. NN )
vdwlem8.s	|- ( ph -> ( A (AP ` K ) D ) C_ ( `' G " { C } ) )
vdwlem8.g	|- G = ( x e. ( 1 ... W ) |-> ( F ` ( x + W ) ) )

Assertion

Ref	Expression
vdwlem8	|- ( ph -> <. 1 , K >. PolyAP F )

Distinct variable groups:   x, A   x, D   x, F   ph, x   x, C   x, K   x, W

Allowed substitution hints:   R( x)   G( x)

Proof of Theorem vdwlem8

Dummy variables a d i m n are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vdwlem8.a	. . . . . . . . . 10 |- ( ph -> A e. NN )
2	1	nncnd 11036	. . . . . . . . 9 |- ( ph -> A e. CC )
3		vdwlem8.d	. . . . . . . . . 10 |- ( ph -> D e. NN )
4	3	nncnd 11036	. . . . . . . . 9 |- ( ph -> D e. CC )
5	2, 4	addcomd 10238	. . . . . . . 8 |- ( ph -> ( A + D ) = ( D + A ) )
6	5	oveq2d 6666	. . . . . . 7 |- ( ph -> ( W - ( A + D ) ) = ( W - ( D + A ) ) )
7		vdwlem8.w	. . . . . . . . 9 |- ( ph -> W e. NN )
8	7	nncnd 11036	. . . . . . . 8 |- ( ph -> W e. CC )
9	8, 4, 2	subsub4d 10423	. . . . . . 7 |- ( ph -> ( ( W - D ) - A ) = ( W - ( D + A ) ) )
10	6, 9	eqtr4d 2659	. . . . . 6 |- ( ph -> ( W - ( A + D ) ) = ( ( W - D ) - A ) )
11	10	oveq2d 6666	. . . . 5 |- ( ph -> ( ( A + A ) + ( W - ( A + D ) ) ) = ( ( A + A ) + ( ( W - D ) - A ) ) )
12	8, 4	subcld 10392	. . . . . 6 |- ( ph -> ( W - D ) e. CC )
13	2, 2, 12	ppncand 10432	. . . . 5 |- ( ph -> ( ( A + A ) + ( ( W - D ) - A ) ) = ( A + ( W - D ) ) )
14	11, 13	eqtrd 2656	. . . 4 |- ( ph -> ( ( A + A ) + ( W - ( A + D ) ) ) = ( A + ( W - D ) ) )
15	1, 1	nnaddcld 11067	. . . . 5 |- ( ph -> ( A + A ) e. NN )
16		vdwlem8.s	. . . . . . . 8 |- ( ph -> ( A (AP ` K ) D ) C_ ( `' G " { C } ) )
17		cnvimass 5485	. . . . . . . . 9 |- ( `' G " { C } ) C_ dom G
18		fvex 6201	. . . . . . . . . 10 |- ( F ` ( x + W ) ) e. _V
19		vdwlem8.g	. . . . . . . . . 10 |- G = ( x e. ( 1 ... W ) |-> ( F ` ( x + W ) ) )
20	18, 19	dmmpti 6023	. . . . . . . . 9 |- dom G = ( 1 ... W )
21	17, 20	sseqtri 3637	. . . . . . . 8 |- ( `' G " { C } ) C_ ( 1 ... W )
22	16, 21	syl6ss 3615	. . . . . . 7 |- ( ph -> ( A (AP ` K ) D ) C_ ( 1 ... W ) )
23		ssun2 3777	. . . . . . . . 9 |- ( ( A + D ) (AP ` ( K - 1 ) ) D ) C_ ( { A } u. ( ( A + D ) (AP ` ( K - 1 ) ) D ) )
24		vdwlem8.k	. . . . . . . . . . 11 |- ( ph -> K e. ( ZZ>= ` 2 ) )
25		uz2m1nn 11763	. . . . . . . . . . 11 |- ( K e. ( ZZ>= ` 2 ) -> ( K - 1 ) e. NN )
26	24, 25	syl 17	. . . . . . . . . 10 |- ( ph -> ( K - 1 ) e. NN )
27	1, 3	nnaddcld 11067	. . . . . . . . . 10 |- ( ph -> ( A + D ) e. NN )
28		vdwapid1 15679	. . . . . . . . . 10 |- ( ( ( K - 1 ) e. NN /\ ( A + D ) e. NN /\ D e. NN ) -> ( A + D ) e. ( ( A + D ) (AP ` ( K - 1 ) ) D ) )
29	26, 27, 3, 28	syl3anc 1326	. . . . . . . . 9 |- ( ph -> ( A + D ) e. ( ( A + D ) (AP ` ( K - 1 ) ) D ) )
30	23, 29	sseldi 3601	. . . . . . . 8 |- ( ph -> ( A + D ) e. ( { A } u. ( ( A + D ) (AP ` ( K - 1 ) ) D ) ) )
31		eluz2nn 11726	. . . . . . . . . . . . . 14 |- ( K e. ( ZZ>= ` 2 ) -> K e. NN )
32	24, 31	syl 17	. . . . . . . . . . . . 13 |- ( ph -> K e. NN )
33	32	nncnd 11036	. . . . . . . . . . . 12 |- ( ph -> K e. CC )
34		ax-1cn 9994	. . . . . . . . . . . 12 |- 1 e. CC
35		npcan 10290	. . . . . . . . . . . 12 |- ( ( K e. CC /\ 1 e. CC ) -> ( ( K - 1 ) + 1 ) = K )
36	33, 34, 35	sylancl 694	. . . . . . . . . . 11 |- ( ph -> ( ( K - 1 ) + 1 ) = K )
37	36	fveq2d 6195	. . . . . . . . . 10 |- ( ph -> (AP ` ( ( K - 1 ) + 1 ) ) = (AP ` K ) )
38	37	oveqd 6667	. . . . . . . . 9 |- ( ph -> ( A (AP ` ( ( K - 1 ) + 1 ) ) D ) = ( A (AP ` K ) D ) )
39	26	nnnn0d 11351	. . . . . . . . . 10 |- ( ph -> ( K - 1 ) e. NN0 )
40		vdwapun 15678	. . . . . . . . . 10 |- ( ( ( K - 1 ) e. NN0 /\ A e. NN /\ D e. NN ) -> ( A (AP ` ( ( K - 1 ) + 1 ) ) D ) = ( { A } u. ( ( A + D ) (AP ` ( K - 1 ) ) D ) ) )
41	39, 1, 3, 40	syl3anc 1326	. . . . . . . . 9 |- ( ph -> ( A (AP ` ( ( K - 1 ) + 1 ) ) D ) = ( { A } u. ( ( A + D ) (AP ` ( K - 1 ) ) D ) ) )
42	38, 41	eqtr3d 2658	. . . . . . . 8 |- ( ph -> ( A (AP ` K ) D ) = ( { A } u. ( ( A + D ) (AP ` ( K - 1 ) ) D ) ) )
43	30, 42	eleqtrrd 2704	. . . . . . 7 |- ( ph -> ( A + D ) e. ( A (AP ` K ) D ) )
44	22, 43	sseldd 3604	. . . . . 6 |- ( ph -> ( A + D ) e. ( 1 ... W ) )
45		elfzuz3 12339	. . . . . 6 |- ( ( A + D ) e. ( 1 ... W ) -> W e. ( ZZ>= ` ( A + D ) ) )
46		uznn0sub 11719	. . . . . 6 |- ( W e. ( ZZ>= ` ( A + D ) ) -> ( W - ( A + D ) ) e. NN0 )
47	44, 45, 46	3syl 18	. . . . 5 |- ( ph -> ( W - ( A + D ) ) e. NN0 )
48		nnnn0addcl 11323	. . . . 5 |- ( ( ( A + A ) e. NN /\ ( W - ( A + D ) ) e. NN0 ) -> ( ( A + A ) + ( W - ( A + D ) ) ) e. NN )
49	15, 47, 48	syl2anc 693	. . . 4 |- ( ph -> ( ( A + A ) + ( W - ( A + D ) ) ) e. NN )
50	14, 49	eqeltrrd 2702	. . 3 |- ( ph -> ( A + ( W - D ) ) e. NN )
51		1nn 11031	. . . . . . . 8 |- 1 e. NN
52		f1osng 6177	. . . . . . . 8 |- ( ( 1 e. NN /\ D e. NN ) -> { <. 1 , D >. } : { 1 } -1-1-onto-> { D } )
53	51, 3, 52	sylancr 695	. . . . . . 7 |- ( ph -> { <. 1 , D >. } : { 1 } -1-1-onto-> { D } )
54		f1of 6137	. . . . . . 7 |- ( { <. 1 , D >. } : { 1 } -1-1-onto-> { D } -> { <. 1 , D >. } : { 1 } --> { D } )
55	53, 54	syl 17	. . . . . 6 |- ( ph -> { <. 1 , D >. } : { 1 } --> { D } )
56	3	snssd 4340	. . . . . 6 |- ( ph -> { D } C_ NN )
57	55, 56	fssd 6057	. . . . 5 |- ( ph -> { <. 1 , D >. } : { 1 } --> NN )
58		1z 11407	. . . . . . 7 |- 1 e. ZZ
59		fzsn 12383	. . . . . . 7 |- ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
60	58, 59	ax-mp 5	. . . . . 6 |- ( 1 ... 1 ) = { 1 }
61	60	feq2i 6037	. . . . 5 |- ( { <. 1 , D >. } : ( 1 ... 1 ) --> NN <-> { <. 1 , D >. } : { 1 } --> NN )
62	57, 61	sylibr 224	. . . 4 |- ( ph -> { <. 1 , D >. } : ( 1 ... 1 ) --> NN )
63		nnex 11026	. . . . 5 |- NN e. _V
64		ovex 6678	. . . . 5 |- ( 1 ... 1 ) e. _V
65	63, 64	elmap 7886	. . . 4 |- ( { <. 1 , D >. } e. ( NN ^m ( 1 ... 1 ) ) <-> { <. 1 , D >. } : ( 1 ... 1 ) --> NN )
66	62, 65	sylibr 224	. . 3 |- ( ph -> { <. 1 , D >. } e. ( NN ^m ( 1 ... 1 ) ) )
67	1, 7	nnaddcld 11067	. . . . . . . . . . . . . 14 |- ( ph -> ( A + W ) e. NN )
68	67	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A + W ) e. NN )
69		elfznn0 12433	. . . . . . . . . . . . . 14 |- ( m e. ( 0 ... ( K - 1 ) ) -> m e. NN0 )
70	3	nnnn0d 11351	. . . . . . . . . . . . . 14 |- ( ph -> D e. NN0 )
71		nn0mulcl 11329	. . . . . . . . . . . . . 14 |- ( ( m e. NN0 /\ D e. NN0 ) -> ( m x. D ) e. NN0 )
72	69, 70, 71	syl2anr 495	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. D ) e. NN0 )
73		nnnn0addcl 11323	. . . . . . . . . . . . 13 |- ( ( ( A + W ) e. NN /\ ( m x. D ) e. NN0 ) -> ( ( A + W ) + ( m x. D ) ) e. NN )
74	68, 72, 73	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( A + W ) + ( m x. D ) ) e. NN )
75		nnuz 11723	. . . . . . . . . . . 12 |- NN = ( ZZ>= ` 1 )
76	74, 75	syl6eleq 2711	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( A + W ) + ( m x. D ) ) e. ( ZZ>= ` 1 ) )
77	16	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A (AP ` K ) D ) C_ ( `' G " { C } ) )
78		eqid 2622	. . . . . . . . . . . . . . . . . 18 |- ( A + ( m x. D ) ) = ( A + ( m x. D ) )
79		oveq1 6657	. . . . . . . . . . . . . . . . . . . . 21 |- ( n = m -> ( n x. D ) = ( m x. D ) )
80	79	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20 |- ( n = m -> ( A + ( n x. D ) ) = ( A + ( m x. D ) ) )
81	80	eqeq2d 2632	. . . . . . . . . . . . . . . . . . 19 |- ( n = m -> ( ( A + ( m x. D ) ) = ( A + ( n x. D ) ) <-> ( A + ( m x. D ) ) = ( A + ( m x. D ) ) ) )
82	81	rspcev 3309	. . . . . . . . . . . . . . . . . 18 |- ( ( m e. ( 0 ... ( K - 1 ) ) /\ ( A + ( m x. D ) ) = ( A + ( m x. D ) ) ) -> E. n e. ( 0 ... ( K - 1 ) ) ( A + ( m x. D ) ) = ( A + ( n x. D ) ) )
83	78, 82	mpan2 707	. . . . . . . . . . . . . . . . 17 |- ( m e. ( 0 ... ( K - 1 ) ) -> E. n e. ( 0 ... ( K - 1 ) ) ( A + ( m x. D ) ) = ( A + ( n x. D ) ) )
84	32	nnnn0d 11351	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> K e. NN0 )
85		vdwapval 15677	. . . . . . . . . . . . . . . . . . 19 |- ( ( K e. NN0 /\ A e. NN /\ D e. NN ) -> ( ( A + ( m x. D ) ) e. ( A (AP ` K ) D ) <-> E. n e. ( 0 ... ( K - 1 ) ) ( A + ( m x. D ) ) = ( A + ( n x. D ) ) ) )
86	84, 1, 3, 85	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( A + ( m x. D ) ) e. ( A (AP ` K ) D ) <-> E. n e. ( 0 ... ( K - 1 ) ) ( A + ( m x. D ) ) = ( A + ( n x. D ) ) ) )
87	86	biimpar 502	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ E. n e. ( 0 ... ( K - 1 ) ) ( A + ( m x. D ) ) = ( A + ( n x. D ) ) ) -> ( A + ( m x. D ) ) e. ( A (AP ` K ) D ) )
88	83, 87	sylan2 491	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A + ( m x. D ) ) e. ( A (AP ` K ) D ) )
89	77, 88	sseldd 3604	. . . . . . . . . . . . . . 15 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A + ( m x. D ) ) e. ( `' G " { C } ) )
90	18, 19	fnmpti 6022	. . . . . . . . . . . . . . . 16 |- G Fn ( 1 ... W )
91		fniniseg 6338	. . . . . . . . . . . . . . . 16 |- ( G Fn ( 1 ... W ) -> ( ( A + ( m x. D ) ) e. ( `' G " { C } ) <-> ( ( A + ( m x. D ) ) e. ( 1 ... W ) /\ ( G ` ( A + ( m x. D ) ) ) = C ) ) )
92	90, 91	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( ( A + ( m x. D ) ) e. ( `' G " { C } ) <-> ( ( A + ( m x. D ) ) e. ( 1 ... W ) /\ ( G ` ( A + ( m x. D ) ) ) = C ) )
93	89, 92	sylib 208	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( A + ( m x. D ) ) e. ( 1 ... W ) /\ ( G ` ( A + ( m x. D ) ) ) = C ) )
94	93	simpld 475	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( A + ( m x. D ) ) e. ( 1 ... W ) )
95		elfzuz3 12339	. . . . . . . . . . . . 13 |- ( ( A + ( m x. D ) ) e. ( 1 ... W ) -> W e. ( ZZ>= ` ( A + ( m x. D ) ) ) )
96		eluzelz 11697	. . . . . . . . . . . . . 14 |- ( W e. ( ZZ>= ` ( A + ( m x. D ) ) ) -> W e. ZZ )
97		eluzadd 11716	. . . . . . . . . . . . . 14 |- ( ( W e. ( ZZ>= ` ( A + ( m x. D ) ) ) /\ W e. ZZ ) -> ( W + W ) e. ( ZZ>= ` ( ( A + ( m x. D ) ) + W ) ) )
98	96, 97	mpdan 702	. . . . . . . . . . . . 13 |- ( W e. ( ZZ>= ` ( A + ( m x. D ) ) ) -> ( W + W ) e. ( ZZ>= ` ( ( A + ( m x. D ) ) + W ) ) )
99	94, 95, 98	3syl 18	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( W + W ) e. ( ZZ>= ` ( ( A + ( m x. D ) ) + W ) ) )
100	8	2timesd 11275	. . . . . . . . . . . . 13 |- ( ph -> ( 2 x. W ) = ( W + W ) )
101	100	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( 2 x. W ) = ( W + W ) )
102	2	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> A e. CC )
103	8	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> W e. CC )
104	72	nn0cnd 11353	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( m x. D ) e. CC )
105	102, 103, 104	add32d 10263	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( A + W ) + ( m x. D ) ) = ( ( A + ( m x. D ) ) + W ) )
106	105	fveq2d 6195	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ZZ>= ` ( ( A + W ) + ( m x. D ) ) ) = ( ZZ>= ` ( ( A + ( m x. D ) ) + W ) ) )
107	99, 101, 106	3eltr4d 2716	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( 2 x. W ) e. ( ZZ>= ` ( ( A + W ) + ( m x. D ) ) ) )
108		elfzuzb 12336	. . . . . . . . . . 11 |- ( ( ( A + W ) + ( m x. D ) ) e. ( 1 ... ( 2 x. W ) ) <-> ( ( ( A + W ) + ( m x. D ) ) e. ( ZZ>= ` 1 ) /\ ( 2 x. W ) e. ( ZZ>= ` ( ( A + W ) + ( m x. D ) ) ) ) )
109	76, 107, 108	sylanbrc 698	. . . . . . . . . 10 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( A + W ) + ( m x. D ) ) e. ( 1 ... ( 2 x. W ) ) )
110	105	fveq2d 6195	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( F ` ( ( A + W ) + ( m x. D ) ) ) = ( F ` ( ( A + ( m x. D ) ) + W ) ) )
111		oveq1 6657	. . . . . . . . . . . . . 14 |- ( x = ( A + ( m x. D ) ) -> ( x + W ) = ( ( A + ( m x. D ) ) + W ) )
112	111	fveq2d 6195	. . . . . . . . . . . . 13 |- ( x = ( A + ( m x. D ) ) -> ( F ` ( x + W ) ) = ( F ` ( ( A + ( m x. D ) ) + W ) ) )
113		fvex 6201	. . . . . . . . . . . . 13 |- ( F ` ( ( A + ( m x. D ) ) + W ) ) e. _V
114	112, 19, 113	fvmpt 6282	. . . . . . . . . . . 12 |- ( ( A + ( m x. D ) ) e. ( 1 ... W ) -> ( G ` ( A + ( m x. D ) ) ) = ( F ` ( ( A + ( m x. D ) ) + W ) ) )
115	94, 114	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( G ` ( A + ( m x. D ) ) ) = ( F ` ( ( A + ( m x. D ) ) + W ) ) )
116	93	simprd 479	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( G ` ( A + ( m x. D ) ) ) = C )
117	110, 115, 116	3eqtr2d 2662	. . . . . . . . . 10 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( F ` ( ( A + W ) + ( m x. D ) ) ) = C )
118	109, 117	jca 554	. . . . . . . . 9 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( ( ( A + W ) + ( m x. D ) ) e. ( 1 ... ( 2 x. W ) ) /\ ( F ` ( ( A + W ) + ( m x. D ) ) ) = C ) )
119		eleq1 2689	. . . . . . . . . 10 |- ( x = ( ( A + W ) + ( m x. D ) ) -> ( x e. ( 1 ... ( 2 x. W ) ) <-> ( ( A + W ) + ( m x. D ) ) e. ( 1 ... ( 2 x. W ) ) ) )
120		fveq2 6191	. . . . . . . . . . 11 |- ( x = ( ( A + W ) + ( m x. D ) ) -> ( F ` x ) = ( F ` ( ( A + W ) + ( m x. D ) ) ) )
121	120	eqeq1d 2624	. . . . . . . . . 10 |- ( x = ( ( A + W ) + ( m x. D ) ) -> ( ( F ` x ) = C <-> ( F ` ( ( A + W ) + ( m x. D ) ) ) = C ) )
122	119, 121	anbi12d 747	. . . . . . . . 9 |- ( x = ( ( A + W ) + ( m x. D ) ) -> ( ( x e. ( 1 ... ( 2 x. W ) ) /\ ( F ` x ) = C ) <-> ( ( ( A + W ) + ( m x. D ) ) e. ( 1 ... ( 2 x. W ) ) /\ ( F ` ( ( A + W ) + ( m x. D ) ) ) = C ) ) )
123	118, 122	syl5ibrcom 237	. . . . . . . 8 |- ( ( ph /\ m e. ( 0 ... ( K - 1 ) ) ) -> ( x = ( ( A + W ) + ( m x. D ) ) -> ( x e. ( 1 ... ( 2 x. W ) ) /\ ( F ` x ) = C ) ) )
124	123	rexlimdva 3031	. . . . . . 7 |- ( ph -> ( E. m e. ( 0 ... ( K - 1 ) ) x = ( ( A + W ) + ( m x. D ) ) -> ( x e. ( 1 ... ( 2 x. W ) ) /\ ( F ` x ) = C ) ) )
125		vdwapval 15677	. . . . . . . 8 |- ( ( K e. NN0 /\ ( A + W ) e. NN /\ D e. NN ) -> ( x e. ( ( A + W ) (AP ` K ) D ) <-> E. m e. ( 0 ... ( K - 1 ) ) x = ( ( A + W ) + ( m x. D ) ) ) )
126	84, 67, 3, 125	syl3anc 1326	. . . . . . 7 |- ( ph -> ( x e. ( ( A + W ) (AP ` K ) D ) <-> E. m e. ( 0 ... ( K - 1 ) ) x = ( ( A + W ) + ( m x. D ) ) ) )
127		vdwlem8.f	. . . . . . . 8 |- ( ph -> F : ( 1 ... ( 2 x. W ) ) --> R )
128		ffn 6045	. . . . . . . 8 |- ( F : ( 1 ... ( 2 x. W ) ) --> R -> F Fn ( 1 ... ( 2 x. W ) ) )
129		fniniseg 6338	. . . . . . . 8 |- ( F Fn ( 1 ... ( 2 x. W ) ) -> ( x e. ( `' F " { C } ) <-> ( x e. ( 1 ... ( 2 x. W ) ) /\ ( F ` x ) = C ) ) )
130	127, 128, 129	3syl 18	. . . . . . 7 |- ( ph -> ( x e. ( `' F " { C } ) <-> ( x e. ( 1 ... ( 2 x. W ) ) /\ ( F ` x ) = C ) ) )
131	124, 126, 130	3imtr4d 283	. . . . . 6 |- ( ph -> ( x e. ( ( A + W ) (AP ` K ) D ) -> x e. ( `' F " { C } ) ) )
132	131	ssrdv 3609	. . . . 5 |- ( ph -> ( ( A + W ) (AP ` K ) D ) C_ ( `' F " { C } ) )
133		fvsng 6447	. . . . . . . . 9 |- ( ( 1 e. NN /\ D e. NN ) -> ( { <. 1 , D >. } ` 1 ) = D )
134	51, 3, 133	sylancr 695	. . . . . . . 8 |- ( ph -> ( { <. 1 , D >. } ` 1 ) = D )
135	134	oveq2d 6666	. . . . . . 7 |- ( ph -> ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) = ( ( A + ( W - D ) ) + D ) )
136	2, 12, 4	addassd 10062	. . . . . . 7 |- ( ph -> ( ( A + ( W - D ) ) + D ) = ( A + ( ( W - D ) + D ) ) )
137	8, 4	npcand 10396	. . . . . . . 8 |- ( ph -> ( ( W - D ) + D ) = W )
138	137	oveq2d 6666	. . . . . . 7 |- ( ph -> ( A + ( ( W - D ) + D ) ) = ( A + W ) )
139	135, 136, 138	3eqtrd 2660	. . . . . 6 |- ( ph -> ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) = ( A + W ) )
140	139, 134	oveq12d 6668	. . . . 5 |- ( ph -> ( ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) (AP ` K ) ( { <. 1 , D >. } ` 1 ) ) = ( ( A + W ) (AP ` K ) D ) )
141	139	fveq2d 6195	. . . . . . . 8 |- ( ph -> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) = ( F ` ( A + W ) ) )
142		vdwapid1 15679	. . . . . . . . . . . . 13 |- ( ( K e. NN /\ A e. NN /\ D e. NN ) -> A e. ( A (AP ` K ) D ) )
143	32, 1, 3, 142	syl3anc 1326	. . . . . . . . . . . 12 |- ( ph -> A e. ( A (AP ` K ) D ) )
144	16, 143	sseldd 3604	. . . . . . . . . . 11 |- ( ph -> A e. ( `' G " { C } ) )
145		fniniseg 6338	. . . . . . . . . . . 12 |- ( G Fn ( 1 ... W ) -> ( A e. ( `' G " { C } ) <-> ( A e. ( 1 ... W ) /\ ( G ` A ) = C ) ) )
146	90, 145	ax-mp 5	. . . . . . . . . . 11 |- ( A e. ( `' G " { C } ) <-> ( A e. ( 1 ... W ) /\ ( G ` A ) = C ) )
147	144, 146	sylib 208	. . . . . . . . . 10 |- ( ph -> ( A e. ( 1 ... W ) /\ ( G ` A ) = C ) )
148	147	simpld 475	. . . . . . . . 9 |- ( ph -> A e. ( 1 ... W ) )
149		oveq1 6657	. . . . . . . . . . 11 |- ( x = A -> ( x + W ) = ( A + W ) )
150	149	fveq2d 6195	. . . . . . . . . 10 |- ( x = A -> ( F ` ( x + W ) ) = ( F ` ( A + W ) ) )
151		fvex 6201	. . . . . . . . . 10 |- ( F ` ( A + W ) ) e. _V
152	150, 19, 151	fvmpt 6282	. . . . . . . . 9 |- ( A e. ( 1 ... W ) -> ( G ` A ) = ( F ` ( A + W ) ) )
153	148, 152	syl 17	. . . . . . . 8 |- ( ph -> ( G ` A ) = ( F ` ( A + W ) ) )
154	147	simprd 479	. . . . . . . 8 |- ( ph -> ( G ` A ) = C )
155	141, 153, 154	3eqtr2d 2662	. . . . . . 7 |- ( ph -> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) = C )
156	155	sneqd 4189	. . . . . 6 |- ( ph -> { ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) } = { C } )
157	156	imaeq2d 5466	. . . . 5 |- ( ph -> ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) } ) = ( `' F " { C } ) )
158	132, 140, 157	3sstr4d 3648	. . . 4 |- ( ph -> ( ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) (AP ` K ) ( { <. 1 , D >. } ` 1 ) ) C_ ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) } ) )
159	158	ralrimivw 2967	. . 3 |- ( ph -> A. i e. ( 1 ... 1 ) ( ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) (AP ` K ) ( { <. 1 , D >. } ` 1 ) ) C_ ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) } ) )
160	155	mpteq2dv 4745	. . . . . . . 8 |- ( ph -> ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) = ( i e. ( 1 ... 1 ) |-> C ) )
161		fconstmpt 5163	. . . . . . . 8 |- ( ( 1 ... 1 ) X. { C } ) = ( i e. ( 1 ... 1 ) |-> C )
162	160, 161	syl6eqr 2674	. . . . . . 7 |- ( ph -> ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) = ( ( 1 ... 1 ) X. { C } ) )
163	162	rneqd 5353	. . . . . 6 |- ( ph -> ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) = ran ( ( 1 ... 1 ) X. { C } ) )
164		elfz3 12351	. . . . . . . 8 |- ( 1 e. ZZ -> 1 e. ( 1 ... 1 ) )
165		ne0i 3921	. . . . . . . 8 |- ( 1 e. ( 1 ... 1 ) -> ( 1 ... 1 ) =/= (/) )
166	58, 164, 165	mp2b 10	. . . . . . 7 |- ( 1 ... 1 ) =/= (/)
167		rnxp 5564	. . . . . . 7 |- ( ( 1 ... 1 ) =/= (/) -> ran ( ( 1 ... 1 ) X. { C } ) = { C } )
168	166, 167	ax-mp 5	. . . . . 6 |- ran ( ( 1 ... 1 ) X. { C } ) = { C }
169	163, 168	syl6eq 2672	. . . . 5 |- ( ph -> ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) = { C } )
170	169	fveq2d 6195	. . . 4 |- ( ph -> ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) ) = ( # ` { C } ) )
171		vdwlem8.c	. . . . 5 |- C e. _V
172		hashsng 13159	. . . . 5 |- ( C e. _V -> ( # ` { C } ) = 1 )
173	171, 172	ax-mp 5	. . . 4 |- ( # ` { C } ) = 1
174	170, 173	syl6eq 2672	. . 3 |- ( ph -> ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) ) = 1 )
175		oveq1 6657	. . . . . . . 8 |- ( a = ( A + ( W - D ) ) -> ( a + ( d ` i ) ) = ( ( A + ( W - D ) ) + ( d ` i ) ) )
176	175	oveq1d 6665	. . . . . . 7 |- ( a = ( A + ( W - D ) ) -> ( ( a + ( d ` i ) ) (AP ` K ) ( d ` i ) ) = ( ( ( A + ( W - D ) ) + ( d ` i ) ) (AP ` K ) ( d ` i ) ) )
177	175	fveq2d 6195	. . . . . . . . 9 |- ( a = ( A + ( W - D ) ) -> ( F ` ( a + ( d ` i ) ) ) = ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) )
178	177	sneqd 4189	. . . . . . . 8 |- ( a = ( A + ( W - D ) ) -> { ( F ` ( a + ( d ` i ) ) ) } = { ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) } )
179	178	imaeq2d 5466	. . . . . . 7 |- ( a = ( A + ( W - D ) ) -> ( `' F " { ( F ` ( a + ( d ` i ) ) ) } ) = ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) } ) )
180	176, 179	sseq12d 3634	. . . . . 6 |- ( a = ( A + ( W - D ) ) -> ( ( ( a + ( d ` i ) ) (AP ` K ) ( d ` i ) ) C_ ( `' F " { ( F ` ( a + ( d ` i ) ) ) } ) <-> ( ( ( A + ( W - D ) ) + ( d ` i ) ) (AP ` K ) ( d ` i ) ) C_ ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) } ) ) )
181	180	ralbidv 2986	. . . . 5 |- ( a = ( A + ( W - D ) ) -> ( A. i e. ( 1 ... 1 ) ( ( a + ( d ` i ) ) (AP ` K ) ( d ` i ) ) C_ ( `' F " { ( F ` ( a + ( d ` i ) ) ) } ) <-> A. i e. ( 1 ... 1 ) ( ( ( A + ( W - D ) ) + ( d ` i ) ) (AP ` K ) ( d ` i ) ) C_ ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) } ) ) )
182	177	mpteq2dv 4745	. . . . . . . 8 |- ( a = ( A + ( W - D ) ) -> ( i e. ( 1 ... 1 ) |-> ( F ` ( a + ( d ` i ) ) ) ) = ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) ) )
183	182	rneqd 5353	. . . . . . 7 |- ( a = ( A + ( W - D ) ) -> ran ( i e. ( 1 ... 1 ) |-> ( F ` ( a + ( d ` i ) ) ) ) = ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) ) )
184	183	fveq2d 6195	. . . . . 6 |- ( a = ( A + ( W - D ) ) -> ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( a + ( d ` i ) ) ) ) ) = ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) ) ) )
185	184	eqeq1d 2624	. . . . 5 |- ( a = ( A + ( W - D ) ) -> ( ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( a + ( d ` i ) ) ) ) ) = 1 <-> ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) ) ) = 1 ) )
186	181, 185	anbi12d 747	. . . 4 |- ( a = ( A + ( W - D ) ) -> ( ( A. i e. ( 1 ... 1 ) ( ( a + ( d ` i ) ) (AP ` K ) ( d ` i ) ) C_ ( `' F " { ( F ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( a + ( d ` i ) ) ) ) ) = 1 ) <-> ( A. i e. ( 1 ... 1 ) ( ( ( A + ( W - D ) ) + ( d ` i ) ) (AP ` K ) ( d ` i ) ) C_ ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) ) ) = 1 ) ) )
187		fveq1 6190	. . . . . . . . . 10 |- ( d = { <. 1 , D >. } -> ( d ` i ) = ( { <. 1 , D >. } ` i ) )
188		elfz1eq 12352	. . . . . . . . . . 11 |- ( i e. ( 1 ... 1 ) -> i = 1 )
189	188	fveq2d 6195	. . . . . . . . . 10 |- ( i e. ( 1 ... 1 ) -> ( { <. 1 , D >. } ` i ) = ( { <. 1 , D >. } ` 1 ) )
190	187, 189	sylan9eq 2676	. . . . . . . . 9 |- ( ( d = { <. 1 , D >. } /\ i e. ( 1 ... 1 ) ) -> ( d ` i ) = ( { <. 1 , D >. } ` 1 ) )
191	190	oveq2d 6666	. . . . . . . 8 |- ( ( d = { <. 1 , D >. } /\ i e. ( 1 ... 1 ) ) -> ( ( A + ( W - D ) ) + ( d ` i ) ) = ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) )
192	191, 190	oveq12d 6668	. . . . . . 7 |- ( ( d = { <. 1 , D >. } /\ i e. ( 1 ... 1 ) ) -> ( ( ( A + ( W - D ) ) + ( d ` i ) ) (AP ` K ) ( d ` i ) ) = ( ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) (AP ` K ) ( { <. 1 , D >. } ` 1 ) ) )
193	191	fveq2d 6195	. . . . . . . . 9 |- ( ( d = { <. 1 , D >. } /\ i e. ( 1 ... 1 ) ) -> ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) = ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) )
194	193	sneqd 4189	. . . . . . . 8 |- ( ( d = { <. 1 , D >. } /\ i e. ( 1 ... 1 ) ) -> { ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) } = { ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) } )
195	194	imaeq2d 5466	. . . . . . 7 |- ( ( d = { <. 1 , D >. } /\ i e. ( 1 ... 1 ) ) -> ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) } ) = ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) } ) )
196	192, 195	sseq12d 3634	. . . . . 6 |- ( ( d = { <. 1 , D >. } /\ i e. ( 1 ... 1 ) ) -> ( ( ( ( A + ( W - D ) ) + ( d ` i ) ) (AP ` K ) ( d ` i ) ) C_ ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) } ) <-> ( ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) (AP ` K ) ( { <. 1 , D >. } ` 1 ) ) C_ ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) } ) ) )
197	196	ralbidva 2985	. . . . 5 |- ( d = { <. 1 , D >. } -> ( A. i e. ( 1 ... 1 ) ( ( ( A + ( W - D ) ) + ( d ` i ) ) (AP ` K ) ( d ` i ) ) C_ ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) } ) <-> A. i e. ( 1 ... 1 ) ( ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) (AP ` K ) ( { <. 1 , D >. } ` 1 ) ) C_ ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) } ) ) )
198	193	mpteq2dva 4744	. . . . . . . 8 |- ( d = { <. 1 , D >. } -> ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) ) = ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) )
199	198	rneqd 5353	. . . . . . 7 |- ( d = { <. 1 , D >. } -> ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) ) = ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) )
200	199	fveq2d 6195	. . . . . 6 |- ( d = { <. 1 , D >. } -> ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) ) ) = ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) ) )
201	200	eqeq1d 2624	. . . . 5 |- ( d = { <. 1 , D >. } -> ( ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) ) ) = 1 <-> ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) ) = 1 ) )
202	197, 201	anbi12d 747	. . . 4 |- ( d = { <. 1 , D >. } -> ( ( A. i e. ( 1 ... 1 ) ( ( ( A + ( W - D ) ) + ( d ` i ) ) (AP ` K ) ( d ` i ) ) C_ ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( d ` i ) ) ) ) ) = 1 ) <-> ( A. i e. ( 1 ... 1 ) ( ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) (AP ` K ) ( { <. 1 , D >. } ` 1 ) ) C_ ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) ) = 1 ) ) )
203	186, 202	rspc2ev 3324	. . 3 |- ( ( ( A + ( W - D ) ) e. NN /\ { <. 1 , D >. } e. ( NN ^m ( 1 ... 1 ) ) /\ ( A. i e. ( 1 ... 1 ) ( ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) (AP ` K ) ( { <. 1 , D >. } ` 1 ) ) C_ ( `' F " { ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( ( A + ( W - D ) ) + ( { <. 1 , D >. } ` 1 ) ) ) ) ) = 1 ) ) -> E. a e. NN E. d e. ( NN ^m ( 1 ... 1 ) ) ( A. i e. ( 1 ... 1 ) ( ( a + ( d ` i ) ) (AP ` K ) ( d ` i ) ) C_ ( `' F " { ( F ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( a + ( d ` i ) ) ) ) ) = 1 ) )
204	50, 66, 159, 174, 203	syl112anc 1330	. 2 |- ( ph -> E. a e. NN E. d e. ( NN ^m ( 1 ... 1 ) ) ( A. i e. ( 1 ... 1 ) ( ( a + ( d ` i ) ) (AP ` K ) ( d ` i ) ) C_ ( `' F " { ( F ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( a + ( d ` i ) ) ) ) ) = 1 ) )
205		ovex 6678	. . 3 |- ( 1 ... ( 2 x. W ) ) e. _V
206	51	a1i 11	. . 3 |- ( ph -> 1 e. NN )
207		eqid 2622	. . 3 |- ( 1 ... 1 ) = ( 1 ... 1 )
208	205, 84, 127, 206, 207	vdwpc 15684	. 2 |- ( ph -> ( <. 1 , K >. PolyAP F <-> E. a e. NN E. d e. ( NN ^m ( 1 ... 1 ) ) ( A. i e. ( 1 ... 1 ) ( ( a + ( d ` i ) ) (AP ` K ) ( d ` i ) ) C_ ( `' F " { ( F ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. ( 1 ... 1 ) |-> ( F ` ( a + ( d ` i ) ) ) ) ) = 1 ) ) )
209	204, 208	mpbird 247	1 |- ( ph -> <. 1 , K >. PolyAP F )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   u. cun 3572   C_ wss 3574   (/)c0 3915   {csn 4177   <.cop 4183   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   `'ccnv 5113   dom cdm 5114   ran crn 5115   "cima 5117   Fn wfn 5883   -->wf 5884   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   ^m cmap 7857   Fincfn 7955   CCcc 9934   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   - cmin 10266   NNcn 11020   2c2 11070   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   ...cfz 12326   #chash 13117  APcvdwa 15669   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-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-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-card 8765  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-fz 12327  df-hash 13118  df-vdwap 15672  df-vdwpc 15674

This theorem is referenced by:  vdwlem10  15694