vdwlem6 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > vdwlem6		Structured version Visualization version GIF version

Theorem vdwlem6 16415

Description: Lemma for vdw 16423. (Contributed by Mario Carneiro, 13-Sep-2014.)

**Hypotheses**
Ref	Expression
vdwlem3.v	⊢ (𝜑 → 𝑉 ∈ ℕ)
vdwlem3.w	⊢ (𝜑 → 𝑊 ∈ ℕ)
vdwlem4.r	⊢ (𝜑 → 𝑅 ∈ Fin)
vdwlem4.h	⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
vdwlem4.f	⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))))
vdwlem7.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
vdwlem7.g	⊢ (𝜑 → 𝐺:(1...𝑊)⟶𝑅)
vdwlem7.k	⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘2))
vdwlem7.a	⊢ (𝜑 → 𝐴 ∈ ℕ)
vdwlem7.d	⊢ (𝜑 → 𝐷 ∈ ℕ)
vdwlem7.s	⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (^◡𝐹 “ {𝐺}))
vdwlem6.b	⊢ (𝜑 → 𝐵 ∈ ℕ)
vdwlem6.e	⊢ (𝜑 → 𝐸:(1...𝑀)⟶ℕ)
vdwlem6.s	⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
vdwlem6.j	⊢ 𝐽 = (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝐵 + (𝐸‘𝑖))))
vdwlem6.r	⊢ (𝜑 → (♯‘ran 𝐽) = 𝑀)
vdwlem6.t	⊢ 𝑇 = (𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)))
vdwlem6.p	⊢ 𝑃 = (𝑗 ∈ (1...(𝑀 + 1)) ↦ (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)))

**Assertion**
Ref	Expression
vdwlem6	⊢ (𝜑 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))

Distinct variable groups: 𝑥,𝑦,𝐴 𝑖,𝑗,𝑥,𝑦,𝐺 𝑖,𝐾,𝑗,𝑥,𝑦 𝑖,𝐽,𝑗,𝑥 𝑃,𝑖,𝑥 𝜑,𝑖,𝑗,𝑥,𝑦 𝑅,𝑖,𝑥,𝑦 𝐵,𝑖,𝑗,𝑥,𝑦 𝑖,𝐻,𝑥,𝑦 𝑖,𝑀,𝑗,𝑥,𝑦 𝐷,𝑗,𝑥,𝑦 𝑖,𝐸,𝑗,𝑥,𝑦 𝑖,𝑊,𝑗,𝑥,𝑦 𝑇,𝑖,𝑥 𝑥,𝑉,𝑦 Allowed substitution hints: 𝐴(𝑖,𝑗) 𝐷(𝑖) 𝑃(𝑦,𝑗) 𝑅(𝑗) 𝑇(𝑦,𝑗) 𝐹(𝑥,𝑦,𝑖,𝑗) 𝐻(𝑗) 𝐽(𝑦) 𝑉(𝑖,𝑗)

Proof of Theorem vdwlem6 Dummy variables 𝑚 𝑛 𝑧 𝑎 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fvex 6681	. . . . . . 7 ⊢ (𝐺‘(𝐵 + (𝐸‘𝑖))) ∈ V
2		vdwlem6.j	. . . . . . 7 ⊢ 𝐽 = (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝐵 + (𝐸‘𝑖))))
3	1, 2	fnmpti 6474	. . . . . 6 ⊢ 𝐽 Fn (1...𝑀)
4		fvelrnb 6724	. . . . . 6 ⊢ (𝐽 Fn (1...𝑀) → ((𝐺‘𝐵) ∈ ran 𝐽 ↔ ∃𝑚 ∈ (1...𝑀)(𝐽‘𝑚) = (𝐺‘𝐵)))
5	3, 4	ax-mp 5	. . . . 5 ⊢ ((𝐺‘𝐵) ∈ ran 𝐽 ↔ ∃𝑚 ∈ (1...𝑀)(𝐽‘𝑚) = (𝐺‘𝐵))
6		vdwlem4.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Fin)
7	6	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝑅 ∈ Fin)
8		vdwlem7.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘2))
9		eluz2nn 12359	. . . . . . . . 9 ⊢ (𝐾 ∈ (ℤ_≥‘2) → 𝐾 ∈ ℕ)
10	8, 9	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ℕ)
11	10	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝐾 ∈ ℕ)
12		vdwlem3.w	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ ℕ)
13	12	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝑊 ∈ ℕ)
14		vdwlem7.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺:(1...𝑊)⟶𝑅)
15	14	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝐺:(1...𝑊)⟶𝑅)
16		vdwlem6.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℕ)
17	16	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝐵 ∈ ℕ)
18		vdwlem7.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ)
19	18	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝑀 ∈ ℕ)
20		vdwlem6.e	. . . . . . . 8 ⊢ (𝜑 → 𝐸:(1...𝑀)⟶ℕ)
21	20	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝐸:(1...𝑀)⟶ℕ)
22		vdwlem6.s	. . . . . . . 8 ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
23	22	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
24		simprl 771	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝑚 ∈ (1...𝑀))
25		simprr 773	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐽‘𝑚) = (𝐺‘𝐵))
26		fveq2 6668	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑚 → (𝐸‘𝑖) = (𝐸‘𝑚))
27	26	oveq2d 7180	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑚 → (𝐵 + (𝐸‘𝑖)) = (𝐵 + (𝐸‘𝑚)))
28	27	fveq2d 6672	. . . . . . . . . 10 ⊢ (𝑖 = 𝑚 → (𝐺‘(𝐵 + (𝐸‘𝑖))) = (𝐺‘(𝐵 + (𝐸‘𝑚))))
29		fvex 6681	. . . . . . . . . 10 ⊢ (𝐺‘(𝐵 + (𝐸‘𝑚))) ∈ V
30	28, 2, 29	fvmpt 6769	. . . . . . . . 9 ⊢ (𝑚 ∈ (1...𝑀) → (𝐽‘𝑚) = (𝐺‘(𝐵 + (𝐸‘𝑚))))
31	24, 30	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐽‘𝑚) = (𝐺‘(𝐵 + (𝐸‘𝑚))))
32	25, 31	eqtr3d 2775	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐺‘𝐵) = (𝐺‘(𝐵 + (𝐸‘𝑚))))
33	7, 11, 13, 15, 17, 19, 21, 23, 24, 32	vdwlem1 16410	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐾 + 1) MonoAP 𝐺)
34	33	rexlimdvaa 3194	. . . . 5 ⊢ (𝜑 → (∃𝑚 ∈ (1...𝑀)(𝐽‘𝑚) = (𝐺‘𝐵) → (𝐾 + 1) MonoAP 𝐺))
35	5, 34	syl5bi 245	. . . 4 ⊢ (𝜑 → ((𝐺‘𝐵) ∈ ran 𝐽 → (𝐾 + 1) MonoAP 𝐺))
36	35	imp 410	. . 3 ⊢ ((𝜑 ∧ (𝐺‘𝐵) ∈ ran 𝐽) → (𝐾 + 1) MonoAP 𝐺)
37	36	olcd 873	. 2 ⊢ ((𝜑 ∧ (𝐺‘𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))
38		vdwlem3.v	. . . . . . 7 ⊢ (𝜑 → 𝑉 ∈ ℕ)
39		vdwlem4.h	. . . . . . 7 ⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
40		vdwlem4.f	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))))
41		vdwlem7.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℕ)
42		vdwlem7.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℕ)
43		vdwlem7.s	. . . . . . 7 ⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (^◡𝐹 “ {𝐺}))
44		vdwlem6.r	. . . . . . 7 ⊢ (𝜑 → (♯‘ran 𝐽) = 𝑀)
45		vdwlem6.t	. . . . . . 7 ⊢ 𝑇 = (𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)))
46		vdwlem6.p	. . . . . . 7 ⊢ 𝑃 = (𝑗 ∈ (1...(𝑀 + 1)) ↦ (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)))
47	38, 12, 6, 39, 40, 18, 14, 8, 41, 42, 43, 16, 20, 22, 2, 44, 45, 46	vdwlem5 16414	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ ℕ)
48	47	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑇 ∈ ℕ)
49		0nn0 11984	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
50	49	a1i 11	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 = (𝑀 + 1)) → 0 ∈ ℕ₀)
51		nnuz 12356	. . . . . . . . . . . . . . . . 17 ⊢ ℕ = (ℤ_≥‘1)
52	18, 51	eleqtrdi 2843	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
53	52	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑀 ∈ (ℤ_≥‘1))
54		elfzp1 13041	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘1) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1))))
55	53, 54	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1))))
56	55	biimpa 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1)))
57	56	ord 863	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 ∈ (1...𝑀) → 𝑗 = (𝑀 + 1)))
58	57	con1d 147	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 = (𝑀 + 1) → 𝑗 ∈ (1...𝑀)))
59	58	imp 410	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → 𝑗 ∈ (1...𝑀))
60	20	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → 𝐸:(1...𝑀)⟶ℕ)
61	60	ffvelrnda 6855	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸‘𝑗) ∈ ℕ)
62	61	nnnn0d 12029	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸‘𝑗) ∈ ℕ₀)
63	59, 62	syldan 594	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → (𝐸‘𝑗) ∈ ℕ₀)
64	50, 63	ifclda 4446	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) ∈ ℕ₀)
65	12, 42	nnmulcld 11762	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 · 𝐷) ∈ ℕ)
66	65	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑊 · 𝐷) ∈ ℕ)
67		nn0nnaddcl 12000	. . . . . . . 8 ⊢ ((if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) ∈ ℕ₀ ∧ (𝑊 · 𝐷) ∈ ℕ) → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
68	64, 66, 67	syl2anc 587	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
69	68, 46	fmptd 6882	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑃:(1...(𝑀 + 1))⟶ℕ)
70		nnex 11715	. . . . . . 7 ⊢ ℕ ∈ V
71		ovex 7197	. . . . . . 7 ⊢ (1...(𝑀 + 1)) ∈ V
72	70, 71	elmap 8474	. . . . . 6 ⊢ (𝑃 ∈ (ℕ ↑_m (1...(𝑀 + 1))) ↔ 𝑃:(1...(𝑀 + 1))⟶ℕ)
73	69, 72	sylibr 237	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑃 ∈ (ℕ ↑_m (1...(𝑀 + 1))))
74		elfzp1 13041	. . . . . . . . . 10 ⊢ (𝑀 ∈ (ℤ_≥‘1) → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1))))
75	52, 74	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1))))
76	16	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℕ)
77	76	nncnd 11725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℂ)
78	77	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ)
79	20	ffvelrnda 6855	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐸‘𝑖) ∈ ℕ)
80	79	nncnd 11725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐸‘𝑖) ∈ ℂ)
81	80	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐸‘𝑖) ∈ ℂ)
82	78, 81	addcld 10731	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝐸‘𝑖)) ∈ ℂ)
83		nnm1nn0 12010	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∈ ℕ → (𝐴 − 1) ∈ ℕ₀)
84	41, 83	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 − 1) ∈ ℕ₀)
85		nn0nnaddcl 12000	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 − 1) ∈ ℕ₀ ∧ 𝑉 ∈ ℕ) → ((𝐴 − 1) + 𝑉) ∈ ℕ)
86	84, 38, 85	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℕ)
87	12, 86	nnmulcld 11762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
88	87	nncnd 11725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
89	88	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
90		elfznn0 13084	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ (0...(𝐾 − 1)) → 𝑚 ∈ ℕ₀)
91	90	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℕ₀)
92	91	nn0cnd 12031	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
93	92	adantlr 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
94	93, 81	mulcld 10732	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝐸‘𝑖)) ∈ ℂ)
95	65	nnnn0d 12029	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑊 · 𝐷) ∈ ℕ₀)
96	95	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℕ₀)
97	91, 96	nn0mulcld 12034	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℕ₀)
98	97	nn0cnd 12031	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
99	98	adantlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
100	82, 89, 94, 99	add4d 10939	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸‘𝑖)) + (𝑚 · (𝑊 · 𝐷)))) = (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
101	65	nncnd 11725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑊 · 𝐷) ∈ ℂ)
102	101	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℂ)
103	93, 81, 102	adddid 10736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))) = ((𝑚 · (𝐸‘𝑖)) + (𝑚 · (𝑊 · 𝐷))))
104	103	oveq2d 7180	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸‘𝑖)) + (𝑚 · (𝑊 · 𝐷)))))
105	12	nncnd 11725	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑊 ∈ ℂ)
106	105	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℂ)
107	86	nncnd 11725	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℂ)
108	107	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 − 1) + 𝑉) ∈ ℂ)
109	42	nncnd 11725	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐷 ∈ ℂ)
110	109	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐷 ∈ ℂ)
111	92, 110	mulcld 10732	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · 𝐷) ∈ ℂ)
112	106, 108, 111	adddid 10736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
113	41	nncnd 11725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐴 ∈ ℂ)
114	113	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐴 ∈ ℂ)
115		1cnd 10707	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 1 ∈ ℂ)
116	114, 111, 115	addsubd 11089	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) − 1) = ((𝐴 − 1) + (𝑚 · 𝐷)))
117	116	oveq1d 7179	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉))
118	84	nn0cnd 12031	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 − 1) ∈ ℂ)
119	118	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 − 1) ∈ ℂ)
120	38	nncnd 11725	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑉 ∈ ℂ)
121	120	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℂ)
122	119, 111, 121	add32d 10938	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
123	117, 122	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
124	123	oveq2d 7180	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))))
125	92, 106, 110	mul12d 10920	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) = (𝑊 · (𝑚 · 𝐷)))
126	125	oveq2d 7180	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
127	112, 124, 126	3eqtr4d 2783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
128	127	adantlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
129	128	oveq2d 7180	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
130	100, 104, 129	3eqtr4d 2783	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
131	38	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
132	12	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
133	43	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴(AP‘𝐾)𝐷) ⊆ (^◡𝐹 “ {𝐺}))
134		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))
135		oveq1 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑚 → (𝑛 · 𝐷) = (𝑚 · 𝐷))
136	135	oveq2d 7180	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = 𝑚 → (𝐴 + (𝑛 · 𝐷)) = (𝐴 + (𝑚 · 𝐷)))
137	136	rspceeqv 3539	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑚 ∈ (0...(𝐾 − 1)) ∧ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
138	134, 137	mpan2 691	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
139	10	nnnn0d 12029	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
140		vdwapval 16402	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
141	139, 41, 42, 140	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
142	141	biimpar 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
143	138, 142	sylan2 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
144	133, 143	sseldd 3876	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (^◡𝐹 “ {𝐺}))
145	38, 12, 6, 39, 40	vdwlem4 16413	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹:(1...𝑉)⟶(𝑅 ↑_m (1...𝑊)))
146	145	ffnd 6499	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹 Fn (1...𝑉))
147		fniniseg 6831	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹 Fn (1...𝑉) → ((𝐴 + (𝑚 · 𝐷)) ∈ (^◡𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
148	146, 147	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (^◡𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
149	148	biimpa 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝐴 + (𝑚 · 𝐷)) ∈ (^◡𝐹 “ {𝐺})) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
150	144, 149	syldan 594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
151	150	simpld 498	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
152	151	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
153	22	r19.21bi 3120	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
154	153	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
155		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))
156		oveq1 7171	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = 𝑚 → (𝑛 · (𝐸‘𝑖)) = (𝑚 · (𝐸‘𝑖)))
157	156	oveq2d 7180	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑚 → ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))))
158	157	rspceeqv 3539	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑚 ∈ (0...(𝐾 − 1)) ∧ ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖))))
159	155, 158	mpan2 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖))))
160	10	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ)
161	160	nnnn0d 12029	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ₀)
162	76, 79	nnaddcld 11761	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ ℕ)
163		vdwapval 16402	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐾 ∈ ℕ₀ ∧ (𝐵 + (𝐸‘𝑖)) ∈ ℕ ∧ (𝐸‘𝑖) ∈ ℕ) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖)))))
164	161, 162, 79, 163	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖)))))
165	164	biimpar 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖)))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)))
166	159, 165	sylan2 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)))
167	154, 166	sseldd 3876	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
168	14	ffnd 6499	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐺 Fn (1...𝑊))
169	168	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐺 Fn (1...𝑊))
170		fniniseg 6831	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 Fn (1...𝑊) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
171	169, 170	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
172	171	biimpa 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))})) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
173	167, 172	syldan 594	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
174	173	simpld 498	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊))
175	131, 132, 152, 174	vdwlem3 16412	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
176	130, 175	eqeltrd 2833	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))))
177		fvoveq1 7187	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
178		eqid 2738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
179		fvex 6681	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
180	177, 178, 179	fvmpt 6769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
181	174, 180	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
182	173	simprd 499	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))
183	150	simprd 499	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)
184		oveq1 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑥 − 1) = ((𝐴 + (𝑚 · 𝐷)) − 1))
185	184	oveq1d 7179	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → ((𝑥 − 1) + 𝑉) = (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))
186	185	oveq2d 7180	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))
187	186	oveq2d 7180	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
188	187	fveq2d 6672	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
189	188	mpteq2dv 5123	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
190		ovex 7197	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1...𝑊) ∈ V
191	190	mptex 6990	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) ∈ V
192	189, 40, 191	fvmpt 6769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
193	151, 192	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
194	183, 193	eqtr3d 2775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
195	194	adantlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
196	195	fveq1d 6670	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))))
197	182, 196	eqtr3d 2775	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘(𝐵 + (𝐸‘𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))))
198	130	fveq2d 6672	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
199	181, 197, 198	3eqtr4rd 2784	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))
200	176, 199	jca 515	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
201		eleq1 2820	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉)))))
202		fveqeq2 6677	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → ((𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))) ↔ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
203	201, 202	anbi12d 634	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → ((𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖)))) ↔ ((((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
204	200, 203	syl5ibrcom 250	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
205	204	rexlimdva 3193	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
206	87	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
207	162, 206	nnaddcld 11761	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
208	65	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℕ)
209	79, 208	nnaddcld 11761	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + (𝑊 · 𝐷)) ∈ ℕ)
210		vdwapval 16402	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ ℕ₀ ∧ ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ ((𝐸‘𝑖) + (𝑊 · 𝐷)) ∈ ℕ) → (𝑥 ∈ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))))
211	161, 207, 209, 210	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))))
212	39	ffnd 6499	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
213	212	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
214		fniniseg 6831	. . . . . . . . . . . . . . 15 ⊢ (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑥 ∈ (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
215	213, 214	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
216	205, 211, 215	3imtr4d 297	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) → 𝑥 ∈ (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))})))
217	216	ssrdv 3881	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) ⊆ (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
218		ssun1 4060	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑀) ⊆ ((1...𝑀) ∪ {(𝑀 + 1)})
219		fzsuc 13038	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (ℤ_≥‘1) → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
220	52, 219	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
221	218, 220	sseqtrrid 3928	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1...𝑀) ⊆ (1...(𝑀 + 1)))
222	221	sselda 3875	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...(𝑀 + 1)))
223		eqeq1 2742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑖 → (𝑗 = (𝑀 + 1) ↔ 𝑖 = (𝑀 + 1)))
224		fveq2 6668	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑖 → (𝐸‘𝑗) = (𝐸‘𝑖))
225	223, 224	ifbieq2d 4437	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) = if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)))
226	225	oveq1d 7179	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) = (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)))
227		ovex 7197	. . . . . . . . . . . . . . . . . 18 ⊢ (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)) ∈ V
228	226, 46, 227	fvmpt 6769	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...(𝑀 + 1)) → (𝑃‘𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)))
229	222, 228	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑃‘𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)))
230	18	nnred 11724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑀 ∈ ℝ)
231	230	ltp1d 11641	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
232		peano2re 10884	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
233	230, 232	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑀 + 1) ∈ ℝ)
234	230, 233	ltnled 10858	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀))
235	231, 234	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀)
236		breq1 5030	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = (𝑀 + 1) → (𝑖 ≤ 𝑀 ↔ (𝑀 + 1) ≤ 𝑀))
237	236	notbid 321	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = (𝑀 + 1) → (¬ 𝑖 ≤ 𝑀 ↔ ¬ (𝑀 + 1) ≤ 𝑀))
238	235, 237	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑖 = (𝑀 + 1) → ¬ 𝑖 ≤ 𝑀))
239	238	con2d 136	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑖 ≤ 𝑀 → ¬ 𝑖 = (𝑀 + 1)))
240		elfzle2 12995	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ≤ 𝑀)
241	239, 240	impel 509	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ¬ 𝑖 = (𝑀 + 1))
242		iffalse 4420	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑖 = (𝑀 + 1) → if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) = (𝐸‘𝑖))
243	242	oveq1d 7179	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑖 = (𝑀 + 1) → (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)) = ((𝐸‘𝑖) + (𝑊 · 𝐷)))
244	241, 243	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)) = ((𝐸‘𝑖) + (𝑊 · 𝐷)))
245	229, 244	eqtrd 2773	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑃‘𝑖) = ((𝐸‘𝑖) + (𝑊 · 𝐷)))
246	245	oveq2d 7180	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃‘𝑖)) = (𝑇 + ((𝐸‘𝑖) + (𝑊 · 𝐷))))
247	47	nncnd 11725	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ ℂ)
248	247	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑇 ∈ ℂ)
249	101	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℂ)
250	248, 80, 249	add12d 10937	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑇 + ((𝐸‘𝑖) + (𝑊 · 𝐷))) = ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))))
251	45	oveq1i 7174	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑇 + (𝑊 · 𝐷)) = ((𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) + (𝑊 · 𝐷))
252	16	nncnd 11725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ ℂ)
253	120, 109	subcld 11068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑉 − 𝐷) ∈ ℂ)
254	113, 253	addcld 10731	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴 + (𝑉 − 𝐷)) ∈ ℂ)
255		ax-1cn 10666	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
256		subcl 10956	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 + (𝑉 − 𝐷)) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 + (𝑉 − 𝐷)) − 1) ∈ ℂ)
257	254, 255, 256	sylancl 589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐴 + (𝑉 − 𝐷)) − 1) ∈ ℂ)
258	105, 257	mulcld 10732	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) ∈ ℂ)
259	252, 258, 101	addassd 10734	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷))))
260	105, 257, 109	adddid 10736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑊 · (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷)) = ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷)))
261	113, 253, 109	addassd 10734	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐴 + (𝑉 − 𝐷)) + 𝐷) = (𝐴 + ((𝑉 − 𝐷) + 𝐷)))
262	120, 109	npcand 11072	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝑉 − 𝐷) + 𝐷) = 𝑉)
263	262	oveq2d 7180	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐴 + ((𝑉 − 𝐷) + 𝐷)) = (𝐴 + 𝑉))
264	261, 263	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐴 + (𝑉 − 𝐷)) + 𝐷) = (𝐴 + 𝑉))
265	264	oveq1d 7179	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴 + (𝑉 − 𝐷)) + 𝐷) − 1) = ((𝐴 + 𝑉) − 1))
266		1cnd 10707	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ ℂ)
267	254, 109, 266	addsubd 11089	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴 + (𝑉 − 𝐷)) + 𝐷) − 1) = (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷))
268	113, 120, 266	addsubd 11089	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 + 𝑉) − 1) = ((𝐴 − 1) + 𝑉))
269	265, 267, 268	3eqtr3d 2781	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷) = ((𝐴 − 1) + 𝑉))
270	269	oveq2d 7180	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑊 · (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
271	260, 270	eqtr3d 2775	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
272	271	oveq2d 7180	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐵 + ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
273	259, 272	eqtrd 2773	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
274	251, 273	syl5eq 2785	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑇 + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
275	274	oveq2d 7180	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸‘𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
276	275	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸‘𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
277	88	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
278	80, 77, 277	addassd 10734	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐸‘𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐸‘𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
279	80, 77	addcomd 10913	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + 𝐵) = (𝐵 + (𝐸‘𝑖)))
280	279	oveq1d 7179	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐸‘𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
281	276, 278, 280	3eqtr2d 2779	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
282	246, 250, 281	3eqtrd 2777	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃‘𝑖)) = ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
283	282, 245	oveq12d 7182	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))))
284		cnvimass 5917	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ⊆ dom 𝐺
285	284, 14	fssdm 6518	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ⊆ (1...𝑊))
286	285	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ⊆ (1...𝑊))
287		vdwapid1 16404	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ ℕ ∧ (𝐵 + (𝐸‘𝑖)) ∈ ℕ ∧ (𝐸‘𝑖) ∈ ℕ) → (𝐵 + (𝐸‘𝑖)) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)))
288	160, 162, 79, 287	syl3anc 1372	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)))
289	153, 288	sseldd 3876	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
290	286, 289	sseldd 3876	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ (1...𝑊))
291		fvoveq1 7187	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝐵 + (𝐸‘𝑖)) → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
292		eqid 2738	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
293		fvex 6681	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
294	291, 292, 293	fvmpt 6769	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 + (𝐸‘𝑖)) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
295	290, 294	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
296		vdwapid1 16404	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
297	10, 41, 42, 296	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
298	43, 297	sseldd 3876	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ (^◡𝐹 “ {𝐺}))
299		fniniseg 6831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 Fn (1...𝑉) → (𝐴 ∈ (^◡𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹‘𝐴) = 𝐺)))
300	146, 299	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴 ∈ (^◡𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹‘𝐴) = 𝐺)))
301	298, 300	mpbid 235	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 ∈ (1...𝑉) ∧ (𝐹‘𝐴) = 𝐺))
302	301	simprd 499	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐺)
303	301	simpld 498	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ (1...𝑉))
304		oveq1 7171	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝐴 → (𝑥 − 1) = (𝐴 − 1))
305	304	oveq1d 7179	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝐴 → ((𝑥 − 1) + 𝑉) = ((𝐴 − 1) + 𝑉))
306	305	oveq2d 7180	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝐴 → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
307	306	oveq2d 7180	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝐴 → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))
308	307	fveq2d 6672	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝐴 → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
309	308	mpteq2dv 5123	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
310	190	mptex 6990	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) ∈ V
311	309, 40, 310	fvmpt 6769	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ (1...𝑉) → (𝐹‘𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
312	303, 311	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹‘𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
313	302, 312	eqtr3d 2775	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
314	313	fveq1d 6670	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐺‘(𝐵 + (𝐸‘𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))))
315	314	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐵 + (𝐸‘𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))))
316	282	fveq2d 6672	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃‘𝑖))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
317	295, 315, 316	3eqtr4rd 2784	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃‘𝑖))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))
318	317	sneqd 4525	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → {(𝐻‘(𝑇 + (𝑃‘𝑖)))} = {(𝐺‘(𝐵 + (𝐸‘𝑖)))})
319	318	imaeq2d 5897	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) = (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
320	217, 283, 319	3sstr4d 3922	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))
321	320	ex 416	. . . . . . . . . 10 ⊢ (𝜑 → (𝑖 ∈ (1...𝑀) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
322	252	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ)
323	88	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
324	322, 323, 98	addassd 10734	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
325	127	oveq2d 7180	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
326	324, 325	eqtr4d 2776	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
327	38	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
328	12	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
329		eluzfz1 12998	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 ∈ (ℤ_≥‘1) → 1 ∈ (1...𝑀))
330	52, 329	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ (1...𝑀))
331	330	ne0d 4222	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1...𝑀) ≠ ∅)
332		elfzuz3 12988	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵 + (𝐸‘𝑖)) ∈ (1...𝑊) → 𝑊 ∈ (ℤ_≥‘(𝐵 + (𝐸‘𝑖))))
333	290, 332	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ_≥‘(𝐵 + (𝐸‘𝑖))))
334	16	nnzd 12160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐵 ∈ ℤ)
335		uzid 12332	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ (ℤ_≥‘𝐵))
336	334, 335	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐵 ∈ (ℤ_≥‘𝐵))
337	336	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ∈ (ℤ_≥‘𝐵))
338	79	nnnn0d 12029	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐸‘𝑖) ∈ ℕ₀)
339		uzaddcl 12379	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵 ∈ (ℤ_≥‘𝐵) ∧ (𝐸‘𝑖) ∈ ℕ₀) → (𝐵 + (𝐸‘𝑖)) ∈ (ℤ_≥‘𝐵))
340	337, 338, 339	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ (ℤ_≥‘𝐵))
341		uztrn 12335	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑊 ∈ (ℤ_≥‘(𝐵 + (𝐸‘𝑖))) ∧ (𝐵 + (𝐸‘𝑖)) ∈ (ℤ_≥‘𝐵)) → 𝑊 ∈ (ℤ_≥‘𝐵))
342	333, 340, 341	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ_≥‘𝐵))
343		eluzle 12330	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑊 ∈ (ℤ_≥‘𝐵) → 𝐵 ≤ 𝑊)
344	342, 343	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ≤ 𝑊)
345	344	ralrimiva 3096	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊)
346		r19.2z 4378	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...𝑀) ≠ ∅ ∧ ∀𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊) → ∃𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊)
347	331, 345, 346	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ∃𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊)
348		idd 24	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ (1...𝑀) → (𝐵 ≤ 𝑊 → 𝐵 ≤ 𝑊))
349	348	rexlimiv 3189	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊 → 𝐵 ≤ 𝑊)
350	347, 349	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ≤ 𝑊)
351	12	nnzd 12160	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑊 ∈ ℤ)
352		fznn 13059	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑊 ∈ ℤ → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵 ≤ 𝑊)))
353	351, 352	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵 ≤ 𝑊)))
354	16, 350, 353	mpbir2and 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ (1...𝑊))
355	354	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ (1...𝑊))
356	327, 328, 151, 355	vdwlem3 16412	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
357	326, 356	eqeltrd 2833	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))))
358		fvoveq1 7187	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
359		fvex 6681	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
360	358, 178, 359	fvmpt 6769	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
361	355, 360	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
362	194	fveq1d 6670	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵))
363	326	fveq2d 6672	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
364	361, 362, 363	3eqtr4rd 2784	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵))
365	357, 364	jca 515	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵)))
366		eleq1 2820	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉)))))
367		fveqeq2 6677	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝐻‘𝑧) = (𝐺‘𝐵) ↔ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵)))
368	366, 367	anbi12d 634	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵)) ↔ (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵))))
369	365, 368	syl5ibrcom 250	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵))))
370	369	rexlimdva 3193	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵))))
371	16, 87	nnaddcld 11761	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
372		vdwapval 16402	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ ℕ₀ ∧ (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ (𝑊 · 𝐷) ∈ ℕ) → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
373	139, 371, 65, 372	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
374		fniniseg 6831	. . . . . . . . . . . . . . 15 ⊢ (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑧 ∈ (^◡𝐻 “ {(𝐺‘𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵))))
375	212, 374	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑧 ∈ (^◡𝐻 “ {(𝐺‘𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵))))
376	370, 373, 375	3imtr4d 297	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) → 𝑧 ∈ (^◡𝐻 “ {(𝐺‘𝐵)})))
377	376	ssrdv 3881	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ⊆ (^◡𝐻 “ {(𝐺‘𝐵)}))
378	18	peano2nnd 11726	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ)
379	378, 51	eleqtrdi 2843	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) ∈ (ℤ_≥‘1))
380		eluzfz2 12999	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘1) → (𝑀 + 1) ∈ (1...(𝑀 + 1)))
381		iftrue 4417	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑀 + 1) → if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) = 0)
382	381	oveq1d 7179	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑀 + 1) → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) = (0 + (𝑊 · 𝐷)))
383		ovex 7197	. . . . . . . . . . . . . . . . . 18 ⊢ (0 + (𝑊 · 𝐷)) ∈ V
384	382, 46, 383	fvmpt 6769	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 + 1) ∈ (1...(𝑀 + 1)) → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
385	379, 380, 384	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
386	101	addid2d 10912	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 + (𝑊 · 𝐷)) = (𝑊 · 𝐷))
387	385, 386	eqtrd 2773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃‘(𝑀 + 1)) = (𝑊 · 𝐷))
388	387	oveq2d 7180	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝑇 + (𝑊 · 𝐷)))
389	388, 274	eqtrd 2773	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
390	389, 387	oveq12d 7182	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)))
391		fvoveq1 7187	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
392		fvex 6681	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
393	391, 292, 392	fvmpt 6769	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
394	354, 393	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
395	313	fveq1d 6670	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵))
396	389	fveq2d 6672	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
397	394, 395, 396	3eqtr4rd 2784	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐺‘𝐵))
398	397	sneqd 4525	. . . . . . . . . . . . 13 ⊢ (𝜑 → {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))} = {(𝐺‘𝐵)})
399	398	imaeq2d 5897	. . . . . . . . . . . 12 ⊢ (𝜑 → (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}) = (^◡𝐻 “ {(𝐺‘𝐵)}))
400	377, 390, 399	3sstr4d 3922	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
401		fveq2 6668	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑀 + 1) → (𝑃‘𝑖) = (𝑃‘(𝑀 + 1)))
402	401	oveq2d 7180	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝑀 + 1) → (𝑇 + (𝑃‘𝑖)) = (𝑇 + (𝑃‘(𝑀 + 1))))
403	402, 401	oveq12d 7182	. . . . . . . . . . . 12 ⊢ (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) = ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))))
404	402	fveq2d 6672	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑀 + 1) → (𝐻‘(𝑇 + (𝑃‘𝑖))) = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
405	404	sneqd 4525	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝑀 + 1) → {(𝐻‘(𝑇 + (𝑃‘𝑖)))} = {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})
406	405	imaeq2d 5897	. . . . . . . . . . . 12 ⊢ (𝑖 = (𝑀 + 1) → (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) = (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
407	403, 406	sseq12d 3908	. . . . . . . . . . 11 ⊢ (𝑖 = (𝑀 + 1) → (((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) ↔ ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})))
408	400, 407	syl5ibrcom 250	. . . . . . . . . 10 ⊢ (𝜑 → (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
409	321, 408	jaod 858	. . . . . . . . 9 ⊢ (𝜑 → ((𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
410	75, 409	sylbid 243	. . . . . . . 8 ⊢ (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
411	410	ralrimiv 3095	. . . . . . 7 ⊢ (𝜑 → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))
412	411	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))
413	220	rexeqdv 3316	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ ∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))))
414		rexun 4078	. . . . . . . . . . . . 13 ⊢ (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))))
415	317	eqeq2d 2749	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
416	415	rexbidva 3205	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
417		ovex 7197	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 + 1) ∈ V
418	404	eqeq2d 2749	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑀 + 1) → (𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))))
419	417, 418	rexsn 4570	. . . . . . . . . . . . . . 15 ⊢ (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
420	397	eqeq2d 2749	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) ↔ 𝑥 = (𝐺‘𝐵)))
421	419, 420	syl5bb 286	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐺‘𝐵)))
422	416, 421	orbi12d 918	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))))
423	414, 422	syl5bb 286	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))))
424	413, 423	bitrd 282	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))))
425	424	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))))
426	425	abbidv 2802	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))} = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))})
427		eqid 2738	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))
428	427	rnmpt 5792	. . . . . . . . 9 ⊢ ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))) = {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))}
429	2	rnmpt 5792	. . . . . . . . . . 11 ⊢ ran 𝐽 = {𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))}
430		df-sn 4514	. . . . . . . . . . 11 ⊢ {(𝐺‘𝐵)} = {𝑥 ∣ 𝑥 = (𝐺‘𝐵)}
431	429, 430	uneq12i 4049	. . . . . . . . . 10 ⊢ (ran 𝐽 ∪ {(𝐺‘𝐵)}) = ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))} ∪ {𝑥 ∣ 𝑥 = (𝐺‘𝐵)})
432		unab 4186	. . . . . . . . . 10 ⊢ ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))} ∪ {𝑥 ∣ 𝑥 = (𝐺‘𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))}
433	431, 432	eqtri 2761	. . . . . . . . 9 ⊢ (ran 𝐽 ∪ {(𝐺‘𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))}
434	426, 428, 433	3eqtr4g 2798	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))) = (ran 𝐽 ∪ {(𝐺‘𝐵)}))
435	434	fveq2d 6672	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (♯‘(ran 𝐽 ∪ {(𝐺‘𝐵)})))
436		fzfi 13424	. . . . . . . . . 10 ⊢ (1...𝑀) ∈ Fin
437		dffn4 6592	. . . . . . . . . . 11 ⊢ (𝐽 Fn (1...𝑀) ↔ 𝐽:(1...𝑀)–onto→ran 𝐽)
438	3, 437	mpbi 233	. . . . . . . . . 10 ⊢ 𝐽:(1...𝑀)–onto→ran 𝐽
439		fofi 8876	. . . . . . . . . 10 ⊢ (((1...𝑀) ∈ Fin ∧ 𝐽:(1...𝑀)–onto→ran 𝐽) → ran 𝐽 ∈ Fin)
440	436, 438, 439	mp2an 692	. . . . . . . . 9 ⊢ ran 𝐽 ∈ Fin
441	440	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ran 𝐽 ∈ Fin)
442		fvex 6681	. . . . . . . . 9 ⊢ (𝐺‘𝐵) ∈ V
443		hashunsng 13838	. . . . . . . . 9 ⊢ ((𝐺‘𝐵) ∈ V → ((ran 𝐽 ∈ Fin ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺‘𝐵)})) = ((♯‘ran 𝐽) + 1)))
444	442, 443	ax-mp 5	. . . . . . . 8 ⊢ ((ran 𝐽 ∈ Fin ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺‘𝐵)})) = ((♯‘ran 𝐽) + 1))
445	441, 444	sylan 583	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺‘𝐵)})) = ((♯‘ran 𝐽) + 1))
446	44	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘ran 𝐽) = 𝑀)
447	446	oveq1d 7179	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ((♯‘ran 𝐽) + 1) = (𝑀 + 1))
448	435, 445, 447	3eqtrd 2777	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1))
449	412, 448	jca 515	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1)))
450		oveq1 7171	. . . . . . . . . 10 ⊢ (𝑎 = 𝑇 → (𝑎 + (𝑑‘𝑖)) = (𝑇 + (𝑑‘𝑖)))
451	450	oveq1d 7179	. . . . . . . . 9 ⊢ (𝑎 = 𝑇 → ((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) = ((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)))
452		fvoveq1 7187	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑇 → (𝐻‘(𝑎 + (𝑑‘𝑖))) = (𝐻‘(𝑇 + (𝑑‘𝑖))))
453	452	sneqd 4525	. . . . . . . . . 10 ⊢ (𝑎 = 𝑇 → {(𝐻‘(𝑎 + (𝑑‘𝑖)))} = {(𝐻‘(𝑇 + (𝑑‘𝑖)))})
454	453	imaeq2d 5897	. . . . . . . . 9 ⊢ (𝑎 = 𝑇 → (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) = (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}))
455	451, 454	sseq12d 3908	. . . . . . . 8 ⊢ (𝑎 = 𝑇 → (((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ↔ ((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))})))
456	455	ralbidv 3109	. . . . . . 7 ⊢ (𝑎 = 𝑇 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))})))
457	452	mpteq2dv 5123	. . . . . . . . 9 ⊢ (𝑎 = 𝑇 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))))
458	457	rneqd 5775	. . . . . . . 8 ⊢ (𝑎 = 𝑇 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))))
459	458	fveqeq2d 6676	. . . . . . 7 ⊢ (𝑎 = 𝑇 → ((♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1) ↔ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1)))
460	456, 459	anbi12d 634	. . . . . 6 ⊢ (𝑎 = 𝑇 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1))))
461		fveq1 6667	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑃 → (𝑑‘𝑖) = (𝑃‘𝑖))
462	461	oveq2d 7180	. . . . . . . . . 10 ⊢ (𝑑 = 𝑃 → (𝑇 + (𝑑‘𝑖)) = (𝑇 + (𝑃‘𝑖)))
463	462, 461	oveq12d 7182	. . . . . . . . 9 ⊢ (𝑑 = 𝑃 → ((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) = ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)))
464	462	fveq2d 6672	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑃 → (𝐻‘(𝑇 + (𝑑‘𝑖))) = (𝐻‘(𝑇 + (𝑃‘𝑖))))
465	464	sneqd 4525	. . . . . . . . . 10 ⊢ (𝑑 = 𝑃 → {(𝐻‘(𝑇 + (𝑑‘𝑖)))} = {(𝐻‘(𝑇 + (𝑃‘𝑖)))})
466	465	imaeq2d 5897	. . . . . . . . 9 ⊢ (𝑑 = 𝑃 → (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) = (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))
467	463, 466	sseq12d 3908	. . . . . . . 8 ⊢ (𝑑 = 𝑃 → (((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ↔ ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
468	467	ralbidv 3109	. . . . . . 7 ⊢ (𝑑 = 𝑃 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
469	464	mpteq2dv 5123	. . . . . . . . 9 ⊢ (𝑑 = 𝑃 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))))
470	469	rneqd 5775	. . . . . . . 8 ⊢ (𝑑 = 𝑃 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))))
471	470	fveqeq2d 6676	. . . . . . 7 ⊢ (𝑑 = 𝑃 → ((♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1) ↔ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1)))
472	468, 471	anbi12d 634	. . . . . 6 ⊢ (𝑑 = 𝑃 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1))))
473	460, 472	rspc2ev 3536	. . . . 5 ⊢ ((𝑇 ∈ ℕ ∧ 𝑃 ∈ (ℕ ↑_m (1...(𝑀 + 1))) ∧ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1))) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑_m (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1)))
474	48, 73, 449, 473	syl3anc 1372	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑_m (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1)))
475		ovex 7197	. . . . 5 ⊢ (1...(𝑊 · (2 · 𝑉))) ∈ V
476	10	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ)
477	476	nnnn0d 12029	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ₀)
478	39	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
479	18	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑀 ∈ ℕ)
480	479	peano2nnd 11726	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (𝑀 + 1) ∈ ℕ)
481		eqid 2738	. . . . 5 ⊢ (1...(𝑀 + 1)) = (1...(𝑀 + 1))
482	475, 477, 478, 480, 481	vdwpc 16409	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑_m (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1))))
483	474, 482	mpbird 260	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻)
484	483	orcd 872	. 2 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))
485	37, 484	pm2.61dan 813	1 ⊢ (𝜑 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 846 = wceq 1542 ∈ wcel 2113 {cab 2716 ≠ wne 2934 ∀wral 3053 ∃wrex 3054 Vcvv 3397 ∪ cun 3839 ⊆ wss 3841 ∅c0 4209 ifcif 4411 {csn 4513 ⟨cop 4519 class class class wbr 5027 ↦ cmpt 5107 ^◡ccnv 5518 ran crn 5520 “ cima 5522 Fn wfn 6328 ⟶wf 6329 –onto→wfo 6331 ‘cfv 6333 (class class class)co 7164 ↑_m cmap 8430 Fincfn 8548 ℂcc 10606 ℝcr 10607 0cc0 10608 1c1 10609 + caddc 10611 · cmul 10613 < clt 10746 ≤ cle 10747 − cmin 10941 ℕcn 11709 2c2 11764 ℕ₀cn0 11969 ℤcz 12055 ℤ_≥cuz 12317 ...cfz 12974 ♯chash 13775 APcvdwa 16394 MonoAP cvdwm 16395 PolyAP cvdwp 16396

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-rep 5151 ax-sep 5164 ax-nul 5171 ax-pow 5229 ax-pr 5293 ax-un 7473 ax-cnex 10664 ax-resscn 10665 ax-1cn 10666 ax-icn 10667 ax-addcl 10668 ax-addrcl 10669 ax-mulcl 10670 ax-mulrcl 10671 ax-mulcom 10672 ax-addass 10673 ax-mulass 10674 ax-distr 10675 ax-i2m1 10676 ax-1ne0 10677 ax-1rid 10678 ax-rnegex 10679 ax-rrecex 10680 ax-cnre 10681 ax-pre-lttri 10682 ax-pre-lttrn 10683 ax-pre-ltadd 10684 ax-pre-mulgt0 10685

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rab 3062 df-v 3399 df-sbc 3680 df-csb 3789 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-pss 3860 df-nul 4210 df-if 4412 df-pw 4487 df-sn 4514 df-pr 4516 df-tp 4518 df-op 4520 df-uni 4794 df-int 4834 df-iun 4880 df-br 5028 df-opab 5090 df-mpt 5108 df-tr 5134 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6123 df-ord 6169 df-on 6170 df-lim 6171 df-suc 6172 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-f1 6338 df-fo 6339 df-f1o 6340 df-fv 6341 df-riota 7121 df-ov 7167 df-oprab 7168 df-mpo 7169 df-om 7594 df-1st 7707 df-2nd 7708 df-wrecs 7969 df-recs 8030 df-rdg 8068 df-1o 8124 df-oadd 8128 df-er 8313 df-map 8432 df-en 8549 df-dom 8550 df-sdom 8551 df-fin 8552 df-dju 9396 df-card 9434 df-pnf 10748 df-mnf 10749 df-xr 10750 df-ltxr 10751 df-le 10752 df-sub 10943 df-neg 10944 df-nn 11710 df-2 11772 df-n0 11970 df-z 12056 df-uz 12318 df-rp 12466 df-fz 12975 df-hash 13776 df-vdwap 16397 df-vdwmc 16398 df-vdwpc 16399

This theorem is referenced by: vdwlem7 16416

W3C validator