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 17009

Description: Lemma for vdw 17017. (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 6918	. . . . . . 7 ⊢ (𝐺‘(𝐵 + (𝐸‘𝑖))) ∈ V
2		vdwlem6.j	. . . . . . 7 ⊢ 𝐽 = (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝐵 + (𝐸‘𝑖))))
3	1, 2	fnmpti 6708	. . . . . 6 ⊢ 𝐽 Fn (1...𝑀)
4		fvelrnb 6967	. . . . . 6 ⊢ (𝐽 Fn (1...𝑀) → ((𝐺‘𝐵) ∈ ran 𝐽 ↔ ∃𝑚 ∈ (1...𝑀)(𝐽‘𝑚) = (𝐺‘𝐵)))
5	3, 4	ax-mp 5	. . . . 5 ⊢ ((𝐺‘𝐵) ∈ ran 𝐽 ↔ ∃𝑚 ∈ (1...𝑀)(𝐽‘𝑚) = (𝐺‘𝐵))
6		vdwlem4.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Fin)
7	6	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝑅 ∈ Fin)
8		vdwlem7.k	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘2))
9		eluz2nn 12930	. . . . . . . . 9 ⊢ (𝐾 ∈ (ℤ_≥‘2) → 𝐾 ∈ ℕ)
10	8, 9	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ℕ)
11	10	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝐾 ∈ ℕ)
12		vdwlem3.w	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ ℕ)
13	12	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝑊 ∈ ℕ)
14		vdwlem7.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺:(1...𝑊)⟶𝑅)
15	14	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝐺:(1...𝑊)⟶𝑅)
16		vdwlem6.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℕ)
17	16	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝐵 ∈ ℕ)
18		vdwlem7.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ)
19	18	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝑀 ∈ ℕ)
20		vdwlem6.e	. . . . . . . 8 ⊢ (𝜑 → 𝐸:(1...𝑀)⟶ℕ)
21	20	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝐸:(1...𝑀)⟶ℕ)
22		vdwlem6.s	. . . . . . . 8 ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
23	22	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
24		simprl 769	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝑚 ∈ (1...𝑀))
25		simprr 771	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐽‘𝑚) = (𝐺‘𝐵))
26		fveq2 6905	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑚 → (𝐸‘𝑖) = (𝐸‘𝑚))
27	26	oveq2d 7446	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑚 → (𝐵 + (𝐸‘𝑖)) = (𝐵 + (𝐸‘𝑚)))
28	27	fveq2d 6909	. . . . . . . . . 10 ⊢ (𝑖 = 𝑚 → (𝐺‘(𝐵 + (𝐸‘𝑖))) = (𝐺‘(𝐵 + (𝐸‘𝑚))))
29		fvex 6918	. . . . . . . . . 10 ⊢ (𝐺‘(𝐵 + (𝐸‘𝑚))) ∈ V
30	28, 2, 29	fvmpt 7014	. . . . . . . . 9 ⊢ (𝑚 ∈ (1...𝑀) → (𝐽‘𝑚) = (𝐺‘(𝐵 + (𝐸‘𝑚))))
31	24, 30	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐽‘𝑚) = (𝐺‘(𝐵 + (𝐸‘𝑚))))
32	25, 31	eqtr3d 2771	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐺‘𝐵) = (𝐺‘(𝐵 + (𝐸‘𝑚))))
33	7, 11, 13, 15, 17, 19, 21, 23, 24, 32	vdwlem1 17004	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐾 + 1) MonoAP 𝐺)
34	33	rexlimdvaa 3149	. . . . 5 ⊢ (𝜑 → (∃𝑚 ∈ (1...𝑀)(𝐽‘𝑚) = (𝐺‘𝐵) → (𝐾 + 1) MonoAP 𝐺))
35	5, 34	biimtrid 241	. . . 4 ⊢ (𝜑 → ((𝐺‘𝐵) ∈ ran 𝐽 → (𝐾 + 1) MonoAP 𝐺))
36	35	imp 405	. . 3 ⊢ ((𝜑 ∧ (𝐺‘𝐵) ∈ ran 𝐽) → (𝐾 + 1) MonoAP 𝐺)
37	36	olcd 872	. 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 17008	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ ℕ)
48	47	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑇 ∈ ℕ)
49		0nn0 12549	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
50	49	a1i 11	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 = (𝑀 + 1)) → 0 ∈ ℕ₀)
51		nnuz 12927	. . . . . . . . . . . . . . . . 17 ⊢ ℕ = (ℤ_≥‘1)
52	18, 51	eleqtrdi 2839	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
53	52	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑀 ∈ (ℤ_≥‘1))
54		elfzp1 13615	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘1) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1))))
55	53, 54	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1))))
56	55	biimpa 475	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1)))
57	56	ord 862	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 ∈ (1...𝑀) → 𝑗 = (𝑀 + 1)))
58	57	con1d 145	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 = (𝑀 + 1) → 𝑗 ∈ (1...𝑀)))
59	58	imp 405	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → 𝑗 ∈ (1...𝑀))
60	20	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → 𝐸:(1...𝑀)⟶ℕ)
61	60	ffvelcdmda 7103	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸‘𝑗) ∈ ℕ)
62	61	nnnn0d 12594	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸‘𝑗) ∈ ℕ₀)
63	59, 62	syldan 589	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → (𝐸‘𝑗) ∈ ℕ₀)
64	50, 63	ifclda 4571	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) ∈ ℕ₀)
65	12, 42	nnmulcld 12327	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 · 𝐷) ∈ ℕ)
66	65	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑊 · 𝐷) ∈ ℕ)
67		nn0nnaddcl 12565	. . . . . . . 8 ⊢ ((if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) ∈ ℕ₀ ∧ (𝑊 · 𝐷) ∈ ℕ) → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
68	64, 66, 67	syl2anc 582	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
69	68, 46	fmptd 7133	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑃:(1...(𝑀 + 1))⟶ℕ)
70		nnex 12280	. . . . . . 7 ⊢ ℕ ∈ V
71		ovex 7463	. . . . . . 7 ⊢ (1...(𝑀 + 1)) ∈ V
72	70, 71	elmap 8908	. . . . . 6 ⊢ (𝑃 ∈ (ℕ ↑_m (1...(𝑀 + 1))) ↔ 𝑃:(1...(𝑀 + 1))⟶ℕ)
73	69, 72	sylibr 233	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑃 ∈ (ℕ ↑_m (1...(𝑀 + 1))))
74		elfzp1 13615	. . . . . . . . . 10 ⊢ (𝑀 ∈ (ℤ_≥‘1) → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1))))
75	52, 74	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1))))
76	16	adantr 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℕ)
77	76	nncnd 12290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℂ)
78	77	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ)
79	20	ffvelcdmda 7103	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐸‘𝑖) ∈ ℕ)
80	79	nncnd 12290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐸‘𝑖) ∈ ℂ)
81	80	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐸‘𝑖) ∈ ℂ)
82	78, 81	addcld 11290	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝐸‘𝑖)) ∈ ℂ)
83		nnm1nn0 12575	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∈ ℕ → (𝐴 − 1) ∈ ℕ₀)
84	41, 83	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐴 − 1) ∈ ℕ₀)
85		nn0nnaddcl 12565	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 − 1) ∈ ℕ₀ ∧ 𝑉 ∈ ℕ) → ((𝐴 − 1) + 𝑉) ∈ ℕ)
86	84, 38, 85	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℕ)
87	12, 86	nnmulcld 12327	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
88	87	nncnd 12290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
89	88	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
90		elfznn0 13658	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ (0...(𝐾 − 1)) → 𝑚 ∈ ℕ₀)
91	90	adantl 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℕ₀)
92	91	nn0cnd 12596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
93	92	adantlr 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
94	93, 81	mulcld 11291	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝐸‘𝑖)) ∈ ℂ)
95	65	nnnn0d 12594	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑊 · 𝐷) ∈ ℕ₀)
96	95	adantr 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℕ₀)
97	91, 96	nn0mulcld 12599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℕ₀)
98	97	nn0cnd 12596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
99	98	adantlr 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
100	82, 89, 94, 99	add4d 11499	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸‘𝑖)) + (𝑚 · (𝑊 · 𝐷)))) = (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
101	65	nncnd 12290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑊 · 𝐷) ∈ ℂ)
102	101	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℂ)
103	93, 81, 102	adddid 11295	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))) = ((𝑚 · (𝐸‘𝑖)) + (𝑚 · (𝑊 · 𝐷))))
104	103	oveq2d 7446	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸‘𝑖)) + (𝑚 · (𝑊 · 𝐷)))))
105	12	nncnd 12290	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑊 ∈ ℂ)
106	105	adantr 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℂ)
107	86	nncnd 12290	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℂ)
108	107	adantr 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 − 1) + 𝑉) ∈ ℂ)
109	42	nncnd 12290	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐷 ∈ ℂ)
110	109	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐷 ∈ ℂ)
111	92, 110	mulcld 11291	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · 𝐷) ∈ ℂ)
112	106, 108, 111	adddid 11295	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
113	41	nncnd 12290	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐴 ∈ ℂ)
114	113	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐴 ∈ ℂ)
115		1cnd 11266	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 1 ∈ ℂ)
116	114, 111, 115	addsubd 11649	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) − 1) = ((𝐴 − 1) + (𝑚 · 𝐷)))
117	116	oveq1d 7445	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉))
118	84	nn0cnd 12596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 − 1) ∈ ℂ)
119	118	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 − 1) ∈ ℂ)
120	38	nncnd 12290	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑉 ∈ ℂ)
121	120	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℂ)
122	119, 111, 121	add32d 11498	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
123	117, 122	eqtrd 2769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
124	123	oveq2d 7446	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))))
125	92, 106, 110	mul12d 11480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) = (𝑊 · (𝑚 · 𝐷)))
126	125	oveq2d 7446	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
127	112, 124, 126	3eqtr4d 2779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
128	127	adantlr 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
129	128	oveq2d 7446	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
130	100, 104, 129	3eqtr4d 2779	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
131	38	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
132	12	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
133	43	adantr 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴(AP‘𝐾)𝐷) ⊆ (^◡𝐹 “ {𝐺}))
134		eqid 2729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))
135		oveq1 7437	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑚 → (𝑛 · 𝐷) = (𝑚 · 𝐷))
136	135	oveq2d 7446	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = 𝑚 → (𝐴 + (𝑛 · 𝐷)) = (𝐴 + (𝑚 · 𝐷)))
137	136	rspceeqv 3642	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑚 ∈ (0...(𝐾 − 1)) ∧ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
138	134, 137	mpan2 689	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
139	10	nnnn0d 12594	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
140		vdwapval 16996	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
141	139, 41, 42, 140	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
142	141	biimpar 476	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
143	138, 142	sylan2 591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
144	133, 143	sseldd 3992	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (^◡𝐹 “ {𝐺}))
145	38, 12, 6, 39, 40	vdwlem4 17007	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹:(1...𝑉)⟶(𝑅 ↑_m (1...𝑊)))
146	145	ffnd 6733	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹 Fn (1...𝑉))
147		fniniseg 7078	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹 Fn (1...𝑉) → ((𝐴 + (𝑚 · 𝐷)) ∈ (^◡𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
148	146, 147	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (^◡𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
149	148	biimpa 475	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝐴 + (𝑚 · 𝐷)) ∈ (^◡𝐹 “ {𝐺})) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
150	144, 149	syldan 589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
151	150	simpld 493	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
152	151	adantlr 713	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
153	22	r19.21bi 3243	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
154	153	adantr 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
155		eqid 2729	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))
156		oveq1 7437	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = 𝑚 → (𝑛 · (𝐸‘𝑖)) = (𝑚 · (𝐸‘𝑖)))
157	156	oveq2d 7446	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑚 → ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))))
158	157	rspceeqv 3642	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑚 ∈ (0...(𝐾 − 1)) ∧ ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖))))
159	155, 158	mpan2 689	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖))))
160	10	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ)
161	160	nnnn0d 12594	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ₀)
162	76, 79	nnaddcld 12326	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ ℕ)
163		vdwapval 16996	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐾 ∈ ℕ₀ ∧ (𝐵 + (𝐸‘𝑖)) ∈ ℕ ∧ (𝐸‘𝑖) ∈ ℕ) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖)))))
164	161, 162, 79, 163	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖)))))
165	164	biimpar 476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖)))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)))
166	159, 165	sylan2 591	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)))
167	154, 166	sseldd 3992	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
168	14	ffnd 6733	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐺 Fn (1...𝑊))
169	168	adantr 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐺 Fn (1...𝑊))
170		fniniseg 7078	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 Fn (1...𝑊) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
171	169, 170	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
172	171	biimpa 475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))})) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
173	167, 172	syldan 589	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
174	173	simpld 493	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊))
175	131, 132, 152, 174	vdwlem3 17006	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
176	130, 175	eqeltrd 2829	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))))
177		fvoveq1 7453	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
178		eqid 2729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
179		fvex 6918	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
180	177, 178, 179	fvmpt 7014	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
181	174, 180	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
182	173	simprd 494	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))
183	150	simprd 494	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)
184		oveq1 7437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑥 − 1) = ((𝐴 + (𝑚 · 𝐷)) − 1))
185	184	oveq1d 7445	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → ((𝑥 − 1) + 𝑉) = (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))
186	185	oveq2d 7446	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))
187	186	oveq2d 7446	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
188	187	fveq2d 6909	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
189	188	mpteq2dv 5258	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
190		ovex 7463	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1...𝑊) ∈ V
191	190	mptex 7245	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) ∈ V
192	189, 40, 191	fvmpt 7014	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
193	151, 192	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
194	183, 193	eqtr3d 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
195	194	adantlr 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
196	195	fveq1d 6907	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))))
197	182, 196	eqtr3d 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘(𝐵 + (𝐸‘𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))))
198	130	fveq2d 6909	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
199	181, 197, 198	3eqtr4rd 2780	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))
200	176, 199	jca 510	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
201		eleq1 2817	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉)))))
202		fveqeq2 6914	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → ((𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))) ↔ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
203	201, 202	anbi12d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → ((𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖)))) ↔ ((((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
204	200, 203	syl5ibrcom 246	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
205	204	rexlimdva 3148	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
206	87	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
207	162, 206	nnaddcld 12326	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
208	65	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℕ)
209	79, 208	nnaddcld 12326	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + (𝑊 · 𝐷)) ∈ ℕ)
210		vdwapval 16996	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ ℕ₀ ∧ ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ ((𝐸‘𝑖) + (𝑊 · 𝐷)) ∈ ℕ) → (𝑥 ∈ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))))
211	161, 207, 209, 210	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))))
212	39	ffnd 6733	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
213	212	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
214		fniniseg 7078	. . . . . . . . . . . . . . 15 ⊢ (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑥 ∈ (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
215	213, 214	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))))))
216	205, 211, 215	3imtr4d 293	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) → 𝑥 ∈ (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))})))
217	216	ssrdv 3997	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) ⊆ (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
218		ssun1 4183	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑀) ⊆ ((1...𝑀) ∪ {(𝑀 + 1)})
219		fzsuc 13612	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (ℤ_≥‘1) → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
220	52, 219	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
221	218, 220	sseqtrrid 4045	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1...𝑀) ⊆ (1...(𝑀 + 1)))
222	221	sselda 3991	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...(𝑀 + 1)))
223		eqeq1 2733	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑖 → (𝑗 = (𝑀 + 1) ↔ 𝑖 = (𝑀 + 1)))
224		fveq2 6905	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑖 → (𝐸‘𝑗) = (𝐸‘𝑖))
225	223, 224	ifbieq2d 4562	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) = if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)))
226	225	oveq1d 7445	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) = (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)))
227		ovex 7463	. . . . . . . . . . . . . . . . . 18 ⊢ (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)) ∈ V
228	226, 46, 227	fvmpt 7014	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (1...(𝑀 + 1)) → (𝑃‘𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)))
229	222, 228	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑃‘𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)))
230	18	nnred 12289	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑀 ∈ ℝ)
231	230	ltp1d 12206	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
232		peano2re 11444	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
233	230, 232	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑀 + 1) ∈ ℝ)
234	230, 233	ltnled 11418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀))
235	231, 234	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀)
236		breq1 5159	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = (𝑀 + 1) → (𝑖 ≤ 𝑀 ↔ (𝑀 + 1) ≤ 𝑀))
237	236	notbid 317	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = (𝑀 + 1) → (¬ 𝑖 ≤ 𝑀 ↔ ¬ (𝑀 + 1) ≤ 𝑀))
238	235, 237	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑖 = (𝑀 + 1) → ¬ 𝑖 ≤ 𝑀))
239	238	con2d 134	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑖 ≤ 𝑀 → ¬ 𝑖 = (𝑀 + 1)))
240		elfzle2 13569	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ≤ 𝑀)
241	239, 240	impel 504	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ¬ 𝑖 = (𝑀 + 1))
242		iffalse 4545	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑖 = (𝑀 + 1) → if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) = (𝐸‘𝑖))
243	242	oveq1d 7445	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑖 = (𝑀 + 1) → (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)) = ((𝐸‘𝑖) + (𝑊 · 𝐷)))
244	241, 243	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)) = ((𝐸‘𝑖) + (𝑊 · 𝐷)))
245	229, 244	eqtrd 2769	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑃‘𝑖) = ((𝐸‘𝑖) + (𝑊 · 𝐷)))
246	245	oveq2d 7446	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃‘𝑖)) = (𝑇 + ((𝐸‘𝑖) + (𝑊 · 𝐷))))
247	47	nncnd 12290	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑇 ∈ ℂ)
248	247	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑇 ∈ ℂ)
249	101	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℂ)
250	248, 80, 249	add12d 11497	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑇 + ((𝐸‘𝑖) + (𝑊 · 𝐷))) = ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))))
251	45	oveq1i 7440	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑇 + (𝑊 · 𝐷)) = ((𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) + (𝑊 · 𝐷))
252	16	nncnd 12290	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ ℂ)
253	120, 109	subcld 11628	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑉 − 𝐷) ∈ ℂ)
254	113, 253	addcld 11290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐴 + (𝑉 − 𝐷)) ∈ ℂ)
255		ax-1cn 11223	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
256		subcl 11516	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 + (𝑉 − 𝐷)) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 + (𝑉 − 𝐷)) − 1) ∈ ℂ)
257	254, 255, 256	sylancl 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝐴 + (𝑉 − 𝐷)) − 1) ∈ ℂ)
258	105, 257	mulcld 11291	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) ∈ ℂ)
259	252, 258, 101	addassd 11293	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷))))
260	105, 257, 109	adddid 11295	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑊 · (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷)) = ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷)))
261	113, 253, 109	addassd 11293	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐴 + (𝑉 − 𝐷)) + 𝐷) = (𝐴 + ((𝑉 − 𝐷) + 𝐷)))
262	120, 109	npcand 11632	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝑉 − 𝐷) + 𝐷) = 𝑉)
263	262	oveq2d 7446	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐴 + ((𝑉 − 𝐷) + 𝐷)) = (𝐴 + 𝑉))
264	261, 263	eqtrd 2769	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐴 + (𝑉 − 𝐷)) + 𝐷) = (𝐴 + 𝑉))
265	264	oveq1d 7445	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴 + (𝑉 − 𝐷)) + 𝐷) − 1) = ((𝐴 + 𝑉) − 1))
266		1cnd 11266	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ ℂ)
267	254, 109, 266	addsubd 11649	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝐴 + (𝑉 − 𝐷)) + 𝐷) − 1) = (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷))
268	113, 120, 266	addsubd 11649	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝐴 + 𝑉) − 1) = ((𝐴 − 1) + 𝑉))
269	265, 267, 268	3eqtr3d 2777	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷) = ((𝐴 − 1) + 𝑉))
270	269	oveq2d 7446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑊 · (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
271	260, 270	eqtr3d 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
272	271	oveq2d 7446	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐵 + ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
273	259, 272	eqtrd 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
274	251, 273	eqtrid 2781	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑇 + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
275	274	oveq2d 7446	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸‘𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
276	275	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸‘𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
277	88	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
278	80, 77, 277	addassd 11293	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐸‘𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐸‘𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
279	80, 77	addcomd 11473	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + 𝐵) = (𝐵 + (𝐸‘𝑖)))
280	279	oveq1d 7445	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐸‘𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
281	276, 278, 280	3eqtr2d 2775	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
282	246, 250, 281	3eqtrd 2773	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃‘𝑖)) = ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
283	282, 245	oveq12d 7448	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))))
284		cnvimass 6096	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ⊆ dom 𝐺
285	284, 14	fssdm 6751	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ⊆ (1...𝑊))
286	285	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ⊆ (1...𝑊))
287		vdwapid1 16998	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ ℕ ∧ (𝐵 + (𝐸‘𝑖)) ∈ ℕ ∧ (𝐸‘𝑖) ∈ ℕ) → (𝐵 + (𝐸‘𝑖)) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)))
288	160, 162, 79, 287	syl3anc 1368	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)))
289	153, 288	sseldd 3992	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
290	286, 289	sseldd 3992	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ (1...𝑊))
291		fvoveq1 7453	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝐵 + (𝐸‘𝑖)) → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
292		eqid 2729	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
293		fvex 6918	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
294	291, 292, 293	fvmpt 7014	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 + (𝐸‘𝑖)) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
295	290, 294	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
296		vdwapid1 16998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
297	10, 41, 42, 296	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
298	43, 297	sseldd 3992	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ (^◡𝐹 “ {𝐺}))
299		fniniseg 7078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 Fn (1...𝑉) → (𝐴 ∈ (^◡𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹‘𝐴) = 𝐺)))
300	146, 299	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐴 ∈ (^◡𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹‘𝐴) = 𝐺)))
301	298, 300	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 ∈ (1...𝑉) ∧ (𝐹‘𝐴) = 𝐺))
302	301	simprd 494	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐺)
303	301	simpld 493	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ (1...𝑉))
304		oveq1 7437	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝐴 → (𝑥 − 1) = (𝐴 − 1))
305	304	oveq1d 7445	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝐴 → ((𝑥 − 1) + 𝑉) = ((𝐴 − 1) + 𝑉))
306	305	oveq2d 7446	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝐴 → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
307	306	oveq2d 7446	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝐴 → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))
308	307	fveq2d 6909	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝐴 → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
309	308	mpteq2dv 5258	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝐴 → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
310	190	mptex 7245	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) ∈ V
311	309, 40, 310	fvmpt 7014	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ (1...𝑉) → (𝐹‘𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
312	303, 311	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹‘𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
313	302, 312	eqtr3d 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
314	313	fveq1d 6907	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐺‘(𝐵 + (𝐸‘𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))))
315	314	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐵 + (𝐸‘𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))))
316	282	fveq2d 6909	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃‘𝑖))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
317	295, 315, 316	3eqtr4rd 2780	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃‘𝑖))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))
318	317	sneqd 4648	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → {(𝐻‘(𝑇 + (𝑃‘𝑖)))} = {(𝐺‘(𝐵 + (𝐸‘𝑖)))})
319	318	imaeq2d 6074	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) = (^◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
320	217, 283, 319	3sstr4d 4039	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))
321	320	ex 411	. . . . . . . . . 10 ⊢ (𝜑 → (𝑖 ∈ (1...𝑀) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
322	252	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ)
323	88	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
324	322, 323, 98	addassd 11293	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
325	127	oveq2d 7446	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
326	324, 325	eqtr4d 2772	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
327	38	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
328	12	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
329		eluzfz1 13572	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 ∈ (ℤ_≥‘1) → 1 ∈ (1...𝑀))
330	52, 329	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 1 ∈ (1...𝑀))
331	330	ne0d 4348	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1...𝑀) ≠ ∅)
332		elfzuz3 13562	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵 + (𝐸‘𝑖)) ∈ (1...𝑊) → 𝑊 ∈ (ℤ_≥‘(𝐵 + (𝐸‘𝑖))))
333	290, 332	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ_≥‘(𝐵 + (𝐸‘𝑖))))
334	16	nnzd 12647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐵 ∈ ℤ)
335		uzid 12899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐵 ∈ ℤ → 𝐵 ∈ (ℤ_≥‘𝐵))
336	334, 335	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐵 ∈ (ℤ_≥‘𝐵))
337	336	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ∈ (ℤ_≥‘𝐵))
338	79	nnnn0d 12594	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐸‘𝑖) ∈ ℕ₀)
339		uzaddcl 12950	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐵 ∈ (ℤ_≥‘𝐵) ∧ (𝐸‘𝑖) ∈ ℕ₀) → (𝐵 + (𝐸‘𝑖)) ∈ (ℤ_≥‘𝐵))
340	337, 338, 339	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ (ℤ_≥‘𝐵))
341		uztrn 12902	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑊 ∈ (ℤ_≥‘(𝐵 + (𝐸‘𝑖))) ∧ (𝐵 + (𝐸‘𝑖)) ∈ (ℤ_≥‘𝐵)) → 𝑊 ∈ (ℤ_≥‘𝐵))
342	333, 340, 341	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ_≥‘𝐵))
343		eluzle 12897	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑊 ∈ (ℤ_≥‘𝐵) → 𝐵 ≤ 𝑊)
344	342, 343	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ≤ 𝑊)
345	344	ralrimiva 3139	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊)
346		r19.2z 4502	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...𝑀) ≠ ∅ ∧ ∀𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊) → ∃𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊)
347	331, 345, 346	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ∃𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊)
348		idd 24	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ (1...𝑀) → (𝐵 ≤ 𝑊 → 𝐵 ≤ 𝑊))
349	348	rexlimiv 3141	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊 → 𝐵 ≤ 𝑊)
350	347, 349	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ≤ 𝑊)
351	12	nnzd 12647	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑊 ∈ ℤ)
352		fznn 13633	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑊 ∈ ℤ → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵 ≤ 𝑊)))
353	351, 352	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵 ≤ 𝑊)))
354	16, 350, 353	mpbir2and 711	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ (1...𝑊))
355	354	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ (1...𝑊))
356	327, 328, 151, 355	vdwlem3 17006	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
357	326, 356	eqeltrd 2829	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))))
358		fvoveq1 7453	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
359		fvex 6918	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
360	358, 178, 359	fvmpt 7014	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
361	355, 360	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
362	194	fveq1d 6907	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵))
363	326	fveq2d 6909	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
364	361, 362, 363	3eqtr4rd 2780	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵))
365	357, 364	jca 510	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵)))
366		eleq1 2817	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉)))))
367		fveqeq2 6914	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝐻‘𝑧) = (𝐺‘𝐵) ↔ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵)))
368	366, 367	anbi12d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵)) ↔ (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵))))
369	365, 368	syl5ibrcom 246	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵))))
370	369	rexlimdva 3148	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵))))
371	16, 87	nnaddcld 12326	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
372		vdwapval 16996	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ ℕ₀ ∧ (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ (𝑊 · 𝐷) ∈ ℕ) → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
373	139, 371, 65, 372	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
374		fniniseg 7078	. . . . . . . . . . . . . . 15 ⊢ (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑧 ∈ (^◡𝐻 “ {(𝐺‘𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵))))
375	212, 374	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑧 ∈ (^◡𝐻 “ {(𝐺‘𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵))))
376	370, 373, 375	3imtr4d 293	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) → 𝑧 ∈ (^◡𝐻 “ {(𝐺‘𝐵)})))
377	376	ssrdv 3997	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ⊆ (^◡𝐻 “ {(𝐺‘𝐵)}))
378	18	peano2nnd 12291	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ)
379	378, 51	eleqtrdi 2839	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) ∈ (ℤ_≥‘1))
380		eluzfz2 13573	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘1) → (𝑀 + 1) ∈ (1...(𝑀 + 1)))
381		iftrue 4542	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑀 + 1) → if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) = 0)
382	381	oveq1d 7445	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑀 + 1) → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) = (0 + (𝑊 · 𝐷)))
383		ovex 7463	. . . . . . . . . . . . . . . . . 18 ⊢ (0 + (𝑊 · 𝐷)) ∈ V
384	382, 46, 383	fvmpt 7014	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 + 1) ∈ (1...(𝑀 + 1)) → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
385	379, 380, 384	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
386	101	addlidd 11472	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 + (𝑊 · 𝐷)) = (𝑊 · 𝐷))
387	385, 386	eqtrd 2769	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃‘(𝑀 + 1)) = (𝑊 · 𝐷))
388	387	oveq2d 7446	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝑇 + (𝑊 · 𝐷)))
389	388, 274	eqtrd 2769	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
390	389, 387	oveq12d 7448	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)))
391		fvoveq1 7453	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
392		fvex 6918	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
393	391, 292, 392	fvmpt 7014	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
394	354, 393	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
395	313	fveq1d 6907	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺‘𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵))
396	389	fveq2d 6909	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
397	394, 395, 396	3eqtr4rd 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐺‘𝐵))
398	397	sneqd 4648	. . . . . . . . . . . . 13 ⊢ (𝜑 → {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))} = {(𝐺‘𝐵)})
399	398	imaeq2d 6074	. . . . . . . . . . . 12 ⊢ (𝜑 → (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}) = (^◡𝐻 “ {(𝐺‘𝐵)}))
400	377, 390, 399	3sstr4d 4039	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
401		fveq2 6905	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑀 + 1) → (𝑃‘𝑖) = (𝑃‘(𝑀 + 1)))
402	401	oveq2d 7446	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝑀 + 1) → (𝑇 + (𝑃‘𝑖)) = (𝑇 + (𝑃‘(𝑀 + 1))))
403	402, 401	oveq12d 7448	. . . . . . . . . . . 12 ⊢ (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) = ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))))
404	402	fveq2d 6909	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝑀 + 1) → (𝐻‘(𝑇 + (𝑃‘𝑖))) = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
405	404	sneqd 4648	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝑀 + 1) → {(𝐻‘(𝑇 + (𝑃‘𝑖)))} = {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})
406	405	imaeq2d 6074	. . . . . . . . . . . 12 ⊢ (𝑖 = (𝑀 + 1) → (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) = (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
407	403, 406	sseq12d 4025	. . . . . . . . . . 11 ⊢ (𝑖 = (𝑀 + 1) → (((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) ↔ ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})))
408	400, 407	syl5ibrcom 246	. . . . . . . . . 10 ⊢ (𝜑 → (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
409	321, 408	jaod 857	. . . . . . . . 9 ⊢ (𝜑 → ((𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
410	75, 409	sylbid 239	. . . . . . . 8 ⊢ (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
411	410	ralrimiv 3138	. . . . . . 7 ⊢ (𝜑 → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))
412	411	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))
413	220	rexeqdv 3320	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ ∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))))
414		rexun 4201	. . . . . . . . . . . . 13 ⊢ (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))))
415	317	eqeq2d 2740	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
416	415	rexbidva 3170	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))))
417		ovex 7463	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 + 1) ∈ V
418	404	eqeq2d 2740	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑀 + 1) → (𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))))
419	417, 418	rexsn 4694	. . . . . . . . . . . . . . 15 ⊢ (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
420	397	eqeq2d 2740	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) ↔ 𝑥 = (𝐺‘𝐵)))
421	419, 420	bitrid 282	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐺‘𝐵)))
422	416, 421	orbi12d 916	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))))
423	414, 422	bitrid 282	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))))
424	413, 423	bitrd 278	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))))
425	424	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))))
426	425	abbidv 2798	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))} = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))})
427		eqid 2729	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))
428	427	rnmpt 5965	. . . . . . . . 9 ⊢ ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))) = {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))}
429	2	rnmpt 5965	. . . . . . . . . . 11 ⊢ ran 𝐽 = {𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))}
430		df-sn 4637	. . . . . . . . . . 11 ⊢ {(𝐺‘𝐵)} = {𝑥 ∣ 𝑥 = (𝐺‘𝐵)}
431	429, 430	uneq12i 4171	. . . . . . . . . 10 ⊢ (ran 𝐽 ∪ {(𝐺‘𝐵)}) = ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))} ∪ {𝑥 ∣ 𝑥 = (𝐺‘𝐵)})
432		unab 4310	. . . . . . . . . 10 ⊢ ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))} ∪ {𝑥 ∣ 𝑥 = (𝐺‘𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))}
433	431, 432	eqtri 2757	. . . . . . . . 9 ⊢ (ran 𝐽 ∪ {(𝐺‘𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))}
434	426, 428, 433	3eqtr4g 2794	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))) = (ran 𝐽 ∪ {(𝐺‘𝐵)}))
435	434	fveq2d 6909	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (♯‘(ran 𝐽 ∪ {(𝐺‘𝐵)})))
436		fzfi 14003	. . . . . . . . . 10 ⊢ (1...𝑀) ∈ Fin
437		dffn4 6825	. . . . . . . . . . 11 ⊢ (𝐽 Fn (1...𝑀) ↔ 𝐽:(1...𝑀)–onto→ran 𝐽)
438	3, 437	mpbi 229	. . . . . . . . . 10 ⊢ 𝐽:(1...𝑀)–onto→ran 𝐽
439		fofi 9360	. . . . . . . . . 10 ⊢ (((1...𝑀) ∈ Fin ∧ 𝐽:(1...𝑀)–onto→ran 𝐽) → ran 𝐽 ∈ Fin)
440	436, 438, 439	mp2an 690	. . . . . . . . 9 ⊢ ran 𝐽 ∈ Fin
441	440	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ran 𝐽 ∈ Fin)
442		fvex 6918	. . . . . . . . 9 ⊢ (𝐺‘𝐵) ∈ V
443		hashunsng 14421	. . . . . . . . 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 578	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺‘𝐵)})) = ((♯‘ran 𝐽) + 1))
446	44	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘ran 𝐽) = 𝑀)
447	446	oveq1d 7445	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ((♯‘ran 𝐽) + 1) = (𝑀 + 1))
448	435, 445, 447	3eqtrd 2773	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1))
449	412, 448	jca 510	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1)))
450		oveq1 7437	. . . . . . . . . 10 ⊢ (𝑎 = 𝑇 → (𝑎 + (𝑑‘𝑖)) = (𝑇 + (𝑑‘𝑖)))
451	450	oveq1d 7445	. . . . . . . . 9 ⊢ (𝑎 = 𝑇 → ((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) = ((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)))
452		fvoveq1 7453	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑇 → (𝐻‘(𝑎 + (𝑑‘𝑖))) = (𝐻‘(𝑇 + (𝑑‘𝑖))))
453	452	sneqd 4648	. . . . . . . . . 10 ⊢ (𝑎 = 𝑇 → {(𝐻‘(𝑎 + (𝑑‘𝑖)))} = {(𝐻‘(𝑇 + (𝑑‘𝑖)))})
454	453	imaeq2d 6074	. . . . . . . . 9 ⊢ (𝑎 = 𝑇 → (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) = (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}))
455	451, 454	sseq12d 4025	. . . . . . . 8 ⊢ (𝑎 = 𝑇 → (((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ↔ ((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))})))
456	455	ralbidv 3171	. . . . . . 7 ⊢ (𝑎 = 𝑇 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))})))
457	452	mpteq2dv 5258	. . . . . . . . 9 ⊢ (𝑎 = 𝑇 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))))
458	457	rneqd 5948	. . . . . . . 8 ⊢ (𝑎 = 𝑇 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))))
459	458	fveqeq2d 6913	. . . . . . 7 ⊢ (𝑎 = 𝑇 → ((♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1) ↔ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1)))
460	456, 459	anbi12d 630	. . . . . 6 ⊢ (𝑎 = 𝑇 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1))))
461		fveq1 6904	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑃 → (𝑑‘𝑖) = (𝑃‘𝑖))
462	461	oveq2d 7446	. . . . . . . . . 10 ⊢ (𝑑 = 𝑃 → (𝑇 + (𝑑‘𝑖)) = (𝑇 + (𝑃‘𝑖)))
463	462, 461	oveq12d 7448	. . . . . . . . 9 ⊢ (𝑑 = 𝑃 → ((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) = ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)))
464	462	fveq2d 6909	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑃 → (𝐻‘(𝑇 + (𝑑‘𝑖))) = (𝐻‘(𝑇 + (𝑃‘𝑖))))
465	464	sneqd 4648	. . . . . . . . . 10 ⊢ (𝑑 = 𝑃 → {(𝐻‘(𝑇 + (𝑑‘𝑖)))} = {(𝐻‘(𝑇 + (𝑃‘𝑖)))})
466	465	imaeq2d 6074	. . . . . . . . 9 ⊢ (𝑑 = 𝑃 → (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) = (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))
467	463, 466	sseq12d 4025	. . . . . . . 8 ⊢ (𝑑 = 𝑃 → (((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ↔ ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
468	467	ralbidv 3171	. . . . . . 7 ⊢ (𝑑 = 𝑃 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})))
469	464	mpteq2dv 5258	. . . . . . . . 9 ⊢ (𝑑 = 𝑃 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))))
470	469	rneqd 5948	. . . . . . . 8 ⊢ (𝑑 = 𝑃 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))))
471	470	fveqeq2d 6913	. . . . . . 7 ⊢ (𝑑 = 𝑃 → ((♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1) ↔ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1)))
472	468, 471	anbi12d 630	. . . . . 6 ⊢ (𝑑 = 𝑃 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1))))
473	460, 472	rspc2ev 3633	. . . . 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 1368	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑_m (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1)))
475		ovex 7463	. . . . 5 ⊢ (1...(𝑊 · (2 · 𝑉))) ∈ V
476	10	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ)
477	476	nnnn0d 12594	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ₀)
478	39	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
479	18	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑀 ∈ ℕ)
480	479	peano2nnd 12291	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (𝑀 + 1) ∈ ℕ)
481		eqid 2729	. . . . 5 ⊢ (1...(𝑀 + 1)) = (1...(𝑀 + 1))
482	475, 477, 478, 480, 481	vdwpc 17003	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑_m (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (^◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1))))
483	474, 482	mpbird 256	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻)
484	483	orcd 871	. 2 ⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))
485	37, 484	pm2.61dan 811	1 ⊢ (𝜑 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∨ wo 845 = wceq 1534 ∈ wcel 2100 {cab 2706 ≠ wne 2933 ∀wral 3054 ∃wrex 3063 Vcvv 3472 ∪ cun 3957 ⊆ wss 3959 ∅c0 4335 ifcif 4536 {csn 4636 ⟨cop 4642 class class class wbr 5156 ↦ cmpt 5239 ^◡ccnv 5685 ran crn 5687 “ cima 5689 Fn wfn 6553 ⟶wf 6554 –onto→wfo 6556 ‘cfv 6558 (class class class)co 7430 ↑_m cmap 8863 Fincfn 8982 ℂcc 11163 ℝcr 11164 0cc0 11165 1c1 11166 + caddc 11168 · cmul 11170 < clt 11305 ≤ cle 11306 − cmin 11501 ℕcn 12274 2c2 12329 ℕ₀cn0 12534 ℤcz 12620 ℤ_≥cuz 12884 ...cfz 13548 ♯chash 14359 APcvdwa 16988 MonoAP cvdwm 16989 PolyAP cvdwp 16990

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2102 ax-9 2110 ax-10 2133 ax-11 2150 ax-12 2170 ax-ext 2700 ax-rep 5293 ax-sep 5307 ax-nul 5314 ax-pow 5373 ax-pr 5437 ax-un 7751 ax-cnex 11221 ax-resscn 11222 ax-1cn 11223 ax-icn 11224 ax-addcl 11225 ax-addrcl 11226 ax-mulcl 11227 ax-mulrcl 11228 ax-mulcom 11229 ax-addass 11230 ax-mulass 11231 ax-distr 11232 ax-i2m1 11233 ax-1ne0 11234 ax-1rid 11235 ax-rnegex 11236 ax-rrecex 11237 ax-cnre 11238 ax-pre-lttri 11239 ax-pre-lttrn 11240 ax-pre-ltadd 11241 ax-pre-mulgt0 11242

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2062 df-mo 2532 df-eu 2561 df-clab 2707 df-cleq 2721 df-clel 2806 df-nfc 2881 df-ne 2934 df-nel 3040 df-ral 3055 df-rex 3064 df-reu 3374 df-rab 3429 df-v 3474 df-sbc 3789 df-csb 3905 df-dif 3962 df-un 3964 df-in 3966 df-ss 3976 df-pss 3979 df-nul 4336 df-if 4537 df-pw 4612 df-sn 4637 df-pr 4639 df-op 4643 df-uni 4919 df-int 4960 df-iun 5008 df-br 5157 df-opab 5219 df-mpt 5240 df-tr 5274 df-id 5584 df-eprel 5590 df-po 5598 df-so 5599 df-fr 5641 df-we 5643 df-xp 5692 df-rel 5693 df-cnv 5694 df-co 5695 df-dm 5696 df-rn 5697 df-res 5698 df-ima 5699 df-pred 6317 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6510 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7386 df-ov 7433 df-oprab 7434 df-mpo 7435 df-om 7885 df-1st 8011 df-2nd 8012 df-frecs 8304 df-wrecs 8335 df-recs 8409 df-rdg 8448 df-1o 8504 df-oadd 8508 df-er 8742 df-map 8865 df-en 8983 df-dom 8984 df-sdom 8985 df-fin 8986 df-dju 9951 df-card 9989 df-pnf 11307 df-mnf 11308 df-xr 11309 df-ltxr 11310 df-le 11311 df-sub 11503 df-neg 11504 df-nn 12275 df-2 12337 df-n0 12535 df-z 12621 df-uz 12885 df-rp 13039 df-fz 13549 df-hash 14360 df-vdwap 16991 df-vdwmc 16992 df-vdwpc 16993

This theorem is referenced by: vdwlem7 17010

W3C validator