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

Theorem vdwlem6 16324
Description: Lemma for vdw 16332. (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 6685 . . . . . . 7 (𝐺‘(𝐵 + (𝐸𝑖))) ∈ V
2 vdwlem6.j . . . . . . 7 𝐽 = (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝐵 + (𝐸𝑖))))
31, 2fnmpti 6493 . . . . . 6 𝐽 Fn (1...𝑀)
4 fvelrnb 6728 . . . . . 6 (𝐽 Fn (1...𝑀) → ((𝐺𝐵) ∈ ran 𝐽 ↔ ∃𝑚 ∈ (1...𝑀)(𝐽𝑚) = (𝐺𝐵)))
53, 4ax-mp 5 . . . . 5 ((𝐺𝐵) ∈ ran 𝐽 ↔ ∃𝑚 ∈ (1...𝑀)(𝐽𝑚) = (𝐺𝐵))
6 vdwlem4.r . . . . . . . 8 (𝜑𝑅 ∈ Fin)
76adantr 483 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝑅 ∈ Fin)
8 vdwlem7.k . . . . . . . . 9 (𝜑𝐾 ∈ (ℤ‘2))
9 eluz2nn 12287 . . . . . . . . 9 (𝐾 ∈ (ℤ‘2) → 𝐾 ∈ ℕ)
108, 9syl 17 . . . . . . . 8 (𝜑𝐾 ∈ ℕ)
1110adantr 483 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝐾 ∈ ℕ)
12 vdwlem3.w . . . . . . . 8 (𝜑𝑊 ∈ ℕ)
1312adantr 483 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝑊 ∈ ℕ)
14 vdwlem7.g . . . . . . . 8 (𝜑𝐺:(1...𝑊)⟶𝑅)
1514adantr 483 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝐺:(1...𝑊)⟶𝑅)
16 vdwlem6.b . . . . . . . 8 (𝜑𝐵 ∈ ℕ)
1716adantr 483 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝐵 ∈ ℕ)
18 vdwlem7.m . . . . . . . 8 (𝜑𝑀 ∈ ℕ)
1918adantr 483 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝑀 ∈ ℕ)
20 vdwlem6.e . . . . . . . 8 (𝜑𝐸:(1...𝑀)⟶ℕ)
2120adantr 483 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝐸:(1...𝑀)⟶ℕ)
22 vdwlem6.s . . . . . . . 8 (𝜑 → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
2322adantr 483 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
24 simprl 769 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝑚 ∈ (1...𝑀))
25 simprr 771 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐽𝑚) = (𝐺𝐵))
26 fveq2 6672 . . . . . . . . . . . 12 (𝑖 = 𝑚 → (𝐸𝑖) = (𝐸𝑚))
2726oveq2d 7174 . . . . . . . . . . 11 (𝑖 = 𝑚 → (𝐵 + (𝐸𝑖)) = (𝐵 + (𝐸𝑚)))
2827fveq2d 6676 . . . . . . . . . 10 (𝑖 = 𝑚 → (𝐺‘(𝐵 + (𝐸𝑖))) = (𝐺‘(𝐵 + (𝐸𝑚))))
29 fvex 6685 . . . . . . . . . 10 (𝐺‘(𝐵 + (𝐸𝑚))) ∈ V
3028, 2, 29fvmpt 6770 . . . . . . . . 9 (𝑚 ∈ (1...𝑀) → (𝐽𝑚) = (𝐺‘(𝐵 + (𝐸𝑚))))
3124, 30syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐽𝑚) = (𝐺‘(𝐵 + (𝐸𝑚))))
3225, 31eqtr3d 2860 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐺𝐵) = (𝐺‘(𝐵 + (𝐸𝑚))))
337, 11, 13, 15, 17, 19, 21, 23, 24, 32vdwlem1 16319 . . . . . 6 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐾 + 1) MonoAP 𝐺)
3433rexlimdvaa 3287 . . . . 5 (𝜑 → (∃𝑚 ∈ (1...𝑀)(𝐽𝑚) = (𝐺𝐵) → (𝐾 + 1) MonoAP 𝐺))
355, 34syl5bi 244 . . . 4 (𝜑 → ((𝐺𝐵) ∈ ran 𝐽 → (𝐾 + 1) MonoAP 𝐺))
3635imp 409 . . 3 ((𝜑 ∧ (𝐺𝐵) ∈ ran 𝐽) → (𝐾 + 1) MonoAP 𝐺)
3736olcd 870 . 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 16323 . . . . . 6 (𝜑𝑇 ∈ ℕ)
4847adantr 483 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑇 ∈ ℕ)
49 0nn0 11915 . . . . . . . . . 10 0 ∈ ℕ0
5049a1i 11 . . . . . . . . 9 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 = (𝑀 + 1)) → 0 ∈ ℕ0)
51 nnuz 12284 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
5218, 51eleqtrdi 2925 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ (ℤ‘1))
5352adantr 483 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑀 ∈ (ℤ‘1))
54 elfzp1 12960 . . . . . . . . . . . . . . 15 (𝑀 ∈ (ℤ‘1) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1))))
5553, 54syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1))))
5655biimpa 479 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1)))
5756ord 860 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 ∈ (1...𝑀) → 𝑗 = (𝑀 + 1)))
5857con1d 147 . . . . . . . . . . 11 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 = (𝑀 + 1) → 𝑗 ∈ (1...𝑀)))
5958imp 409 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → 𝑗 ∈ (1...𝑀))
6020ad2antrr 724 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → 𝐸:(1...𝑀)⟶ℕ)
6160ffvelrnda 6853 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸𝑗) ∈ ℕ)
6261nnnn0d 11958 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸𝑗) ∈ ℕ0)
6359, 62syldan 593 . . . . . . . . 9 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → (𝐸𝑗) ∈ ℕ0)
6450, 63ifclda 4503 . . . . . . . 8 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) ∈ ℕ0)
6512, 42nnmulcld 11693 . . . . . . . . 9 (𝜑 → (𝑊 · 𝐷) ∈ ℕ)
6665ad2antrr 724 . . . . . . . 8 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑊 · 𝐷) ∈ ℕ)
67 nn0nnaddcl 11931 . . . . . . . 8 ((if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) ∈ ℕ0 ∧ (𝑊 · 𝐷) ∈ ℕ) → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
6864, 66, 67syl2anc 586 . . . . . . 7 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
6968, 46fmptd 6880 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑃:(1...(𝑀 + 1))⟶ℕ)
70 nnex 11646 . . . . . . 7 ℕ ∈ V
71 ovex 7191 . . . . . . 7 (1...(𝑀 + 1)) ∈ V
7270, 71elmap 8437 . . . . . 6 (𝑃 ∈ (ℕ ↑m (1...(𝑀 + 1))) ↔ 𝑃:(1...(𝑀 + 1))⟶ℕ)
7369, 72sylibr 236 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑃 ∈ (ℕ ↑m (1...(𝑀 + 1))))
74 elfzp1 12960 . . . . . . . . . 10 (𝑀 ∈ (ℤ‘1) → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1))))
7552, 74syl 17 . . . . . . . . 9 (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1))))
7616adantr 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℕ)
7776nncnd 11656 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℂ)
7877adantr 483 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ)
7920ffvelrnda 6853 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐸𝑖) ∈ ℕ)
8079nncnd 11656 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐸𝑖) ∈ ℂ)
8180adantr 483 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐸𝑖) ∈ ℂ)
8278, 81addcld 10662 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝐸𝑖)) ∈ ℂ)
83 nnm1nn0 11941 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ ℕ → (𝐴 − 1) ∈ ℕ0)
8441, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐴 − 1) ∈ ℕ0)
85 nn0nnaddcl 11931 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 − 1) ∈ ℕ0𝑉 ∈ ℕ) → ((𝐴 − 1) + 𝑉) ∈ ℕ)
8684, 38, 85syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℕ)
8712, 86nnmulcld 11693 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
8887nncnd 11656 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
8988ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
90 elfznn0 13003 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ (0...(𝐾 − 1)) → 𝑚 ∈ ℕ0)
9190adantl 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℕ0)
9291nn0cnd 11960 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
9392adantlr 713 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
9493, 81mulcld 10663 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝐸𝑖)) ∈ ℂ)
9565nnnn0d 11958 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑊 · 𝐷) ∈ ℕ0)
9695adantr 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℕ0)
9791, 96nn0mulcld 11963 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℕ0)
9897nn0cnd 11960 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
9998adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
10082, 89, 94, 99add4d 10870 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸𝑖)) + (𝑚 · (𝑊 · 𝐷)))) = (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
10165nncnd 11656 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑊 · 𝐷) ∈ ℂ)
102101ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℂ)
10393, 81, 102adddid 10667 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))) = ((𝑚 · (𝐸𝑖)) + (𝑚 · (𝑊 · 𝐷))))
104103oveq2d 7174 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸𝑖)) + (𝑚 · (𝑊 · 𝐷)))))
10512nncnd 11656 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑊 ∈ ℂ)
106105adantr 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℂ)
10786nncnd 11656 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℂ)
108107adantr 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 − 1) + 𝑉) ∈ ℂ)
10942nncnd 11656 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐷 ∈ ℂ)
110109adantr 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐷 ∈ ℂ)
11192, 110mulcld 10663 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · 𝐷) ∈ ℂ)
112106, 108, 111adddid 10667 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
11341nncnd 11656 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐴 ∈ ℂ)
114113adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐴 ∈ ℂ)
115 1cnd 10638 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 1 ∈ ℂ)
116114, 111, 115addsubd 11020 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) − 1) = ((𝐴 − 1) + (𝑚 · 𝐷)))
117116oveq1d 7173 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉))
11884nn0cnd 11960 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 − 1) ∈ ℂ)
119118adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 − 1) ∈ ℂ)
12038nncnd 11656 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑉 ∈ ℂ)
121120adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℂ)
122119, 111, 121add32d 10869 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
123117, 122eqtrd 2858 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
124123oveq2d 7174 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))))
12592, 106, 110mul12d 10851 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) = (𝑊 · (𝑚 · 𝐷)))
126125oveq2d 7174 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
127112, 124, 1263eqtr4d 2868 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
128127adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
129128oveq2d 7174 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
130100, 104, 1293eqtr4d 2868 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
13138ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
13212ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
13343adantr 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴(AP‘𝐾)𝐷) ⊆ (𝐹 “ {𝐺}))
134 eqid 2823 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))
135 oveq1 7165 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑚 → (𝑛 · 𝐷) = (𝑚 · 𝐷))
136135oveq2d 7174 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → (𝐴 + (𝑛 · 𝐷)) = (𝐴 + (𝑚 · 𝐷)))
137136rspceeqv 3640 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 ∈ (0...(𝐾 − 1)) ∧ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
138134, 137mpan2 689 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
13910nnnn0d 11958 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐾 ∈ ℕ0)
140 vdwapval 16311 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
141139, 41, 42, 140syl3anc 1367 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
142141biimpar 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
143138, 142sylan2 594 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
144133, 143sseldd 3970 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺}))
14538, 12, 6, 39, 40vdwlem4 16322 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹:(1...𝑉)⟶(𝑅m (1...𝑊)))
146145ffnd 6517 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹 Fn (1...𝑉))
147 fniniseg 6832 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 Fn (1...𝑉) → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
148146, 147syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
149148biimpa 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺})) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
150144, 149syldan 593 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
151150simpld 497 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
152151adantlr 713 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
15322r19.21bi 3210 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
154153adantr 483 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
155 eqid 2823 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))
156 oveq1 7165 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → (𝑛 · (𝐸𝑖)) = (𝑚 · (𝐸𝑖)))
157156oveq2d 7174 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑚 → ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))))
158157rspceeqv 3640 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚 ∈ (0...(𝐾 − 1)) ∧ ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖))))
159155, 158mpan2 689 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖))))
16010adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ)
161160nnnn0d 11958 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ0)
16276, 79nnaddcld 11692 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ ℕ)
163 vdwapval 16311 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐾 ∈ ℕ0 ∧ (𝐵 + (𝐸𝑖)) ∈ ℕ ∧ (𝐸𝑖) ∈ ℕ) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖)))))
164161, 162, 79, 163syl3anc 1367 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖)))))
165164biimpar 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖 ∈ (1...𝑀)) ∧ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖)))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
166159, 165sylan2 594 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
167154, 166sseldd 3970 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
16814ffnd 6517 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐺 Fn (1...𝑊))
169168adantr 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐺 Fn (1...𝑊))
170 fniniseg 6832 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 Fn (1...𝑊) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖))))))
171169, 170syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖))))))
172171biimpa 479 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))})) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
173167, 172syldan 593 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
174173simpld 497 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊))
175131, 132, 152, 174vdwlem3 16321 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
176130, 175eqeltrd 2915 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))))
177 fvoveq1 7181 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
178 eqid 2823 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
179 fvex 6685 . . . . . . . . . . . . . . . . . . . 20 (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
180177, 178, 179fvmpt 6770 . . . . . . . . . . . . . . . . . . 19 (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
181174, 180syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
182173simprd 498 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖))))
183150simprd 498 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)
184 oveq1 7165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑥 − 1) = ((𝐴 + (𝑚 · 𝐷)) − 1))
185184oveq1d 7173 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → ((𝑥 − 1) + 𝑉) = (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))
186185oveq2d 7174 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))
187186oveq2d 7174 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
188187fveq2d 6676 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
189188mpteq2dv 5164 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
190 ovex 7191 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1...𝑊) ∈ V
191190mptex 6988 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) ∈ V
192189, 40, 191fvmpt 6770 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
193151, 192syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
194183, 193eqtr3d 2860 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
195194adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
196195fveq1d 6674 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))))
197182, 196eqtr3d 2860 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘(𝐵 + (𝐸𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))))
198130fveq2d 6676 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
199181, 197, 1983eqtr4rd 2869 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖))))
200176, 199jca 514 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
201 eleq1 2902 . . . . . . . . . . . . . . . . 17 (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉)))))
202 fveqeq2 6681 . . . . . . . . . . . . . . . . 17 (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → ((𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))) ↔ (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
203201, 202anbi12d 632 . . . . . . . . . . . . . . . 16 (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → ((𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖)))) ↔ ((((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖))))))
204200, 203syl5ibrcom 249 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
205204rexlimdva 3286 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
20687adantr 483 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
207162, 206nnaddcld 11692 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
20865adantr 483 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℕ)
20979, 208nnaddcld 11692 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + (𝑊 · 𝐷)) ∈ ℕ)
210 vdwapval 16311 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℕ0 ∧ ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ ((𝐸𝑖) + (𝑊 · 𝐷)) ∈ ℕ) → (𝑥 ∈ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))))
211161, 207, 209, 210syl3anc 1367 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))))
21239ffnd 6517 . . . . . . . . . . . . . . . 16 (𝜑𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
213212adantr 483 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
214 fniniseg 6832 . . . . . . . . . . . . . . 15 (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑥 ∈ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
215213, 214syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
216205, 211, 2153imtr4d 296 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) → 𝑥 ∈ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))})))
217216ssrdv 3975 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) ⊆ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
218 ssun1 4150 . . . . . . . . . . . . . . . . . . 19 (1...𝑀) ⊆ ((1...𝑀) ∪ {(𝑀 + 1)})
219 fzsuc 12957 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (ℤ‘1) → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
22052, 219syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
221218, 220sseqtrrid 4022 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1...𝑀) ⊆ (1...(𝑀 + 1)))
222221sselda 3969 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...(𝑀 + 1)))
223 eqeq1 2827 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝑗 = (𝑀 + 1) ↔ 𝑖 = (𝑀 + 1)))
224 fveq2 6672 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝐸𝑗) = (𝐸𝑖))
225223, 224ifbieq2d 4494 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) = if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)))
226225oveq1d 7173 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) = (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)))
227 ovex 7191 . . . . . . . . . . . . . . . . . 18 (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)) ∈ V
228226, 46, 227fvmpt 6770 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...(𝑀 + 1)) → (𝑃𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)))
229222, 228syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑃𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)))
23018nnred 11655 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑀 ∈ ℝ)
231230ltp1d 11572 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑀 < (𝑀 + 1))
232 peano2re 10815 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
233230, 232syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑀 + 1) ∈ ℝ)
234230, 233ltnled 10789 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀))
235231, 234mpbid 234 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀)
236 breq1 5071 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = (𝑀 + 1) → (𝑖𝑀 ↔ (𝑀 + 1) ≤ 𝑀))
237236notbid 320 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = (𝑀 + 1) → (¬ 𝑖𝑀 ↔ ¬ (𝑀 + 1) ≤ 𝑀))
238235, 237syl5ibrcom 249 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑖 = (𝑀 + 1) → ¬ 𝑖𝑀))
239238con2d 136 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑖𝑀 → ¬ 𝑖 = (𝑀 + 1)))
240 elfzle2 12914 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑀) → 𝑖𝑀)
241239, 240impel 508 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → ¬ 𝑖 = (𝑀 + 1))
242 iffalse 4478 . . . . . . . . . . . . . . . . . 18 𝑖 = (𝑀 + 1) → if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) = (𝐸𝑖))
243242oveq1d 7173 . . . . . . . . . . . . . . . . 17 𝑖 = (𝑀 + 1) → (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)) = ((𝐸𝑖) + (𝑊 · 𝐷)))
244241, 243syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)) = ((𝐸𝑖) + (𝑊 · 𝐷)))
245229, 244eqtrd 2858 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑃𝑖) = ((𝐸𝑖) + (𝑊 · 𝐷)))
246245oveq2d 7174 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃𝑖)) = (𝑇 + ((𝐸𝑖) + (𝑊 · 𝐷))))
24747nncnd 11656 . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ ℂ)
248247adantr 483 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑇 ∈ ℂ)
249101adantr 483 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℂ)
250248, 80, 249add12d 10868 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑇 + ((𝐸𝑖) + (𝑊 · 𝐷))) = ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))))
25145oveq1i 7168 . . . . . . . . . . . . . . . . . 18 (𝑇 + (𝑊 · 𝐷)) = ((𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1))) + (𝑊 · 𝐷))
25216nncnd 11656 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℂ)
253120, 109subcld 10999 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑉𝐷) ∈ ℂ)
254113, 253addcld 10662 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 + (𝑉𝐷)) ∈ ℂ)
255 ax-1cn 10597 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℂ
256 subcl 10887 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 + (𝑉𝐷)) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 + (𝑉𝐷)) − 1) ∈ ℂ)
257254, 255, 256sylancl 588 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 + (𝑉𝐷)) − 1) ∈ ℂ)
258105, 257mulcld 10663 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) ∈ ℂ)
259252, 258, 101addassd 10665 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷))))
260105, 257, 109adddid 10667 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑊 · (((𝐴 + (𝑉𝐷)) − 1) + 𝐷)) = ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷)))
261113, 253, 109addassd 10665 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 + (𝑉𝐷)) + 𝐷) = (𝐴 + ((𝑉𝐷) + 𝐷)))
262120, 109npcand 11003 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑉𝐷) + 𝐷) = 𝑉)
263262oveq2d 7174 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐴 + ((𝑉𝐷) + 𝐷)) = (𝐴 + 𝑉))
264261, 263eqtrd 2858 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐴 + (𝑉𝐷)) + 𝐷) = (𝐴 + 𝑉))
265264oveq1d 7173 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝐴 + (𝑉𝐷)) + 𝐷) − 1) = ((𝐴 + 𝑉) − 1))
266 1cnd 10638 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ∈ ℂ)
267254, 109, 266addsubd 11020 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝐴 + (𝑉𝐷)) + 𝐷) − 1) = (((𝐴 + (𝑉𝐷)) − 1) + 𝐷))
268113, 120, 266addsubd 11020 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 + 𝑉) − 1) = ((𝐴 − 1) + 𝑉))
269265, 267, 2683eqtr3d 2866 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐴 + (𝑉𝐷)) − 1) + 𝐷) = ((𝐴 − 1) + 𝑉))
270269oveq2d 7174 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑊 · (((𝐴 + (𝑉𝐷)) − 1) + 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
271260, 270eqtr3d 2860 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
272271oveq2d 7174 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵 + ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
273259, 272eqtrd 2858 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
274251, 273syl5eq 2870 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑇 + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
275274oveq2d 7174 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
276275adantr 483 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
27788adantr 483 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
27880, 77, 277addassd 10665 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐸𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐸𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
27980, 77addcomd 10844 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + 𝐵) = (𝐵 + (𝐸𝑖)))
280279oveq1d 7173 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐸𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
281276, 278, 2803eqtr2d 2864 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
282246, 250, 2813eqtrd 2862 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃𝑖)) = ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
283282, 245oveq12d 7176 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))))
284 cnvimass 5951 . . . . . . . . . . . . . . . . . . 19 (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ⊆ dom 𝐺
285284, 14fssdm 6532 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ⊆ (1...𝑊))
286285adantr 483 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ⊆ (1...𝑊))
287 vdwapid1 16313 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ ℕ ∧ (𝐵 + (𝐸𝑖)) ∈ ℕ ∧ (𝐸𝑖) ∈ ℕ) → (𝐵 + (𝐸𝑖)) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
288160, 162, 79, 287syl3anc 1367 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
289153, 288sseldd 3970 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
290286, 289sseldd 3970 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ (1...𝑊))
291 fvoveq1 7181 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝐵 + (𝐸𝑖)) → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
292 eqid 2823 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
293 fvex 6685 . . . . . . . . . . . . . . . . 17 (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
294291, 292, 293fvmpt 6770 . . . . . . . . . . . . . . . 16 ((𝐵 + (𝐸𝑖)) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
295290, 294syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
296 vdwapid1 16313 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
29710, 41, 42, 296syl3anc 1367 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
29843, 297sseldd 3970 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ (𝐹 “ {𝐺}))
299 fniniseg 6832 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn (1...𝑉) → (𝐴 ∈ (𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹𝐴) = 𝐺)))
300146, 299syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐴 ∈ (𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹𝐴) = 𝐺)))
301298, 300mpbid 234 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 ∈ (1...𝑉) ∧ (𝐹𝐴) = 𝐺))
302301simprd 498 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹𝐴) = 𝐺)
303301simpld 497 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ (1...𝑉))
304 oveq1 7165 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝐴 → (𝑥 − 1) = (𝐴 − 1))
305304oveq1d 7173 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝐴 → ((𝑥 − 1) + 𝑉) = ((𝐴 − 1) + 𝑉))
306305oveq2d 7174 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝐴 → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
307306oveq2d 7174 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝐴 → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))
308307fveq2d 6676 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝐴 → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
309308mpteq2dv 5164 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝐴 → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
310190mptex 6988 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) ∈ V
311309, 40, 310fvmpt 6770 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ (1...𝑉) → (𝐹𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
312303, 311syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
313302, 312eqtr3d 2860 . . . . . . . . . . . . . . . . 17 (𝜑𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
314313fveq1d 6674 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐺‘(𝐵 + (𝐸𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))))
315314adantr 483 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐵 + (𝐸𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))))
316282fveq2d 6676 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃𝑖))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
317295, 315, 3163eqtr4rd 2869 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃𝑖))) = (𝐺‘(𝐵 + (𝐸𝑖))))
318317sneqd 4581 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → {(𝐻‘(𝑇 + (𝑃𝑖)))} = {(𝐺‘(𝐵 + (𝐸𝑖)))})
319318imaeq2d 5931 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) = (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
320217, 283, 3193sstr4d 4016 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
321320ex 415 . . . . . . . . . 10 (𝜑 → (𝑖 ∈ (1...𝑀) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
322252adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ)
32388adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
324322, 323, 98addassd 10665 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
325127oveq2d 7174 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
326324, 325eqtr4d 2861 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
32738adantr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
32812adantr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
329 eluzfz1 12917 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ (ℤ‘1) → 1 ∈ (1...𝑀))
33052, 329syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ∈ (1...𝑀))
331330ne0d 4303 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑀) ≠ ∅)
332 elfzuz3 12908 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 + (𝐸𝑖)) ∈ (1...𝑊) → 𝑊 ∈ (ℤ‘(𝐵 + (𝐸𝑖))))
333290, 332syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ‘(𝐵 + (𝐸𝑖))))
33416nnzd 12089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐵 ∈ ℤ)
335 uzid 12261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵 ∈ ℤ → 𝐵 ∈ (ℤ𝐵))
336334, 335syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ∈ (ℤ𝐵))
337336adantr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵 ∈ (ℤ𝐵))
33879nnnn0d 11958 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐸𝑖) ∈ ℕ0)
339 uzaddcl 12307 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ∈ (ℤ𝐵) ∧ (𝐸𝑖) ∈ ℕ0) → (𝐵 + (𝐸𝑖)) ∈ (ℤ𝐵))
340337, 338, 339syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ (ℤ𝐵))
341 uztrn 12264 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑊 ∈ (ℤ‘(𝐵 + (𝐸𝑖))) ∧ (𝐵 + (𝐸𝑖)) ∈ (ℤ𝐵)) → 𝑊 ∈ (ℤ𝐵))
342333, 340, 341syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ𝐵))
343 eluzle 12259 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑊 ∈ (ℤ𝐵) → 𝐵𝑊)
344342, 343syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵𝑊)
345344ralrimiva 3184 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑖 ∈ (1...𝑀)𝐵𝑊)
346 r19.2z 4442 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...𝑀) ≠ ∅ ∧ ∀𝑖 ∈ (1...𝑀)𝐵𝑊) → ∃𝑖 ∈ (1...𝑀)𝐵𝑊)
347331, 345, 346syl2anc 586 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∃𝑖 ∈ (1...𝑀)𝐵𝑊)
348 idd 24 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (1...𝑀) → (𝐵𝑊𝐵𝑊))
349348rexlimiv 3282 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑖 ∈ (1...𝑀)𝐵𝑊𝐵𝑊)
350347, 349syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵𝑊)
35112nnzd 12089 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑊 ∈ ℤ)
352 fznn 12978 . . . . . . . . . . . . . . . . . . . . . 22 (𝑊 ∈ ℤ → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵𝑊)))
353351, 352syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵𝑊)))
35416, 350, 353mpbir2and 711 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ (1...𝑊))
355354adantr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ (1...𝑊))
356327, 328, 151, 355vdwlem3 16321 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
357326, 356eqeltrd 2915 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))))
358 fvoveq1 7181 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
359 fvex 6685 . . . . . . . . . . . . . . . . . . . 20 (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
360358, 178, 359fvmpt 6770 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
361355, 360syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
362194fveq1d 6674 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐺𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵))
363326fveq2d 6676 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
364361, 362, 3633eqtr4rd 2869 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵))
365357, 364jca 514 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵)))
366 eleq1 2902 . . . . . . . . . . . . . . . . 17 (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉)))))
367 fveqeq2 6681 . . . . . . . . . . . . . . . . 17 (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝐻𝑧) = (𝐺𝐵) ↔ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵)))
368366, 367anbi12d 632 . . . . . . . . . . . . . . . 16 (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵)) ↔ (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵))))
369365, 368syl5ibrcom 249 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
370369rexlimdva 3286 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
37116, 87nnaddcld 11692 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
372 vdwapval 16311 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℕ0 ∧ (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ (𝑊 · 𝐷) ∈ ℕ) → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
373139, 371, 65, 372syl3anc 1367 . . . . . . . . . . . . . 14 (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
374 fniniseg 6832 . . . . . . . . . . . . . . 15 (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑧 ∈ (𝐻 “ {(𝐺𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
375212, 374syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑧 ∈ (𝐻 “ {(𝐺𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
376370, 373, 3753imtr4d 296 . . . . . . . . . . . . 13 (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) → 𝑧 ∈ (𝐻 “ {(𝐺𝐵)})))
377376ssrdv 3975 . . . . . . . . . . . 12 (𝜑 → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ⊆ (𝐻 “ {(𝐺𝐵)}))
37818peano2nnd 11657 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 + 1) ∈ ℕ)
379378, 51eleqtrdi 2925 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 + 1) ∈ (ℤ‘1))
380 eluzfz2 12918 . . . . . . . . . . . . . . . . 17 ((𝑀 + 1) ∈ (ℤ‘1) → (𝑀 + 1) ∈ (1...(𝑀 + 1)))
381 iftrue 4475 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑀 + 1) → if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) = 0)
382381oveq1d 7173 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑀 + 1) → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) = (0 + (𝑊 · 𝐷)))
383 ovex 7191 . . . . . . . . . . . . . . . . . 18 (0 + (𝑊 · 𝐷)) ∈ V
384382, 46, 383fvmpt 6770 . . . . . . . . . . . . . . . . 17 ((𝑀 + 1) ∈ (1...(𝑀 + 1)) → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
385379, 380, 3843syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
386101addid2d 10843 . . . . . . . . . . . . . . . 16 (𝜑 → (0 + (𝑊 · 𝐷)) = (𝑊 · 𝐷))
387385, 386eqtrd 2858 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃‘(𝑀 + 1)) = (𝑊 · 𝐷))
388387oveq2d 7174 . . . . . . . . . . . . . 14 (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝑇 + (𝑊 · 𝐷)))
389388, 274eqtrd 2858 . . . . . . . . . . . . 13 (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
390389, 387oveq12d 7176 . . . . . . . . . . . 12 (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)))
391 fvoveq1 7181 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
392 fvex 6685 . . . . . . . . . . . . . . . . 17 (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
393391, 292, 392fvmpt 6770 . . . . . . . . . . . . . . . 16 (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
394354, 393syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
395313fveq1d 6674 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵))
396389fveq2d 6676 . . . . . . . . . . . . . . 15 (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
397394, 395, 3963eqtr4rd 2869 . . . . . . . . . . . . . 14 (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐺𝐵))
398397sneqd 4581 . . . . . . . . . . . . 13 (𝜑 → {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))} = {(𝐺𝐵)})
399398imaeq2d 5931 . . . . . . . . . . . 12 (𝜑 → (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}) = (𝐻 “ {(𝐺𝐵)}))
400377, 390, 3993sstr4d 4016 . . . . . . . . . . 11 (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
401 fveq2 6672 . . . . . . . . . . . . . 14 (𝑖 = (𝑀 + 1) → (𝑃𝑖) = (𝑃‘(𝑀 + 1)))
402401oveq2d 7174 . . . . . . . . . . . . 13 (𝑖 = (𝑀 + 1) → (𝑇 + (𝑃𝑖)) = (𝑇 + (𝑃‘(𝑀 + 1))))
403402, 401oveq12d 7176 . . . . . . . . . . . 12 (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) = ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))))
404402fveq2d 6676 . . . . . . . . . . . . . 14 (𝑖 = (𝑀 + 1) → (𝐻‘(𝑇 + (𝑃𝑖))) = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
405404sneqd 4581 . . . . . . . . . . . . 13 (𝑖 = (𝑀 + 1) → {(𝐻‘(𝑇 + (𝑃𝑖)))} = {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})
406405imaeq2d 5931 . . . . . . . . . . . 12 (𝑖 = (𝑀 + 1) → (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) = (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
407403, 406sseq12d 4002 . . . . . . . . . . 11 (𝑖 = (𝑀 + 1) → (((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) ↔ ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})))
408400, 407syl5ibrcom 249 . . . . . . . . . 10 (𝜑 → (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
409321, 408jaod 855 . . . . . . . . 9 (𝜑 → ((𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
41075, 409sylbid 242 . . . . . . . 8 (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
411410ralrimiv 3183 . . . . . . 7 (𝜑 → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
412411adantr 483 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
413220rexeqdv 3418 . . . . . . . . . . . 12 (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ ∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))))
414 rexun 4168 . . . . . . . . . . . . 13 (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))))
415317eqeq2d 2834 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))))
416415rexbidva 3298 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))))
417 ovex 7191 . . . . . . . . . . . . . . . 16 (𝑀 + 1) ∈ V
418404eqeq2d 2834 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑀 + 1) → (𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))))
419417, 418rexsn 4622 . . . . . . . . . . . . . . 15 (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
420397eqeq2d 2834 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) ↔ 𝑥 = (𝐺𝐵)))
421419, 420syl5bb 285 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐺𝐵)))
422416, 421orbi12d 915 . . . . . . . . . . . . 13 (𝜑 → ((∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))))
423414, 422syl5bb 285 . . . . . . . . . . . 12 (𝜑 → (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))))
424413, 423bitrd 281 . . . . . . . . . . 11 (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))))
425424adantr 483 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))))
426425abbidv 2887 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))} = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))})
427 eqid 2823 . . . . . . . . . 10 (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))
428427rnmpt 5829 . . . . . . . . 9 ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))) = {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))}
4292rnmpt 5829 . . . . . . . . . . 11 ran 𝐽 = {𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))}
430 df-sn 4570 . . . . . . . . . . 11 {(𝐺𝐵)} = {𝑥𝑥 = (𝐺𝐵)}
431429, 430uneq12i 4139 . . . . . . . . . 10 (ran 𝐽 ∪ {(𝐺𝐵)}) = ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))} ∪ {𝑥𝑥 = (𝐺𝐵)})
432 unab 4272 . . . . . . . . . 10 ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))} ∪ {𝑥𝑥 = (𝐺𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))}
433431, 432eqtri 2846 . . . . . . . . 9 (ran 𝐽 ∪ {(𝐺𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))}
434426, 428, 4333eqtr4g 2883 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))) = (ran 𝐽 ∪ {(𝐺𝐵)}))
435434fveq2d 6676 . . . . . . 7 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (♯‘(ran 𝐽 ∪ {(𝐺𝐵)})))
436 fzfi 13343 . . . . . . . . . 10 (1...𝑀) ∈ Fin
437 dffn4 6598 . . . . . . . . . . 11 (𝐽 Fn (1...𝑀) ↔ 𝐽:(1...𝑀)–onto→ran 𝐽)
4383, 437mpbi 232 . . . . . . . . . 10 𝐽:(1...𝑀)–onto→ran 𝐽
439 fofi 8812 . . . . . . . . . 10 (((1...𝑀) ∈ Fin ∧ 𝐽:(1...𝑀)–onto→ran 𝐽) → ran 𝐽 ∈ Fin)
440436, 438, 439mp2an 690 . . . . . . . . 9 ran 𝐽 ∈ Fin
441440a1i 11 . . . . . . . 8 (𝜑 → ran 𝐽 ∈ Fin)
442 fvex 6685 . . . . . . . . 9 (𝐺𝐵) ∈ V
443 hashunsng 13756 . . . . . . . . 9 ((𝐺𝐵) ∈ V → ((ran 𝐽 ∈ Fin ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺𝐵)})) = ((♯‘ran 𝐽) + 1)))
444442, 443ax-mp 5 . . . . . . . 8 ((ran 𝐽 ∈ Fin ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺𝐵)})) = ((♯‘ran 𝐽) + 1))
445441, 444sylan 582 . . . . . . 7 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺𝐵)})) = ((♯‘ran 𝐽) + 1))
44644adantr 483 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘ran 𝐽) = 𝑀)
447446oveq1d 7173 . . . . . . 7 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ((♯‘ran 𝐽) + 1) = (𝑀 + 1))
448435, 445, 4473eqtrd 2862 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1))
449412, 448jca 514 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1)))
450 oveq1 7165 . . . . . . . . . 10 (𝑎 = 𝑇 → (𝑎 + (𝑑𝑖)) = (𝑇 + (𝑑𝑖)))
451450oveq1d 7173 . . . . . . . . 9 (𝑎 = 𝑇 → ((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) = ((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)))
452 fvoveq1 7181 . . . . . . . . . . 11 (𝑎 = 𝑇 → (𝐻‘(𝑎 + (𝑑𝑖))) = (𝐻‘(𝑇 + (𝑑𝑖))))
453452sneqd 4581 . . . . . . . . . 10 (𝑎 = 𝑇 → {(𝐻‘(𝑎 + (𝑑𝑖)))} = {(𝐻‘(𝑇 + (𝑑𝑖)))})
454453imaeq2d 5931 . . . . . . . . 9 (𝑎 = 𝑇 → (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) = (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}))
455451, 454sseq12d 4002 . . . . . . . 8 (𝑎 = 𝑇 → (((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ↔ ((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))})))
456455ralbidv 3199 . . . . . . 7 (𝑎 = 𝑇 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))})))
457452mpteq2dv 5164 . . . . . . . . 9 (𝑎 = 𝑇 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))))
458457rneqd 5810 . . . . . . . 8 (𝑎 = 𝑇 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))))
459458fveqeq2d 6680 . . . . . . 7 (𝑎 = 𝑇 → ((♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1) ↔ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))) = (𝑀 + 1)))
460456, 459anbi12d 632 . . . . . 6 (𝑎 = 𝑇 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))) = (𝑀 + 1))))
461 fveq1 6671 . . . . . . . . . . 11 (𝑑 = 𝑃 → (𝑑𝑖) = (𝑃𝑖))
462461oveq2d 7174 . . . . . . . . . 10 (𝑑 = 𝑃 → (𝑇 + (𝑑𝑖)) = (𝑇 + (𝑃𝑖)))
463462, 461oveq12d 7176 . . . . . . . . 9 (𝑑 = 𝑃 → ((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) = ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)))
464462fveq2d 6676 . . . . . . . . . . 11 (𝑑 = 𝑃 → (𝐻‘(𝑇 + (𝑑𝑖))) = (𝐻‘(𝑇 + (𝑃𝑖))))
465464sneqd 4581 . . . . . . . . . 10 (𝑑 = 𝑃 → {(𝐻‘(𝑇 + (𝑑𝑖)))} = {(𝐻‘(𝑇 + (𝑃𝑖)))})
466465imaeq2d 5931 . . . . . . . . 9 (𝑑 = 𝑃 → (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) = (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
467463, 466sseq12d 4002 . . . . . . . 8 (𝑑 = 𝑃 → (((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ↔ ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
468467ralbidv 3199 . . . . . . 7 (𝑑 = 𝑃 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
469464mpteq2dv 5164 . . . . . . . . 9 (𝑑 = 𝑃 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))))
470469rneqd 5810 . . . . . . . 8 (𝑑 = 𝑃 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))))
471470fveqeq2d 6680 . . . . . . 7 (𝑑 = 𝑃 → ((♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))) = (𝑀 + 1) ↔ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1)))
472468, 471anbi12d 632 . . . . . 6 (𝑑 = 𝑃 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1))))
473460, 472rspc2ev 3637 . . . . 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 1367 . . . 4 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1)))
475 ovex 7191 . . . . 5 (1...(𝑊 · (2 · 𝑉))) ∈ V
47610adantr 483 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ)
477476nnnn0d 11958 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ0)
47839adantr 483 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
47918adantr 483 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑀 ∈ ℕ)
480479peano2nnd 11657 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (𝑀 + 1) ∈ ℕ)
481 eqid 2823 . . . . 5 (1...(𝑀 + 1)) = (1...(𝑀 + 1))
482475, 477, 478, 480, 481vdwpc 16318 . . . 4 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1))))
483474, 482mpbird 259 . . 3 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻)
484483orcd 869 . 2 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))
48537, 484pm2.61dan 811 1 (𝜑 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843   = wceq 1537  wcel 2114  {cab 2801  wne 3018  wral 3140  wrex 3141  Vcvv 3496  cun 3936  wss 3938  c0 4293  ifcif 4469  {csn 4569  cop 4575   class class class wbr 5068  cmpt 5148  ccnv 5556  ran crn 5558  cima 5560   Fn wfn 6352  wf 6353  ontowfo 6355  cfv 6357  (class class class)co 7158  m cmap 8408  Fincfn 8511  cc 10537  cr 10538  0cc0 10539  1c1 10540   + caddc 10542   · cmul 10544   < clt 10677  cle 10678  cmin 10872  cn 11640  2c2 11695  0cn0 11900  cz 11984  cuz 12246  ...cfz 12895  chash 13693  APcvdwa 16303   MonoAP cvdwm 16304   PolyAP cvdwp 16305
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-om 7583  df-1st 7691  df-2nd 7692  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-1o 8104  df-oadd 8108  df-er 8291  df-map 8410  df-en 8512  df-dom 8513  df-sdom 8514  df-fin 8515  df-dju 9332  df-card 9370  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-nn 11641  df-2 11703  df-n0 11901  df-z 11985  df-uz 12247  df-rp 12393  df-fz 12896  df-hash 13694  df-vdwap 16306  df-vdwmc 16307  df-vdwpc 16308
This theorem is referenced by:  vdwlem7  16325
  Copyright terms: Public domain W3C validator