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 17022

Description: Lemma for vdw 17030. (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 6880	. . . . . . 7 ⊢ (𝐺‘(𝐵 + (𝐸‘𝑖))) ∈ V
2		vdwlem6.j	. . . . . . 7 ⊢ 𝐽 = (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝐵 + (𝐸‘𝑖))))
3	1, 2	fnmpti 6664	. . . . . 6 ⊢ 𝐽 Fn (1...𝑀)
4		fvelrnb 6927	. . . . . 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 12889	. . . . . . . . 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 780	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝑚 ∈ (1...𝑀))
25		simprr 782	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐽‘𝑚) = (𝐺‘𝐵))
26		fveq2 6867	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑚 → (𝐸‘𝑖) = (𝐸‘𝑚))
27	26	oveq2d 7412	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑚 → (𝐵 + (𝐸‘𝑖)) = (𝐵 + (𝐸‘𝑚)))
28	27	fveq2d 6871	. . . . . . . . . 10 ⊢ (𝑖 = 𝑚 → (𝐺‘(𝐵 + (𝐸‘𝑖))) = (𝐺‘(𝐵 + (𝐸‘𝑚))))
29		fvex 6880	. . . . . . . . . 10 ⊢ (𝐺‘(𝐵 + (𝐸‘𝑚))) ∈ V
30	28, 2, 29	fvmpt 6975	. . . . . . . . 9 ⊢ (𝑚 ∈ (1...𝑀) → (𝐽‘𝑚) = (𝐺‘(𝐵 + (𝐸‘𝑚))))
31	24, 30	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐽‘𝑚) = (𝐺‘(𝐵 + (𝐸‘𝑚))))
32	25, 31	eqtr3d 2799	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐺‘𝐵) = (𝐺‘(𝐵 + (𝐸‘𝑚))))
33	7, 11, 13, 15, 17, 19, 21, 23, 24, 32	vdwlem1 17017	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐾 + 1) MonoAP 𝐺)
34	33	rexlimdvaa 3164	. . . . 5 ⊢ (𝜑 → (∃𝑚 ∈ (1...𝑀)(𝐽‘𝑚) = (𝐺‘𝐵) → (𝐾 + 1) MonoAP 𝐺))
35	5, 34	biimtrid 244	. . . 4 ⊢ (𝜑 → ((𝐺‘𝐵) ∈ ran 𝐽 → (𝐾 + 1) MonoAP 𝐺))
36	35	imp 410	. . 3 ⊢ ((𝜑 ∧ (𝐺‘𝐵) ∈ ran 𝐽) → (𝐾 + 1) MonoAP 𝐺)
37	36	olcd 885	. 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 17021	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ ℕ)
48	47	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑇 ∈ ℕ)
49		0nn0 12496	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
50	49	a1i 11	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 = (𝑀 + 1)) → 0 ∈ ℕ₀)
51		nnuz 12878	. . . . . . . . . . . . . . . . 17 ⊢ ℕ = (ℤ_≥‘1)
52	18, 51	eleqtrdi 2872	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
53	52	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑀 ∈ (ℤ_≥‘1))
54		elfzp1 13579	. . . . . . . . . . . . . . 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 875	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 ∈ (1...𝑀) → 𝑗 = (𝑀 + 1)))
58	57	con1d 145	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 = (𝑀 + 1) → 𝑗 ∈ (1...𝑀)))
59	58	imp 410	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → 𝑗 ∈ (1...𝑀))
60	20	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → 𝐸:(1...𝑀)⟶ℕ)
61	60	ffvelcdmda 7065	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸‘𝑗) ∈ ℕ)
62	61	nnnn0d 12542	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸‘𝑗) ∈ ℕ₀)
63	59, 62	syldan 600	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → (𝐸‘𝑗) ∈ ℕ₀)
64	50, 63	ifclda 4516	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) ∈ ℕ₀)
65	12, 42	nnmulcld 12266	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 · 𝐷) ∈ ℕ)
66	65	ad2antrr 736	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑊 · 𝐷) ∈ ℕ)
67		nn0nnaddcl 12512	. . . . . . . 8 ⊢ ((if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) ∈ ℕ₀ ∧ (𝑊 · 𝐷) ∈ ℕ) → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
68	64, 66, 67	syl2anc 593	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
69	68, 46	fmptd 7095	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑃:(1...(𝑀 + 1))⟶ℕ)
70		nnex 12216	. . . . . . 7 ⊢ ℕ ∈ V
71		ovex 7429	. . . . . . 7 ⊢ (1...(𝑀 + 1)) ∈ V
72	70, 71	elmap 8853	. . . . . 6 ⊢ (𝑃 ∈ (ℕ ↑_m (1...(𝑀 + 1))) ↔ 𝑃:(1...(𝑀 + 1))⟶ℕ)
73	69, 72	sylibr 236	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑃 ∈ (ℕ ↑_m (1...(𝑀 + 1))))
74		elfzp1 13579	. . . . . . . . . 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 12226	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℂ)
78	77	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ)
79	20	ffvelcdmda 7065	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐸‘𝑖) ∈ ℕ)
80	79	nncnd 12226	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐸‘𝑖) ∈ ℂ)
81	80	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐸‘𝑖) ∈ ℂ)
82	78, 81	addcld 11201	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝐸‘𝑖)) ∈ ℂ)
83		nnm1nn0 12522	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∈ ℕ → (𝐴 − 1) ∈ ℕ₀)
84	41, 83	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 − 1) ∈ ℕ₀)
85		nn0nnaddcl 12512	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 − 1) ∈ ℕ₀ ∧ 𝑉 ∈ ℕ) → ((𝐴 − 1) + 𝑉) ∈ ℕ)
86	84, 38, 85	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℕ)
87	12, 86	nnmulcld 12266	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
88	87	nncnd 12226	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
89	88	ad2antrr 736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
90		elfznn0 13625	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ (0...(𝐾 − 1)) → 𝑚 ∈ ℕ₀)
91	90	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℕ₀)
92	91	nn0cnd 12544	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
93	92	adantlr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
94	93, 81	mulcld 11202	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝐸‘𝑖)) ∈ ℂ)
95	65	nnnn0d 12542	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑊 · 𝐷) ∈ ℕ₀)
96	95	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℕ₀)
97	91, 96	nn0mulcld 12547	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℕ₀)
98	97	nn0cnd 12544	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
99	98	adantlr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
100	82, 89, 94, 99	add4d 11412	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸‘𝑖)) + (𝑚 · (𝑊 · 𝐷)))) = (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
101	65	nncnd 12226	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑊 · 𝐷) ∈ ℂ)
102	101	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℂ)
103	93, 81, 102	adddid 11206	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))) = ((𝑚 · (𝐸‘𝑖)) + (𝑚 · (𝑊 · 𝐷))))
104	103	oveq2d 7412	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸‘𝑖)) + (𝑚 · (𝑊 · 𝐷)))))
105	12	nncnd 12226	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑊 ∈ ℂ)
106	105	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℂ)
107	86	nncnd 12226	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℂ)
108	107	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 − 1) + 𝑉) ∈ ℂ)
109	42	nncnd 12226	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐷 ∈ ℂ)
110	109	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐷 ∈ ℂ)
111	92, 110	mulcld 11202	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · 𝐷) ∈ ℂ)
112	106, 108, 111	adddid 11206	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
113	41	nncnd 12226	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐴 ∈ ℂ)
114	113	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐴 ∈ ℂ)
115		1cnd 11175	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 1 ∈ ℂ)
116	114, 111, 115	addsubd 11563	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) − 1) = ((𝐴 − 1) + (𝑚 · 𝐷)))
117	116	oveq1d 7411	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉))
118	84	nn0cnd 12544	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 − 1) ∈ ℂ)
119	118	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 − 1) ∈ ℂ)
120	38	nncnd 12226	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑉 ∈ ℂ)
121	120	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℂ)
122	119, 111, 121	add32d 11411	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
123	117, 122	eqtrd 2797	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
124	123	oveq2d 7412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))))
125	92, 106, 110	mul12d 11392	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) = (𝑊 · (𝑚 · 𝐷)))
126	125	oveq2d 7412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
127	112, 124, 126	3eqtr4d 2807	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
128	127	adantlr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
129	128	oveq2d 7412	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
130	100, 104, 129	3eqtr4d 2807	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
131	38	ad2antrr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
132	12	ad2antrr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
133	43	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴(AP‘𝐾)𝐷) ⊆ (^◡𝐹 “ {𝐺}))
134		eqid 2762	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))
135		oveq1 7403	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑚 → (𝑛 · 𝐷) = (𝑚 · 𝐷))
136	135	oveq2d 7412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = 𝑚 → (𝐴 + (𝑛 · 𝐷)) = (𝐴 + (𝑚 · 𝐷)))
137	136	rspceeqv 3604	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑚 ∈ (0...(𝐾 − 1)) ∧ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
138	134, 137	mpan2 701	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
139	10	nnnn0d 12542	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
140		vdwapval 17009	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
141	139, 41, 42, 140	syl3anc 1390	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
142	141	biimpar 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
143	138, 142	sylan2 602	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
144	133, 143	sseldd 3937	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (^◡𝐹 “ {𝐺}))
145	38, 12, 6, 39, 40	vdwlem4 17020	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹:(1...𝑉)⟶(𝑅 ↑_m (1...𝑊)))
146	145	ffnd 6692	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹 Fn (1...𝑉))
147		fniniseg 7041	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹 Fn (1...𝑉) → ((𝐴 + (𝑚 · 𝐷)) ∈ (^◡𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
148	146, 147	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (^◡𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
149	148	biimpa 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝐴 + (𝑚 · 𝐷)) ∈ (^◡𝐹 “ {𝐺})) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
150	144, 149	syldan 600	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
151	150	simpld 498	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
152	151	adantlr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
153	22	r19.21bi 3254	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
154	153	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
155		eqid 2762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))
156		oveq1 7403	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = 𝑚 → (𝑛 · (𝐸‘𝑖)) = (𝑚 · (𝐸‘𝑖)))
157	156	oveq2d 7412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑚 → ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))))
158	157	rspceeqv 3604	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑚 ∈ (0...(𝐾 − 1)) ∧ ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖))))
159	155, 158	mpan2 701	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖))))
160	10	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ)
161	160	nnnn0d 12542	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ₀)
162	76, 79	nnaddcld 12265	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ ℕ)
163		vdwapval 17009	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐾 ∈ ℕ₀ ∧ (𝐵 + (𝐸‘𝑖)) ∈ ℕ ∧ (𝐸‘𝑖) ∈ ℕ) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖)))))
164	161, 162, 79, 163	syl3anc 1390	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖)))))
165	164	biimpar 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖)))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)))
166	159, 165	sylan2 602	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)))
167	154, 166	sseldd 3937	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
168	14	ffnd 6692	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐺 Fn (1...𝑊))
169	168	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐺 Fn (1...𝑊))
170		fniniseg 7041	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 Fn (1...𝑊) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
171	169, 170	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
172	171	biimpa 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))})) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
173	167, 172	syldan 600	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
174	173	simpld 498	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊))
175	131, 132, 152, 174	vdwlem3 17019	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
176	130, 175	eqeltrd 2862	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))))
177		fvoveq1 7419	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
178		eqid 2762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
179		fvex 6880	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
180	177, 178, 179	fvmpt 6975	. . . . . . . . . . . . . . . . . . 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 7403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑥 − 1) = ((𝐴 + (𝑚 · 𝐷)) − 1))
185	184	oveq1d 7411	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → ((𝑥 − 1) + 𝑉) = (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))
186	185	oveq2d 7412	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))
187	186	oveq2d 7412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
188	187	fveq2d 6871	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
189	188	mpteq2dv 5194	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
190		ovex 7429	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1...𝑊) ∈ V
191	190	mptex 7207	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) ∈ V
192	189, 40, 191	fvmpt 6975	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
193	151, 192	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
194	183, 193	eqtr3d 2799	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
195	194	adantlr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
196	195	fveq1d 6869	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))))
197	182, 196	eqtr3d 2799	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘(𝐵 + (𝐸‘𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))))
198	130	fveq2d 6871	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
199	181, 197, 198	3eqtr4rd 2808	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))
200	176, 199	jca 519	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
201		eleq1 2850	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉)))))
202		fveqeq2 6876	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → ((𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))) ↔ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
203	201, 202	anbi12d 641	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → ((𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖)))) ↔ ((((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
204	200, 203	syl5ibrcom 249	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
205	204	rexlimdva 3163	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
206	87	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
207	162, 206	nnaddcld 12265	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
208	65	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℕ)
209	79, 208	nnaddcld 12265	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + (𝑊 · 𝐷)) ∈ ℕ)
210		vdwapval 17009	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ ℕ₀ ∧ ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ ((𝐸‘𝑖) + (𝑊 · 𝐷)) ∈ ℕ) → (𝑥 ∈ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))))
211	161, 207, 209, 210	syl3anc 1390	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))))
212	39	ffnd 6692	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
213	212	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
214		fniniseg 7041	. . . . . . . . . . . . . . 15 ⊢ (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑥 ∈ (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
215	213, 214	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
216	205, 211, 215	3imtr4d 296	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) → 𝑥 ∈ (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))})))
217	216	ssrdv 3942	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) ⊆ (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
218		ssun1 4130	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑀) ⊆ ((1...𝑀) ∪ {(𝑀 + 1)})
219		fzsuc 13576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (ℤ_≥‘1) → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
220	52, 219	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
221	218, 220	sseqtrrid 3979	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1...𝑀) ⊆ (1...(𝑀 + 1)))
222	221	sselda 3936	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...(𝑀 + 1)))
223		eqeq1 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑖 → (𝑗 = (𝑀 + 1) ↔ 𝑖 = (𝑀 + 1)))
224		fveq2 6867	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑖 → (𝐸‘𝑗) = (𝐸‘𝑖))
225	223, 224	ifbieq2d 4507	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) = if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)))
226	225	oveq1d 7411	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) = (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)))
227		ovex 7429	. . . . . . . . . . . . . . . . . 18 ⊢ (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)) ∈ V
228	226, 46, 227	fvmpt 6975	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...(𝑀 + 1)) → (𝑃‘𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)))
229	222, 228	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑃‘𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)))
230	18	nnred 12225	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑀 ∈ ℝ)
231	230	ltp1d 12122	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
232		peano2re 11356	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
233	230, 232	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑀 + 1) ∈ ℝ)
234	230, 233	ltnled 11330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀))
235	231, 234	mpbid 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀)
236		breq1 5103	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = (𝑀 + 1) → (𝑖 ≤ 𝑀 ↔ (𝑀 + 1) ≤ 𝑀))
237	236	notbid 320	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = (𝑀 + 1) → (¬ 𝑖 ≤ 𝑀 ↔ ¬ (𝑀 + 1) ≤ 𝑀))
238	235, 237	syl5ibrcom 249	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑖 = (𝑀 + 1) → ¬ 𝑖 ≤ 𝑀))
239	238	con2d 134	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑖 ≤ 𝑀 → ¬ 𝑖 = (𝑀 + 1)))
240		elfzle2 13533	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ≤ 𝑀)
241	239, 240	impel 513	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ¬ 𝑖 = (𝑀 + 1))
242		iffalse 4489	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑖 = (𝑀 + 1) → if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) = (𝐸‘𝑖))
243	242	oveq1d 7411	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑖 = (𝑀 + 1) → (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)) = ((𝐸‘𝑖) + (𝑊 · 𝐷)))
244	241, 243	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)) = ((𝐸‘𝑖) + (𝑊 · 𝐷)))
245	229, 244	eqtrd 2797	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑃‘𝑖) = ((𝐸‘𝑖) + (𝑊 · 𝐷)))
246	245	oveq2d 7412	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃‘𝑖)) = (𝑇 + ((𝐸‘𝑖) + (𝑊 · 𝐷))))
247	47	nncnd 12226	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ ℂ)
248	247	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑇 ∈ ℂ)
249	101	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℂ)
250	248, 80, 249	add12d 11410	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑇 + ((𝐸‘𝑖) + (𝑊 · 𝐷))) = ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))))
251	45	oveq1i 7406	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑇 + (𝑊 · 𝐷)) = ((𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) + (𝑊 · 𝐷))
252	16	nncnd 12226	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ ℂ)
253	120, 109	subcld 11542	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑉 − 𝐷) ∈ ℂ)
254	113, 253	addcld 11201	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴 + (𝑉 − 𝐷)) ∈ ℂ)
255		ax-1cn 11131	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
256		subcl 11429	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 + (𝑉 − 𝐷)) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 + (𝑉 − 𝐷)) − 1) ∈ ℂ)
257	254, 255, 256	sylancl 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐴 + (𝑉 − 𝐷)) − 1) ∈ ℂ)
258	105, 257	mulcld 11202	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) ∈ ℂ)
259	252, 258, 101	addassd 11204	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷))))
260	105, 257, 109	adddid 11206	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑊 · (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷)) = ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷)))
261	113, 253, 109	addassd 11204	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐴 + (𝑉 − 𝐷)) + 𝐷) = (𝐴 + ((𝑉 − 𝐷) + 𝐷)))
262	120, 109	npcand 11546	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝑉 − 𝐷) + 𝐷) = 𝑉)
263	262	oveq2d 7412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐴 + ((𝑉 − 𝐷) + 𝐷)) = (𝐴 + 𝑉))
264	261, 263	eqtrd 2797	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐴 + (𝑉 − 𝐷)) + 𝐷) = (𝐴 + 𝑉))
265	264	oveq1d 7411	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴 + (𝑉 − 𝐷)) + 𝐷) − 1) = ((𝐴 + 𝑉) − 1))
266		1cnd 11175	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ ℂ)
267	254, 109, 266	addsubd 11563	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴 + (𝑉 − 𝐷)) + 𝐷) − 1) = (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷))
268	113, 120, 266	addsubd 11563	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 + 𝑉) − 1) = ((𝐴 − 1) + 𝑉))
269	265, 267, 268	3eqtr3d 2805	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷) = ((𝐴 − 1) + 𝑉))
270	269	oveq2d 7412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑊 · (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
271	260, 270	eqtr3d 2799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
272	271	oveq2d 7412	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐵 + ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
273	259, 272	eqtrd 2797	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
274	251, 273	eqtrid 2809	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑇 + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
275	274	oveq2d 7412	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸‘𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
276	275	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸‘𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
277	88	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
278	80, 77, 277	addassd 11204	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐸‘𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐸‘𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
279	80, 77	addcomd 11385	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + 𝐵) = (𝐵 + (𝐸‘𝑖)))
280	279	oveq1d 7411	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐸‘𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
281	276, 278, 280	3eqtr2d 2803	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
282	246, 250, 281	3eqtrd 2801	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃‘𝑖)) = ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
283	282, 245	oveq12d 7414	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))))
284		cnvimass 6071	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ⊆ dom 𝐺
285	284, 14	fssdm 6711	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ⊆ (1...𝑊))
286	285	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ⊆ (1...𝑊))
287		vdwapid1 17011	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ ℕ ∧ (𝐵 + (𝐸‘𝑖)) ∈ ℕ ∧ (𝐸‘𝑖) ∈ ℕ) → (𝐵 + (𝐸‘𝑖)) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)))
288	160, 162, 79, 287	syl3anc 1390	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)))
289	153, 288	sseldd 3937	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
290	286, 289	sseldd 3937	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ (1...𝑊))
291		fvoveq1 7419	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝐵 + (𝐸‘𝑖)) → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
292		eqid 2762	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
293		fvex 6880	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
294	291, 292, 293	fvmpt 6975	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 + (𝐸‘𝑖)) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
295	290, 294	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
296		vdwapid1 17011	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
297	10, 41, 42, 296	syl3anc 1390	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
298	43, 297	sseldd 3937	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ (^◡𝐹 “ {𝐺}))
299		fniniseg 7041	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 Fn (1...𝑉) → (𝐴 ∈ (^◡𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹‘𝐴) = 𝐺)))
300	146, 299	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴 ∈ (^◡𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹‘𝐴) = 𝐺)))
301	298, 300	mpbid 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 ∈ (1...𝑉) ∧ (𝐹‘𝐴) = 𝐺))
302	301	simprd 499	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐺)
303	301	simpld 498	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ (1...𝑉))
304		oveq1 7403	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝐴 → (𝑥 − 1) = (𝐴 − 1))
305	304	oveq1d 7411	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝐴 → ((𝑥 − 1) + 𝑉) = ((𝐴 − 1) + 𝑉))
306	305	oveq2d 7412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝐴 → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
307	306	oveq2d 7412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝐴 → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))
308	307	fveq2d 6871	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝐴 → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
309	308	mpteq2dv 5194	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
310	190	mptex 7207	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) ∈ V
311	309, 40, 310	fvmpt 6975	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ (1...𝑉) → (𝐹‘𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
312	303, 311	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹‘𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
313	302, 312	eqtr3d 2799	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
314	313	fveq1d 6869	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐺‘(𝐵 + (𝐸‘𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))))
315	314	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐵 + (𝐸‘𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))))
316	282	fveq2d 6871	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃‘𝑖))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
317	295, 315, 316	3eqtr4rd 2808	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃‘𝑖))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))
318	317	sneqd 4594	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → {(𝐻‘(𝑇 + (𝑃‘𝑖)))} = {(𝐺‘(𝐵 + (𝐸‘𝑖)))})
319	318	imaeq2d 6049	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) = (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
320	217, 283, 319	3sstr4d 3991	. . . . . . . . . . 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 11204	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
325	127	oveq2d 7412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
326	324, 325	eqtr4d 2800	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
327	38	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
328	12	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
329		eluzfz1 13536	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 ∈ (ℤ_≥‘1) → 1 ∈ (1...𝑀))
330	52, 329	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ (1...𝑀))
331	330	ne0d 4294	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1...𝑀) ≠ ∅)
332		elfzuz3 13526	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵 + (𝐸‘𝑖)) ∈ (1...𝑊) → 𝑊 ∈ (ℤ_≥‘(𝐵 + (𝐸‘𝑖))))
333	290, 332	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ_≥‘(𝐵 + (𝐸‘𝑖))))
334	16	nnzd 12594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐵 ∈ ℤ)
335		uzid 12854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ (ℤ_≥‘𝐵))
336	334, 335	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐵 ∈ (ℤ_≥‘𝐵))
337	336	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ∈ (ℤ_≥‘𝐵))
338	79	nnnn0d 12542	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐸‘𝑖) ∈ ℕ₀)
339		uzaddcl 12905	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵 ∈ (ℤ_≥‘𝐵) ∧ (𝐸‘𝑖) ∈ ℕ₀) → (𝐵 + (𝐸‘𝑖)) ∈ (ℤ_≥‘𝐵))
340	337, 338, 339	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ (ℤ_≥‘𝐵))
341		uztrn 12857	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑊 ∈ (ℤ_≥‘(𝐵 + (𝐸‘𝑖))) ∧ (𝐵 + (𝐸‘𝑖)) ∈ (ℤ_≥‘𝐵)) → 𝑊 ∈ (ℤ_≥‘𝐵))
342	333, 340, 341	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ_≥‘𝐵))
343		eluzle 12852	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑊 ∈ (ℤ_≥‘𝐵) → 𝐵 ≤ 𝑊)
344	342, 343	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ≤ 𝑊)
345	344	ralrimiva 3154	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊)
346		r19.2z 4453	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...𝑀) ≠ ∅ ∧ ∀𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊) → ∃𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊)
347	331, 345, 346	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ∃𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊)
348		idd 24	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ (1...𝑀) → (𝐵 ≤ 𝑊 → 𝐵 ≤ 𝑊))
349	348	rexlimiv 3156	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊 → 𝐵 ≤ 𝑊)
350	347, 349	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ≤ 𝑊)
351	12	nnzd 12594	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑊 ∈ ℤ)
352		fznn 13597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑊 ∈ ℤ → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵 ≤ 𝑊)))
353	351, 352	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵 ≤ 𝑊)))
354	16, 350, 353	mpbir2and 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ (1...𝑊))
355	354	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ (1...𝑊))
356	327, 328, 151, 355	vdwlem3 17019	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
357	326, 356	eqeltrd 2862	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))))
358		fvoveq1 7419	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
359		fvex 6880	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
360	358, 178, 359	fvmpt 6975	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
361	355, 360	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
362	194	fveq1d 6869	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵))
363	326	fveq2d 6871	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
364	361, 362, 363	3eqtr4rd 2808	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵))
365	357, 364	jca 519	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵)))
366		eleq1 2850	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉)))))
367		fveqeq2 6876	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝐻‘𝑧) = (𝐺‘𝐵) ↔ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵)))
368	366, 367	anbi12d 641	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵)) ↔ (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵))))
369	365, 368	syl5ibrcom 249	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵))))
370	369	rexlimdva 3163	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵))))
371	16, 87	nnaddcld 12265	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
372		vdwapval 17009	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ ℕ₀ ∧ (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ (𝑊 · 𝐷) ∈ ℕ) → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
373	139, 371, 65, 372	syl3anc 1390	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
374		fniniseg 7041	. . . . . . . . . . . . . . 15 ⊢ (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑧 ∈ (^◡𝐻 “ {(𝐺‘𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵))))
375	212, 374	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑧 ∈ (^◡𝐻 “ {(𝐺‘𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵))))
376	370, 373, 375	3imtr4d 296	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) → 𝑧 ∈ (^◡𝐻 “ {(𝐺‘𝐵)})))
377	376	ssrdv 3942	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ⊆ (^◡𝐻 “ {(𝐺‘𝐵)}))
378	18	peano2nnd 12227	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ)
379	378, 51	eleqtrdi 2872	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) ∈ (ℤ_≥‘1))
380		eluzfz2 13537	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘1) → (𝑀 + 1) ∈ (1...(𝑀 + 1)))
381		iftrue 4486	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑀 + 1) → if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) = 0)
382	381	oveq1d 7411	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑀 + 1) → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) = (0 + (𝑊 · 𝐷)))
383		ovex 7429	. . . . . . . . . . . . . . . . . 18 ⊢ (0 + (𝑊 · 𝐷)) ∈ V
384	382, 46, 383	fvmpt 6975	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 + 1) ∈ (1...(𝑀 + 1)) → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
385	379, 380, 384	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
386	101	addlidd 11384	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 + (𝑊 · 𝐷)) = (𝑊 · 𝐷))
387	385, 386	eqtrd 2797	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃‘(𝑀 + 1)) = (𝑊 · 𝐷))
388	387	oveq2d 7412	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝑇 + (𝑊 · 𝐷)))
389	388, 274	eqtrd 2797	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
390	389, 387	oveq12d 7414	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)))
391		fvoveq1 7419	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
392		fvex 6880	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
393	391, 292, 392	fvmpt 6975	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
394	354, 393	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
395	313	fveq1d 6869	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵))
396	389	fveq2d 6871	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
397	394, 395, 396	3eqtr4rd 2808	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐺‘𝐵))
398	397	sneqd 4594	. . . . . . . . . . . . 13 ⊢ (𝜑 → {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))} = {(𝐺‘𝐵)})
399	398	imaeq2d 6049	. . . . . . . . . . . 12 ⊢ (𝜑 → (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}) = (^◡𝐻 “ {(𝐺‘𝐵)}))
400	377, 390, 399	3sstr4d 3991	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
401		fveq2 6867	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑀 + 1) → (𝑃‘𝑖) = (𝑃‘(𝑀 + 1)))
402	401	oveq2d 7412	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝑀 + 1) → (𝑇 + (𝑃‘𝑖)) = (𝑇 + (𝑃‘(𝑀 + 1))))
403	402, 401	oveq12d 7414	. . . . . . . . . . . 12 ⊢ (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) = ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))))
404	402	fveq2d 6871	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑀 + 1) → (𝐻‘(𝑇 + (𝑃‘𝑖))) = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
405	404	sneqd 4594	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝑀 + 1) → {(𝐻‘(𝑇 + (𝑃‘𝑖)))} = {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})
406	405	imaeq2d 6049	. . . . . . . . . . . 12 ⊢ (𝑖 = (𝑀 + 1) → (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) = (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
407	403, 406	sseq12d 3969	. . . . . . . . . . 11 ⊢ (𝑖 = (𝑀 + 1) → (((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) ↔ ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})))
408	400, 407	syl5ibrcom 249	. . . . . . . . . 10 ⊢ (𝜑 → (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
409	321, 408	jaod 870	. . . . . . . . 9 ⊢ (𝜑 → ((𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
410	75, 409	sylbid 242	. . . . . . . 8 ⊢ (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
411	410	ralrimiv 3153	. . . . . . 7 ⊢ (𝜑 → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))
412	411	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))
413	220	rexeqdv 3321	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ ∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))))
414		rexun 4148	. . . . . . . . . . . . 13 ⊢ (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))))
415	317	eqeq2d 2773	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
416	415	rexbidva 3184	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
417		ovex 7429	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 + 1) ∈ V
418	404	eqeq2d 2773	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑀 + 1) → (𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))))
419	417, 418	rexsn 4641	. . . . . . . . . . . . . . 15 ⊢ (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
420	397	eqeq2d 2773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) ↔ 𝑥 = (𝐺‘𝐵)))
421	419, 420	bitrid 285	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐺‘𝐵)))
422	416, 421	orbi12d 929	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))))
423	414, 422	bitrid 285	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))))
424	413, 423	bitrd 281	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))))
425	424	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))))
426	425	abbidv 2828	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))} = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))})
427		eqid 2762	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))
428	427	rnmpt 5933	. . . . . . . . 9 ⊢ ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))) = {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))}
429	2	rnmpt 5933	. . . . . . . . . . 11 ⊢ ran 𝐽 = {𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))}
430		df-sn 4583	. . . . . . . . . . 11 ⊢ {(𝐺‘𝐵)} = {𝑥 ∣ 𝑥 = (𝐺‘𝐵)}
431	429, 430	uneq12i 4119	. . . . . . . . . 10 ⊢ (ran 𝐽 ∪ {(𝐺‘𝐵)}) = ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))} ∪ {𝑥 ∣ 𝑥 = (𝐺‘𝐵)})
432		unab 4260	. . . . . . . . . 10 ⊢ ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))} ∪ {𝑥 ∣ 𝑥 = (𝐺‘𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))}
433	431, 432	eqtri 2785	. . . . . . . . 9 ⊢ (ran 𝐽 ∪ {(𝐺‘𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))}
434	426, 428, 433	3eqtr4g 2822	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))) = (ran 𝐽 ∪ {(𝐺‘𝐵)}))
435	434	fveq2d 6871	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (♯‘(ran 𝐽 ∪ {(𝐺‘𝐵)})))
436		fzfi 13985	. . . . . . . . . 10 ⊢ (1...𝑀) ∈ Fin
437		dffn4 6784	. . . . . . . . . . 11 ⊢ (𝐽 Fn (1...𝑀) ↔ 𝐽:(1...𝑀)–onto→ran 𝐽)
438	3, 437	mpbi 232	. . . . . . . . . 10 ⊢ 𝐽:(1...𝑀)–onto→ran 𝐽
439		fofi 9257	. . . . . . . . . 10 ⊢ (((1...𝑀) ∈ Fin ∧ 𝐽:(1...𝑀)–onto→ran 𝐽) → ran 𝐽 ∈ Fin)
440	436, 438, 439	mp2an 702	. . . . . . . . 9 ⊢ ran 𝐽 ∈ Fin
441	440	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ran 𝐽 ∈ Fin)
442		fvex 6880	. . . . . . . . 9 ⊢ (𝐺‘𝐵) ∈ V
443		hashunsng 14405	. . . . . . . . 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 589	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺‘𝐵)})) = ((♯‘ran 𝐽) + 1))
446	44	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘ran 𝐽) = 𝑀)
447	446	oveq1d 7411	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ((♯‘ran 𝐽) + 1) = (𝑀 + 1))
448	435, 445, 447	3eqtrd 2801	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1))
449	412, 448	jca 519	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1)))
450		oveq1 7403	. . . . . . . . . 10 ⊢ (𝑎 = 𝑇 → (𝑎 + (𝑑‘𝑖)) = (𝑇 + (𝑑‘𝑖)))
451	450	oveq1d 7411	. . . . . . . . 9 ⊢ (𝑎 = 𝑇 → ((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) = ((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)))
452		fvoveq1 7419	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑇 → (𝐻‘(𝑎 + (𝑑‘𝑖))) = (𝐻‘(𝑇 + (𝑑‘𝑖))))
453	452	sneqd 4594	. . . . . . . . . 10 ⊢ (𝑎 = 𝑇 → {(𝐻‘(𝑎 + (𝑑‘𝑖)))} = {(𝐻‘(𝑇 + (𝑑‘𝑖)))})
454	453	imaeq2d 6049	. . . . . . . . 9 ⊢ (𝑎 = 𝑇 → (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) = (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}))
455	451, 454	sseq12d 3969	. . . . . . . 8 ⊢ (𝑎 = 𝑇 → (((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ↔ ((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))})))
456	455	ralbidv 3185	. . . . . . 7 ⊢ (𝑎 = 𝑇 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))})))
457	452	mpteq2dv 5194	. . . . . . . . 9 ⊢ (𝑎 = 𝑇 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))))
458	457	rneqd 5914	. . . . . . . 8 ⊢ (𝑎 = 𝑇 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))))
459	458	fveqeq2d 6875	. . . . . . 7 ⊢ (𝑎 = 𝑇 → ((♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1) ↔ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1)))
460	456, 459	anbi12d 641	. . . . . 6 ⊢ (𝑎 = 𝑇 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1))))
461		fveq1 6866	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑃 → (𝑑‘𝑖) = (𝑃‘𝑖))
462	461	oveq2d 7412	. . . . . . . . . 10 ⊢ (𝑑 = 𝑃 → (𝑇 + (𝑑‘𝑖)) = (𝑇 + (𝑃‘𝑖)))
463	462, 461	oveq12d 7414	. . . . . . . . 9 ⊢ (𝑑 = 𝑃 → ((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) = ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)))
464	462	fveq2d 6871	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑃 → (𝐻‘(𝑇 + (𝑑‘𝑖))) = (𝐻‘(𝑇 + (𝑃‘𝑖))))
465	464	sneqd 4594	. . . . . . . . . 10 ⊢ (𝑑 = 𝑃 → {(𝐻‘(𝑇 + (𝑑‘𝑖)))} = {(𝐻‘(𝑇 + (𝑃‘𝑖)))})
466	465	imaeq2d 6049	. . . . . . . . 9 ⊢ (𝑑 = 𝑃 → (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) = (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))
467	463, 466	sseq12d 3969	. . . . . . . 8 ⊢ (𝑑 = 𝑃 → (((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ↔ ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
468	467	ralbidv 3185	. . . . . . 7 ⊢ (𝑑 = 𝑃 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
469	464	mpteq2dv 5194	. . . . . . . . 9 ⊢ (𝑑 = 𝑃 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))))
470	469	rneqd 5914	. . . . . . . 8 ⊢ (𝑑 = 𝑃 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))))
471	470	fveqeq2d 6875	. . . . . . 7 ⊢ (𝑑 = 𝑃 → ((♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1) ↔ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1)))
472	468, 471	anbi12d 641	. . . . . 6 ⊢ (𝑑 = 𝑃 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1))))
473	460, 472	rspc2ev 3594	. . . . 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 1390	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑_m (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1)))
475		ovex 7429	. . . . 5 ⊢ (1...(𝑊 · (2 · 𝑉))) ∈ V
476	10	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ)
477	476	nnnn0d 12542	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ₀)
478	39	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
479	18	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑀 ∈ ℕ)
480	479	peano2nnd 12227	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (𝑀 + 1) ∈ ℕ)
481		eqid 2762	. . . . 5 ⊢ (1...(𝑀 + 1)) = (1...(𝑀 + 1))
482	475, 477, 478, 480, 481	vdwpc 17016	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑_m (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1))))
483	474, 482	mpbird 259	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻)
484	483	orcd 884	. 2 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))
485	37, 484	pm2.61dan 822	1 ⊢ (𝜑 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 = wceq 1560 ∈ wcel 2142 {cab 2740 ≠ wne 2957 ∀wral 3076 ∃wrex 3086 Vcvv 3454 ∪ cun 3902 ⊆ wss 3904 ∅c0 4285 ifcif 4480 {csn 4582 ⟨cop 4588 class class class wbr 5100 ↦ cmpt 5181 ^◡ccnv 5646 ran crn 5648 “ cima 5650 Fn wfn 6516 ⟶wf 6517 –onto→wfo 6519 ‘cfv 6521 (class class class)co 7396 ↑_m cmap 8808 Fincfn 8927 ℂcc 11071 ℝcr 11072 0cc0 11073 1c1 11074 + caddc 11076 · cmul 11078 < clt 11216 ≤ cle 11217 − cmin 11414 ℕcn 12210 2c2 12272 ℕ₀cn0 12481 ℤcz 12568 ℤ_≥cuz 12839 ...cfz 13512 ♯chash 14343 APcvdwa 17001 MonoAP cvdwm 17002 PolyAP cvdwp 17003

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4906 df-iun 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-om 7847 df-1st 7970 df-2nd 7971 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-1o 8437 df-oadd 8441 df-er 8678 df-map 8810 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-dju 9859 df-card 9897 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-nn 12211 df-2 12280 df-n0 12482 df-z 12569 df-uz 12840 df-rp 12994 df-fz 13513 df-hash 14344 df-vdwap 17004 df-vdwmc 17005 df-vdwpc 17006

This theorem is referenced by: vdwlem7 17023

W3C validator