Metamath Proof Explorer

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 syl5bi ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝐵 ) ∈ 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 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝐺 ‘ 𝐵 ) ∈ 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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 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 addid2d ⊢ ( 𝜑 → ( 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 syl5bb ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ { ( 𝑀 + 1 ) } 𝑥 = ( 𝐻 ‘ ( 𝑇 + ( 𝑃 ‘ 𝑖 ) ) ) ↔ 𝑥 = ( 𝐺 ‘ 𝐵 ) ) )
422 416 421 orbi12d ⊢ ( 𝜑 → ( ( ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 𝑥 = ( 𝐻 ‘ ( 𝑇 + ( 𝑃 ‘ 𝑖 ) ) ) ∨ ∃ 𝑖 ∈ { ( 𝑀 + 1 ) } 𝑥 = ( 𝐻 ‘ ( 𝑇 + ( 𝑃 ‘ 𝑖 ) ) ) ) ↔ ( ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 𝑥 = ( 𝐺 ‘ ( 𝐵 + ( 𝐸 ‘ 𝑖 ) ) ) ∨ 𝑥 = ( 𝐺 ‘ 𝐵 ) ) ) )
423 414 422 syl5bb ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ( ( 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 𝐺 ) )