vdwlem5

	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	vdwlem5	$⊢ φ \to T \in ℕ$

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	2	nnnn0d	$⊢ φ \to W \in ℕ_{0}$
20	1	nncnd	$⊢ φ \to V \in ℂ$
21	10	nncnd	$⊢ φ \to D \in ℂ$
22	20 21	subcld	$⊢ φ \to V - D \in ℂ$
23	9	nncnd	$⊢ φ \to A \in ℂ$
24	22 23	npcand	$⊢ φ \to (V - D) - A + A = V - D$
25	20 21 23	subsub4d	$⊢ φ \to V - D - A = V - (D + A)$
26	21 23	addcomd	$⊢ φ \to D + A = A + D$
27	26	oveq2d	$⊢ φ \to V - (D + A) = V - (A + D)$
28	25 27	eqtrd	$⊢ φ \to V - D - A = V - (A + D)$
29		cnvimass	$⊢ F^{-1} [\{G\}] \subseteq dom F$
30	1 2 3 4 5	vdwlem4	$⊢ φ \to F : (1 \dots V) ⟶ R^{(1 \dots W)}$
31	29 30	fssdm	$⊢ φ \to F^{-1} [\{G\}] \subseteq (1 \dots V)$
32		ssun2	$⊢ (A + D) AP (K - 1) D \subseteq \{A\} \cup ((A + D) AP (K - 1) D)$
33		uz2m1nn	$⊢ K \in ℤ_{\geq 2} \to K - 1 \in ℕ$
34	8 33	syl	$⊢ φ \to K - 1 \in ℕ$
35	9 10	nnaddcld	$⊢ φ \to A + D \in ℕ$
36		vdwapid1	$⊢ (K - 1 \in ℕ \land A + D \in ℕ \land D \in ℕ) \to A + D \in ((A + D) AP (K - 1) D)$
37	34 35 10 36	syl3anc	$⊢ φ \to A + D \in ((A + D) AP (K - 1) D)$
38	32 37	sseldi	$⊢ φ \to A + D \in (\{A\} \cup ((A + D) AP (K - 1) D))$
39		eluz2nn	$⊢ K \in ℤ_{\geq 2} \to K \in ℕ$
40	8 39	syl	$⊢ φ \to K \in ℕ$
41	40	nncnd	$⊢ φ \to K \in ℂ$
42		ax-1cn	$⊢ 1 \in ℂ$
43		npcan	$⊢ (K \in ℂ \land 1 \in ℂ) \to K - 1 + 1 = K$
44	41 42 43	sylancl	$⊢ φ \to K - 1 + 1 = K$
45	44	fveq2d	$⊢ φ \to AP (K - 1 + 1) = AP (K)$
46	45	oveqd	$⊢ φ \to A AP (K - 1 + 1) D = A AP (K) D$
47		nnm1nn0	$⊢ K \in ℕ \to K - 1 \in ℕ_{0}$
48	40 47	syl	$⊢ φ \to K - 1 \in ℕ_{0}$
49		vdwapun	$⊢ (K - 1 \in ℕ_{0} \land A \in ℕ \land D \in ℕ) \to A AP (K - 1 + 1) D = \{A\} \cup ((A + D) AP (K - 1) D)$
50	48 9 10 49	syl3anc	$⊢ φ \to A AP (K - 1 + 1) D = \{A\} \cup ((A + D) AP (K - 1) D)$
51	46 50	eqtr3d	$⊢ φ \to A AP (K) D = \{A\} \cup ((A + D) AP (K - 1) D)$
52	38 51	eleqtrrd	$⊢ φ \to A + D \in (A AP (K) D)$
53	11 52	sseldd	$⊢ φ \to A + D \in F^{-1} [\{G\}]$
54	31 53	sseldd	$⊢ φ \to A + D \in (1 \dots V)$
55		elfzuz3	$⊢ A + D \in (1 \dots V) \to V \in ℤ_{\geq (A + D)}$
56	54 55	syl	$⊢ φ \to V \in ℤ_{\geq (A + D)}$
57		uznn0sub	$⊢ V \in ℤ_{\geq (A + D)} \to V - (A + D) \in ℕ_{0}$
58	56 57	syl	$⊢ φ \to V - (A + D) \in ℕ_{0}$
59	28 58	eqeltrd	$⊢ φ \to V - D - A \in ℕ_{0}$
60		nn0nnaddcl	$⊢ (V - D - A \in ℕ_{0} \land A \in ℕ) \to (V - D) - A + A \in ℕ$
61	59 9 60	syl2anc	$⊢ φ \to (V - D) - A + A \in ℕ$
62	24 61	eqeltrrd	$⊢ φ \to V - D \in ℕ$
63	9 62	nnaddcld	$⊢ φ \to A + V - D \in ℕ$
64		nnm1nn0	$⊢ A + V - D \in ℕ \to A + (V - D) - 1 \in ℕ_{0}$
65	63 64	syl	$⊢ φ \to A + (V - D) - 1 \in ℕ_{0}$
66	19 65	nn0mulcld	$⊢ φ \to W (A + (V - D) - 1) \in ℕ_{0}$
67		nnnn0addcl	$⊢ (B \in ℕ \land W (A + (V - D) - 1) \in ℕ_{0}) \to B + W (A + (V - D) - 1) \in ℕ$
68	12 66 67	syl2anc	$⊢ φ \to B + W (A + (V - D) - 1) \in ℕ$
69	17 68	eqeltrid	$⊢ φ \to T \in ℕ$

Metamath Proof Explorer

Theorem vdwlem5

Proof