vdwlem6

	Ref	Expression
Hypotheses	vdwlem3.v	$⊢ φ \to V \in ℕ$
	vdwlem3.w	$⊢ φ \to W \in ℕ$
	vdwlem4.r	$⊢ φ \to R \in Fin$
	vdwlem4.h	$⊢ φ \to H : (1 \dots W 2 V) ⟶ R$
	vdwlem4.f	$⊢ F = (x \in (1 \dots V) ⟼ (y \in (1 \dots W) ⟼ H (y + W (x - 1 + V))))$
	vdwlem7.m	$⊢ φ \to M \in ℕ$
	vdwlem7.g	$⊢ φ \to G : (1 \dots W) ⟶ R$
	vdwlem7.k	$⊢ φ \to K \in ℤ_{\geq 2}$
	vdwlem7.a	$⊢ φ \to A \in ℕ$
	vdwlem7.d	$⊢ φ \to D \in ℕ$
	vdwlem7.s	$⊢ φ \to A AP (K) D \subseteq F^{-1} [\{G\}]$
	vdwlem6.b	$⊢ φ \to B \in ℕ$
	vdwlem6.e	$⊢ φ \to E : (1 \dots M) ⟶ ℕ$
	vdwlem6.s	$⊢ φ \to \forall i \in (1 \dots M) (B + E (i)) AP (K) E (i) \subseteq G^{-1} [\{G (B + E (i))\}]$
	vdwlem6.j	$⊢ J = (i \in (1 \dots M) ⟼ G (B + E (i)))$
	vdwlem6.r	$⊢ φ \to \|ran J\| = M$
	vdwlem6.t	$⊢ T = B + W (A + (V - D) - 1)$
	vdwlem6.p	$⊢ P = (j \in (1 \dots M + 1) ⟼ if (j = M + 1, 0, E (j)) + W D)$
Assertion	vdwlem6	$⊢ φ \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP G)$

Proof

Step	Hyp	Ref	Expression
1		vdwlem3.v	$⊢ φ \to V \in ℕ$
2		vdwlem3.w	$⊢ φ \to W \in ℕ$
3		vdwlem4.r	$⊢ φ \to R \in Fin$
4		vdwlem4.h	$⊢ φ \to H : (1 \dots W 2 V) ⟶ R$
5		vdwlem4.f	$⊢ F = (x \in (1 \dots V) ⟼ (y \in (1 \dots W) ⟼ H (y + W (x - 1 + V))))$
6		vdwlem7.m	$⊢ φ \to M \in ℕ$
7		vdwlem7.g	$⊢ φ \to G : (1 \dots W) ⟶ R$
8		vdwlem7.k	$⊢ φ \to K \in ℤ_{\geq 2}$
9		vdwlem7.a	$⊢ φ \to A \in ℕ$
10		vdwlem7.d	$⊢ φ \to D \in ℕ$
11		vdwlem7.s	$⊢ φ \to A AP (K) D \subseteq F^{-1} [\{G\}]$
12		vdwlem6.b	$⊢ φ \to B \in ℕ$
13		vdwlem6.e	$⊢ φ \to E : (1 \dots M) ⟶ ℕ$
14		vdwlem6.s	$⊢ φ \to \forall i \in (1 \dots M) (B + E (i)) AP (K) E (i) \subseteq G^{-1} [\{G (B + E (i))\}]$
15		vdwlem6.j	$⊢ J = (i \in (1 \dots M) ⟼ G (B + E (i)))$
16		vdwlem6.r	$⊢ φ \to \|ran J\| = M$
17		vdwlem6.t	$⊢ T = B + W (A + (V - D) - 1)$
18		vdwlem6.p	$⊢ P = (j \in (1 \dots M + 1) ⟼ if (j = M + 1, 0, E (j)) + W D)$
19		fvex	$⊢ G (B + E (i)) \in V$
20	19 15	fnmpti	$⊢ J Fn (1 \dots M)$
21		fvelrnb	$⊢ J Fn (1 \dots M) \to (G (B) \in ran J \leftrightarrow \exists m \in (1 \dots M) J (m) = G (B))$
22	20 21	ax-mp	$⊢ G (B) \in ran J \leftrightarrow \exists m \in (1 \dots M) J (m) = G (B)$
23	3	adantr	$⊢ (φ \land (m \in (1 \dots M) \land J (m) = G (B))) \to R \in Fin$
24		eluz2nn	$⊢ K \in ℤ_{\geq 2} \to K \in ℕ$
25	8 24	syl	$⊢ φ \to K \in ℕ$
26	25	adantr	$⊢ (φ \land (m \in (1 \dots M) \land J (m) = G (B))) \to K \in ℕ$
27	2	adantr	$⊢ (φ \land (m \in (1 \dots M) \land J (m) = G (B))) \to W \in ℕ$
28	7	adantr	$⊢ (φ \land (m \in (1 \dots M) \land J (m) = G (B))) \to G : (1 \dots W) ⟶ R$
29	12	adantr	$⊢ (φ \land (m \in (1 \dots M) \land J (m) = G (B))) \to B \in ℕ$
30	6	adantr	$⊢ (φ \land (m \in (1 \dots M) \land J (m) = G (B))) \to M \in ℕ$
31	13	adantr	$⊢ (φ \land (m \in (1 \dots M) \land J (m) = G (B))) \to E : (1 \dots M) ⟶ ℕ$
32	14	adantr	$⊢ (φ \land (m \in (1 \dots M) \land J (m) = G (B))) \to \forall i \in (1 \dots M) (B + E (i)) AP (K) E (i) \subseteq G^{-1} [\{G (B + E (i))\}]$
33		simprl	$⊢ (φ \land (m \in (1 \dots M) \land J (m) = G (B))) \to m \in (1 \dots M)$
34		simprr	$⊢ (φ \land (m \in (1 \dots M) \land J (m) = G (B))) \to J (m) = G (B)$
35		fveq2	$⊢ i = m \to E (i) = E (m)$
36	35	oveq2d	$⊢ i = m \to B + E (i) = B + E (m)$
37	36	fveq2d	$⊢ i = m \to G (B + E (i)) = G (B + E (m))$
38		fvex	$⊢ G (B + E (m)) \in V$
39	37 15 38	fvmpt	$⊢ m \in (1 \dots M) \to J (m) = G (B + E (m))$
40	33 39	syl	$⊢ (φ \land (m \in (1 \dots M) \land J (m) = G (B))) \to J (m) = G (B + E (m))$
41	34 40	eqtr3d	$⊢ (φ \land (m \in (1 \dots M) \land J (m) = G (B))) \to G (B) = G (B + E (m))$
42	23 26 27 28 29 30 31 32 33 41	vdwlem1	$⊢ (φ \land (m \in (1 \dots M) \land J (m) = G (B))) \to (K + 1) MonoAP G$
43	42	rexlimdvaa	$⊢ φ \to (\exists m \in (1 \dots M) J (m) = G (B) \to (K + 1) MonoAP G)$
44	22 43	syl5bi	$⊢ φ \to (G (B) \in ran J \to (K + 1) MonoAP G)$
45	44	imp	$⊢ (φ \land G (B) \in ran J) \to (K + 1) MonoAP G$
46	45	olcd	$⊢ (φ \land G (B) \in ran J) \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP G)$
47	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	vdwlem5	$⊢ φ \to T \in ℕ$
48	47	adantr	$⊢ (φ \land \neg G (B) \in ran J) \to T \in ℕ$
49		0nn0	$⊢ 0 \in ℕ_{0}$
50	49	a1i	$⊢ (((φ \land \neg G (B) \in ran J) \land j \in (1 \dots M + 1)) \land j = M + 1) \to 0 \in ℕ_{0}$
51		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
52	6 51	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 1}$
53	52	adantr	$⊢ (φ \land \neg G (B) \in ran J) \to M \in ℤ_{\geq 1}$
54		elfzp1	$⊢ M \in ℤ_{\geq 1} \to (j \in (1 \dots M + 1) \leftrightarrow (j \in (1 \dots M) \lor j = M + 1))$
55	53 54	syl	$⊢ (φ \land \neg G (B) \in ran J) \to (j \in (1 \dots M + 1) \leftrightarrow (j \in (1 \dots M) \lor j = M + 1))$
56	55	biimpa	$⊢ ((φ \land \neg G (B) \in ran J) \land j \in (1 \dots M + 1)) \to (j \in (1 \dots M) \lor j = M + 1)$
57	56	ord	$⊢ ((φ \land \neg G (B) \in ran J) \land j \in (1 \dots M + 1)) \to (\neg j \in (1 \dots M) \to j = M + 1)$
58	57	con1d	$⊢ ((φ \land \neg G (B) \in ran J) \land j \in (1 \dots M + 1)) \to (\neg j = M + 1 \to j \in (1 \dots M))$
59	58	imp	$⊢ (((φ \land \neg G (B) \in ran J) \land j \in (1 \dots M + 1)) \land \neg j = M + 1) \to j \in (1 \dots M)$
60	13	ad2antrr	$⊢ ((φ \land \neg G (B) \in ran J) \land j \in (1 \dots M + 1)) \to E : (1 \dots M) ⟶ ℕ$
61	60	ffvelrnda	$⊢ (((φ \land \neg G (B) \in ran J) \land j \in (1 \dots M + 1)) \land j \in (1 \dots M)) \to E (j) \in ℕ$
62	61	nnnn0d	$⊢ (((φ \land \neg G (B) \in ran J) \land j \in (1 \dots M + 1)) \land j \in (1 \dots M)) \to E (j) \in ℕ_{0}$
63	59 62	syldan	$⊢ (((φ \land \neg G (B) \in ran J) \land j \in (1 \dots M + 1)) \land \neg j = M + 1) \to E (j) \in ℕ_{0}$
64	50 63	ifclda	$⊢ ((φ \land \neg G (B) \in ran J) \land j \in (1 \dots M + 1)) \to if (j = M + 1, 0, E (j)) \in ℕ_{0}$
65	2 10	nnmulcld	$⊢ φ \to W D \in ℕ$
66	65	ad2antrr	$⊢ ((φ \land \neg G (B) \in ran J) \land j \in (1 \dots M + 1)) \to W D \in ℕ$
67		nn0nnaddcl	$⊢ (if (j = M + 1, 0, E (j)) \in ℕ_{0} \land W D \in ℕ) \to if (j = M + 1, 0, E (j)) + W D \in ℕ$
68	64 66 67	syl2anc	$⊢ ((φ \land \neg G (B) \in ran J) \land j \in (1 \dots M + 1)) \to if (j = M + 1, 0, E (j)) + W D \in ℕ$
69	68 18	fmptd	$⊢ (φ \land \neg G (B) \in ran J) \to P : (1 \dots M + 1) ⟶ ℕ$
70		nnex	$⊢ ℕ \in V$
71		ovex	$⊢ (1 \dots M + 1) \in V$
72	70 71	elmap	$⊢ P \in (ℕ^{(1 \dots M + 1)}) \leftrightarrow P : (1 \dots M + 1) ⟶ ℕ$
73	69 72	sylibr	$⊢ (φ \land \neg G (B) \in ran J) \to P \in (ℕ^{(1 \dots M + 1)})$
74		elfzp1	$⊢ M \in ℤ_{\geq 1} \to (i \in (1 \dots M + 1) \leftrightarrow (i \in (1 \dots M) \lor i = M + 1))$
75	52 74	syl	$⊢ φ \to (i \in (1 \dots M + 1) \leftrightarrow (i \in (1 \dots M) \lor i = M + 1))$
76	12	adantr	$⊢ (φ \land i \in (1 \dots M)) \to B \in ℕ$
77	76	nncnd	$⊢ (φ \land i \in (1 \dots M)) \to B \in ℂ$
78	77	adantr	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to B \in ℂ$
79	13	ffvelrnda	$⊢ (φ \land i \in (1 \dots M)) \to E (i) \in ℕ$
80	79	nncnd	$⊢ (φ \land i \in (1 \dots M)) \to E (i) \in ℂ$
81	80	adantr	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to E (i) \in ℂ$
82	78 81	addcld	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to B + E (i) \in ℂ$
83		nnm1nn0	$⊢ A \in ℕ \to A - 1 \in ℕ_{0}$
84	9 83	syl	$⊢ φ \to A - 1 \in ℕ_{0}$
85		nn0nnaddcl	$⊢ (A - 1 \in ℕ_{0} \land V \in ℕ) \to A - 1 + V \in ℕ$
86	84 1 85	syl2anc	$⊢ φ \to A - 1 + V \in ℕ$
87	2 86	nnmulcld	$⊢ φ \to W (A - 1 + V) \in ℕ$
88	87	nncnd	$⊢ φ \to W (A - 1 + V) \in ℂ$
89	88	ad2antrr	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to W (A - 1 + V) \in ℂ$
90		elfznn0	$⊢ m \in (0 \dots K - 1) \to m \in ℕ_{0}$
91	90	adantl	$⊢ (φ \land m \in (0 \dots K - 1)) \to m \in ℕ_{0}$
92	91	nn0cnd	$⊢ (φ \land m \in (0 \dots K - 1)) \to m \in ℂ$
93	92	adantlr	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to m \in ℂ$
94	93 81	mulcld	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to m E (i) \in ℂ$
95	65	nnnn0d	$⊢ φ \to W D \in ℕ_{0}$
96	95	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to W D \in ℕ_{0}$
97	91 96	nn0mulcld	$⊢ (φ \land m \in (0 \dots K - 1)) \to m W D \in ℕ_{0}$
98	97	nn0cnd	$⊢ (φ \land m \in (0 \dots K - 1)) \to m W D \in ℂ$
99	98	adantlr	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to m W D \in ℂ$
100	82 89 94 99	add4d	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to (B + E (i)) + W (A - 1 + V) + m E (i) + m W D = (B + E (i)) + m E (i) + W (A - 1 + V) + m W D$
101	65	nncnd	$⊢ φ \to W D \in ℂ$
102	101	ad2antrr	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to W D \in ℂ$
103	93 81 102	adddid	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to m (E (i) + W D) = m E (i) + m W D$
104	103	oveq2d	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to (B + E (i)) + W (A - 1 + V) + m (E (i) + W D) = (B + E (i)) + W (A - 1 + V) + m E (i) + m W D$
105	2	nncnd	$⊢ φ \to W \in ℂ$
106	105	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to W \in ℂ$
107	86	nncnd	$⊢ φ \to A - 1 + V \in ℂ$
108	107	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to A - 1 + V \in ℂ$
109	10	nncnd	$⊢ φ \to D \in ℂ$
110	109	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to D \in ℂ$
111	92 110	mulcld	$⊢ (φ \land m \in (0 \dots K - 1)) \to m D \in ℂ$
112	106 108 111	adddid	$⊢ (φ \land m \in (0 \dots K - 1)) \to W ((A - 1) + V + m D) = W (A - 1 + V) + W m D$
113	9	nncnd	$⊢ φ \to A \in ℂ$
114	113	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to A \in ℂ$
115		1cnd	$⊢ (φ \land m \in (0 \dots K - 1)) \to 1 \in ℂ$
116	114 111 115	addsubd	$⊢ (φ \land m \in (0 \dots K - 1)) \to A + m D - 1 = A - 1 + m D$
117	116	oveq1d	$⊢ (φ \land m \in (0 \dots K - 1)) \to (A + m D) - 1 + V = (A - 1) + m D + V$
118	84	nn0cnd	$⊢ φ \to A - 1 \in ℂ$
119	118	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to A - 1 \in ℂ$
120	1	nncnd	$⊢ φ \to V \in ℂ$
121	120	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to V \in ℂ$
122	119 111 121	add32d	$⊢ (φ \land m \in (0 \dots K - 1)) \to (A - 1) + m D + V = (A - 1) + V + m D$
123	117 122	eqtrd	$⊢ (φ \land m \in (0 \dots K - 1)) \to (A + m D) - 1 + V = (A - 1) + V + m D$
124	123	oveq2d	$⊢ (φ \land m \in (0 \dots K - 1)) \to W ((A + m D) - 1 + V) = W ((A - 1) + V + m D)$
125	92 106 110	mul12d	$⊢ (φ \land m \in (0 \dots K - 1)) \to m W D = W m D$
126	125	oveq2d	$⊢ (φ \land m \in (0 \dots K - 1)) \to W (A - 1 + V) + m W D = W (A - 1 + V) + W m D$
127	112 124 126	3eqtr4d	$⊢ (φ \land m \in (0 \dots K - 1)) \to W ((A + m D) - 1 + V) = W (A - 1 + V) + m W D$
128	127	adantlr	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to W ((A + m D) - 1 + V) = W (A - 1 + V) + m W D$
129	128	oveq2d	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to (B + E (i)) + m E (i) + W ((A + m D) - 1 + V) = (B + E (i)) + m E (i) + W (A - 1 + V) + m W D$
130	100 104 129	3eqtr4d	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to (B + E (i)) + W (A - 1 + V) + m (E (i) + W D) = (B + E (i)) + m E (i) + W ((A + m D) - 1 + V)$
131	1	ad2antrr	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to V \in ℕ$
132	2	ad2antrr	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to W \in ℕ$
133	11	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to A AP (K) D \subseteq F^{-1} [\{G\}]$
134		eqid	$⊢ A + m D = A + m D$
135		oveq1	$⊢ n = m \to n D = m D$
136	135	oveq2d	$⊢ n = m \to A + n D = A + m D$
137	136	rspceeqv	$⊢ (m \in (0 \dots K - 1) \land A + m D = A + m D) \to \exists n \in (0 \dots K - 1) A + m D = A + n D$
138	134 137	mpan2	$⊢ m \in (0 \dots K - 1) \to \exists n \in (0 \dots K - 1) A + m D = A + n D$
139	25	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
140		vdwapval	$⊢ (K \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to (A + m D \in (A AP (K) D) \leftrightarrow \exists n \in (0 \dots K - 1) A + m D = A + n D)$
141	139 9 10 140	syl3anc	$⊢ φ \to (A + m D \in (A AP (K) D) \leftrightarrow \exists n \in (0 \dots K - 1) A + m D = A + n D)$
142	141	biimpar	$⊢ (φ \land \exists n \in (0 \dots K - 1) A + m D = A + n D) \to A + m D \in (A AP (K) D)$
143	138 142	sylan2	$⊢ (φ \land m \in (0 \dots K - 1)) \to A + m D \in (A AP (K) D)$
144	133 143	sseldd	$⊢ (φ \land m \in (0 \dots K - 1)) \to A + m D \in F^{-1} [\{G\}]$
145	1 2 3 4 5	vdwlem4	$⊢ φ \to F : (1 \dots V) ⟶ R^{(1 \dots W)}$
146	145	ffnd	$⊢ φ \to F Fn (1 \dots V)$
147		fniniseg	$⊢ F Fn (1 \dots V) \to (A + m D \in F^{-1} [\{G\}] \leftrightarrow (A + m D \in (1 \dots V) \land F (A + m D) = G))$
148	146 147	syl	$⊢ φ \to (A + m D \in F^{-1} [\{G\}] \leftrightarrow (A + m D \in (1 \dots V) \land F (A + m D) = G))$
149	148	biimpa	$⊢ (φ \land A + m D \in F^{-1} [\{G\}]) \to (A + m D \in (1 \dots V) \land F (A + m D) = G)$
150	144 149	syldan	$⊢ (φ \land m \in (0 \dots K - 1)) \to (A + m D \in (1 \dots V) \land F (A + m D) = G)$
151	150	simpld	$⊢ (φ \land m \in (0 \dots K - 1)) \to A + m D \in (1 \dots V)$
152	151	adantlr	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to A + m D \in (1 \dots V)$
153	14	r19.21bi	$⊢ (φ \land i \in (1 \dots M)) \to (B + E (i)) AP (K) E (i) \subseteq G^{-1} [\{G (B + E (i))\}]$
154	153	adantr	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to (B + E (i)) AP (K) E (i) \subseteq G^{-1} [\{G (B + E (i))\}]$
155		eqid	$⊢ B + E (i) + m E (i) = B + E (i) + m E (i)$
156		oveq1	$⊢ n = m \to n E (i) = m E (i)$
157	156	oveq2d	$⊢ n = m \to B + E (i) + n E (i) = B + E (i) + m E (i)$
158	157	rspceeqv	$⊢ (m \in (0 \dots K - 1) \land B + E (i) + m E (i) = B + E (i) + m E (i)) \to \exists n \in (0 \dots K - 1) B + E (i) + m E (i) = B + E (i) + n E (i)$
159	155 158	mpan2	$⊢ m \in (0 \dots K - 1) \to \exists n \in (0 \dots K - 1) B + E (i) + m E (i) = B + E (i) + n E (i)$
160	25	adantr	$⊢ (φ \land i \in (1 \dots M)) \to K \in ℕ$
161	160	nnnn0d	$⊢ (φ \land i \in (1 \dots M)) \to K \in ℕ_{0}$
162	76 79	nnaddcld	$⊢ (φ \land i \in (1 \dots M)) \to B + E (i) \in ℕ$
163		vdwapval	$⊢ (K \in ℕ_{0} \land B + E (i) \in ℕ \land E (i) \in ℕ) \to (B + E (i) + m E (i) \in ((B + E (i)) AP (K) E (i)) \leftrightarrow \exists n \in (0 \dots K - 1) B + E (i) + m E (i) = B + E (i) + n E (i))$
164	161 162 79 163	syl3anc	$⊢ (φ \land i \in (1 \dots M)) \to (B + E (i) + m E (i) \in ((B + E (i)) AP (K) E (i)) \leftrightarrow \exists n \in (0 \dots K - 1) B + E (i) + m E (i) = B + E (i) + n E (i))$
165	164	biimpar	$⊢ ((φ \land i \in (1 \dots M)) \land \exists n \in (0 \dots K - 1) B + E (i) + m E (i) = B + E (i) + n E (i)) \to B + E (i) + m E (i) \in ((B + E (i)) AP (K) E (i))$
166	159 165	sylan2	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to B + E (i) + m E (i) \in ((B + E (i)) AP (K) E (i))$
167	154 166	sseldd	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to B + E (i) + m E (i) \in G^{-1} [\{G (B + E (i))\}]$
168	7	ffnd	$⊢ φ \to G Fn (1 \dots W)$
169	168	adantr	$⊢ (φ \land i \in (1 \dots M)) \to G Fn (1 \dots W)$
170		fniniseg	$⊢ G Fn (1 \dots W) \to (B + E (i) + m E (i) \in G^{-1} [\{G (B + E (i))\}] \leftrightarrow (B + E (i) + m E (i) \in (1 \dots W) \land G (B + E (i) + m E (i)) = G (B + E (i))))$
171	169 170	syl	$⊢ (φ \land i \in (1 \dots M)) \to (B + E (i) + m E (i) \in G^{-1} [\{G (B + E (i))\}] \leftrightarrow (B + E (i) + m E (i) \in (1 \dots W) \land G (B + E (i) + m E (i)) = G (B + E (i))))$
172	171	biimpa	$⊢ ((φ \land i \in (1 \dots M)) \land B + E (i) + m E (i) \in G^{-1} [\{G (B + E (i))\}]) \to (B + E (i) + m E (i) \in (1 \dots W) \land G (B + E (i) + m E (i)) = G (B + E (i)))$
173	167 172	syldan	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to (B + E (i) + m E (i) \in (1 \dots W) \land G (B + E (i) + m E (i)) = G (B + E (i)))$
174	173	simpld	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to B + E (i) + m E (i) \in (1 \dots W)$
175	131 132 152 174	vdwlem3	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to (B + E (i)) + m E (i) + W ((A + m D) - 1 + V) \in (1 \dots W 2 V)$
176	130 175	eqeltrd	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to (B + E (i)) + W (A - 1 + V) + m (E (i) + W D) \in (1 \dots W 2 V)$
177		fvoveq1	$⊢ y = B + E (i) + m E (i) \to H (y + W ((A + m D) - 1 + V)) = H ((B + E (i)) + m E (i) + W ((A + m D) - 1 + V))$
178		eqid	$⊢ (y \in (1 \dots W) ⟼ H (y + W ((A + m D) - 1 + V))) = (y \in (1 \dots W) ⟼ H (y + W ((A + m D) - 1 + V)))$
179		fvex	$⊢ H ((B + E (i)) + m E (i) + W ((A + m D) - 1 + V)) \in V$
180	177 178 179	fvmpt	$⊢ B + E (i) + m E (i) \in (1 \dots W) \to (y \in (1 \dots W) ⟼ H (y + W ((A + m D) - 1 + V))) (B + E (i) + m E (i)) = H ((B + E (i)) + m E (i) + W ((A + m D) - 1 + V))$
181	174 180	syl	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to (y \in (1 \dots W) ⟼ H (y + W ((A + m D) - 1 + V))) (B + E (i) + m E (i)) = H ((B + E (i)) + m E (i) + W ((A + m D) - 1 + V))$
182	173	simprd	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to G (B + E (i) + m E (i)) = G (B + E (i))$
183	150	simprd	$⊢ (φ \land m \in (0 \dots K - 1)) \to F (A + m D) = G$
184		oveq1	$⊢ x = A + m D \to x - 1 = A + m D - 1$
185	184	oveq1d	$⊢ x = A + m D \to x - 1 + V = (A + m D) - 1 + V$
186	185	oveq2d	$⊢ x = A + m D \to W (x - 1 + V) = W ((A + m D) - 1 + V)$
187	186	oveq2d	$⊢ x = A + m D \to y + W (x - 1 + V) = y + W ((A + m D) - 1 + V)$
188	187	fveq2d	$⊢ x = A + m D \to H (y + W (x - 1 + V)) = H (y + W ((A + m D) - 1 + V))$
189	188	mpteq2dv	$⊢ x = A + m D \to (y \in (1 \dots W) ⟼ H (y + W (x - 1 + V))) = (y \in (1 \dots W) ⟼ H (y + W ((A + m D) - 1 + V)))$
190		ovex	$⊢ (1 \dots W) \in V$
191	190	mptex	$⊢ (y \in (1 \dots W) ⟼ H (y + W ((A + m D) - 1 + V))) \in V$
192	189 5 191	fvmpt	$⊢ A + m D \in (1 \dots V) \to F (A + m D) = (y \in (1 \dots W) ⟼ H (y + W ((A + m D) - 1 + V)))$
193	151 192	syl	$⊢ (φ \land m \in (0 \dots K - 1)) \to F (A + m D) = (y \in (1 \dots W) ⟼ H (y + W ((A + m D) - 1 + V)))$
194	183 193	eqtr3d	$⊢ (φ \land m \in (0 \dots K - 1)) \to G = (y \in (1 \dots W) ⟼ H (y + W ((A + m D) - 1 + V)))$
195	194	adantlr	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to G = (y \in (1 \dots W) ⟼ H (y + W ((A + m D) - 1 + V)))$
196	195	fveq1d	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to G (B + E (i) + m E (i)) = (y \in (1 \dots W) ⟼ H (y + W ((A + m D) - 1 + V))) (B + E (i) + m E (i))$
197	182 196	eqtr3d	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to G (B + E (i)) = (y \in (1 \dots W) ⟼ H (y + W ((A + m D) - 1 + V))) (B + E (i) + m E (i))$
198	130	fveq2d	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to H ((B + E (i)) + W (A - 1 + V) + m (E (i) + W D)) = H ((B + E (i)) + m E (i) + W ((A + m D) - 1 + V))$
199	181 197 198	3eqtr4rd	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to H ((B + E (i)) + W (A - 1 + V) + m (E (i) + W D)) = G (B + E (i))$
200	176 199	jca	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to ((B + E (i)) + W (A - 1 + V) + m (E (i) + W D) \in (1 \dots W 2 V) \land H ((B + E (i)) + W (A - 1 + V) + m (E (i) + W D)) = G (B + E (i)))$
201		eleq1	$⊢ x = (B + E (i)) + W (A - 1 + V) + m (E (i) + W D) \to (x \in (1 \dots W 2 V) \leftrightarrow (B + E (i)) + W (A - 1 + V) + m (E (i) + W D) \in (1 \dots W 2 V))$
202		fveqeq2	$⊢ x = (B + E (i)) + W (A - 1 + V) + m (E (i) + W D) \to (H (x) = G (B + E (i)) \leftrightarrow H ((B + E (i)) + W (A - 1 + V) + m (E (i) + W D)) = G (B + E (i)))$
203	201 202	anbi12d	$⊢ x = (B + E (i)) + W (A - 1 + V) + m (E (i) + W D) \to ((x \in (1 \dots W 2 V) \land H (x) = G (B + E (i))) \leftrightarrow ((B + E (i)) + W (A - 1 + V) + m (E (i) + W D) \in (1 \dots W 2 V) \land H ((B + E (i)) + W (A - 1 + V) + m (E (i) + W D)) = G (B + E (i))))$
204	200 203	syl5ibrcom	$⊢ ((φ \land i \in (1 \dots M)) \land m \in (0 \dots K - 1)) \to (x = (B + E (i)) + W (A - 1 + V) + m (E (i) + W D) \to (x \in (1 \dots W 2 V) \land H (x) = G (B + E (i))))$
205	204	rexlimdva	$⊢ (φ \land i \in (1 \dots M)) \to (\exists m \in (0 \dots K - 1) x = (B + E (i)) + W (A - 1 + V) + m (E (i) + W D) \to (x \in (1 \dots W 2 V) \land H (x) = G (B + E (i))))$
206	87	adantr	$⊢ (φ \land i \in (1 \dots M)) \to W (A - 1 + V) \in ℕ$
207	162 206	nnaddcld	$⊢ (φ \land i \in (1 \dots M)) \to B + E (i) + W (A - 1 + V) \in ℕ$
208	65	adantr	$⊢ (φ \land i \in (1 \dots M)) \to W D \in ℕ$
209	79 208	nnaddcld	$⊢ (φ \land i \in (1 \dots M)) \to E (i) + W D \in ℕ$
210		vdwapval	$⊢ (K \in ℕ_{0} \land B + E (i) + W (A - 1 + V) \in ℕ \land E (i) + W D \in ℕ) \to (x \in ((B + E (i) + W (A - 1 + V)) AP (K) (E (i) + W D)) \leftrightarrow \exists m \in (0 \dots K - 1) x = (B + E (i)) + W (A - 1 + V) + m (E (i) + W D))$
211	161 207 209 210	syl3anc	$⊢ (φ \land i \in (1 \dots M)) \to (x \in ((B + E (i) + W (A - 1 + V)) AP (K) (E (i) + W D)) \leftrightarrow \exists m \in (0 \dots K - 1) x = (B + E (i)) + W (A - 1 + V) + m (E (i) + W D))$
212	4	ffnd	$⊢ φ \to H Fn (1 \dots W 2 V)$
213	212	adantr	$⊢ (φ \land i \in (1 \dots M)) \to H Fn (1 \dots W 2 V)$
214		fniniseg	$⊢ H Fn (1 \dots W 2 V) \to (x \in H^{-1} [\{G (B + E (i))\}] \leftrightarrow (x \in (1 \dots W 2 V) \land H (x) = G (B + E (i))))$
215	213 214	syl	$⊢ (φ \land i \in (1 \dots M)) \to (x \in H^{-1} [\{G (B + E (i))\}] \leftrightarrow (x \in (1 \dots W 2 V) \land H (x) = G (B + E (i))))$
216	205 211 215	3imtr4d	$⊢ (φ \land i \in (1 \dots M)) \to (x \in ((B + E (i) + W (A - 1 + V)) AP (K) (E (i) + W D)) \to x \in H^{-1} [\{G (B + E (i))\}])$
217	216	ssrdv	$⊢ (φ \land i \in (1 \dots M)) \to (B + E (i) + W (A - 1 + V)) AP (K) (E (i) + W D) \subseteq H^{-1} [\{G (B + E (i))\}]$
218		ssun1	$⊢ (1 \dots M) \subseteq (1 \dots M) \cup \{M + 1\}$
219		fzsuc	$⊢ M \in ℤ_{\geq 1} \to (1 \dots M + 1) = (1 \dots M) \cup \{M + 1\}$
220	52 219	syl	$⊢ φ \to (1 \dots M + 1) = (1 \dots M) \cup \{M + 1\}$
221	218 220	sseqtrrid	$⊢ φ \to (1 \dots M) \subseteq (1 \dots M + 1)$
222	221	sselda	$⊢ (φ \land i \in (1 \dots M)) \to i \in (1 \dots M + 1)$
223		eqeq1	$⊢ j = i \to (j = M + 1 \leftrightarrow i = M + 1)$
224		fveq2	$⊢ j = i \to E (j) = E (i)$
225	223 224	ifbieq2d	$⊢ j = i \to if (j = M + 1, 0, E (j)) = if (i = M + 1, 0, E (i))$
226	225	oveq1d	$⊢ j = i \to if (j = M + 1, 0, E (j)) + W D = if (i = M + 1, 0, E (i)) + W D$
227		ovex	$⊢ if (i = M + 1, 0, E (i)) + W D \in V$
228	226 18 227	fvmpt	$⊢ i \in (1 \dots M + 1) \to P (i) = if (i = M + 1, 0, E (i)) + W D$
229	222 228	syl	$⊢ (φ \land i \in (1 \dots M)) \to P (i) = if (i = M + 1, 0, E (i)) + W D$
230	6	nnred	$⊢ φ \to M \in ℝ$
231	230	ltp1d	$⊢ φ \to M < M + 1$
232		peano2re	$⊢ M \in ℝ \to M + 1 \in ℝ$
233	230 232	syl	$⊢ φ \to M + 1 \in ℝ$
234	230 233	ltnled	$⊢ φ \to (M < M + 1 \leftrightarrow \neg M + 1 \leq M)$
235	231 234	mpbid	$⊢ φ \to \neg M + 1 \leq M$
236		breq1	$⊢ i = M + 1 \to (i \leq M \leftrightarrow M + 1 \leq M)$
237	236	notbid	$⊢ i = M + 1 \to (\neg i \leq M \leftrightarrow \neg M + 1 \leq M)$
238	235 237	syl5ibrcom	$⊢ φ \to (i = M + 1 \to \neg i \leq M)$
239	238	con2d	$⊢ φ \to (i \leq M \to \neg i = M + 1)$
240		elfzle2	$⊢ i \in (1 \dots M) \to i \leq M$
241	239 240	impel	$⊢ (φ \land i \in (1 \dots M)) \to \neg i = M + 1$
242		iffalse	$⊢ \neg i = M + 1 \to if (i = M + 1, 0, E (i)) = E (i)$
243	242	oveq1d	$⊢ \neg i = M + 1 \to if (i = M + 1, 0, E (i)) + W D = E (i) + W D$
244	241 243	syl	$⊢ (φ \land i \in (1 \dots M)) \to if (i = M + 1, 0, E (i)) + W D = E (i) + W D$
245	229 244	eqtrd	$⊢ (φ \land i \in (1 \dots M)) \to P (i) = E (i) + W D$
246	245	oveq2d	$⊢ (φ \land i \in (1 \dots M)) \to T + P (i) = T + E (i) + W D$
247	47	nncnd	$⊢ φ \to T \in ℂ$
248	247	adantr	$⊢ (φ \land i \in (1 \dots M)) \to T \in ℂ$
249	101	adantr	$⊢ (φ \land i \in (1 \dots M)) \to W D \in ℂ$
250	248 80 249	add12d	$⊢ (φ \land i \in (1 \dots M)) \to T + E (i) + W D = E (i) + T + W D$
251	17	oveq1i	$⊢ T + W D = B + W (A + (V - D) - 1) + W D$
252	12	nncnd	$⊢ φ \to B \in ℂ$
253	120 109	subcld	$⊢ φ \to V - D \in ℂ$
254	113 253	addcld	$⊢ φ \to A + V - D \in ℂ$
255		ax-1cn	$⊢ 1 \in ℂ$
256		subcl	$⊢ (A + V - D \in ℂ \land 1 \in ℂ) \to A + (V - D) - 1 \in ℂ$
257	254 255 256	sylancl	$⊢ φ \to A + (V - D) - 1 \in ℂ$
258	105 257	mulcld	$⊢ φ \to W (A + (V - D) - 1) \in ℂ$
259	252 258 101	addassd	$⊢ φ \to B + W (A + (V - D) - 1) + W D = B + W (A + (V - D) - 1) + W D$
260	105 257 109	adddid	$⊢ φ \to W ((A + V - D) - 1 + D) = W (A + (V - D) - 1) + W D$
261	113 253 109	addassd	$⊢ φ \to A + (V - D) + D = A + (V - D) + D$
262	120 109	npcand	$⊢ φ \to V - D + D = V$
263	262	oveq2d	$⊢ φ \to A + (V - D) + D = A + V$
264	261 263	eqtrd	$⊢ φ \to A + (V - D) + D = A + V$
265	264	oveq1d	$⊢ φ \to (A + V - D) + D - 1 = A + V - 1$
266		1cnd	$⊢ φ \to 1 \in ℂ$
267	254 109 266	addsubd	$⊢ φ \to (A + V - D) + D - 1 = (A + V - D) - 1 + D$
268	113 120 266	addsubd	$⊢ φ \to A + V - 1 = A - 1 + V$
269	265 267 268	3eqtr3d	$⊢ φ \to (A + V - D) - 1 + D = A - 1 + V$
270	269	oveq2d	$⊢ φ \to W ((A + V - D) - 1 + D) = W (A - 1 + V)$
271	260 270	eqtr3d	$⊢ φ \to W (A + (V - D) - 1) + W D = W (A - 1 + V)$
272	271	oveq2d	$⊢ φ \to B + W (A + (V - D) - 1) + W D = B + W (A - 1 + V)$
273	259 272	eqtrd	$⊢ φ \to B + W (A + (V - D) - 1) + W D = B + W (A - 1 + V)$
274	251 273	eqtrid	$⊢ φ \to T + W D = B + W (A - 1 + V)$
275	274	oveq2d	$⊢ φ \to E (i) + T + W D = E (i) + B + W (A - 1 + V)$
276	275	adantr	$⊢ (φ \land i \in (1 \dots M)) \to E (i) + T + W D = E (i) + B + W (A - 1 + V)$
277	88	adantr	$⊢ (φ \land i \in (1 \dots M)) \to W (A - 1 + V) \in ℂ$
278	80 77 277	addassd	$⊢ (φ \land i \in (1 \dots M)) \to E (i) + B + W (A - 1 + V) = E (i) + B + W (A - 1 + V)$
279	80 77	addcomd	$⊢ (φ \land i \in (1 \dots M)) \to E (i) + B = B + E (i)$
280	279	oveq1d	$⊢ (φ \land i \in (1 \dots M)) \to E (i) + B + W (A - 1 + V) = B + E (i) + W (A - 1 + V)$
281	276 278 280	3eqtr2d	$⊢ (φ \land i \in (1 \dots M)) \to E (i) + T + W D = B + E (i) + W (A - 1 + V)$
282	246 250 281	3eqtrd	$⊢ (φ \land i \in (1 \dots M)) \to T + P (i) = B + E (i) + W (A - 1 + V)$
283	282 245	oveq12d	$⊢ (φ \land i \in (1 \dots M)) \to (T + P (i)) AP (K) P (i) = (B + E (i) + W (A - 1 + V)) AP (K) (E (i) + W D)$
284		cnvimass	$⊢ G^{-1} [\{G (B + E (i))\}] \subseteq dom G$
285	284 7	fssdm	$⊢ φ \to G^{-1} [\{G (B + E (i))\}] \subseteq (1 \dots W)$
286	285	adantr	$⊢ (φ \land i \in (1 \dots M)) \to G^{-1} [\{G (B + E (i))\}] \subseteq (1 \dots W)$
287		vdwapid1	$⊢ (K \in ℕ \land B + E (i) \in ℕ \land E (i) \in ℕ) \to B + E (i) \in ((B + E (i)) AP (K) E (i))$
288	160 162 79 287	syl3anc	$⊢ (φ \land i \in (1 \dots M)) \to B + E (i) \in ((B + E (i)) AP (K) E (i))$
289	153 288	sseldd	$⊢ (φ \land i \in (1 \dots M)) \to B + E (i) \in G^{-1} [\{G (B + E (i))\}]$
290	286 289	sseldd	$⊢ (φ \land i \in (1 \dots M)) \to B + E (i) \in (1 \dots W)$
291		fvoveq1	$⊢ y = B + E (i) \to H (y + W (A - 1 + V)) = H (B + E (i) + W (A - 1 + V))$
292		eqid	$⊢ (y \in (1 \dots W) ⟼ H (y + W (A - 1 + V))) = (y \in (1 \dots W) ⟼ H (y + W (A - 1 + V)))$
293		fvex	$⊢ H (B + E (i) + W (A - 1 + V)) \in V$
294	291 292 293	fvmpt	$⊢ B + E (i) \in (1 \dots W) \to (y \in (1 \dots W) ⟼ H (y + W (A - 1 + V))) (B + E (i)) = H (B + E (i) + W (A - 1 + V))$
295	290 294	syl	$⊢ (φ \land i \in (1 \dots M)) \to (y \in (1 \dots W) ⟼ H (y + W (A - 1 + V))) (B + E (i)) = H (B + E (i) + W (A - 1 + V))$
296		vdwapid1	$⊢ (K \in ℕ \land A \in ℕ \land D \in ℕ) \to A \in (A AP (K) D)$
297	25 9 10 296	syl3anc	$⊢ φ \to A \in (A AP (K) D)$
298	11 297	sseldd	$⊢ φ \to A \in F^{-1} [\{G\}]$
299		fniniseg	$⊢ F Fn (1 \dots V) \to (A \in F^{-1} [\{G\}] \leftrightarrow (A \in (1 \dots V) \land F (A) = G))$
300	146 299	syl	$⊢ φ \to (A \in F^{-1} [\{G\}] \leftrightarrow (A \in (1 \dots V) \land F (A) = G))$
301	298 300	mpbid	$⊢ φ \to (A \in (1 \dots V) \land F (A) = G)$
302	301	simprd	$⊢ φ \to F (A) = G$
303	301	simpld	$⊢ φ \to A \in (1 \dots V)$
304		oveq1	$⊢ x = A \to x - 1 = A - 1$
305	304	oveq1d	$⊢ x = A \to x - 1 + V = A - 1 + V$
306	305	oveq2d	$⊢ x = A \to W (x - 1 + V) = W (A - 1 + V)$
307	306	oveq2d	$⊢ x = A \to y + W (x - 1 + V) = y + W (A - 1 + V)$
308	307	fveq2d	$⊢ x = A \to H (y + W (x - 1 + V)) = H (y + W (A - 1 + V))$
309	308	mpteq2dv	$⊢ x = A \to (y \in (1 \dots W) ⟼ H (y + W (x - 1 + V))) = (y \in (1 \dots W) ⟼ H (y + W (A - 1 + V)))$
310	190	mptex	$⊢ (y \in (1 \dots W) ⟼ H (y + W (A - 1 + V))) \in V$
311	309 5 310	fvmpt	$⊢ A \in (1 \dots V) \to F (A) = (y \in (1 \dots W) ⟼ H (y + W (A - 1 + V)))$
312	303 311	syl	$⊢ φ \to F (A) = (y \in (1 \dots W) ⟼ H (y + W (A - 1 + V)))$
313	302 312	eqtr3d	$⊢ φ \to G = (y \in (1 \dots W) ⟼ H (y + W (A - 1 + V)))$
314	313	fveq1d	$⊢ φ \to G (B + E (i)) = (y \in (1 \dots W) ⟼ H (y + W (A - 1 + V))) (B + E (i))$
315	314	adantr	$⊢ (φ \land i \in (1 \dots M)) \to G (B + E (i)) = (y \in (1 \dots W) ⟼ H (y + W (A - 1 + V))) (B + E (i))$
316	282	fveq2d	$⊢ (φ \land i \in (1 \dots M)) \to H (T + P (i)) = H (B + E (i) + W (A - 1 + V))$
317	295 315 316	3eqtr4rd	$⊢ (φ \land i \in (1 \dots M)) \to H (T + P (i)) = G (B + E (i))$
318	317	sneqd	$⊢ (φ \land i \in (1 \dots M)) \to \{H (T + P (i))\} = \{G (B + E (i))\}$
319	318	imaeq2d	$⊢ (φ \land i \in (1 \dots M)) \to H^{-1} [\{H (T + P (i))\}] = H^{-1} [\{G (B + E (i))\}]$
320	217 283 319	3sstr4d	$⊢ (φ \land i \in (1 \dots M)) \to (T + P (i)) AP (K) P (i) \subseteq H^{-1} [\{H (T + P (i))\}]$
321	320	ex	$⊢ φ \to (i \in (1 \dots M) \to (T + P (i)) AP (K) P (i) \subseteq H^{-1} [\{H (T + P (i))\}])$
322	252	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to B \in ℂ$
323	88	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to W (A - 1 + V) \in ℂ$
324	322 323 98	addassd	$⊢ (φ \land m \in (0 \dots K - 1)) \to B + W (A - 1 + V) + m W D = B + W (A - 1 + V) + m W D$
325	127	oveq2d	$⊢ (φ \land m \in (0 \dots K - 1)) \to B + W ((A + m D) - 1 + V) = B + W (A - 1 + V) + m W D$
326	324 325	eqtr4d	$⊢ (φ \land m \in (0 \dots K - 1)) \to B + W (A - 1 + V) + m W D = B + W ((A + m D) - 1 + V)$
327	1	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to V \in ℕ$
328	2	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to W \in ℕ$
329		eluzfz1	$⊢ M \in ℤ_{\geq 1} \to 1 \in (1 \dots M)$
330	52 329	syl	$⊢ φ \to 1 \in (1 \dots M)$
331	330	ne0d	$⊢ φ \to (1 \dots M) \neq \emptyset$
332		elfzuz3	$⊢ B + E (i) \in (1 \dots W) \to W \in ℤ_{\geq (B + E (i))}$
333	290 332	syl	$⊢ (φ \land i \in (1 \dots M)) \to W \in ℤ_{\geq (B + E (i))}$
334	12	nnzd	$⊢ φ \to B \in ℤ$
335		uzid	$⊢ B \in ℤ \to B \in ℤ_{\geq B}$
336	334 335	syl	$⊢ φ \to B \in ℤ_{\geq B}$
337	336	adantr	$⊢ (φ \land i \in (1 \dots M)) \to B \in ℤ_{\geq B}$
338	79	nnnn0d	$⊢ (φ \land i \in (1 \dots M)) \to E (i) \in ℕ_{0}$
339		uzaddcl	$⊢ (B \in ℤ_{\geq B} \land E (i) \in ℕ_{0}) \to B + E (i) \in ℤ_{\geq B}$
340	337 338 339	syl2anc	$⊢ (φ \land i \in (1 \dots M)) \to B + E (i) \in ℤ_{\geq B}$
341		uztrn	$⊢ (W \in ℤ_{\geq (B + E (i))} \land B + E (i) \in ℤ_{\geq B}) \to W \in ℤ_{\geq B}$
342	333 340 341	syl2anc	$⊢ (φ \land i \in (1 \dots M)) \to W \in ℤ_{\geq B}$
343		eluzle	$⊢ W \in ℤ_{\geq B} \to B \leq W$
344	342 343	syl	$⊢ (φ \land i \in (1 \dots M)) \to B \leq W$
345	344	ralrimiva	$⊢ φ \to \forall i \in (1 \dots M) B \leq W$
346		r19.2z	$⊢ ((1 \dots M) \neq \emptyset \land \forall i \in (1 \dots M) B \leq W) \to \exists i \in (1 \dots M) B \leq W$
347	331 345 346	syl2anc	$⊢ φ \to \exists i \in (1 \dots M) B \leq W$
348		idd	$⊢ i \in (1 \dots M) \to (B \leq W \to B \leq W)$
349	348	rexlimiv	$⊢ \exists i \in (1 \dots M) B \leq W \to B \leq W$
350	347 349	syl	$⊢ φ \to B \leq W$
351	2	nnzd	$⊢ φ \to W \in ℤ$
352		fznn	$⊢ W \in ℤ \to (B \in (1 \dots W) \leftrightarrow (B \in ℕ \land B \leq W))$
353	351 352	syl	$⊢ φ \to (B \in (1 \dots W) \leftrightarrow (B \in ℕ \land B \leq W))$
354	12 350 353	mpbir2and	$⊢ φ \to B \in (1 \dots W)$
355	354	adantr	$⊢ (φ \land m \in (0 \dots K - 1)) \to B \in (1 \dots W)$
356	327 328 151 355	vdwlem3	$⊢ (φ \land m \in (0 \dots K - 1)) \to B + W ((A + m D) - 1 + V) \in (1 \dots W 2 V)$
357	326 356	eqeltrd	$⊢ (φ \land m \in (0 \dots K - 1)) \to B + W (A - 1 + V) + m W D \in (1 \dots W 2 V)$
358		fvoveq1	$⊢ y = B \to H (y + W ((A + m D) - 1 + V)) = H (B + W ((A + m D) - 1 + V))$
359		fvex	$⊢ H (B + W ((A + m D) - 1 + V)) \in V$
360	358 178 359	fvmpt	$⊢ B \in (1 \dots W) \to (y \in (1 \dots W) ⟼ H (y + W ((A + m D) - 1 + V))) (B) = H (B + W ((A + m D) - 1 + V))$
361	355 360	syl	$⊢ (φ \land m \in (0 \dots K - 1)) \to (y \in (1 \dots W) ⟼ H (y + W ((A + m D) - 1 + V))) (B) = H (B + W ((A + m D) - 1 + V))$
362	194	fveq1d	$⊢ (φ \land m \in (0 \dots K - 1)) \to G (B) = (y \in (1 \dots W) ⟼ H (y + W ((A + m D) - 1 + V))) (B)$
363	326	fveq2d	$⊢ (φ \land m \in (0 \dots K - 1)) \to H (B + W (A - 1 + V) + m W D) = H (B + W ((A + m D) - 1 + V))$
364	361 362 363	3eqtr4rd	$⊢ (φ \land m \in (0 \dots K - 1)) \to H (B + W (A - 1 + V) + m W D) = G (B)$
365	357 364	jca	$⊢ (φ \land m \in (0 \dots K - 1)) \to (B + W (A - 1 + V) + m W D \in (1 \dots W 2 V) \land H (B + W (A - 1 + V) + m W D) = G (B))$
366		eleq1	$⊢ z = B + W (A - 1 + V) + m W D \to (z \in (1 \dots W 2 V) \leftrightarrow B + W (A - 1 + V) + m W D \in (1 \dots W 2 V))$
367		fveqeq2	$⊢ z = B + W (A - 1 + V) + m W D \to (H (z) = G (B) \leftrightarrow H (B + W (A - 1 + V) + m W D) = G (B))$
368	366 367	anbi12d	$⊢ z = B + W (A - 1 + V) + m W D \to ((z \in (1 \dots W 2 V) \land H (z) = G (B)) \leftrightarrow (B + W (A - 1 + V) + m W D \in (1 \dots W 2 V) \land H (B + W (A - 1 + V) + m W D) = G (B)))$
369	365 368	syl5ibrcom	$⊢ (φ \land m \in (0 \dots K - 1)) \to (z = B + W (A - 1 + V) + m W D \to (z \in (1 \dots W 2 V) \land H (z) = G (B)))$
370	369	rexlimdva	$⊢ φ \to (\exists m \in (0 \dots K - 1) z = B + W (A - 1 + V) + m W D \to (z \in (1 \dots W 2 V) \land H (z) = G (B)))$
371	12 87	nnaddcld	$⊢ φ \to B + W (A - 1 + V) \in ℕ$
372		vdwapval	$⊢ (K \in ℕ_{0} \land B + W (A - 1 + V) \in ℕ \land W D \in ℕ) \to (z \in ((B + W (A - 1 + V)) AP (K) W D) \leftrightarrow \exists m \in (0 \dots K - 1) z = B + W (A - 1 + V) + m W D)$
373	139 371 65 372	syl3anc	$⊢ φ \to (z \in ((B + W (A - 1 + V)) AP (K) W D) \leftrightarrow \exists m \in (0 \dots K - 1) z = B + W (A - 1 + V) + m W D)$
374		fniniseg	$⊢ H Fn (1 \dots W 2 V) \to (z \in H^{-1} [\{G (B)\}] \leftrightarrow (z \in (1 \dots W 2 V) \land H (z) = G (B)))$
375	212 374	syl	$⊢ φ \to (z \in H^{-1} [\{G (B)\}] \leftrightarrow (z \in (1 \dots W 2 V) \land H (z) = G (B)))$
376	370 373 375	3imtr4d	$⊢ φ \to (z \in ((B + W (A - 1 + V)) AP (K) W D) \to z \in H^{-1} [\{G (B)\}])$
377	376	ssrdv	$⊢ φ \to (B + W (A - 1 + V)) AP (K) W D \subseteq H^{-1} [\{G (B)\}]$
378	6	peano2nnd	$⊢ φ \to M + 1 \in ℕ$
379	378 51	eleqtrdi	$⊢ φ \to M + 1 \in ℤ_{\geq 1}$
380		eluzfz2	$⊢ M + 1 \in ℤ_{\geq 1} \to M + 1 \in (1 \dots M + 1)$
381		iftrue	$⊢ j = M + 1 \to if (j = M + 1, 0, E (j)) = 0$
382	381	oveq1d	$⊢ j = M + 1 \to if (j = M + 1, 0, E (j)) + W D = 0 + W D$
383		ovex	$⊢ 0 + W D \in V$
384	382 18 383	fvmpt	$⊢ M + 1 \in (1 \dots M + 1) \to P (M + 1) = 0 + W D$
385	379 380 384	3syl	$⊢ φ \to P (M + 1) = 0 + W D$
386	101	addid2d	$⊢ φ \to 0 + W D = W D$
387	385 386	eqtrd	$⊢ φ \to P (M + 1) = W D$
388	387	oveq2d	$⊢ φ \to T + P (M + 1) = T + W D$
389	388 274	eqtrd	$⊢ φ \to T + P (M + 1) = B + W (A - 1 + V)$
390	389 387	oveq12d	$⊢ φ \to (T + P (M + 1)) AP (K) P (M + 1) = (B + W (A - 1 + V)) AP (K) W D$
391		fvoveq1	$⊢ y = B \to H (y + W (A - 1 + V)) = H (B + W (A - 1 + V))$
392		fvex	$⊢ H (B + W (A - 1 + V)) \in V$
393	391 292 392	fvmpt	$⊢ B \in (1 \dots W) \to (y \in (1 \dots W) ⟼ H (y + W (A - 1 + V))) (B) = H (B + W (A - 1 + V))$
394	354 393	syl	$⊢ φ \to (y \in (1 \dots W) ⟼ H (y + W (A - 1 + V))) (B) = H (B + W (A - 1 + V))$
395	313	fveq1d	$⊢ φ \to G (B) = (y \in (1 \dots W) ⟼ H (y + W (A - 1 + V))) (B)$
396	389	fveq2d	$⊢ φ \to H (T + P (M + 1)) = H (B + W (A - 1 + V))$
397	394 395 396	3eqtr4rd	$⊢ φ \to H (T + P (M + 1)) = G (B)$
398	397	sneqd	$⊢ φ \to \{H (T + P (M + 1))\} = \{G (B)\}$
399	398	imaeq2d	$⊢ φ \to H^{-1} [\{H (T + P (M + 1))\}] = H^{-1} [\{G (B)\}]$
400	377 390 399	3sstr4d	$⊢ φ \to (T + P (M + 1)) AP (K) P (M + 1) \subseteq H^{-1} [\{H (T + P (M + 1))\}]$
401		fveq2	$⊢ i = M + 1 \to P (i) = P (M + 1)$
402	401	oveq2d	$⊢ i = M + 1 \to T + P (i) = T + P (M + 1)$
403	402 401	oveq12d	$⊢ i = M + 1 \to (T + P (i)) AP (K) P (i) = (T + P (M + 1)) AP (K) P (M + 1)$
404	402	fveq2d	$⊢ i = M + 1 \to H (T + P (i)) = H (T + P (M + 1))$
405	404	sneqd	$⊢ i = M + 1 \to \{H (T + P (i))\} = \{H (T + P (M + 1))\}$
406	405	imaeq2d	$⊢ i = M + 1 \to H^{-1} [\{H (T + P (i))\}] = H^{-1} [\{H (T + P (M + 1))\}]$
407	403 406	sseq12d	$⊢ i = M + 1 \to ((T + P (i)) AP (K) P (i) \subseteq H^{-1} [\{H (T + P (i))\}] \leftrightarrow (T + P (M + 1)) AP (K) P (M + 1) \subseteq H^{-1} [\{H (T + P (M + 1))\}])$
408	400 407	syl5ibrcom	$⊢ φ \to (i = M + 1 \to (T + P (i)) AP (K) P (i) \subseteq H^{-1} [\{H (T + P (i))\}])$
409	321 408	jaod	$⊢ φ \to ((i \in (1 \dots M) \lor i = M + 1) \to (T + P (i)) AP (K) P (i) \subseteq H^{-1} [\{H (T + P (i))\}])$
410	75 409	sylbid	$⊢ φ \to (i \in (1 \dots M + 1) \to (T + P (i)) AP (K) P (i) \subseteq H^{-1} [\{H (T + P (i))\}])$
411	410	ralrimiv	$⊢ φ \to \forall i \in (1 \dots M + 1) (T + P (i)) AP (K) P (i) \subseteq H^{-1} [\{H (T + P (i))\}]$
412	411	adantr	$⊢ (φ \land \neg G (B) \in ran J) \to \forall i \in (1 \dots M + 1) (T + P (i)) AP (K) P (i) \subseteq H^{-1} [\{H (T + P (i))\}]$
413	220	rexeqdv	$⊢ φ \to (\exists i \in (1 \dots M + 1) x = H (T + P (i)) \leftrightarrow \exists i \in ((1 \dots M) \cup \{M + 1\}) x = H (T + P (i)))$
414		rexun	$⊢ \exists i \in ((1 \dots M) \cup \{M + 1\}) x = H (T + P (i)) \leftrightarrow (\exists i \in (1 \dots M) x = H (T + P (i)) \lor \exists i \in \{M + 1\} x = H (T + P (i)))$
415	317	eqeq2d	$⊢ (φ \land i \in (1 \dots M)) \to (x = H (T + P (i)) \leftrightarrow x = G (B + E (i)))$
416	415	rexbidva	$⊢ φ \to (\exists i \in (1 \dots M) x = H (T + P (i)) \leftrightarrow \exists i \in (1 \dots M) x = G (B + E (i)))$
417		ovex	$⊢ M + 1 \in V$
418	404	eqeq2d	$⊢ i = M + 1 \to (x = H (T + P (i)) \leftrightarrow x = H (T + P (M + 1)))$
419	417 418	rexsn	$⊢ \exists i \in \{M + 1\} x = H (T + P (i)) \leftrightarrow x = H (T + P (M + 1))$
420	397	eqeq2d	$⊢ φ \to (x = H (T + P (M + 1)) \leftrightarrow x = G (B))$
421	419 420	syl5bb	$⊢ φ \to (\exists i \in \{M + 1\} x = H (T + P (i)) \leftrightarrow x = G (B))$
422	416 421	orbi12d	$⊢ φ \to ((\exists i \in (1 \dots M) x = H (T + P (i)) \lor \exists i \in \{M + 1\} x = H (T + P (i))) \leftrightarrow (\exists i \in (1 \dots M) x = G (B + E (i)) \lor x = G (B)))$
423	414 422	syl5bb	$⊢ φ \to (\exists i \in ((1 \dots M) \cup \{M + 1\}) x = H (T + P (i)) \leftrightarrow (\exists i \in (1 \dots M) x = G (B + E (i)) \lor x = G (B)))$
424	413 423	bitrd	$⊢ φ \to (\exists i \in (1 \dots M + 1) x = H (T + P (i)) \leftrightarrow (\exists i \in (1 \dots M) x = G (B + E (i)) \lor x = G (B)))$
425	424	adantr	$⊢ (φ \land \neg G (B) \in ran J) \to (\exists i \in (1 \dots M + 1) x = H (T + P (i)) \leftrightarrow (\exists i \in (1 \dots M) x = G (B + E (i)) \lor x = G (B)))$
426	425	abbidv	$⊢ (φ \land \neg G (B) \in ran J) \to \{x \| \exists i \in (1 \dots M + 1) x = H (T + P (i))\} = \{x \| (\exists i \in (1 \dots M) x = G (B + E (i)) \lor x = G (B))\}$
427		eqid	$⊢ (i \in (1 \dots M + 1) ⟼ H (T + P (i))) = (i \in (1 \dots M + 1) ⟼ H (T + P (i)))$
428	427	rnmpt	$⊢ ran (i \in (1 \dots M + 1) ⟼ H (T + P (i))) = \{x \| \exists i \in (1 \dots M + 1) x = H (T + P (i))\}$
429	15	rnmpt	$⊢ ran J = \{x \| \exists i \in (1 \dots M) x = G (B + E (i))\}$
430		df-sn	$⊢ \{G (B)\} = \{x \| x = G (B)\}$
431	429 430	uneq12i	$⊢ ran J \cup \{G (B)\} = \{x \| \exists i \in (1 \dots M) x = G (B + E (i))\} \cup \{x \| x = G (B)\}$
432		unab	$⊢ \{x \| \exists i \in (1 \dots M) x = G (B + E (i))\} \cup \{x \| x = G (B)\} = \{x \| (\exists i \in (1 \dots M) x = G (B + E (i)) \lor x = G (B))\}$
433	431 432	eqtri	$⊢ ran J \cup \{G (B)\} = \{x \| (\exists i \in (1 \dots M) x = G (B + E (i)) \lor x = G (B))\}$
434	426 428 433	3eqtr4g	$⊢ (φ \land \neg G (B) \in ran J) \to ran (i \in (1 \dots M + 1) ⟼ H (T + P (i))) = ran J \cup \{G (B)\}$
435	434	fveq2d	$⊢ (φ \land \neg G (B) \in ran J) \to \|ran (i \in (1 \dots M + 1) ⟼ H (T + P (i)))\| = \|ran J \cup \{G (B)\}\|$
436		fzfi	$⊢ (1 \dots M) \in Fin$
437		dffn4	$⊢ J Fn (1 \dots M) \leftrightarrow J : (1 \dots M) \underset{onto}{⟶} ran J$
438	20 437	mpbi	$⊢ J : (1 \dots M) \underset{onto}{⟶} ran J$
439		fofi	$⊢ ((1 \dots M) \in Fin \land J : (1 \dots M) \underset{onto}{⟶} ran J) \to ran J \in Fin$
440	436 438 439	mp2an	$⊢ ran J \in Fin$
441	440	a1i	$⊢ φ \to ran J \in Fin$
442		fvex	$⊢ G (B) \in V$
443		hashunsng	$⊢ G (B) \in V \to ((ran J \in Fin \land \neg G (B) \in ran J) \to \|ran J \cup \{G (B)\}\| = \|ran J\| + 1)$
444	442 443	ax-mp	$⊢ (ran J \in Fin \land \neg G (B) \in ran J) \to \|ran J \cup \{G (B)\}\| = \|ran J\| + 1$
445	441 444	sylan	$⊢ (φ \land \neg G (B) \in ran J) \to \|ran J \cup \{G (B)\}\| = \|ran J\| + 1$
446	16	adantr	$⊢ (φ \land \neg G (B) \in ran J) \to \|ran J\| = M$
447	446	oveq1d	$⊢ (φ \land \neg G (B) \in ran J) \to \|ran J\| + 1 = M + 1$
448	435 445 447	3eqtrd	$⊢ (φ \land \neg G (B) \in ran J) \to \|ran (i \in (1 \dots M + 1) ⟼ H (T + P (i)))\| = M + 1$
449	412 448	jca	$⊢ (φ \land \neg G (B) \in ran J) \to (\forall i \in (1 \dots M + 1) (T + P (i)) AP (K) P (i) \subseteq H^{-1} [\{H (T + P (i))\}] \land \|ran (i \in (1 \dots M + 1) ⟼ H (T + P (i)))\| = M + 1)$
450		oveq1	$⊢ a = T \to a + d (i) = T + d (i)$
451	450	oveq1d	$⊢ a = T \to (a + d (i)) AP (K) d (i) = (T + d (i)) AP (K) d (i)$
452		fvoveq1	$⊢ a = T \to H (a + d (i)) = H (T + d (i))$
453	452	sneqd	$⊢ a = T \to \{H (a + d (i))\} = \{H (T + d (i))\}$
454	453	imaeq2d	$⊢ a = T \to H^{-1} [\{H (a + d (i))\}] = H^{-1} [\{H (T + d (i))\}]$
455	451 454	sseq12d	$⊢ a = T \to ((a + d (i)) AP (K) d (i) \subseteq H^{-1} [\{H (a + d (i))\}] \leftrightarrow (T + d (i)) AP (K) d (i) \subseteq H^{-1} [\{H (T + d (i))\}])$
456	455	ralbidv	$⊢ a = T \to (\forall i \in (1 \dots M + 1) (a + d (i)) AP (K) d (i) \subseteq H^{-1} [\{H (a + d (i))\}] \leftrightarrow \forall i \in (1 \dots M + 1) (T + d (i)) AP (K) d (i) \subseteq H^{-1} [\{H (T + d (i))\}])$
457	452	mpteq2dv	$⊢ a = T \to (i \in (1 \dots M + 1) ⟼ H (a + d (i))) = (i \in (1 \dots M + 1) ⟼ H (T + d (i)))$
458	457	rneqd	$⊢ a = T \to ran (i \in (1 \dots M + 1) ⟼ H (a + d (i))) = ran (i \in (1 \dots M + 1) ⟼ H (T + d (i)))$
459	458	fveqeq2d	$⊢ a = T \to (\|ran (i \in (1 \dots M + 1) ⟼ H (a + d (i)))\| = M + 1 \leftrightarrow \|ran (i \in (1 \dots M + 1) ⟼ H (T + d (i)))\| = M + 1)$
460	456 459	anbi12d	$⊢ a = T \to ((\forall i \in (1 \dots M + 1) (a + d (i)) AP (K) d (i) \subseteq H^{-1} [\{H (a + d (i))\}] \land \|ran (i \in (1 \dots M + 1) ⟼ H (a + d (i)))\| = M + 1) \leftrightarrow (\forall i \in (1 \dots M + 1) (T + d (i)) AP (K) d (i) \subseteq H^{-1} [\{H (T + d (i))\}] \land \|ran (i \in (1 \dots M + 1) ⟼ H (T + d (i)))\| = M + 1))$
461		fveq1	$⊢ d = P \to d (i) = P (i)$
462	461	oveq2d	$⊢ d = P \to T + d (i) = T + P (i)$
463	462 461	oveq12d	$⊢ d = P \to (T + d (i)) AP (K) d (i) = (T + P (i)) AP (K) P (i)$
464	462	fveq2d	$⊢ d = P \to H (T + d (i)) = H (T + P (i))$
465	464	sneqd	$⊢ d = P \to \{H (T + d (i))\} = \{H (T + P (i))\}$
466	465	imaeq2d	$⊢ d = P \to H^{-1} [\{H (T + d (i))\}] = H^{-1} [\{H (T + P (i))\}]$
467	463 466	sseq12d	$⊢ d = P \to ((T + d (i)) AP (K) d (i) \subseteq H^{-1} [\{H (T + d (i))\}] \leftrightarrow (T + P (i)) AP (K) P (i) \subseteq H^{-1} [\{H (T + P (i))\}])$
468	467	ralbidv	$⊢ d = P \to (\forall i \in (1 \dots M + 1) (T + d (i)) AP (K) d (i) \subseteq H^{-1} [\{H (T + d (i))\}] \leftrightarrow \forall i \in (1 \dots M + 1) (T + P (i)) AP (K) P (i) \subseteq H^{-1} [\{H (T + P (i))\}])$
469	464	mpteq2dv	$⊢ d = P \to (i \in (1 \dots M + 1) ⟼ H (T + d (i))) = (i \in (1 \dots M + 1) ⟼ H (T + P (i)))$
470	469	rneqd	$⊢ d = P \to ran (i \in (1 \dots M + 1) ⟼ H (T + d (i))) = ran (i \in (1 \dots M + 1) ⟼ H (T + P (i)))$
471	470	fveqeq2d	$⊢ d = P \to (\|ran (i \in (1 \dots M + 1) ⟼ H (T + d (i)))\| = M + 1 \leftrightarrow \|ran (i \in (1 \dots M + 1) ⟼ H (T + P (i)))\| = M + 1)$
472	468 471	anbi12d	$⊢ d = P \to ((\forall i \in (1 \dots M + 1) (T + d (i)) AP (K) d (i) \subseteq H^{-1} [\{H (T + d (i))\}] \land \|ran (i \in (1 \dots M + 1) ⟼ H (T + d (i)))\| = M + 1) \leftrightarrow (\forall i \in (1 \dots M + 1) (T + P (i)) AP (K) P (i) \subseteq H^{-1} [\{H (T + P (i))\}] \land \|ran (i \in (1 \dots M + 1) ⟼ H (T + P (i)))\| = M + 1))$
473	460 472	rspc2ev	$⊢ (T \in ℕ \land P \in (ℕ^{(1 \dots M + 1)}) \land (\forall i \in (1 \dots M + 1) (T + P (i)) AP (K) P (i) \subseteq H^{-1} [\{H (T + P (i))\}] \land \|ran (i \in (1 \dots M + 1) ⟼ H (T + P (i)))\| = M + 1)) \to \exists a \in ℕ \exists d \in (ℕ^{(1 \dots M + 1)}) (\forall i \in (1 \dots M + 1) (a + d (i)) AP (K) d (i) \subseteq H^{-1} [\{H (a + d (i))\}] \land \|ran (i \in (1 \dots M + 1) ⟼ H (a + d (i)))\| = M + 1)$
474	48 73 449 473	syl3anc	$⊢ (φ \land \neg G (B) \in ran J) \to \exists a \in ℕ \exists d \in (ℕ^{(1 \dots M + 1)}) (\forall i \in (1 \dots M + 1) (a + d (i)) AP (K) d (i) \subseteq H^{-1} [\{H (a + d (i))\}] \land \|ran (i \in (1 \dots M + 1) ⟼ H (a + d (i)))\| = M + 1)$
475		ovex	$⊢ (1 \dots W 2 V) \in V$
476	25	adantr	$⊢ (φ \land \neg G (B) \in ran J) \to K \in ℕ$
477	476	nnnn0d	$⊢ (φ \land \neg G (B) \in ran J) \to K \in ℕ_{0}$
478	4	adantr	$⊢ (φ \land \neg G (B) \in ran J) \to H : (1 \dots W 2 V) ⟶ R$
479	6	adantr	$⊢ (φ \land \neg G (B) \in ran J) \to M \in ℕ$
480	479	peano2nnd	$⊢ (φ \land \neg G (B) \in ran J) \to M + 1 \in ℕ$
481		eqid	$⊢ (1 \dots M + 1) = (1 \dots M + 1)$
482	475 477 478 480 481	vdwpc	$⊢ (φ \land \neg G (B) \in ran J) \to (⟨M + 1, K⟩ PolyAP H \leftrightarrow \exists a \in ℕ \exists d \in (ℕ^{(1 \dots M + 1)}) (\forall i \in (1 \dots M + 1) (a + d (i)) AP (K) d (i) \subseteq H^{-1} [\{H (a + d (i))\}] \land \|ran (i \in (1 \dots M + 1) ⟼ H (a + d (i)))\| = M + 1))$
483	474 482	mpbird	$⊢ (φ \land \neg G (B) \in ran J) \to ⟨M + 1, K⟩ PolyAP H$
484	483	orcd	$⊢ (φ \land \neg G (B) \in ran J) \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP G)$
485	46 484	pm2.61dan	$⊢ φ \to (⟨M + 1, K⟩ PolyAP H \lor (K + 1) MonoAP G)$

Metamath Proof Explorer

Theorem vdwlem6

Proof