MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vdwlem6 Structured version   Visualization version   GIF version

Theorem vdwlem6 15737
Description: Lemma for vdw 15745. (Contributed by Mario Carneiro, 13-Sep-2014.)
Hypotheses
Ref Expression
vdwlem3.v (𝜑𝑉 ∈ ℕ)
vdwlem3.w (𝜑𝑊 ∈ ℕ)
vdwlem4.r (𝜑𝑅 ∈ Fin)
vdwlem4.h (𝜑𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
vdwlem4.f 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))))
vdwlem7.m (𝜑𝑀 ∈ ℕ)
vdwlem7.g (𝜑𝐺:(1...𝑊)⟶𝑅)
vdwlem7.k (𝜑𝐾 ∈ (ℤ‘2))
vdwlem7.a (𝜑𝐴 ∈ ℕ)
vdwlem7.d (𝜑𝐷 ∈ ℕ)
vdwlem7.s (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (𝐹 “ {𝐺}))
vdwlem6.b (𝜑𝐵 ∈ ℕ)
vdwlem6.e (𝜑𝐸:(1...𝑀)⟶ℕ)
vdwlem6.s (𝜑 → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
vdwlem6.j 𝐽 = (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝐵 + (𝐸𝑖))))
vdwlem6.r (𝜑 → (#‘ran 𝐽) = 𝑀)
vdwlem6.t 𝑇 = (𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1)))
vdwlem6.p 𝑃 = (𝑗 ∈ (1...(𝑀 + 1)) ↦ (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)))
Assertion
Ref Expression
vdwlem6 (𝜑 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑖,𝑗,𝑥,𝑦,𝐺   𝑖,𝐾,𝑗,𝑥,𝑦   𝑖,𝐽,𝑗,𝑥   𝑃,𝑖,𝑥   𝜑,𝑖,𝑗,𝑥,𝑦   𝑅,𝑖,𝑥,𝑦   𝐵,𝑖,𝑗,𝑥,𝑦   𝑖,𝐻,𝑥,𝑦   𝑖,𝑀,𝑗,𝑥,𝑦   𝐷,𝑗,𝑥,𝑦   𝑖,𝐸,𝑗,𝑥,𝑦   𝑖,𝑊,𝑗,𝑥,𝑦   𝑇,𝑖,𝑥   𝑥,𝑉,𝑦
Allowed substitution hints:   𝐴(𝑖,𝑗)   𝐷(𝑖)   𝑃(𝑦,𝑗)   𝑅(𝑗)   𝑇(𝑦,𝑗)   𝐹(𝑥,𝑦,𝑖,𝑗)   𝐻(𝑗)   𝐽(𝑦)   𝑉(𝑖,𝑗)

Proof of Theorem vdwlem6
Dummy variables 𝑚 𝑛 𝑧 𝑎 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 6239 . . . . . . 7 (𝐺‘(𝐵 + (𝐸𝑖))) ∈ V
2 vdwlem6.j . . . . . . 7 𝐽 = (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝐵 + (𝐸𝑖))))
31, 2fnmpti 6060 . . . . . 6 𝐽 Fn (1...𝑀)
4 fvelrnb 6282 . . . . . 6 (𝐽 Fn (1...𝑀) → ((𝐺𝐵) ∈ ran 𝐽 ↔ ∃𝑚 ∈ (1...𝑀)(𝐽𝑚) = (𝐺𝐵)))
53, 4ax-mp 5 . . . . 5 ((𝐺𝐵) ∈ ran 𝐽 ↔ ∃𝑚 ∈ (1...𝑀)(𝐽𝑚) = (𝐺𝐵))
6 vdwlem4.r . . . . . . . 8 (𝜑𝑅 ∈ Fin)
76adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝑅 ∈ Fin)
8 vdwlem7.k . . . . . . . . 9 (𝜑𝐾 ∈ (ℤ‘2))
9 eluz2nn 11764 . . . . . . . . 9 (𝐾 ∈ (ℤ‘2) → 𝐾 ∈ ℕ)
108, 9syl 17 . . . . . . . 8 (𝜑𝐾 ∈ ℕ)
1110adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝐾 ∈ ℕ)
12 vdwlem3.w . . . . . . . 8 (𝜑𝑊 ∈ ℕ)
1312adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝑊 ∈ ℕ)
14 vdwlem7.g . . . . . . . 8 (𝜑𝐺:(1...𝑊)⟶𝑅)
1514adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝐺:(1...𝑊)⟶𝑅)
16 vdwlem6.b . . . . . . . 8 (𝜑𝐵 ∈ ℕ)
1716adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝐵 ∈ ℕ)
18 vdwlem7.m . . . . . . . 8 (𝜑𝑀 ∈ ℕ)
1918adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝑀 ∈ ℕ)
20 vdwlem6.e . . . . . . . 8 (𝜑𝐸:(1...𝑀)⟶ℕ)
2120adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝐸:(1...𝑀)⟶ℕ)
22 vdwlem6.s . . . . . . . 8 (𝜑 → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
2322adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
24 simprl 809 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝑚 ∈ (1...𝑀))
25 simprr 811 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐽𝑚) = (𝐺𝐵))
26 fveq2 6229 . . . . . . . . . . . 12 (𝑖 = 𝑚 → (𝐸𝑖) = (𝐸𝑚))
2726oveq2d 6706 . . . . . . . . . . 11 (𝑖 = 𝑚 → (𝐵 + (𝐸𝑖)) = (𝐵 + (𝐸𝑚)))
2827fveq2d 6233 . . . . . . . . . 10 (𝑖 = 𝑚 → (𝐺‘(𝐵 + (𝐸𝑖))) = (𝐺‘(𝐵 + (𝐸𝑚))))
29 fvex 6239 . . . . . . . . . 10 (𝐺‘(𝐵 + (𝐸𝑚))) ∈ V
3028, 2, 29fvmpt 6321 . . . . . . . . 9 (𝑚 ∈ (1...𝑀) → (𝐽𝑚) = (𝐺‘(𝐵 + (𝐸𝑚))))
3124, 30syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐽𝑚) = (𝐺‘(𝐵 + (𝐸𝑚))))
3225, 31eqtr3d 2687 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐺𝐵) = (𝐺‘(𝐵 + (𝐸𝑚))))
337, 11, 13, 15, 17, 19, 21, 23, 24, 32vdwlem1 15732 . . . . . 6 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐾 + 1) MonoAP 𝐺)
3433rexlimdvaa 3061 . . . . 5 (𝜑 → (∃𝑚 ∈ (1...𝑀)(𝐽𝑚) = (𝐺𝐵) → (𝐾 + 1) MonoAP 𝐺))
355, 34syl5bi 232 . . . 4 (𝜑 → ((𝐺𝐵) ∈ ran 𝐽 → (𝐾 + 1) MonoAP 𝐺))
3635imp 444 . . 3 ((𝜑 ∧ (𝐺𝐵) ∈ ran 𝐽) → (𝐾 + 1) MonoAP 𝐺)
3736olcd 407 . 2 ((𝜑 ∧ (𝐺𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))
38 vdwlem3.v . . . . . . 7 (𝜑𝑉 ∈ ℕ)
39 vdwlem4.h . . . . . . 7 (𝜑𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
40 vdwlem4.f . . . . . . 7 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))))
41 vdwlem7.a . . . . . . 7 (𝜑𝐴 ∈ ℕ)
42 vdwlem7.d . . . . . . 7 (𝜑𝐷 ∈ ℕ)
43 vdwlem7.s . . . . . . 7 (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (𝐹 “ {𝐺}))
44 vdwlem6.r . . . . . . 7 (𝜑 → (#‘ran 𝐽) = 𝑀)
45 vdwlem6.t . . . . . . 7 𝑇 = (𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1)))
46 vdwlem6.p . . . . . . 7 𝑃 = (𝑗 ∈ (1...(𝑀 + 1)) ↦ (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)))
4738, 12, 6, 39, 40, 18, 14, 8, 41, 42, 43, 16, 20, 22, 2, 44, 45, 46vdwlem5 15736 . . . . . 6 (𝜑𝑇 ∈ ℕ)
4847adantr 480 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑇 ∈ ℕ)
49 0nn0 11345 . . . . . . . . . 10 0 ∈ ℕ0
5049a1i 11 . . . . . . . . 9 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 = (𝑀 + 1)) → 0 ∈ ℕ0)
51 nnuz 11761 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
5218, 51syl6eleq 2740 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ (ℤ‘1))
5352adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑀 ∈ (ℤ‘1))
54 elfzp1 12429 . . . . . . . . . . . . . . 15 (𝑀 ∈ (ℤ‘1) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1))))
5553, 54syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1))))
5655biimpa 500 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1)))
5756ord 391 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 ∈ (1...𝑀) → 𝑗 = (𝑀 + 1)))
5857con1d 139 . . . . . . . . . . 11 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 = (𝑀 + 1) → 𝑗 ∈ (1...𝑀)))
5958imp 444 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → 𝑗 ∈ (1...𝑀))
6020ad2antrr 762 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → 𝐸:(1...𝑀)⟶ℕ)
6160ffvelrnda 6399 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸𝑗) ∈ ℕ)
6261nnnn0d 11389 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸𝑗) ∈ ℕ0)
6359, 62syldan 486 . . . . . . . . 9 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → (𝐸𝑗) ∈ ℕ0)
6450, 63ifclda 4153 . . . . . . . 8 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) ∈ ℕ0)
6512, 42nnmulcld 11106 . . . . . . . . 9 (𝜑 → (𝑊 · 𝐷) ∈ ℕ)
6665ad2antrr 762 . . . . . . . 8 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑊 · 𝐷) ∈ ℕ)
67 nn0nnaddcl 11362 . . . . . . . 8 ((if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) ∈ ℕ0 ∧ (𝑊 · 𝐷) ∈ ℕ) → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
6864, 66, 67syl2anc 694 . . . . . . 7 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
6968, 46fmptd 6425 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑃:(1...(𝑀 + 1))⟶ℕ)
70 nnex 11064 . . . . . . 7 ℕ ∈ V
71 ovex 6718 . . . . . . 7 (1...(𝑀 + 1)) ∈ V
7270, 71elmap 7928 . . . . . 6 (𝑃 ∈ (ℕ ↑𝑚 (1...(𝑀 + 1))) ↔ 𝑃:(1...(𝑀 + 1))⟶ℕ)
7369, 72sylibr 224 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑃 ∈ (ℕ ↑𝑚 (1...(𝑀 + 1))))
74 elfzp1 12429 . . . . . . . . . 10 (𝑀 ∈ (ℤ‘1) → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1))))
7552, 74syl 17 . . . . . . . . 9 (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1))))
7616adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℕ)
7776nncnd 11074 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℂ)
7877adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ)
7920ffvelrnda 6399 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐸𝑖) ∈ ℕ)
8079nncnd 11074 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐸𝑖) ∈ ℂ)
8180adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐸𝑖) ∈ ℂ)
8278, 81addcld 10097 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝐸𝑖)) ∈ ℂ)
83 nnm1nn0 11372 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ ℕ → (𝐴 − 1) ∈ ℕ0)
8441, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐴 − 1) ∈ ℕ0)
85 nn0nnaddcl 11362 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 − 1) ∈ ℕ0𝑉 ∈ ℕ) → ((𝐴 − 1) + 𝑉) ∈ ℕ)
8684, 38, 85syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℕ)
8712, 86nnmulcld 11106 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
8887nncnd 11074 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
8988ad2antrr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
90 elfznn0 12471 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ (0...(𝐾 − 1)) → 𝑚 ∈ ℕ0)
9190adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℕ0)
9291nn0cnd 11391 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
9392adantlr 751 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
9493, 81mulcld 10098 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝐸𝑖)) ∈ ℂ)
9565nnnn0d 11389 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑊 · 𝐷) ∈ ℕ0)
9695adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℕ0)
9791, 96nn0mulcld 11394 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℕ0)
9897nn0cnd 11391 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
9998adantlr 751 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
10082, 89, 94, 99add4d 10302 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸𝑖)) + (𝑚 · (𝑊 · 𝐷)))) = (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
10165nncnd 11074 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑊 · 𝐷) ∈ ℂ)
102101ad2antrr 762 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℂ)
10393, 81, 102adddid 10102 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))) = ((𝑚 · (𝐸𝑖)) + (𝑚 · (𝑊 · 𝐷))))
104103oveq2d 6706 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸𝑖)) + (𝑚 · (𝑊 · 𝐷)))))
10512nncnd 11074 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑊 ∈ ℂ)
106105adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℂ)
10786nncnd 11074 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℂ)
108107adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 − 1) + 𝑉) ∈ ℂ)
10942nncnd 11074 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐷 ∈ ℂ)
110109adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐷 ∈ ℂ)
11192, 110mulcld 10098 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · 𝐷) ∈ ℂ)
112106, 108, 111adddid 10102 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
11341nncnd 11074 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐴 ∈ ℂ)
114113adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐴 ∈ ℂ)
115 1cnd 10094 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 1 ∈ ℂ)
116114, 111, 115addsubd 10451 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) − 1) = ((𝐴 − 1) + (𝑚 · 𝐷)))
117116oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉))
11884nn0cnd 11391 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 − 1) ∈ ℂ)
119118adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 − 1) ∈ ℂ)
12038nncnd 11074 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑉 ∈ ℂ)
121120adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℂ)
122119, 111, 121add32d 10301 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
123117, 122eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
124123oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))))
12592, 106, 110mul12d 10283 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) = (𝑊 · (𝑚 · 𝐷)))
126125oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
127112, 124, 1263eqtr4d 2695 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
128127adantlr 751 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
129128oveq2d 6706 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
130100, 104, 1293eqtr4d 2695 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
13138ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
13212ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
13343adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴(AP‘𝐾)𝐷) ⊆ (𝐹 “ {𝐺}))
134 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))
135 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑚 → (𝑛 · 𝐷) = (𝑚 · 𝐷))
136135oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑚 → (𝐴 + (𝑛 · 𝐷)) = (𝐴 + (𝑚 · 𝐷)))
137136eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → ((𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)) ↔ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))))
138137rspcev 3340 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 ∈ (0...(𝐾 − 1)) ∧ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
139134, 138mpan2 707 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
14010nnnn0d 11389 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐾 ∈ ℕ0)
141 vdwapval 15724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
142140, 41, 42, 141syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
143142biimpar 501 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
144139, 143sylan2 490 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
145133, 144sseldd 3637 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺}))
14638, 12, 6, 39, 40vdwlem4 15735 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹:(1...𝑉)⟶(𝑅𝑚 (1...𝑊)))
147 ffn 6083 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹:(1...𝑉)⟶(𝑅𝑚 (1...𝑊)) → 𝐹 Fn (1...𝑉))
148146, 147syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹 Fn (1...𝑉))
149 fniniseg 6378 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 Fn (1...𝑉) → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
150148, 149syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
151150biimpa 500 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺})) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
152145, 151syldan 486 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
153152simpld 474 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
154153adantlr 751 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
15522r19.21bi 2961 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
156155adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
157 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))
158 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑚 → (𝑛 · (𝐸𝑖)) = (𝑚 · (𝐸𝑖)))
159158oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))))
160159eqeq2d 2661 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑚 → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖))) ↔ ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))))
161160rspcev 3340 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚 ∈ (0...(𝐾 − 1)) ∧ ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖))))
162157, 161mpan2 707 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖))))
16310adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ)
164163nnnn0d 11389 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ0)
16576, 79nnaddcld 11105 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ ℕ)
166 vdwapval 15724 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐾 ∈ ℕ0 ∧ (𝐵 + (𝐸𝑖)) ∈ ℕ ∧ (𝐸𝑖) ∈ ℕ) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖)))))
167164, 165, 79, 166syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖)))))
168167biimpar 501 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖 ∈ (1...𝑀)) ∧ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖)))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
169162, 168sylan2 490 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
170156, 169sseldd 3637 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
171 ffn 6083 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐺:(1...𝑊)⟶𝑅𝐺 Fn (1...𝑊))
17214, 171syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐺 Fn (1...𝑊))
173172adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐺 Fn (1...𝑊))
174 fniniseg 6378 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 Fn (1...𝑊) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖))))))
175173, 174syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖))))))
176175biimpa 500 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))})) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
177170, 176syldan 486 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
178177simpld 474 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊))
179131, 132, 154, 178vdwlem3 15734 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
180130, 179eqeltrd 2730 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))))
181 oveq1 6697 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) → (𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
182181fveq2d 6233 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
183 eqid 2651 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
184 fvex 6239 . . . . . . . . . . . . . . . . . . . 20 (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
185182, 183, 184fvmpt 6321 . . . . . . . . . . . . . . . . . . 19 (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
186178, 185syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
187177simprd 478 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖))))
188152simprd 478 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)
189 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑥 − 1) = ((𝐴 + (𝑚 · 𝐷)) − 1))
190189oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → ((𝑥 − 1) + 𝑉) = (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))
191190oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))
192191oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
193192fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
194193mpteq2dv 4778 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
195 ovex 6718 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1...𝑊) ∈ V
196195mptex 6527 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) ∈ V
197194, 40, 196fvmpt 6321 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
198153, 197syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
199188, 198eqtr3d 2687 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
200199adantlr 751 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
201200fveq1d 6231 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))))
202187, 201eqtr3d 2687 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘(𝐵 + (𝐸𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))))
203130fveq2d 6233 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
204186, 202, 2033eqtr4rd 2696 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖))))
205180, 204jca 553 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
206 eleq1 2718 . . . . . . . . . . . . . . . . 17 (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉)))))
207 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → (𝐻𝑥) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))))
208207eqeq1d 2653 . . . . . . . . . . . . . . . . 17 (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → ((𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))) ↔ (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
209206, 208anbi12d 747 . . . . . . . . . . . . . . . 16 (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → ((𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖)))) ↔ ((((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖))))))
210205, 209syl5ibrcom 237 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
211210rexlimdva 3060 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
21287adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
213165, 212nnaddcld 11105 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
21465adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℕ)
21579, 214nnaddcld 11105 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + (𝑊 · 𝐷)) ∈ ℕ)
216 vdwapval 15724 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℕ0 ∧ ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ ((𝐸𝑖) + (𝑊 · 𝐷)) ∈ ℕ) → (𝑥 ∈ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))))
217164, 213, 215, 216syl3anc 1366 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))))
218 ffn 6083 . . . . . . . . . . . . . . . . 17 (𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
21939, 218syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
220219adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
221 fniniseg 6378 . . . . . . . . . . . . . . 15 (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑥 ∈ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
222220, 221syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
223211, 217, 2223imtr4d 283 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) → 𝑥 ∈ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))})))
224223ssrdv 3642 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) ⊆ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
225 ssun1 3809 . . . . . . . . . . . . . . . . . . 19 (1...𝑀) ⊆ ((1...𝑀) ∪ {(𝑀 + 1)})
226 fzsuc 12426 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (ℤ‘1) → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
22752, 226syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
228225, 227syl5sseqr 3687 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1...𝑀) ⊆ (1...(𝑀 + 1)))
229228sselda 3636 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...(𝑀 + 1)))
230 eqeq1 2655 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝑗 = (𝑀 + 1) ↔ 𝑖 = (𝑀 + 1)))
231 fveq2 6229 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝐸𝑗) = (𝐸𝑖))
232230, 231ifbieq2d 4144 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) = if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)))
233232oveq1d 6705 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) = (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)))
234 ovex 6718 . . . . . . . . . . . . . . . . . 18 (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)) ∈ V
235233, 46, 234fvmpt 6321 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...(𝑀 + 1)) → (𝑃𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)))
236229, 235syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑃𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)))
237 elfzle2 12383 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (1...𝑀) → 𝑖𝑀)
23818nnred 11073 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑀 ∈ ℝ)
239238ltp1d 10992 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑀 < (𝑀 + 1))
240 peano2re 10247 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
241238, 240syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑀 + 1) ∈ ℝ)
242238, 241ltnled 10222 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀))
243239, 242mpbid 222 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀)
244 breq1 4688 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑀 + 1) → (𝑖𝑀 ↔ (𝑀 + 1) ≤ 𝑀))
245244notbid 307 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = (𝑀 + 1) → (¬ 𝑖𝑀 ↔ ¬ (𝑀 + 1) ≤ 𝑀))
246243, 245syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑖 = (𝑀 + 1) → ¬ 𝑖𝑀))
247246con2d 129 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑖𝑀 → ¬ 𝑖 = (𝑀 + 1)))
248237, 247syl5 34 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑖 ∈ (1...𝑀) → ¬ 𝑖 = (𝑀 + 1)))
249248imp 444 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → ¬ 𝑖 = (𝑀 + 1))
250 iffalse 4128 . . . . . . . . . . . . . . . . . 18 𝑖 = (𝑀 + 1) → if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) = (𝐸𝑖))
251250oveq1d 6705 . . . . . . . . . . . . . . . . 17 𝑖 = (𝑀 + 1) → (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)) = ((𝐸𝑖) + (𝑊 · 𝐷)))
252249, 251syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)) = ((𝐸𝑖) + (𝑊 · 𝐷)))
253236, 252eqtrd 2685 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑃𝑖) = ((𝐸𝑖) + (𝑊 · 𝐷)))
254253oveq2d 6706 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃𝑖)) = (𝑇 + ((𝐸𝑖) + (𝑊 · 𝐷))))
25547nncnd 11074 . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ ℂ)
256255adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑇 ∈ ℂ)
257101adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℂ)
258256, 80, 257add12d 10300 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑇 + ((𝐸𝑖) + (𝑊 · 𝐷))) = ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))))
25945oveq1i 6700 . . . . . . . . . . . . . . . . . 18 (𝑇 + (𝑊 · 𝐷)) = ((𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1))) + (𝑊 · 𝐷))
26016nncnd 11074 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℂ)
261120, 109subcld 10430 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑉𝐷) ∈ ℂ)
262113, 261addcld 10097 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 + (𝑉𝐷)) ∈ ℂ)
263 ax-1cn 10032 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℂ
264 subcl 10318 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 + (𝑉𝐷)) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 + (𝑉𝐷)) − 1) ∈ ℂ)
265262, 263, 264sylancl 695 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 + (𝑉𝐷)) − 1) ∈ ℂ)
266105, 265mulcld 10098 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) ∈ ℂ)
267260, 266, 101addassd 10100 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷))))
268105, 265, 109adddid 10102 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑊 · (((𝐴 + (𝑉𝐷)) − 1) + 𝐷)) = ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷)))
269113, 261, 109addassd 10100 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 + (𝑉𝐷)) + 𝐷) = (𝐴 + ((𝑉𝐷) + 𝐷)))
270120, 109npcand 10434 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑉𝐷) + 𝐷) = 𝑉)
271270oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐴 + ((𝑉𝐷) + 𝐷)) = (𝐴 + 𝑉))
272269, 271eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐴 + (𝑉𝐷)) + 𝐷) = (𝐴 + 𝑉))
273272oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝐴 + (𝑉𝐷)) + 𝐷) − 1) = ((𝐴 + 𝑉) − 1))
274 1cnd 10094 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ∈ ℂ)
275262, 109, 274addsubd 10451 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝐴 + (𝑉𝐷)) + 𝐷) − 1) = (((𝐴 + (𝑉𝐷)) − 1) + 𝐷))
276113, 120, 274addsubd 10451 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 + 𝑉) − 1) = ((𝐴 − 1) + 𝑉))
277273, 275, 2763eqtr3d 2693 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐴 + (𝑉𝐷)) − 1) + 𝐷) = ((𝐴 − 1) + 𝑉))
278277oveq2d 6706 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑊 · (((𝐴 + (𝑉𝐷)) − 1) + 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
279268, 278eqtr3d 2687 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
280279oveq2d 6706 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵 + ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
281267, 280eqtrd 2685 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
282259, 281syl5eq 2697 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑇 + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
283282oveq2d 6706 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
284283adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
28588adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
28680, 77, 285addassd 10100 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐸𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐸𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
28780, 77addcomd 10276 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + 𝐵) = (𝐵 + (𝐸𝑖)))
288287oveq1d 6705 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐸𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
289284, 286, 2883eqtr2d 2691 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
290254, 258, 2893eqtrd 2689 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃𝑖)) = ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
291290, 253oveq12d 6708 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))))
292 cnvimass 5520 . . . . . . . . . . . . . . . . . . 19 (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ⊆ dom 𝐺
293 fdm 6089 . . . . . . . . . . . . . . . . . . . 20 (𝐺:(1...𝑊)⟶𝑅 → dom 𝐺 = (1...𝑊))
29414, 293syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → dom 𝐺 = (1...𝑊))
295292, 294syl5sseq 3686 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ⊆ (1...𝑊))
296295adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ⊆ (1...𝑊))
297 vdwapid1 15726 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ ℕ ∧ (𝐵 + (𝐸𝑖)) ∈ ℕ ∧ (𝐸𝑖) ∈ ℕ) → (𝐵 + (𝐸𝑖)) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
298163, 165, 79, 297syl3anc 1366 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
299155, 298sseldd 3637 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
300296, 299sseldd 3637 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ (1...𝑊))
301 oveq1 6697 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝐵 + (𝐸𝑖)) → (𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
302301fveq2d 6233 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝐵 + (𝐸𝑖)) → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
303 eqid 2651 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
304 fvex 6239 . . . . . . . . . . . . . . . . 17 (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
305302, 303, 304fvmpt 6321 . . . . . . . . . . . . . . . 16 ((𝐵 + (𝐸𝑖)) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
306300, 305syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
307 vdwapid1 15726 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
30810, 41, 42, 307syl3anc 1366 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
30943, 308sseldd 3637 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ (𝐹 “ {𝐺}))
310 fniniseg 6378 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn (1...𝑉) → (𝐴 ∈ (𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹𝐴) = 𝐺)))
311148, 310syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐴 ∈ (𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹𝐴) = 𝐺)))
312309, 311mpbid 222 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 ∈ (1...𝑉) ∧ (𝐹𝐴) = 𝐺))
313312simprd 478 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹𝐴) = 𝐺)
314312simpld 474 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ (1...𝑉))
315 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝐴 → (𝑥 − 1) = (𝐴 − 1))
316315oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝐴 → ((𝑥 − 1) + 𝑉) = ((𝐴 − 1) + 𝑉))
317316oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝐴 → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
318317oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝐴 → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))
319318fveq2d 6233 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝐴 → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
320319mpteq2dv 4778 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝐴 → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
321195mptex 6527 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) ∈ V
322320, 40, 321fvmpt 6321 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ (1...𝑉) → (𝐹𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
323314, 322syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
324313, 323eqtr3d 2687 . . . . . . . . . . . . . . . . 17 (𝜑𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
325324fveq1d 6231 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐺‘(𝐵 + (𝐸𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))))
326325adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐵 + (𝐸𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))))
327290fveq2d 6233 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃𝑖))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
328306, 326, 3273eqtr4rd 2696 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃𝑖))) = (𝐺‘(𝐵 + (𝐸𝑖))))
329328sneqd 4222 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → {(𝐻‘(𝑇 + (𝑃𝑖)))} = {(𝐺‘(𝐵 + (𝐸𝑖)))})
330329imaeq2d 5501 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) = (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
331224, 291, 3303sstr4d 3681 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
332331ex 449 . . . . . . . . . 10 (𝜑 → (𝑖 ∈ (1...𝑀) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
333260adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ)
33488adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
335333, 334, 98addassd 10100 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
336127oveq2d 6706 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
337335, 336eqtr4d 2688 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
33838adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
33912adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
340 eluzfz1 12386 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ (ℤ‘1) → 1 ∈ (1...𝑀))
34152, 340syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ∈ (1...𝑀))
342 ne0i 3954 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 ∈ (1...𝑀) → (1...𝑀) ≠ ∅)
343341, 342syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑀) ≠ ∅)
344 elfzuz3 12377 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 + (𝐸𝑖)) ∈ (1...𝑊) → 𝑊 ∈ (ℤ‘(𝐵 + (𝐸𝑖))))
345300, 344syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ‘(𝐵 + (𝐸𝑖))))
34616nnzd 11519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐵 ∈ ℤ)
347 uzid 11740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵 ∈ ℤ → 𝐵 ∈ (ℤ𝐵))
348346, 347syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ∈ (ℤ𝐵))
349348adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵 ∈ (ℤ𝐵))
35079nnnn0d 11389 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐸𝑖) ∈ ℕ0)
351 uzaddcl 11782 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ∈ (ℤ𝐵) ∧ (𝐸𝑖) ∈ ℕ0) → (𝐵 + (𝐸𝑖)) ∈ (ℤ𝐵))
352349, 350, 351syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ (ℤ𝐵))
353 uztrn 11742 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑊 ∈ (ℤ‘(𝐵 + (𝐸𝑖))) ∧ (𝐵 + (𝐸𝑖)) ∈ (ℤ𝐵)) → 𝑊 ∈ (ℤ𝐵))
354345, 352, 353syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ𝐵))
355 eluzle 11738 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑊 ∈ (ℤ𝐵) → 𝐵𝑊)
356354, 355syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵𝑊)
357356ralrimiva 2995 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑖 ∈ (1...𝑀)𝐵𝑊)
358 r19.2z 4093 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...𝑀) ≠ ∅ ∧ ∀𝑖 ∈ (1...𝑀)𝐵𝑊) → ∃𝑖 ∈ (1...𝑀)𝐵𝑊)
359343, 357, 358syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∃𝑖 ∈ (1...𝑀)𝐵𝑊)
360 idd 24 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (1...𝑀) → (𝐵𝑊𝐵𝑊))
361360rexlimiv 3056 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑖 ∈ (1...𝑀)𝐵𝑊𝐵𝑊)
362359, 361syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵𝑊)
36312nnzd 11519 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑊 ∈ ℤ)
364 fznn 12446 . . . . . . . . . . . . . . . . . . . . . 22 (𝑊 ∈ ℤ → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵𝑊)))
365363, 364syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵𝑊)))
36616, 362, 365mpbir2and 977 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ (1...𝑊))
367366adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ (1...𝑊))
368338, 339, 153, 367vdwlem3 15734 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
369337, 368eqeltrd 2730 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))))
370 oveq1 6697 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝐵 → (𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
371370fveq2d 6233 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
372 fvex 6239 . . . . . . . . . . . . . . . . . . . 20 (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
373371, 183, 372fvmpt 6321 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
374367, 373syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
375199fveq1d 6231 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐺𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵))
376337fveq2d 6233 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
377374, 375, 3763eqtr4rd 2696 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵))
378369, 377jca 553 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵)))
379 eleq1 2718 . . . . . . . . . . . . . . . . 17 (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉)))))
380 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝐻𝑧) = (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
381380eqeq1d 2653 . . . . . . . . . . . . . . . . 17 (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝐻𝑧) = (𝐺𝐵) ↔ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵)))
382379, 381anbi12d 747 . . . . . . . . . . . . . . . 16 (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵)) ↔ (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵))))
383378, 382syl5ibrcom 237 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
384383rexlimdva 3060 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
38516, 87nnaddcld 11105 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
386 vdwapval 15724 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℕ0 ∧ (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ (𝑊 · 𝐷) ∈ ℕ) → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
387140, 385, 65, 386syl3anc 1366 . . . . . . . . . . . . . 14 (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
388 fniniseg 6378 . . . . . . . . . . . . . . 15 (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑧 ∈ (𝐻 “ {(𝐺𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
389219, 388syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑧 ∈ (𝐻 “ {(𝐺𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
390384, 387, 3893imtr4d 283 . . . . . . . . . . . . 13 (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) → 𝑧 ∈ (𝐻 “ {(𝐺𝐵)})))
391390ssrdv 3642 . . . . . . . . . . . 12 (𝜑 → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ⊆ (𝐻 “ {(𝐺𝐵)}))
39218peano2nnd 11075 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀 + 1) ∈ ℕ)
393392, 51syl6eleq 2740 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 + 1) ∈ (ℤ‘1))
394 eluzfz2 12387 . . . . . . . . . . . . . . . . . 18 ((𝑀 + 1) ∈ (ℤ‘1) → (𝑀 + 1) ∈ (1...(𝑀 + 1)))
395393, 394syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 + 1) ∈ (1...(𝑀 + 1)))
396 iftrue 4125 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑀 + 1) → if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) = 0)
397396oveq1d 6705 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑀 + 1) → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) = (0 + (𝑊 · 𝐷)))
398 ovex 6718 . . . . . . . . . . . . . . . . . 18 (0 + (𝑊 · 𝐷)) ∈ V
399397, 46, 398fvmpt 6321 . . . . . . . . . . . . . . . . 17 ((𝑀 + 1) ∈ (1...(𝑀 + 1)) → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
400395, 399syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
401101addid2d 10275 . . . . . . . . . . . . . . . 16 (𝜑 → (0 + (𝑊 · 𝐷)) = (𝑊 · 𝐷))
402400, 401eqtrd 2685 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃‘(𝑀 + 1)) = (𝑊 · 𝐷))
403402oveq2d 6706 . . . . . . . . . . . . . 14 (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝑇 + (𝑊 · 𝐷)))
404403, 282eqtrd 2685 . . . . . . . . . . . . 13 (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
405404, 402oveq12d 6708 . . . . . . . . . . . 12 (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)))
406 oveq1 6697 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝐵 → (𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
407406fveq2d 6233 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
408 fvex 6239 . . . . . . . . . . . . . . . . 17 (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
409407, 303, 408fvmpt 6321 . . . . . . . . . . . . . . . 16 (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
410366, 409syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
411324fveq1d 6231 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵))
412404fveq2d 6233 . . . . . . . . . . . . . . 15 (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
413410, 411, 4123eqtr4rd 2696 . . . . . . . . . . . . . 14 (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐺𝐵))
414413sneqd 4222 . . . . . . . . . . . . 13 (𝜑 → {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))} = {(𝐺𝐵)})
415414imaeq2d 5501 . . . . . . . . . . . 12 (𝜑 → (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}) = (𝐻 “ {(𝐺𝐵)}))
416391, 405, 4153sstr4d 3681 . . . . . . . . . . 11 (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
417 fveq2 6229 . . . . . . . . . . . . . 14 (𝑖 = (𝑀 + 1) → (𝑃𝑖) = (𝑃‘(𝑀 + 1)))
418417oveq2d 6706 . . . . . . . . . . . . 13 (𝑖 = (𝑀 + 1) → (𝑇 + (𝑃𝑖)) = (𝑇 + (𝑃‘(𝑀 + 1))))
419418, 417oveq12d 6708 . . . . . . . . . . . 12 (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) = ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))))
420418fveq2d 6233 . . . . . . . . . . . . . 14 (𝑖 = (𝑀 + 1) → (𝐻‘(𝑇 + (𝑃𝑖))) = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
421420sneqd 4222 . . . . . . . . . . . . 13 (𝑖 = (𝑀 + 1) → {(𝐻‘(𝑇 + (𝑃𝑖)))} = {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})
422421imaeq2d 5501 . . . . . . . . . . . 12 (𝑖 = (𝑀 + 1) → (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) = (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
423419, 422sseq12d 3667 . . . . . . . . . . 11 (𝑖 = (𝑀 + 1) → (((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) ↔ ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})))
424416, 423syl5ibrcom 237 . . . . . . . . . 10 (𝜑 → (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
425332, 424jaod 394 . . . . . . . . 9 (𝜑 → ((𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
42675, 425sylbid 230 . . . . . . . 8 (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
427426ralrimiv 2994 . . . . . . 7 (𝜑 → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
428427adantr 480 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
429227rexeqdv 3175 . . . . . . . . . . . 12 (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ ∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))))
430 rexun 3826 . . . . . . . . . . . . 13 (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))))
431328eqeq2d 2661 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))))
432431rexbidva 3078 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))))
433 ovex 6718 . . . . . . . . . . . . . . . 16 (𝑀 + 1) ∈ V
434420eqeq2d 2661 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑀 + 1) → (𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))))
435433, 434rexsn 4255 . . . . . . . . . . . . . . 15 (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
436413eqeq2d 2661 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) ↔ 𝑥 = (𝐺𝐵)))
437435, 436syl5bb 272 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐺𝐵)))
438432, 437orbi12d 746 . . . . . . . . . . . . 13 (𝜑 → ((∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))))
439430, 438syl5bb 272 . . . . . . . . . . . 12 (𝜑 → (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))))
440429, 439bitrd 268 . . . . . . . . . . 11 (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))))
441440adantr 480 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))))
442441abbidv 2770 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))} = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))})
443 eqid 2651 . . . . . . . . . 10 (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))
444443rnmpt 5403 . . . . . . . . 9 ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))) = {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))}
4452rnmpt 5403 . . . . . . . . . . 11 ran 𝐽 = {𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))}
446 df-sn 4211 . . . . . . . . . . 11 {(𝐺𝐵)} = {𝑥𝑥 = (𝐺𝐵)}
447445, 446uneq12i 3798 . . . . . . . . . 10 (ran 𝐽 ∪ {(𝐺𝐵)}) = ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))} ∪ {𝑥𝑥 = (𝐺𝐵)})
448 unab 3927 . . . . . . . . . 10 ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))} ∪ {𝑥𝑥 = (𝐺𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))}
449447, 448eqtri 2673 . . . . . . . . 9 (ran 𝐽 ∪ {(𝐺𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))}
450442, 444, 4493eqtr4g 2710 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))) = (ran 𝐽 ∪ {(𝐺𝐵)}))
451450fveq2d 6233 . . . . . . 7 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (#‘(ran 𝐽 ∪ {(𝐺𝐵)})))
452 fzfi 12811 . . . . . . . . . 10 (1...𝑀) ∈ Fin
453 dffn4 6159 . . . . . . . . . . 11 (𝐽 Fn (1...𝑀) ↔ 𝐽:(1...𝑀)–onto→ran 𝐽)
4543, 453mpbi 220 . . . . . . . . . 10 𝐽:(1...𝑀)–onto→ran 𝐽
455 fofi 8293 . . . . . . . . . 10 (((1...𝑀) ∈ Fin ∧ 𝐽:(1...𝑀)–onto→ran 𝐽) → ran 𝐽 ∈ Fin)
456452, 454, 455mp2an 708 . . . . . . . . 9 ran 𝐽 ∈ Fin
457456a1i 11 . . . . . . . 8 (𝜑 → ran 𝐽 ∈ Fin)
458 fvex 6239 . . . . . . . . 9 (𝐺𝐵) ∈ V
459 hashunsng 13219 . . . . . . . . 9 ((𝐺𝐵) ∈ V → ((ran 𝐽 ∈ Fin ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (#‘(ran 𝐽 ∪ {(𝐺𝐵)})) = ((#‘ran 𝐽) + 1)))
460458, 459ax-mp 5 . . . . . . . 8 ((ran 𝐽 ∈ Fin ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (#‘(ran 𝐽 ∪ {(𝐺𝐵)})) = ((#‘ran 𝐽) + 1))
461457, 460sylan 487 . . . . . . 7 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (#‘(ran 𝐽 ∪ {(𝐺𝐵)})) = ((#‘ran 𝐽) + 1))
46244adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (#‘ran 𝐽) = 𝑀)
463462oveq1d 6705 . . . . . . 7 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ((#‘ran 𝐽) + 1) = (𝑀 + 1))
464451, 461, 4633eqtrd 2689 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1))
465428, 464jca 553 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1)))
466 oveq1 6697 . . . . . . . . . 10 (𝑎 = 𝑇 → (𝑎 + (𝑑𝑖)) = (𝑇 + (𝑑𝑖)))
467466oveq1d 6705 . . . . . . . . 9 (𝑎 = 𝑇 → ((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) = ((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)))
468466fveq2d 6233 . . . . . . . . . . 11 (𝑎 = 𝑇 → (𝐻‘(𝑎 + (𝑑𝑖))) = (𝐻‘(𝑇 + (𝑑𝑖))))
469468sneqd 4222 . . . . . . . . . 10 (𝑎 = 𝑇 → {(𝐻‘(𝑎 + (𝑑𝑖)))} = {(𝐻‘(𝑇 + (𝑑𝑖)))})
470469imaeq2d 5501 . . . . . . . . 9 (𝑎 = 𝑇 → (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) = (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}))
471467, 470sseq12d 3667 . . . . . . . 8 (𝑎 = 𝑇 → (((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ↔ ((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))})))
472471ralbidv 3015 . . . . . . 7 (𝑎 = 𝑇 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))})))
473468mpteq2dv 4778 . . . . . . . . . 10 (𝑎 = 𝑇 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))))
474473rneqd 5385 . . . . . . . . 9 (𝑎 = 𝑇 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))))
475474fveq2d 6233 . . . . . . . 8 (𝑎 = 𝑇 → (#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))))
476475eqeq1d 2653 . . . . . . 7 (𝑎 = 𝑇 → ((#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1) ↔ (#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))) = (𝑀 + 1)))
477472, 476anbi12d 747 . . . . . 6 (𝑎 = 𝑇 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))) = (𝑀 + 1))))
478 fveq1 6228 . . . . . . . . . . 11 (𝑑 = 𝑃 → (𝑑𝑖) = (𝑃𝑖))
479478oveq2d 6706 . . . . . . . . . 10 (𝑑 = 𝑃 → (𝑇 + (𝑑𝑖)) = (𝑇 + (𝑃𝑖)))
480479, 478oveq12d 6708 . . . . . . . . 9 (𝑑 = 𝑃 → ((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) = ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)))
481479fveq2d 6233 . . . . . . . . . . 11 (𝑑 = 𝑃 → (𝐻‘(𝑇 + (𝑑𝑖))) = (𝐻‘(𝑇 + (𝑃𝑖))))
482481sneqd 4222 . . . . . . . . . 10 (𝑑 = 𝑃 → {(𝐻‘(𝑇 + (𝑑𝑖)))} = {(𝐻‘(𝑇 + (𝑃𝑖)))})
483482imaeq2d 5501 . . . . . . . . 9 (𝑑 = 𝑃 → (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) = (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
484480, 483sseq12d 3667 . . . . . . . 8 (𝑑 = 𝑃 → (((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ↔ ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
485484ralbidv 3015 . . . . . . 7 (𝑑 = 𝑃 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
486481mpteq2dv 4778 . . . . . . . . . 10 (𝑑 = 𝑃 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))))
487486rneqd 5385 . . . . . . . . 9 (𝑑 = 𝑃 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))))
488487fveq2d 6233 . . . . . . . 8 (𝑑 = 𝑃 → (#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))) = (#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))))
489488eqeq1d 2653 . . . . . . 7 (𝑑 = 𝑃 → ((#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))) = (𝑀 + 1) ↔ (#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1)))
490485, 489anbi12d 747 . . . . . 6 (𝑑 = 𝑃 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1))))
491477, 490rspc2ev 3355 . . . . 5 ((𝑇 ∈ ℕ ∧ 𝑃 ∈ (ℕ ↑𝑚 (1...(𝑀 + 1))) ∧ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1))) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑𝑚 (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1)))
49248, 73, 465, 491syl3anc 1366 . . . 4 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑𝑚 (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1)))
493 ovex 6718 . . . . 5 (1...(𝑊 · (2 · 𝑉))) ∈ V
49410adantr 480 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ)
495494nnnn0d 11389 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ0)
49639adantr 480 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
49718adantr 480 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑀 ∈ ℕ)
498497peano2nnd 11075 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (𝑀 + 1) ∈ ℕ)
499 eqid 2651 . . . . 5 (1...(𝑀 + 1)) = (1...(𝑀 + 1))
500493, 495, 496, 498, 499vdwpc 15731 . . . 4 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑𝑚 (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1))))
501492, 500mpbird 247 . . 3 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻)
502501orcd 406 . 2 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))
50337, 502pm2.61dan 849 1 (𝜑 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1523  wcel 2030  {cab 2637  wne 2823  wral 2941  wrex 2942  Vcvv 3231  cun 3605  wss 3607  c0 3948  ifcif 4119  {csn 4210  cop 4216   class class class wbr 4685  cmpt 4762  ccnv 5142  dom cdm 5143  ran crn 5144  cima 5146   Fn wfn 5921  wf 5922  ontowfo 5924  cfv 5926  (class class class)co 6690  𝑚 cmap 7899  Fincfn 7997  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112  cle 10113  cmin 10304  cn 11058  2c2 11108  0cn0 11330  cz 11415  cuz 11725  ...cfz 12364  #chash 13157  APcvdwa 15716   MonoAP cvdwm 15717   PolyAP cvdwp 15718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-hash 13158  df-vdwap 15719  df-vdwmc 15720  df-vdwpc 15721
This theorem is referenced by:  vdwlem7  15738
  Copyright terms: Public domain W3C validator