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

Theorem vdwlem6 16415
Description: Lemma for vdw 16423. (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 6681 . . . . . . 7 (𝐺‘(𝐵 + (𝐸𝑖))) ∈ V
2 vdwlem6.j . . . . . . 7 𝐽 = (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝐵 + (𝐸𝑖))))
31, 2fnmpti 6474 . . . . . 6 𝐽 Fn (1...𝑀)
4 fvelrnb 6724 . . . . . 6 (𝐽 Fn (1...𝑀) → ((𝐺𝐵) ∈ ran 𝐽 ↔ ∃𝑚 ∈ (1...𝑀)(𝐽𝑚) = (𝐺𝐵)))
53, 4ax-mp 5 . . . . 5 ((𝐺𝐵) ∈ ran 𝐽 ↔ ∃𝑚 ∈ (1...𝑀)(𝐽𝑚) = (𝐺𝐵))
6 vdwlem4.r . . . . . . . 8 (𝜑𝑅 ∈ Fin)
76adantr 484 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝑅 ∈ Fin)
8 vdwlem7.k . . . . . . . . 9 (𝜑𝐾 ∈ (ℤ‘2))
9 eluz2nn 12359 . . . . . . . . 9 (𝐾 ∈ (ℤ‘2) → 𝐾 ∈ ℕ)
108, 9syl 17 . . . . . . . 8 (𝜑𝐾 ∈ ℕ)
1110adantr 484 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝐾 ∈ ℕ)
12 vdwlem3.w . . . . . . . 8 (𝜑𝑊 ∈ ℕ)
1312adantr 484 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝑊 ∈ ℕ)
14 vdwlem7.g . . . . . . . 8 (𝜑𝐺:(1...𝑊)⟶𝑅)
1514adantr 484 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝐺:(1...𝑊)⟶𝑅)
16 vdwlem6.b . . . . . . . 8 (𝜑𝐵 ∈ ℕ)
1716adantr 484 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝐵 ∈ ℕ)
18 vdwlem7.m . . . . . . . 8 (𝜑𝑀 ∈ ℕ)
1918adantr 484 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝑀 ∈ ℕ)
20 vdwlem6.e . . . . . . . 8 (𝜑𝐸:(1...𝑀)⟶ℕ)
2120adantr 484 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝐸:(1...𝑀)⟶ℕ)
22 vdwlem6.s . . . . . . . 8 (𝜑 → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
2322adantr 484 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
24 simprl 771 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝑚 ∈ (1...𝑀))
25 simprr 773 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐽𝑚) = (𝐺𝐵))
26 fveq2 6668 . . . . . . . . . . . 12 (𝑖 = 𝑚 → (𝐸𝑖) = (𝐸𝑚))
2726oveq2d 7180 . . . . . . . . . . 11 (𝑖 = 𝑚 → (𝐵 + (𝐸𝑖)) = (𝐵 + (𝐸𝑚)))
2827fveq2d 6672 . . . . . . . . . 10 (𝑖 = 𝑚 → (𝐺‘(𝐵 + (𝐸𝑖))) = (𝐺‘(𝐵 + (𝐸𝑚))))
29 fvex 6681 . . . . . . . . . 10 (𝐺‘(𝐵 + (𝐸𝑚))) ∈ V
3028, 2, 29fvmpt 6769 . . . . . . . . 9 (𝑚 ∈ (1...𝑀) → (𝐽𝑚) = (𝐺‘(𝐵 + (𝐸𝑚))))
3124, 30syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐽𝑚) = (𝐺‘(𝐵 + (𝐸𝑚))))
3225, 31eqtr3d 2775 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐺𝐵) = (𝐺‘(𝐵 + (𝐸𝑚))))
337, 11, 13, 15, 17, 19, 21, 23, 24, 32vdwlem1 16410 . . . . . 6 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐾 + 1) MonoAP 𝐺)
3433rexlimdvaa 3194 . . . . 5 (𝜑 → (∃𝑚 ∈ (1...𝑀)(𝐽𝑚) = (𝐺𝐵) → (𝐾 + 1) MonoAP 𝐺))
355, 34syl5bi 245 . . . 4 (𝜑 → ((𝐺𝐵) ∈ ran 𝐽 → (𝐾 + 1) MonoAP 𝐺))
3635imp 410 . . 3 ((𝜑 ∧ (𝐺𝐵) ∈ ran 𝐽) → (𝐾 + 1) MonoAP 𝐺)
3736olcd 873 . 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 16414 . . . . . 6 (𝜑𝑇 ∈ ℕ)
4847adantr 484 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑇 ∈ ℕ)
49 0nn0 11984 . . . . . . . . . 10 0 ∈ ℕ0
5049a1i 11 . . . . . . . . 9 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 = (𝑀 + 1)) → 0 ∈ ℕ0)
51 nnuz 12356 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
5218, 51eleqtrdi 2843 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ (ℤ‘1))
5352adantr 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑀 ∈ (ℤ‘1))
54 elfzp1 13041 . . . . . . . . . . . . . . 15 (𝑀 ∈ (ℤ‘1) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1))))
5553, 54syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1))))
5655biimpa 480 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1)))
5756ord 863 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 ∈ (1...𝑀) → 𝑗 = (𝑀 + 1)))
5857con1d 147 . . . . . . . . . . 11 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 = (𝑀 + 1) → 𝑗 ∈ (1...𝑀)))
5958imp 410 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → 𝑗 ∈ (1...𝑀))
6020ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → 𝐸:(1...𝑀)⟶ℕ)
6160ffvelrnda 6855 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸𝑗) ∈ ℕ)
6261nnnn0d 12029 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸𝑗) ∈ ℕ0)
6359, 62syldan 594 . . . . . . . . 9 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → (𝐸𝑗) ∈ ℕ0)
6450, 63ifclda 4446 . . . . . . . 8 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) ∈ ℕ0)
6512, 42nnmulcld 11762 . . . . . . . . 9 (𝜑 → (𝑊 · 𝐷) ∈ ℕ)
6665ad2antrr 726 . . . . . . . 8 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑊 · 𝐷) ∈ ℕ)
67 nn0nnaddcl 12000 . . . . . . . 8 ((if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) ∈ ℕ0 ∧ (𝑊 · 𝐷) ∈ ℕ) → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
6864, 66, 67syl2anc 587 . . . . . . 7 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
6968, 46fmptd 6882 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑃:(1...(𝑀 + 1))⟶ℕ)
70 nnex 11715 . . . . . . 7 ℕ ∈ V
71 ovex 7197 . . . . . . 7 (1...(𝑀 + 1)) ∈ V
7270, 71elmap 8474 . . . . . 6 (𝑃 ∈ (ℕ ↑m (1...(𝑀 + 1))) ↔ 𝑃:(1...(𝑀 + 1))⟶ℕ)
7369, 72sylibr 237 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑃 ∈ (ℕ ↑m (1...(𝑀 + 1))))
74 elfzp1 13041 . . . . . . . . . 10 (𝑀 ∈ (ℤ‘1) → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1))))
7552, 74syl 17 . . . . . . . . 9 (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1))))
7616adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℕ)
7776nncnd 11725 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℂ)
7877adantr 484 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ)
7920ffvelrnda 6855 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐸𝑖) ∈ ℕ)
8079nncnd 11725 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐸𝑖) ∈ ℂ)
8180adantr 484 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐸𝑖) ∈ ℂ)
8278, 81addcld 10731 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝐸𝑖)) ∈ ℂ)
83 nnm1nn0 12010 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ ℕ → (𝐴 − 1) ∈ ℕ0)
8441, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐴 − 1) ∈ ℕ0)
85 nn0nnaddcl 12000 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 − 1) ∈ ℕ0𝑉 ∈ ℕ) → ((𝐴 − 1) + 𝑉) ∈ ℕ)
8684, 38, 85syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℕ)
8712, 86nnmulcld 11762 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
8887nncnd 11725 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
8988ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
90 elfznn0 13084 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ (0...(𝐾 − 1)) → 𝑚 ∈ ℕ0)
9190adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℕ0)
9291nn0cnd 12031 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
9392adantlr 715 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
9493, 81mulcld 10732 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝐸𝑖)) ∈ ℂ)
9565nnnn0d 12029 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑊 · 𝐷) ∈ ℕ0)
9695adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℕ0)
9791, 96nn0mulcld 12034 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℕ0)
9897nn0cnd 12031 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
9998adantlr 715 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
10082, 89, 94, 99add4d 10939 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸𝑖)) + (𝑚 · (𝑊 · 𝐷)))) = (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
10165nncnd 11725 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑊 · 𝐷) ∈ ℂ)
102101ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℂ)
10393, 81, 102adddid 10736 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))) = ((𝑚 · (𝐸𝑖)) + (𝑚 · (𝑊 · 𝐷))))
104103oveq2d 7180 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸𝑖)) + (𝑚 · (𝑊 · 𝐷)))))
10512nncnd 11725 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑊 ∈ ℂ)
106105adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℂ)
10786nncnd 11725 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℂ)
108107adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 − 1) + 𝑉) ∈ ℂ)
10942nncnd 11725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐷 ∈ ℂ)
110109adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐷 ∈ ℂ)
11192, 110mulcld 10732 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · 𝐷) ∈ ℂ)
112106, 108, 111adddid 10736 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
11341nncnd 11725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐴 ∈ ℂ)
114113adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐴 ∈ ℂ)
115 1cnd 10707 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 1 ∈ ℂ)
116114, 111, 115addsubd 11089 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) − 1) = ((𝐴 − 1) + (𝑚 · 𝐷)))
117116oveq1d 7179 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉))
11884nn0cnd 12031 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 − 1) ∈ ℂ)
119118adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 − 1) ∈ ℂ)
12038nncnd 11725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑉 ∈ ℂ)
121120adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℂ)
122119, 111, 121add32d 10938 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
123117, 122eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
124123oveq2d 7180 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))))
12592, 106, 110mul12d 10920 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) = (𝑊 · (𝑚 · 𝐷)))
126125oveq2d 7180 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
127112, 124, 1263eqtr4d 2783 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
128127adantlr 715 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
129128oveq2d 7180 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
130100, 104, 1293eqtr4d 2783 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
13138ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
13212ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
13343adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴(AP‘𝐾)𝐷) ⊆ (𝐹 “ {𝐺}))
134 eqid 2738 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))
135 oveq1 7171 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑚 → (𝑛 · 𝐷) = (𝑚 · 𝐷))
136135oveq2d 7180 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → (𝐴 + (𝑛 · 𝐷)) = (𝐴 + (𝑚 · 𝐷)))
137136rspceeqv 3539 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 ∈ (0...(𝐾 − 1)) ∧ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
138134, 137mpan2 691 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
13910nnnn0d 12029 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐾 ∈ ℕ0)
140 vdwapval 16402 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
141139, 41, 42, 140syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
142141biimpar 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
143138, 142sylan2 596 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
144133, 143sseldd 3876 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺}))
14538, 12, 6, 39, 40vdwlem4 16413 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹:(1...𝑉)⟶(𝑅m (1...𝑊)))
146145ffnd 6499 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹 Fn (1...𝑉))
147 fniniseg 6831 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 Fn (1...𝑉) → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
148146, 147syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
149148biimpa 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺})) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
150144, 149syldan 594 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
151150simpld 498 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
152151adantlr 715 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
15322r19.21bi 3120 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
154153adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
155 eqid 2738 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))
156 oveq1 7171 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → (𝑛 · (𝐸𝑖)) = (𝑚 · (𝐸𝑖)))
157156oveq2d 7180 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑚 → ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))))
158157rspceeqv 3539 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚 ∈ (0...(𝐾 − 1)) ∧ ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖))))
159155, 158mpan2 691 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖))))
16010adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ)
161160nnnn0d 12029 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ0)
16276, 79nnaddcld 11761 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ ℕ)
163 vdwapval 16402 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐾 ∈ ℕ0 ∧ (𝐵 + (𝐸𝑖)) ∈ ℕ ∧ (𝐸𝑖) ∈ ℕ) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖)))))
164161, 162, 79, 163syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖)))))
165164biimpar 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖 ∈ (1...𝑀)) ∧ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖)))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
166159, 165sylan2 596 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
167154, 166sseldd 3876 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
16814ffnd 6499 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐺 Fn (1...𝑊))
169168adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐺 Fn (1...𝑊))
170 fniniseg 6831 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 Fn (1...𝑊) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖))))))
171169, 170syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖))))))
172171biimpa 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))})) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
173167, 172syldan 594 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
174173simpld 498 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊))
175131, 132, 152, 174vdwlem3 16412 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
176130, 175eqeltrd 2833 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))))
177 fvoveq1 7187 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
178 eqid 2738 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
179 fvex 6681 . . . . . . . . . . . . . . . . . . . 20 (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
180177, 178, 179fvmpt 6769 . . . . . . . . . . . . . . . . . . 19 (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
181174, 180syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
182173simprd 499 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖))))
183150simprd 499 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)
184 oveq1 7171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑥 − 1) = ((𝐴 + (𝑚 · 𝐷)) − 1))
185184oveq1d 7179 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → ((𝑥 − 1) + 𝑉) = (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))
186185oveq2d 7180 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))
187186oveq2d 7180 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
188187fveq2d 6672 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
189188mpteq2dv 5123 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
190 ovex 7197 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1...𝑊) ∈ V
191190mptex 6990 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) ∈ V
192189, 40, 191fvmpt 6769 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
193151, 192syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
194183, 193eqtr3d 2775 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
195194adantlr 715 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
196195fveq1d 6670 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))))
197182, 196eqtr3d 2775 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘(𝐵 + (𝐸𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))))
198130fveq2d 6672 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
199181, 197, 1983eqtr4rd 2784 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖))))
200176, 199jca 515 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
201 eleq1 2820 . . . . . . . . . . . . . . . . 17 (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉)))))
202 fveqeq2 6677 . . . . . . . . . . . . . . . . 17 (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → ((𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))) ↔ (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
203201, 202anbi12d 634 . . . . . . . . . . . . . . . 16 (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → ((𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖)))) ↔ ((((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖))))))
204200, 203syl5ibrcom 250 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
205204rexlimdva 3193 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
20687adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
207162, 206nnaddcld 11761 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
20865adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℕ)
20979, 208nnaddcld 11761 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + (𝑊 · 𝐷)) ∈ ℕ)
210 vdwapval 16402 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℕ0 ∧ ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ ((𝐸𝑖) + (𝑊 · 𝐷)) ∈ ℕ) → (𝑥 ∈ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))))
211161, 207, 209, 210syl3anc 1372 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))))
21239ffnd 6499 . . . . . . . . . . . . . . . 16 (𝜑𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
213212adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
214 fniniseg 6831 . . . . . . . . . . . . . . 15 (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑥 ∈ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
215213, 214syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
216205, 211, 2153imtr4d 297 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) → 𝑥 ∈ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))})))
217216ssrdv 3881 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) ⊆ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
218 ssun1 4060 . . . . . . . . . . . . . . . . . . 19 (1...𝑀) ⊆ ((1...𝑀) ∪ {(𝑀 + 1)})
219 fzsuc 13038 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (ℤ‘1) → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
22052, 219syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
221218, 220sseqtrrid 3928 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1...𝑀) ⊆ (1...(𝑀 + 1)))
222221sselda 3875 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...(𝑀 + 1)))
223 eqeq1 2742 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝑗 = (𝑀 + 1) ↔ 𝑖 = (𝑀 + 1)))
224 fveq2 6668 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝐸𝑗) = (𝐸𝑖))
225223, 224ifbieq2d 4437 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) = if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)))
226225oveq1d 7179 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) = (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)))
227 ovex 7197 . . . . . . . . . . . . . . . . . 18 (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)) ∈ V
228226, 46, 227fvmpt 6769 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...(𝑀 + 1)) → (𝑃𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)))
229222, 228syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑃𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)))
23018nnred 11724 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑀 ∈ ℝ)
231230ltp1d 11641 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑀 < (𝑀 + 1))
232 peano2re 10884 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
233230, 232syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑀 + 1) ∈ ℝ)
234230, 233ltnled 10858 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀))
235231, 234mpbid 235 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀)
236 breq1 5030 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = (𝑀 + 1) → (𝑖𝑀 ↔ (𝑀 + 1) ≤ 𝑀))
237236notbid 321 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = (𝑀 + 1) → (¬ 𝑖𝑀 ↔ ¬ (𝑀 + 1) ≤ 𝑀))
238235, 237syl5ibrcom 250 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑖 = (𝑀 + 1) → ¬ 𝑖𝑀))
239238con2d 136 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑖𝑀 → ¬ 𝑖 = (𝑀 + 1)))
240 elfzle2 12995 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑀) → 𝑖𝑀)
241239, 240impel 509 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → ¬ 𝑖 = (𝑀 + 1))
242 iffalse 4420 . . . . . . . . . . . . . . . . . 18 𝑖 = (𝑀 + 1) → if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) = (𝐸𝑖))
243242oveq1d 7179 . . . . . . . . . . . . . . . . 17 𝑖 = (𝑀 + 1) → (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)) = ((𝐸𝑖) + (𝑊 · 𝐷)))
244241, 243syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)) = ((𝐸𝑖) + (𝑊 · 𝐷)))
245229, 244eqtrd 2773 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑃𝑖) = ((𝐸𝑖) + (𝑊 · 𝐷)))
246245oveq2d 7180 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃𝑖)) = (𝑇 + ((𝐸𝑖) + (𝑊 · 𝐷))))
24747nncnd 11725 . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ ℂ)
248247adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑇 ∈ ℂ)
249101adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℂ)
250248, 80, 249add12d 10937 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑇 + ((𝐸𝑖) + (𝑊 · 𝐷))) = ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))))
25145oveq1i 7174 . . . . . . . . . . . . . . . . . 18 (𝑇 + (𝑊 · 𝐷)) = ((𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1))) + (𝑊 · 𝐷))
25216nncnd 11725 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℂ)
253120, 109subcld 11068 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑉𝐷) ∈ ℂ)
254113, 253addcld 10731 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 + (𝑉𝐷)) ∈ ℂ)
255 ax-1cn 10666 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℂ
256 subcl 10956 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 + (𝑉𝐷)) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 + (𝑉𝐷)) − 1) ∈ ℂ)
257254, 255, 256sylancl 589 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 + (𝑉𝐷)) − 1) ∈ ℂ)
258105, 257mulcld 10732 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) ∈ ℂ)
259252, 258, 101addassd 10734 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷))))
260105, 257, 109adddid 10736 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑊 · (((𝐴 + (𝑉𝐷)) − 1) + 𝐷)) = ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷)))
261113, 253, 109addassd 10734 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 + (𝑉𝐷)) + 𝐷) = (𝐴 + ((𝑉𝐷) + 𝐷)))
262120, 109npcand 11072 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑉𝐷) + 𝐷) = 𝑉)
263262oveq2d 7180 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐴 + ((𝑉𝐷) + 𝐷)) = (𝐴 + 𝑉))
264261, 263eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐴 + (𝑉𝐷)) + 𝐷) = (𝐴 + 𝑉))
265264oveq1d 7179 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝐴 + (𝑉𝐷)) + 𝐷) − 1) = ((𝐴 + 𝑉) − 1))
266 1cnd 10707 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ∈ ℂ)
267254, 109, 266addsubd 11089 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝐴 + (𝑉𝐷)) + 𝐷) − 1) = (((𝐴 + (𝑉𝐷)) − 1) + 𝐷))
268113, 120, 266addsubd 11089 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 + 𝑉) − 1) = ((𝐴 − 1) + 𝑉))
269265, 267, 2683eqtr3d 2781 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐴 + (𝑉𝐷)) − 1) + 𝐷) = ((𝐴 − 1) + 𝑉))
270269oveq2d 7180 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑊 · (((𝐴 + (𝑉𝐷)) − 1) + 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
271260, 270eqtr3d 2775 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
272271oveq2d 7180 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵 + ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
273259, 272eqtrd 2773 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
274251, 273syl5eq 2785 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑇 + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
275274oveq2d 7180 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
276275adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
27788adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
27880, 77, 277addassd 10734 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐸𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐸𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
27980, 77addcomd 10913 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + 𝐵) = (𝐵 + (𝐸𝑖)))
280279oveq1d 7179 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐸𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
281276, 278, 2803eqtr2d 2779 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
282246, 250, 2813eqtrd 2777 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃𝑖)) = ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
283282, 245oveq12d 7182 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))))
284 cnvimass 5917 . . . . . . . . . . . . . . . . . . 19 (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ⊆ dom 𝐺
285284, 14fssdm 6518 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ⊆ (1...𝑊))
286285adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ⊆ (1...𝑊))
287 vdwapid1 16404 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ ℕ ∧ (𝐵 + (𝐸𝑖)) ∈ ℕ ∧ (𝐸𝑖) ∈ ℕ) → (𝐵 + (𝐸𝑖)) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
288160, 162, 79, 287syl3anc 1372 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
289153, 288sseldd 3876 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
290286, 289sseldd 3876 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ (1...𝑊))
291 fvoveq1 7187 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝐵 + (𝐸𝑖)) → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
292 eqid 2738 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
293 fvex 6681 . . . . . . . . . . . . . . . . 17 (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
294291, 292, 293fvmpt 6769 . . . . . . . . . . . . . . . 16 ((𝐵 + (𝐸𝑖)) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
295290, 294syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
296 vdwapid1 16404 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
29710, 41, 42, 296syl3anc 1372 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
29843, 297sseldd 3876 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ (𝐹 “ {𝐺}))
299 fniniseg 6831 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn (1...𝑉) → (𝐴 ∈ (𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹𝐴) = 𝐺)))
300146, 299syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐴 ∈ (𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹𝐴) = 𝐺)))
301298, 300mpbid 235 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 ∈ (1...𝑉) ∧ (𝐹𝐴) = 𝐺))
302301simprd 499 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹𝐴) = 𝐺)
303301simpld 498 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ (1...𝑉))
304 oveq1 7171 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝐴 → (𝑥 − 1) = (𝐴 − 1))
305304oveq1d 7179 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝐴 → ((𝑥 − 1) + 𝑉) = ((𝐴 − 1) + 𝑉))
306305oveq2d 7180 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝐴 → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
307306oveq2d 7180 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝐴 → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))
308307fveq2d 6672 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝐴 → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
309308mpteq2dv 5123 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝐴 → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
310190mptex 6990 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) ∈ V
311309, 40, 310fvmpt 6769 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ (1...𝑉) → (𝐹𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
312303, 311syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
313302, 312eqtr3d 2775 . . . . . . . . . . . . . . . . 17 (𝜑𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
314313fveq1d 6670 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐺‘(𝐵 + (𝐸𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))))
315314adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐵 + (𝐸𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))))
316282fveq2d 6672 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃𝑖))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
317295, 315, 3163eqtr4rd 2784 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃𝑖))) = (𝐺‘(𝐵 + (𝐸𝑖))))
318317sneqd 4525 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → {(𝐻‘(𝑇 + (𝑃𝑖)))} = {(𝐺‘(𝐵 + (𝐸𝑖)))})
319318imaeq2d 5897 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) = (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
320217, 283, 3193sstr4d 3922 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
321320ex 416 . . . . . . . . . 10 (𝜑 → (𝑖 ∈ (1...𝑀) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
322252adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ)
32388adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
324322, 323, 98addassd 10734 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
325127oveq2d 7180 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
326324, 325eqtr4d 2776 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
32738adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
32812adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
329 eluzfz1 12998 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ (ℤ‘1) → 1 ∈ (1...𝑀))
33052, 329syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ∈ (1...𝑀))
331330ne0d 4222 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑀) ≠ ∅)
332 elfzuz3 12988 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 + (𝐸𝑖)) ∈ (1...𝑊) → 𝑊 ∈ (ℤ‘(𝐵 + (𝐸𝑖))))
333290, 332syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ‘(𝐵 + (𝐸𝑖))))
33416nnzd 12160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐵 ∈ ℤ)
335 uzid 12332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵 ∈ ℤ → 𝐵 ∈ (ℤ𝐵))
336334, 335syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ∈ (ℤ𝐵))
337336adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵 ∈ (ℤ𝐵))
33879nnnn0d 12029 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐸𝑖) ∈ ℕ0)
339 uzaddcl 12379 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ∈ (ℤ𝐵) ∧ (𝐸𝑖) ∈ ℕ0) → (𝐵 + (𝐸𝑖)) ∈ (ℤ𝐵))
340337, 338, 339syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ (ℤ𝐵))
341 uztrn 12335 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑊 ∈ (ℤ‘(𝐵 + (𝐸𝑖))) ∧ (𝐵 + (𝐸𝑖)) ∈ (ℤ𝐵)) → 𝑊 ∈ (ℤ𝐵))
342333, 340, 341syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ𝐵))
343 eluzle 12330 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑊 ∈ (ℤ𝐵) → 𝐵𝑊)
344342, 343syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵𝑊)
345344ralrimiva 3096 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑖 ∈ (1...𝑀)𝐵𝑊)
346 r19.2z 4378 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...𝑀) ≠ ∅ ∧ ∀𝑖 ∈ (1...𝑀)𝐵𝑊) → ∃𝑖 ∈ (1...𝑀)𝐵𝑊)
347331, 345, 346syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∃𝑖 ∈ (1...𝑀)𝐵𝑊)
348 idd 24 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (1...𝑀) → (𝐵𝑊𝐵𝑊))
349348rexlimiv 3189 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑖 ∈ (1...𝑀)𝐵𝑊𝐵𝑊)
350347, 349syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵𝑊)
35112nnzd 12160 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑊 ∈ ℤ)
352 fznn 13059 . . . . . . . . . . . . . . . . . . . . . 22 (𝑊 ∈ ℤ → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵𝑊)))
353351, 352syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵𝑊)))
35416, 350, 353mpbir2and 713 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ (1...𝑊))
355354adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ (1...𝑊))
356327, 328, 151, 355vdwlem3 16412 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
357326, 356eqeltrd 2833 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))))
358 fvoveq1 7187 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
359 fvex 6681 . . . . . . . . . . . . . . . . . . . 20 (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
360358, 178, 359fvmpt 6769 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
361355, 360syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
362194fveq1d 6670 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐺𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵))
363326fveq2d 6672 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
364361, 362, 3633eqtr4rd 2784 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵))
365357, 364jca 515 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵)))
366 eleq1 2820 . . . . . . . . . . . . . . . . 17 (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉)))))
367 fveqeq2 6677 . . . . . . . . . . . . . . . . 17 (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝐻𝑧) = (𝐺𝐵) ↔ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵)))
368366, 367anbi12d 634 . . . . . . . . . . . . . . . 16 (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵)) ↔ (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵))))
369365, 368syl5ibrcom 250 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
370369rexlimdva 3193 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
37116, 87nnaddcld 11761 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
372 vdwapval 16402 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℕ0 ∧ (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ (𝑊 · 𝐷) ∈ ℕ) → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
373139, 371, 65, 372syl3anc 1372 . . . . . . . . . . . . . 14 (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
374 fniniseg 6831 . . . . . . . . . . . . . . 15 (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑧 ∈ (𝐻 “ {(𝐺𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
375212, 374syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑧 ∈ (𝐻 “ {(𝐺𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
376370, 373, 3753imtr4d 297 . . . . . . . . . . . . 13 (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) → 𝑧 ∈ (𝐻 “ {(𝐺𝐵)})))
377376ssrdv 3881 . . . . . . . . . . . 12 (𝜑 → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ⊆ (𝐻 “ {(𝐺𝐵)}))
37818peano2nnd 11726 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 + 1) ∈ ℕ)
379378, 51eleqtrdi 2843 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 + 1) ∈ (ℤ‘1))
380 eluzfz2 12999 . . . . . . . . . . . . . . . . 17 ((𝑀 + 1) ∈ (ℤ‘1) → (𝑀 + 1) ∈ (1...(𝑀 + 1)))
381 iftrue 4417 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑀 + 1) → if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) = 0)
382381oveq1d 7179 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑀 + 1) → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) = (0 + (𝑊 · 𝐷)))
383 ovex 7197 . . . . . . . . . . . . . . . . . 18 (0 + (𝑊 · 𝐷)) ∈ V
384382, 46, 383fvmpt 6769 . . . . . . . . . . . . . . . . 17 ((𝑀 + 1) ∈ (1...(𝑀 + 1)) → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
385379, 380, 3843syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
386101addid2d 10912 . . . . . . . . . . . . . . . 16 (𝜑 → (0 + (𝑊 · 𝐷)) = (𝑊 · 𝐷))
387385, 386eqtrd 2773 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃‘(𝑀 + 1)) = (𝑊 · 𝐷))
388387oveq2d 7180 . . . . . . . . . . . . . 14 (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝑇 + (𝑊 · 𝐷)))
389388, 274eqtrd 2773 . . . . . . . . . . . . 13 (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
390389, 387oveq12d 7182 . . . . . . . . . . . 12 (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)))
391 fvoveq1 7187 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
392 fvex 6681 . . . . . . . . . . . . . . . . 17 (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
393391, 292, 392fvmpt 6769 . . . . . . . . . . . . . . . 16 (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
394354, 393syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
395313fveq1d 6670 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵))
396389fveq2d 6672 . . . . . . . . . . . . . . 15 (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
397394, 395, 3963eqtr4rd 2784 . . . . . . . . . . . . . 14 (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐺𝐵))
398397sneqd 4525 . . . . . . . . . . . . 13 (𝜑 → {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))} = {(𝐺𝐵)})
399398imaeq2d 5897 . . . . . . . . . . . 12 (𝜑 → (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}) = (𝐻 “ {(𝐺𝐵)}))
400377, 390, 3993sstr4d 3922 . . . . . . . . . . 11 (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
401 fveq2 6668 . . . . . . . . . . . . . 14 (𝑖 = (𝑀 + 1) → (𝑃𝑖) = (𝑃‘(𝑀 + 1)))
402401oveq2d 7180 . . . . . . . . . . . . 13 (𝑖 = (𝑀 + 1) → (𝑇 + (𝑃𝑖)) = (𝑇 + (𝑃‘(𝑀 + 1))))
403402, 401oveq12d 7182 . . . . . . . . . . . 12 (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) = ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))))
404402fveq2d 6672 . . . . . . . . . . . . . 14 (𝑖 = (𝑀 + 1) → (𝐻‘(𝑇 + (𝑃𝑖))) = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
405404sneqd 4525 . . . . . . . . . . . . 13 (𝑖 = (𝑀 + 1) → {(𝐻‘(𝑇 + (𝑃𝑖)))} = {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})
406405imaeq2d 5897 . . . . . . . . . . . 12 (𝑖 = (𝑀 + 1) → (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) = (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
407403, 406sseq12d 3908 . . . . . . . . . . 11 (𝑖 = (𝑀 + 1) → (((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) ↔ ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})))
408400, 407syl5ibrcom 250 . . . . . . . . . 10 (𝜑 → (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
409321, 408jaod 858 . . . . . . . . 9 (𝜑 → ((𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
41075, 409sylbid 243 . . . . . . . 8 (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
411410ralrimiv 3095 . . . . . . 7 (𝜑 → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
412411adantr 484 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
413220rexeqdv 3316 . . . . . . . . . . . 12 (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ ∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))))
414 rexun 4078 . . . . . . . . . . . . 13 (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))))
415317eqeq2d 2749 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))))
416415rexbidva 3205 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))))
417 ovex 7197 . . . . . . . . . . . . . . . 16 (𝑀 + 1) ∈ V
418404eqeq2d 2749 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑀 + 1) → (𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))))
419417, 418rexsn 4570 . . . . . . . . . . . . . . 15 (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
420397eqeq2d 2749 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) ↔ 𝑥 = (𝐺𝐵)))
421419, 420syl5bb 286 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐺𝐵)))
422416, 421orbi12d 918 . . . . . . . . . . . . 13 (𝜑 → ((∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))))
423414, 422syl5bb 286 . . . . . . . . . . . 12 (𝜑 → (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))))
424413, 423bitrd 282 . . . . . . . . . . 11 (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))))
425424adantr 484 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))))
426425abbidv 2802 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))} = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))})
427 eqid 2738 . . . . . . . . . 10 (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))
428427rnmpt 5792 . . . . . . . . 9 ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))) = {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))}
4292rnmpt 5792 . . . . . . . . . . 11 ran 𝐽 = {𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))}
430 df-sn 4514 . . . . . . . . . . 11 {(𝐺𝐵)} = {𝑥𝑥 = (𝐺𝐵)}
431429, 430uneq12i 4049 . . . . . . . . . 10 (ran 𝐽 ∪ {(𝐺𝐵)}) = ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))} ∪ {𝑥𝑥 = (𝐺𝐵)})
432 unab 4186 . . . . . . . . . 10 ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))} ∪ {𝑥𝑥 = (𝐺𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))}
433431, 432eqtri 2761 . . . . . . . . 9 (ran 𝐽 ∪ {(𝐺𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))}
434426, 428, 4333eqtr4g 2798 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))) = (ran 𝐽 ∪ {(𝐺𝐵)}))
435434fveq2d 6672 . . . . . . 7 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (♯‘(ran 𝐽 ∪ {(𝐺𝐵)})))
436 fzfi 13424 . . . . . . . . . 10 (1...𝑀) ∈ Fin
437 dffn4 6592 . . . . . . . . . . 11 (𝐽 Fn (1...𝑀) ↔ 𝐽:(1...𝑀)–onto→ran 𝐽)
4383, 437mpbi 233 . . . . . . . . . 10 𝐽:(1...𝑀)–onto→ran 𝐽
439 fofi 8876 . . . . . . . . . 10 (((1...𝑀) ∈ Fin ∧ 𝐽:(1...𝑀)–onto→ran 𝐽) → ran 𝐽 ∈ Fin)
440436, 438, 439mp2an 692 . . . . . . . . 9 ran 𝐽 ∈ Fin
441440a1i 11 . . . . . . . 8 (𝜑 → ran 𝐽 ∈ Fin)
442 fvex 6681 . . . . . . . . 9 (𝐺𝐵) ∈ V
443 hashunsng 13838 . . . . . . . . 9 ((𝐺𝐵) ∈ V → ((ran 𝐽 ∈ Fin ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺𝐵)})) = ((♯‘ran 𝐽) + 1)))
444442, 443ax-mp 5 . . . . . . . 8 ((ran 𝐽 ∈ Fin ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺𝐵)})) = ((♯‘ran 𝐽) + 1))
445441, 444sylan 583 . . . . . . 7 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺𝐵)})) = ((♯‘ran 𝐽) + 1))
44644adantr 484 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘ran 𝐽) = 𝑀)
447446oveq1d 7179 . . . . . . 7 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ((♯‘ran 𝐽) + 1) = (𝑀 + 1))
448435, 445, 4473eqtrd 2777 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1))
449412, 448jca 515 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1)))
450 oveq1 7171 . . . . . . . . . 10 (𝑎 = 𝑇 → (𝑎 + (𝑑𝑖)) = (𝑇 + (𝑑𝑖)))
451450oveq1d 7179 . . . . . . . . 9 (𝑎 = 𝑇 → ((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) = ((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)))
452 fvoveq1 7187 . . . . . . . . . . 11 (𝑎 = 𝑇 → (𝐻‘(𝑎 + (𝑑𝑖))) = (𝐻‘(𝑇 + (𝑑𝑖))))
453452sneqd 4525 . . . . . . . . . 10 (𝑎 = 𝑇 → {(𝐻‘(𝑎 + (𝑑𝑖)))} = {(𝐻‘(𝑇 + (𝑑𝑖)))})
454453imaeq2d 5897 . . . . . . . . 9 (𝑎 = 𝑇 → (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) = (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}))
455451, 454sseq12d 3908 . . . . . . . 8 (𝑎 = 𝑇 → (((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ↔ ((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))})))
456455ralbidv 3109 . . . . . . 7 (𝑎 = 𝑇 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))})))
457452mpteq2dv 5123 . . . . . . . . 9 (𝑎 = 𝑇 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))))
458457rneqd 5775 . . . . . . . 8 (𝑎 = 𝑇 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))))
459458fveqeq2d 6676 . . . . . . 7 (𝑎 = 𝑇 → ((♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1) ↔ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))) = (𝑀 + 1)))
460456, 459anbi12d 634 . . . . . 6 (𝑎 = 𝑇 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))) = (𝑀 + 1))))
461 fveq1 6667 . . . . . . . . . . 11 (𝑑 = 𝑃 → (𝑑𝑖) = (𝑃𝑖))
462461oveq2d 7180 . . . . . . . . . 10 (𝑑 = 𝑃 → (𝑇 + (𝑑𝑖)) = (𝑇 + (𝑃𝑖)))
463462, 461oveq12d 7182 . . . . . . . . 9 (𝑑 = 𝑃 → ((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) = ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)))
464462fveq2d 6672 . . . . . . . . . . 11 (𝑑 = 𝑃 → (𝐻‘(𝑇 + (𝑑𝑖))) = (𝐻‘(𝑇 + (𝑃𝑖))))
465464sneqd 4525 . . . . . . . . . 10 (𝑑 = 𝑃 → {(𝐻‘(𝑇 + (𝑑𝑖)))} = {(𝐻‘(𝑇 + (𝑃𝑖)))})
466465imaeq2d 5897 . . . . . . . . 9 (𝑑 = 𝑃 → (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) = (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
467463, 466sseq12d 3908 . . . . . . . 8 (𝑑 = 𝑃 → (((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ↔ ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
468467ralbidv 3109 . . . . . . 7 (𝑑 = 𝑃 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
469464mpteq2dv 5123 . . . . . . . . 9 (𝑑 = 𝑃 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))))
470469rneqd 5775 . . . . . . . 8 (𝑑 = 𝑃 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))))
471470fveqeq2d 6676 . . . . . . 7 (𝑑 = 𝑃 → ((♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))) = (𝑀 + 1) ↔ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1)))
472468, 471anbi12d 634 . . . . . 6 (𝑑 = 𝑃 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1))))
473460, 472rspc2ev 3536 . . . . 5 ((𝑇 ∈ ℕ ∧ 𝑃 ∈ (ℕ ↑m (1...(𝑀 + 1))) ∧ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1))) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1)))
47448, 73, 449, 473syl3anc 1372 . . . 4 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1)))
475 ovex 7197 . . . . 5 (1...(𝑊 · (2 · 𝑉))) ∈ V
47610adantr 484 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ)
477476nnnn0d 12029 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ0)
47839adantr 484 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
47918adantr 484 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑀 ∈ ℕ)
480479peano2nnd 11726 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (𝑀 + 1) ∈ ℕ)
481 eqid 2738 . . . . 5 (1...(𝑀 + 1)) = (1...(𝑀 + 1))
482475, 477, 478, 480, 481vdwpc 16409 . . . 4 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1))))
483474, 482mpbird 260 . . 3 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻)
484483orcd 872 . 2 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))
48537, 484pm2.61dan 813 1 (𝜑 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 846   = wceq 1542  wcel 2113  {cab 2716  wne 2934  wral 3053  wrex 3054  Vcvv 3397  cun 3839  wss 3841  c0 4209  ifcif 4411  {csn 4513  cop 4519   class class class wbr 5027  cmpt 5107  ccnv 5518  ran crn 5520  cima 5522   Fn wfn 6328  wf 6329  ontowfo 6331  cfv 6333  (class class class)co 7164  m cmap 8430  Fincfn 8548  cc 10606  cr 10607  0cc0 10608  1c1 10609   + caddc 10611   · cmul 10613   < clt 10746  cle 10747  cmin 10941  cn 11709  2c2 11764  0cn0 11969  cz 12055  cuz 12317  ...cfz 12974  chash 13775  APcvdwa 16394   MonoAP cvdwm 16395   PolyAP cvdwp 16396
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5151  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473  ax-cnex 10664  ax-resscn 10665  ax-1cn 10666  ax-icn 10667  ax-addcl 10668  ax-addrcl 10669  ax-mulcl 10670  ax-mulrcl 10671  ax-mulcom 10672  ax-addass 10673  ax-mulass 10674  ax-distr 10675  ax-i2m1 10676  ax-1ne0 10677  ax-1rid 10678  ax-rnegex 10679  ax-rrecex 10680  ax-cnre 10681  ax-pre-lttri 10682  ax-pre-lttrn 10683  ax-pre-ltadd 10684  ax-pre-mulgt0 10685
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-int 4834  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7121  df-ov 7167  df-oprab 7168  df-mpo 7169  df-om 7594  df-1st 7707  df-2nd 7708  df-wrecs 7969  df-recs 8030  df-rdg 8068  df-1o 8124  df-oadd 8128  df-er 8313  df-map 8432  df-en 8549  df-dom 8550  df-sdom 8551  df-fin 8552  df-dju 9396  df-card 9434  df-pnf 10748  df-mnf 10749  df-xr 10750  df-ltxr 10751  df-le 10752  df-sub 10943  df-neg 10944  df-nn 11710  df-2 11772  df-n0 11970  df-z 12056  df-uz 12318  df-rp 12466  df-fz 12975  df-hash 13776  df-vdwap 16397  df-vdwmc 16398  df-vdwpc 16399
This theorem is referenced by:  vdwlem7  16416
  Copyright terms: Public domain W3C validator