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 16919

Description: Lemma for vdw 16927. (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 6905	. . . . . . 7 ⊢ (𝐺‘(𝐵 + (𝐸‘𝑖))) ∈ V
2		vdwlem6.j	. . . . . . 7 ⊢ 𝐽 = (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝐵 + (𝐸‘𝑖))))
3	1, 2	fnmpti 6694	. . . . . 6 ⊢ 𝐽 Fn (1...𝑀)
4		fvelrnb 6953	. . . . . 6 ⊢ (𝐽 Fn (1...𝑀) → ((𝐺‘𝐵) ∈ ran 𝐽 ↔ ∃𝑚 ∈ (1...𝑀)(𝐽‘𝑚) = (𝐺‘𝐵)))
5	3, 4	ax-mp 5	. . . . 5 ⊢ ((𝐺‘𝐵) ∈ ran 𝐽 ↔ ∃𝑚 ∈ (1...𝑀)(𝐽‘𝑚) = (𝐺‘𝐵))
6		vdwlem4.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Fin)
7	6	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝑅 ∈ Fin)
8		vdwlem7.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘2))
9		eluz2nn 12868	. . . . . . . . 9 ⊢ (𝐾 ∈ (ℤ_≥‘2) → 𝐾 ∈ ℕ)
10	8, 9	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ℕ)
11	10	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝐾 ∈ ℕ)
12		vdwlem3.w	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ ℕ)
13	12	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝑊 ∈ ℕ)
14		vdwlem7.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺:(1...𝑊)⟶𝑅)
15	14	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝐺:(1...𝑊)⟶𝑅)
16		vdwlem6.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℕ)
17	16	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝐵 ∈ ℕ)
18		vdwlem7.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ)
19	18	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝑀 ∈ ℕ)
20		vdwlem6.e	. . . . . . . 8 ⊢ (𝜑 → 𝐸:(1...𝑀)⟶ℕ)
21	20	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝐸:(1...𝑀)⟶ℕ)
22		vdwlem6.s	. . . . . . . 8 ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
23	22	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
24		simprl 770	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝑚 ∈ (1...𝑀))
25		simprr 772	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐽‘𝑚) = (𝐺‘𝐵))
26		fveq2 6892	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑚 → (𝐸‘𝑖) = (𝐸‘𝑚))
27	26	oveq2d 7425	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑚 → (𝐵 + (𝐸‘𝑖)) = (𝐵 + (𝐸‘𝑚)))
28	27	fveq2d 6896	. . . . . . . . . 10 ⊢ (𝑖 = 𝑚 → (𝐺‘(𝐵 + (𝐸‘𝑖))) = (𝐺‘(𝐵 + (𝐸‘𝑚))))
29		fvex 6905	. . . . . . . . . 10 ⊢ (𝐺‘(𝐵 + (𝐸‘𝑚))) ∈ V
30	28, 2, 29	fvmpt 6999	. . . . . . . . 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 16914	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐾 + 1) MonoAP 𝐺)
34	33	rexlimdvaa 3157	. . . . 5 ⊢ (𝜑 → (∃𝑚 ∈ (1...𝑀)(𝐽‘𝑚) = (𝐺‘𝐵) → (𝐾 + 1) MonoAP 𝐺))
35	5, 34	biimtrid 241	. . . 4 ⊢ (𝜑 → ((𝐺‘𝐵) ∈ ran 𝐽 → (𝐾 + 1) MonoAP 𝐺))
36	35	imp 408	. . 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 16918	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ ℕ)
48	47	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑇 ∈ ℕ)
49		0nn0 12487	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
50	49	a1i 11	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 = (𝑀 + 1)) → 0 ∈ ℕ₀)
51		nnuz 12865	. . . . . . . . . . . . . . . . 17 ⊢ ℕ = (ℤ_≥‘1)
52	18, 51	eleqtrdi 2844	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
53	52	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑀 ∈ (ℤ_≥‘1))
54		elfzp1 13551	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘1) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1))))
55	53, 54	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1))))
56	55	biimpa 478	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1)))
57	56	ord 863	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 ∈ (1...𝑀) → 𝑗 = (𝑀 + 1)))
58	57	con1d 145	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 = (𝑀 + 1) → 𝑗 ∈ (1...𝑀)))
59	58	imp 408	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → 𝑗 ∈ (1...𝑀))
60	20	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → 𝐸:(1...𝑀)⟶ℕ)
61	60	ffvelcdmda 7087	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸‘𝑗) ∈ ℕ)
62	61	nnnn0d 12532	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸‘𝑗) ∈ ℕ₀)
63	59, 62	syldan 592	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → (𝐸‘𝑗) ∈ ℕ₀)
64	50, 63	ifclda 4564	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) ∈ ℕ₀)
65	12, 42	nnmulcld 12265	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 · 𝐷) ∈ ℕ)
66	65	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑊 · 𝐷) ∈ ℕ)
67		nn0nnaddcl 12503	. . . . . . . 8 ⊢ ((if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) ∈ ℕ₀ ∧ (𝑊 · 𝐷) ∈ ℕ) → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
68	64, 66, 67	syl2anc 585	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
69	68, 46	fmptd 7114	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑃:(1...(𝑀 + 1))⟶ℕ)
70		nnex 12218	. . . . . . 7 ⊢ ℕ ∈ V
71		ovex 7442	. . . . . . 7 ⊢ (1...(𝑀 + 1)) ∈ V
72	70, 71	elmap 8865	. . . . . 6 ⊢ (𝑃 ∈ (ℕ ↑_m (1...(𝑀 + 1))) ↔ 𝑃:(1...(𝑀 + 1))⟶ℕ)
73	69, 72	sylibr 233	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑃 ∈ (ℕ ↑_m (1...(𝑀 + 1))))
74		elfzp1 13551	. . . . . . . . . 10 ⊢ (𝑀 ∈ (ℤ_≥‘1) → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1))))
75	52, 74	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1))))
76	16	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℕ)
77	76	nncnd 12228	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℂ)
78	77	adantr 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ)
79	20	ffvelcdmda 7087	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐸‘𝑖) ∈ ℕ)
80	79	nncnd 12228	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐸‘𝑖) ∈ ℂ)
81	80	adantr 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐸‘𝑖) ∈ ℂ)
82	78, 81	addcld 11233	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝐸‘𝑖)) ∈ ℂ)
83		nnm1nn0 12513	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∈ ℕ → (𝐴 − 1) ∈ ℕ₀)
84	41, 83	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 − 1) ∈ ℕ₀)
85		nn0nnaddcl 12503	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 − 1) ∈ ℕ₀ ∧ 𝑉 ∈ ℕ) → ((𝐴 − 1) + 𝑉) ∈ ℕ)
86	84, 38, 85	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℕ)
87	12, 86	nnmulcld 12265	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
88	87	nncnd 12228	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
89	88	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
90		elfznn0 13594	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ (0...(𝐾 − 1)) → 𝑚 ∈ ℕ₀)
91	90	adantl 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℕ₀)
92	91	nn0cnd 12534	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
93	92	adantlr 714	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
94	93, 81	mulcld 11234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝐸‘𝑖)) ∈ ℂ)
95	65	nnnn0d 12532	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑊 · 𝐷) ∈ ℕ₀)
96	95	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℕ₀)
97	91, 96	nn0mulcld 12537	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℕ₀)
98	97	nn0cnd 12534	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
99	98	adantlr 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
100	82, 89, 94, 99	add4d 11442	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸‘𝑖)) + (𝑚 · (𝑊 · 𝐷)))) = (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
101	65	nncnd 12228	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑊 · 𝐷) ∈ ℂ)
102	101	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℂ)
103	93, 81, 102	adddid 11238	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))) = ((𝑚 · (𝐸‘𝑖)) + (𝑚 · (𝑊 · 𝐷))))
104	103	oveq2d 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸‘𝑖)) + (𝑚 · (𝑊 · 𝐷)))))
105	12	nncnd 12228	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑊 ∈ ℂ)
106	105	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℂ)
107	86	nncnd 12228	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℂ)
108	107	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 − 1) + 𝑉) ∈ ℂ)
109	42	nncnd 12228	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐷 ∈ ℂ)
110	109	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐷 ∈ ℂ)
111	92, 110	mulcld 11234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · 𝐷) ∈ ℂ)
112	106, 108, 111	adddid 11238	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
113	41	nncnd 12228	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐴 ∈ ℂ)
114	113	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐴 ∈ ℂ)
115		1cnd 11209	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 1 ∈ ℂ)
116	114, 111, 115	addsubd 11592	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) − 1) = ((𝐴 − 1) + (𝑚 · 𝐷)))
117	116	oveq1d 7424	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉))
118	84	nn0cnd 12534	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 − 1) ∈ ℂ)
119	118	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 − 1) ∈ ℂ)
120	38	nncnd 12228	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑉 ∈ ℂ)
121	120	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℂ)
122	119, 111, 121	add32d 11441	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
123	117, 122	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
124	123	oveq2d 7425	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))))
125	92, 106, 110	mul12d 11423	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) = (𝑊 · (𝑚 · 𝐷)))
126	125	oveq2d 7425	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
127	112, 124, 126	3eqtr4d 2783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
128	127	adantlr 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
129	128	oveq2d 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
130	100, 104, 129	3eqtr4d 2783	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
131	38	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
132	12	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
133	43	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴(AP‘𝐾)𝐷) ⊆ (^◡𝐹 “ {𝐺}))
134		eqid 2733	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))
135		oveq1 7416	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑚 → (𝑛 · 𝐷) = (𝑚 · 𝐷))
136	135	oveq2d 7425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = 𝑚 → (𝐴 + (𝑛 · 𝐷)) = (𝐴 + (𝑚 · 𝐷)))
137	136	rspceeqv 3634	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑚 ∈ (0...(𝐾 − 1)) ∧ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
138	134, 137	mpan2 690	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
139	10	nnnn0d 12532	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
140		vdwapval 16906	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
141	139, 41, 42, 140	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
142	141	biimpar 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
143	138, 142	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
144	133, 143	sseldd 3984	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (^◡𝐹 “ {𝐺}))
145	38, 12, 6, 39, 40	vdwlem4 16917	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹:(1...𝑉)⟶(𝑅 ↑_m (1...𝑊)))
146	145	ffnd 6719	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹 Fn (1...𝑉))
147		fniniseg 7062	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹 Fn (1...𝑉) → ((𝐴 + (𝑚 · 𝐷)) ∈ (^◡𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
148	146, 147	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (^◡𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
149	148	biimpa 478	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝐴 + (𝑚 · 𝐷)) ∈ (^◡𝐹 “ {𝐺})) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
150	144, 149	syldan 592	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
151	150	simpld 496	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
152	151	adantlr 714	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
153	22	r19.21bi 3249	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
154	153	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
155		eqid 2733	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))
156		oveq1 7416	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = 𝑚 → (𝑛 · (𝐸‘𝑖)) = (𝑚 · (𝐸‘𝑖)))
157	156	oveq2d 7425	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑚 → ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))))
158	157	rspceeqv 3634	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑚 ∈ (0...(𝐾 − 1)) ∧ ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖))))
159	155, 158	mpan2 690	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖))))
160	10	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ)
161	160	nnnn0d 12532	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ₀)
162	76, 79	nnaddcld 12264	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ ℕ)
163		vdwapval 16906	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐾 ∈ ℕ₀ ∧ (𝐵 + (𝐸‘𝑖)) ∈ ℕ ∧ (𝐸‘𝑖) ∈ ℕ) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖)))))
164	161, 162, 79, 163	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖)))))
165	164	biimpar 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖)))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)))
166	159, 165	sylan2 594	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)))
167	154, 166	sseldd 3984	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
168	14	ffnd 6719	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐺 Fn (1...𝑊))
169	168	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐺 Fn (1...𝑊))
170		fniniseg 7062	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 Fn (1...𝑊) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
171	169, 170	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
172	171	biimpa 478	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))})) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
173	167, 172	syldan 592	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
174	173	simpld 496	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊))
175	131, 132, 152, 174	vdwlem3 16916	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
176	130, 175	eqeltrd 2834	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))))
177		fvoveq1 7432	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
178		eqid 2733	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
179		fvex 6905	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
180	177, 178, 179	fvmpt 6999	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
181	174, 180	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
182	173	simprd 497	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))
183	150	simprd 497	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)
184		oveq1 7416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑥 − 1) = ((𝐴 + (𝑚 · 𝐷)) − 1))
185	184	oveq1d 7424	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → ((𝑥 − 1) + 𝑉) = (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))
186	185	oveq2d 7425	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))
187	186	oveq2d 7425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
188	187	fveq2d 6896	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
189	188	mpteq2dv 5251	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
190		ovex 7442	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1...𝑊) ∈ V
191	190	mptex 7225	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) ∈ V
192	189, 40, 191	fvmpt 6999	. . . . . . . . . . . . . . . . . . . . . . 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 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
196	195	fveq1d 6894	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))))
197	182, 196	eqtr3d 2775	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘(𝐵 + (𝐸‘𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))))
198	130	fveq2d 6896	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
199	181, 197, 198	3eqtr4rd 2784	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))
200	176, 199	jca 513	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
201		eleq1 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉)))))
202		fveqeq2 6901	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → ((𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))) ↔ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
203	201, 202	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → ((𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖)))) ↔ ((((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
204	200, 203	syl5ibrcom 246	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
205	204	rexlimdva 3156	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
206	87	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
207	162, 206	nnaddcld 12264	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
208	65	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℕ)
209	79, 208	nnaddcld 12264	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + (𝑊 · 𝐷)) ∈ ℕ)
210		vdwapval 16906	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ ℕ₀ ∧ ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ ((𝐸‘𝑖) + (𝑊 · 𝐷)) ∈ ℕ) → (𝑥 ∈ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))))
211	161, 207, 209, 210	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))))
212	39	ffnd 6719	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
213	212	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
214		fniniseg 7062	. . . . . . . . . . . . . . 15 ⊢ (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑥 ∈ (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
215	213, 214	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
216	205, 211, 215	3imtr4d 294	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) → 𝑥 ∈ (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))})))
217	216	ssrdv 3989	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) ⊆ (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
218		ssun1 4173	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑀) ⊆ ((1...𝑀) ∪ {(𝑀 + 1)})
219		fzsuc 13548	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (ℤ_≥‘1) → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
220	52, 219	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
221	218, 220	sseqtrrid 4036	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1...𝑀) ⊆ (1...(𝑀 + 1)))
222	221	sselda 3983	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...(𝑀 + 1)))
223		eqeq1 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑖 → (𝑗 = (𝑀 + 1) ↔ 𝑖 = (𝑀 + 1)))
224		fveq2 6892	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑖 → (𝐸‘𝑗) = (𝐸‘𝑖))
225	223, 224	ifbieq2d 4555	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) = if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)))
226	225	oveq1d 7424	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) = (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)))
227		ovex 7442	. . . . . . . . . . . . . . . . . 18 ⊢ (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)) ∈ V
228	226, 46, 227	fvmpt 6999	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...(𝑀 + 1)) → (𝑃‘𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)))
229	222, 228	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑃‘𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)))
230	18	nnred 12227	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑀 ∈ ℝ)
231	230	ltp1d 12144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
232		peano2re 11387	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
233	230, 232	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑀 + 1) ∈ ℝ)
234	230, 233	ltnled 11361	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀))
235	231, 234	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀)
236		breq1 5152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = (𝑀 + 1) → (𝑖 ≤ 𝑀 ↔ (𝑀 + 1) ≤ 𝑀))
237	236	notbid 318	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = (𝑀 + 1) → (¬ 𝑖 ≤ 𝑀 ↔ ¬ (𝑀 + 1) ≤ 𝑀))
238	235, 237	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑖 = (𝑀 + 1) → ¬ 𝑖 ≤ 𝑀))
239	238	con2d 134	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑖 ≤ 𝑀 → ¬ 𝑖 = (𝑀 + 1)))
240		elfzle2 13505	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ≤ 𝑀)
241	239, 240	impel 507	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ¬ 𝑖 = (𝑀 + 1))
242		iffalse 4538	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑖 = (𝑀 + 1) → if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) = (𝐸‘𝑖))
243	242	oveq1d 7424	. . . . . . . . . . . . . . . . 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 7425	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃‘𝑖)) = (𝑇 + ((𝐸‘𝑖) + (𝑊 · 𝐷))))
247	47	nncnd 12228	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ ℂ)
248	247	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑇 ∈ ℂ)
249	101	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℂ)
250	248, 80, 249	add12d 11440	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑇 + ((𝐸‘𝑖) + (𝑊 · 𝐷))) = ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))))
251	45	oveq1i 7419	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑇 + (𝑊 · 𝐷)) = ((𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) + (𝑊 · 𝐷))
252	16	nncnd 12228	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ ℂ)
253	120, 109	subcld 11571	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑉 − 𝐷) ∈ ℂ)
254	113, 253	addcld 11233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴 + (𝑉 − 𝐷)) ∈ ℂ)
255		ax-1cn 11168	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
256		subcl 11459	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 + (𝑉 − 𝐷)) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 + (𝑉 − 𝐷)) − 1) ∈ ℂ)
257	254, 255, 256	sylancl 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐴 + (𝑉 − 𝐷)) − 1) ∈ ℂ)
258	105, 257	mulcld 11234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) ∈ ℂ)
259	252, 258, 101	addassd 11236	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷))))
260	105, 257, 109	adddid 11238	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑊 · (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷)) = ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷)))
261	113, 253, 109	addassd 11236	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐴 + (𝑉 − 𝐷)) + 𝐷) = (𝐴 + ((𝑉 − 𝐷) + 𝐷)))
262	120, 109	npcand 11575	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝑉 − 𝐷) + 𝐷) = 𝑉)
263	262	oveq2d 7425	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐴 + ((𝑉 − 𝐷) + 𝐷)) = (𝐴 + 𝑉))
264	261, 263	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐴 + (𝑉 − 𝐷)) + 𝐷) = (𝐴 + 𝑉))
265	264	oveq1d 7424	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴 + (𝑉 − 𝐷)) + 𝐷) − 1) = ((𝐴 + 𝑉) − 1))
266		1cnd 11209	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ ℂ)
267	254, 109, 266	addsubd 11592	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴 + (𝑉 − 𝐷)) + 𝐷) − 1) = (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷))
268	113, 120, 266	addsubd 11592	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 + 𝑉) − 1) = ((𝐴 − 1) + 𝑉))
269	265, 267, 268	3eqtr3d 2781	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷) = ((𝐴 − 1) + 𝑉))
270	269	oveq2d 7425	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑊 · (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
271	260, 270	eqtr3d 2775	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
272	271	oveq2d 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐵 + ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
273	259, 272	eqtrd 2773	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
274	251, 273	eqtrid 2785	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑇 + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
275	274	oveq2d 7425	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸‘𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
276	275	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸‘𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
277	88	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
278	80, 77, 277	addassd 11236	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐸‘𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐸‘𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
279	80, 77	addcomd 11416	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + 𝐵) = (𝐵 + (𝐸‘𝑖)))
280	279	oveq1d 7424	. . . . . . . . . . . . . . 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 7427	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))))
284		cnvimass 6081	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ⊆ dom 𝐺
285	284, 14	fssdm 6738	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ⊆ (1...𝑊))
286	285	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ⊆ (1...𝑊))
287		vdwapid1 16908	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ ℕ ∧ (𝐵 + (𝐸‘𝑖)) ∈ ℕ ∧ (𝐸‘𝑖) ∈ ℕ) → (𝐵 + (𝐸‘𝑖)) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)))
288	160, 162, 79, 287	syl3anc 1372	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)))
289	153, 288	sseldd 3984	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
290	286, 289	sseldd 3984	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ (1...𝑊))
291		fvoveq1 7432	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝐵 + (𝐸‘𝑖)) → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
292		eqid 2733	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
293		fvex 6905	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
294	291, 292, 293	fvmpt 6999	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 + (𝐸‘𝑖)) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
295	290, 294	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
296		vdwapid1 16908	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
297	10, 41, 42, 296	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
298	43, 297	sseldd 3984	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ (^◡𝐹 “ {𝐺}))
299		fniniseg 7062	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 Fn (1...𝑉) → (𝐴 ∈ (^◡𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹‘𝐴) = 𝐺)))
300	146, 299	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴 ∈ (^◡𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹‘𝐴) = 𝐺)))
301	298, 300	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 ∈ (1...𝑉) ∧ (𝐹‘𝐴) = 𝐺))
302	301	simprd 497	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐺)
303	301	simpld 496	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ (1...𝑉))
304		oveq1 7416	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝐴 → (𝑥 − 1) = (𝐴 − 1))
305	304	oveq1d 7424	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝐴 → ((𝑥 − 1) + 𝑉) = ((𝐴 − 1) + 𝑉))
306	305	oveq2d 7425	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝐴 → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
307	306	oveq2d 7425	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝐴 → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))
308	307	fveq2d 6896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝐴 → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
309	308	mpteq2dv 5251	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
310	190	mptex 7225	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) ∈ V
311	309, 40, 310	fvmpt 6999	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ (1...𝑉) → (𝐹‘𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
312	303, 311	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹‘𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
313	302, 312	eqtr3d 2775	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
314	313	fveq1d 6894	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐺‘(𝐵 + (𝐸‘𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))))
315	314	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐵 + (𝐸‘𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))))
316	282	fveq2d 6896	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃‘𝑖))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
317	295, 315, 316	3eqtr4rd 2784	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃‘𝑖))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))
318	317	sneqd 4641	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → {(𝐻‘(𝑇 + (𝑃‘𝑖)))} = {(𝐺‘(𝐵 + (𝐸‘𝑖)))})
319	318	imaeq2d 6060	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) = (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
320	217, 283, 319	3sstr4d 4030	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))
321	320	ex 414	. . . . . . . . . 10 ⊢ (𝜑 → (𝑖 ∈ (1...𝑀) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
322	252	adantr 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ)
323	88	adantr 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
324	322, 323, 98	addassd 11236	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
325	127	oveq2d 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
326	324, 325	eqtr4d 2776	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
327	38	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
328	12	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
329		eluzfz1 13508	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 ∈ (ℤ_≥‘1) → 1 ∈ (1...𝑀))
330	52, 329	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ (1...𝑀))
331	330	ne0d 4336	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1...𝑀) ≠ ∅)
332		elfzuz3 13498	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵 + (𝐸‘𝑖)) ∈ (1...𝑊) → 𝑊 ∈ (ℤ_≥‘(𝐵 + (𝐸‘𝑖))))
333	290, 332	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ_≥‘(𝐵 + (𝐸‘𝑖))))
334	16	nnzd 12585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐵 ∈ ℤ)
335		uzid 12837	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ (ℤ_≥‘𝐵))
336	334, 335	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐵 ∈ (ℤ_≥‘𝐵))
337	336	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ∈ (ℤ_≥‘𝐵))
338	79	nnnn0d 12532	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐸‘𝑖) ∈ ℕ₀)
339		uzaddcl 12888	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵 ∈ (ℤ_≥‘𝐵) ∧ (𝐸‘𝑖) ∈ ℕ₀) → (𝐵 + (𝐸‘𝑖)) ∈ (ℤ_≥‘𝐵))
340	337, 338, 339	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ (ℤ_≥‘𝐵))
341		uztrn 12840	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑊 ∈ (ℤ_≥‘(𝐵 + (𝐸‘𝑖))) ∧ (𝐵 + (𝐸‘𝑖)) ∈ (ℤ_≥‘𝐵)) → 𝑊 ∈ (ℤ_≥‘𝐵))
342	333, 340, 341	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ_≥‘𝐵))
343		eluzle 12835	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑊 ∈ (ℤ_≥‘𝐵) → 𝐵 ≤ 𝑊)
344	342, 343	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ≤ 𝑊)
345	344	ralrimiva 3147	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊)
346		r19.2z 4495	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...𝑀) ≠ ∅ ∧ ∀𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊) → ∃𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊)
347	331, 345, 346	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ∃𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊)
348		idd 24	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ (1...𝑀) → (𝐵 ≤ 𝑊 → 𝐵 ≤ 𝑊))
349	348	rexlimiv 3149	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊 → 𝐵 ≤ 𝑊)
350	347, 349	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ≤ 𝑊)
351	12	nnzd 12585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑊 ∈ ℤ)
352		fznn 13569	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑊 ∈ ℤ → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵 ≤ 𝑊)))
353	351, 352	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵 ≤ 𝑊)))
354	16, 350, 353	mpbir2and 712	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ (1...𝑊))
355	354	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ (1...𝑊))
356	327, 328, 151, 355	vdwlem3 16916	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
357	326, 356	eqeltrd 2834	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))))
358		fvoveq1 7432	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
359		fvex 6905	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
360	358, 178, 359	fvmpt 6999	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
361	355, 360	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
362	194	fveq1d 6894	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵))
363	326	fveq2d 6896	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
364	361, 362, 363	3eqtr4rd 2784	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵))
365	357, 364	jca 513	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵)))
366		eleq1 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉)))))
367		fveqeq2 6901	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝐻‘𝑧) = (𝐺‘𝐵) ↔ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵)))
368	366, 367	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵)) ↔ (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵))))
369	365, 368	syl5ibrcom 246	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵))))
370	369	rexlimdva 3156	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵))))
371	16, 87	nnaddcld 12264	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
372		vdwapval 16906	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ ℕ₀ ∧ (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ (𝑊 · 𝐷) ∈ ℕ) → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
373	139, 371, 65, 372	syl3anc 1372	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
374		fniniseg 7062	. . . . . . . . . . . . . . 15 ⊢ (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑧 ∈ (^◡𝐻 “ {(𝐺‘𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵))))
375	212, 374	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑧 ∈ (^◡𝐻 “ {(𝐺‘𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵))))
376	370, 373, 375	3imtr4d 294	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) → 𝑧 ∈ (^◡𝐻 “ {(𝐺‘𝐵)})))
377	376	ssrdv 3989	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ⊆ (^◡𝐻 “ {(𝐺‘𝐵)}))
378	18	peano2nnd 12229	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ)
379	378, 51	eleqtrdi 2844	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) ∈ (ℤ_≥‘1))
380		eluzfz2 13509	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘1) → (𝑀 + 1) ∈ (1...(𝑀 + 1)))
381		iftrue 4535	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑀 + 1) → if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) = 0)
382	381	oveq1d 7424	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑀 + 1) → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) = (0 + (𝑊 · 𝐷)))
383		ovex 7442	. . . . . . . . . . . . . . . . . 18 ⊢ (0 + (𝑊 · 𝐷)) ∈ V
384	382, 46, 383	fvmpt 6999	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 + 1) ∈ (1...(𝑀 + 1)) → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
385	379, 380, 384	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
386	101	addlidd 11415	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 + (𝑊 · 𝐷)) = (𝑊 · 𝐷))
387	385, 386	eqtrd 2773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃‘(𝑀 + 1)) = (𝑊 · 𝐷))
388	387	oveq2d 7425	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝑇 + (𝑊 · 𝐷)))
389	388, 274	eqtrd 2773	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
390	389, 387	oveq12d 7427	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)))
391		fvoveq1 7432	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
392		fvex 6905	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
393	391, 292, 392	fvmpt 6999	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
394	354, 393	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
395	313	fveq1d 6894	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵))
396	389	fveq2d 6896	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
397	394, 395, 396	3eqtr4rd 2784	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐺‘𝐵))
398	397	sneqd 4641	. . . . . . . . . . . . 13 ⊢ (𝜑 → {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))} = {(𝐺‘𝐵)})
399	398	imaeq2d 6060	. . . . . . . . . . . 12 ⊢ (𝜑 → (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}) = (^◡𝐻 “ {(𝐺‘𝐵)}))
400	377, 390, 399	3sstr4d 4030	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
401		fveq2 6892	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑀 + 1) → (𝑃‘𝑖) = (𝑃‘(𝑀 + 1)))
402	401	oveq2d 7425	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝑀 + 1) → (𝑇 + (𝑃‘𝑖)) = (𝑇 + (𝑃‘(𝑀 + 1))))
403	402, 401	oveq12d 7427	. . . . . . . . . . . 12 ⊢ (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) = ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))))
404	402	fveq2d 6896	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑀 + 1) → (𝐻‘(𝑇 + (𝑃‘𝑖))) = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
405	404	sneqd 4641	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝑀 + 1) → {(𝐻‘(𝑇 + (𝑃‘𝑖)))} = {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})
406	405	imaeq2d 6060	. . . . . . . . . . . 12 ⊢ (𝑖 = (𝑀 + 1) → (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) = (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
407	403, 406	sseq12d 4016	. . . . . . . . . . 11 ⊢ (𝑖 = (𝑀 + 1) → (((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) ↔ ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})))
408	400, 407	syl5ibrcom 246	. . . . . . . . . 10 ⊢ (𝜑 → (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
409	321, 408	jaod 858	. . . . . . . . 9 ⊢ (𝜑 → ((𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
410	75, 409	sylbid 239	. . . . . . . 8 ⊢ (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
411	410	ralrimiv 3146	. . . . . . 7 ⊢ (𝜑 → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))
412	411	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))
413	220	rexeqdv 3327	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ ∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))))
414		rexun 4191	. . . . . . . . . . . . 13 ⊢ (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))))
415	317	eqeq2d 2744	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
416	415	rexbidva 3177	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
417		ovex 7442	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 + 1) ∈ V
418	404	eqeq2d 2744	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑀 + 1) → (𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))))
419	417, 418	rexsn 4687	. . . . . . . . . . . . . . 15 ⊢ (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
420	397	eqeq2d 2744	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) ↔ 𝑥 = (𝐺‘𝐵)))
421	419, 420	bitrid 283	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐺‘𝐵)))
422	416, 421	orbi12d 918	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))))
423	414, 422	bitrid 283	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))))
424	413, 423	bitrd 279	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))))
425	424	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))))
426	425	abbidv 2802	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))} = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))})
427		eqid 2733	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))
428	427	rnmpt 5955	. . . . . . . . 9 ⊢ ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))) = {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))}
429	2	rnmpt 5955	. . . . . . . . . . 11 ⊢ ran 𝐽 = {𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))}
430		df-sn 4630	. . . . . . . . . . 11 ⊢ {(𝐺‘𝐵)} = {𝑥 ∣ 𝑥 = (𝐺‘𝐵)}
431	429, 430	uneq12i 4162	. . . . . . . . . 10 ⊢ (ran 𝐽 ∪ {(𝐺‘𝐵)}) = ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))} ∪ {𝑥 ∣ 𝑥 = (𝐺‘𝐵)})
432		unab 4299	. . . . . . . . . 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 6896	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (♯‘(ran 𝐽 ∪ {(𝐺‘𝐵)})))
436		fzfi 13937	. . . . . . . . . 10 ⊢ (1...𝑀) ∈ Fin
437		dffn4 6812	. . . . . . . . . . 11 ⊢ (𝐽 Fn (1...𝑀) ↔ 𝐽:(1...𝑀)–onto→ran 𝐽)
438	3, 437	mpbi 229	. . . . . . . . . 10 ⊢ 𝐽:(1...𝑀)–onto→ran 𝐽
439		fofi 9338	. . . . . . . . . 10 ⊢ (((1...𝑀) ∈ Fin ∧ 𝐽:(1...𝑀)–onto→ran 𝐽) → ran 𝐽 ∈ Fin)
440	436, 438, 439	mp2an 691	. . . . . . . . 9 ⊢ ran 𝐽 ∈ Fin
441	440	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ran 𝐽 ∈ Fin)
442		fvex 6905	. . . . . . . . 9 ⊢ (𝐺‘𝐵) ∈ V
443		hashunsng 14352	. . . . . . . . 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 581	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺‘𝐵)})) = ((♯‘ran 𝐽) + 1))
446	44	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘ran 𝐽) = 𝑀)
447	446	oveq1d 7424	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ((♯‘ran 𝐽) + 1) = (𝑀 + 1))
448	435, 445, 447	3eqtrd 2777	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1))
449	412, 448	jca 513	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1)))
450		oveq1 7416	. . . . . . . . . 10 ⊢ (𝑎 = 𝑇 → (𝑎 + (𝑑‘𝑖)) = (𝑇 + (𝑑‘𝑖)))
451	450	oveq1d 7424	. . . . . . . . 9 ⊢ (𝑎 = 𝑇 → ((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) = ((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)))
452		fvoveq1 7432	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑇 → (𝐻‘(𝑎 + (𝑑‘𝑖))) = (𝐻‘(𝑇 + (𝑑‘𝑖))))
453	452	sneqd 4641	. . . . . . . . . 10 ⊢ (𝑎 = 𝑇 → {(𝐻‘(𝑎 + (𝑑‘𝑖)))} = {(𝐻‘(𝑇 + (𝑑‘𝑖)))})
454	453	imaeq2d 6060	. . . . . . . . 9 ⊢ (𝑎 = 𝑇 → (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) = (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}))
455	451, 454	sseq12d 4016	. . . . . . . 8 ⊢ (𝑎 = 𝑇 → (((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ↔ ((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))})))
456	455	ralbidv 3178	. . . . . . 7 ⊢ (𝑎 = 𝑇 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))})))
457	452	mpteq2dv 5251	. . . . . . . . 9 ⊢ (𝑎 = 𝑇 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))))
458	457	rneqd 5938	. . . . . . . 8 ⊢ (𝑎 = 𝑇 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))))
459	458	fveqeq2d 6900	. . . . . . 7 ⊢ (𝑎 = 𝑇 → ((♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1) ↔ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1)))
460	456, 459	anbi12d 632	. . . . . 6 ⊢ (𝑎 = 𝑇 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1))))
461		fveq1 6891	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑃 → (𝑑‘𝑖) = (𝑃‘𝑖))
462	461	oveq2d 7425	. . . . . . . . . 10 ⊢ (𝑑 = 𝑃 → (𝑇 + (𝑑‘𝑖)) = (𝑇 + (𝑃‘𝑖)))
463	462, 461	oveq12d 7427	. . . . . . . . 9 ⊢ (𝑑 = 𝑃 → ((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) = ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)))
464	462	fveq2d 6896	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑃 → (𝐻‘(𝑇 + (𝑑‘𝑖))) = (𝐻‘(𝑇 + (𝑃‘𝑖))))
465	464	sneqd 4641	. . . . . . . . . 10 ⊢ (𝑑 = 𝑃 → {(𝐻‘(𝑇 + (𝑑‘𝑖)))} = {(𝐻‘(𝑇 + (𝑃‘𝑖)))})
466	465	imaeq2d 6060	. . . . . . . . 9 ⊢ (𝑑 = 𝑃 → (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) = (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))
467	463, 466	sseq12d 4016	. . . . . . . 8 ⊢ (𝑑 = 𝑃 → (((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ↔ ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
468	467	ralbidv 3178	. . . . . . 7 ⊢ (𝑑 = 𝑃 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
469	464	mpteq2dv 5251	. . . . . . . . 9 ⊢ (𝑑 = 𝑃 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))))
470	469	rneqd 5938	. . . . . . . 8 ⊢ (𝑑 = 𝑃 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))))
471	470	fveqeq2d 6900	. . . . . . 7 ⊢ (𝑑 = 𝑃 → ((♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1) ↔ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1)))
472	468, 471	anbi12d 632	. . . . . 6 ⊢ (𝑑 = 𝑃 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1))))
473	460, 472	rspc2ev 3625	. . . . 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 7442	. . . . 5 ⊢ (1...(𝑊 · (2 · 𝑉))) ∈ V
476	10	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ)
477	476	nnnn0d 12532	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ₀)
478	39	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
479	18	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑀 ∈ ℕ)
480	479	peano2nnd 12229	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (𝑀 + 1) ∈ ℕ)
481		eqid 2733	. . . . 5 ⊢ (1...(𝑀 + 1)) = (1...(𝑀 + 1))
482	475, 477, 478, 480, 481	vdwpc 16913	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑_m (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1))))
483	474, 482	mpbird 257	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻)
484	483	orcd 872	. 2 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))
485	37, 484	pm2.61dan 812	1 ⊢ (𝜑 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 846 = wceq 1542 ∈ wcel 2107 {cab 2710 ≠ wne 2941 ∀wral 3062 ∃wrex 3071 Vcvv 3475 ∪ cun 3947 ⊆ wss 3949 ∅c0 4323 ifcif 4529 {csn 4629 ⟨cop 4635 class class class wbr 5149 ↦ cmpt 5232 ^◡ccnv 5676 ran crn 5678 “ cima 5680 Fn wfn 6539 ⟶wf 6540 –onto→wfo 6542 ‘cfv 6544 (class class class)co 7409 ↑_m cmap 8820 Fincfn 8939 ℂcc 11108 ℝcr 11109 0cc0 11110 1c1 11111 + caddc 11113 · cmul 11115 < clt 11248 ≤ cle 11249 − cmin 11444 ℕcn 12212 2c2 12267 ℕ₀cn0 12472 ℤcz 12558 ℤ_≥cuz 12822 ...cfz 13484 ♯chash 14290 APcvdwa 16898 MonoAP cvdwm 16899 PolyAP cvdwp 16900

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-1st 7975 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-1o 8466 df-oadd 8470 df-er 8703 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-dju 9896 df-card 9934 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-nn 12213 df-2 12275 df-n0 12473 df-z 12559 df-uz 12823 df-rp 12975 df-fz 13485 df-hash 14291 df-vdwap 16901 df-vdwmc 16902 df-vdwpc 16903

This theorem is referenced by: vdwlem7 16920

W3C validator