Theorem vdwlem6

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

	Ref	Expression
Hypotheses	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	vdwlem6	⊢ ( 𝜑 → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐺 ) )

Proof

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