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

Theorem vdwlem6 17019
Description: Lemma for vdw 17027. (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 6919 . . . . . . 7 (𝐺‘(𝐵 + (𝐸𝑖))) ∈ V
2 vdwlem6.j . . . . . . 7 𝐽 = (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝐵 + (𝐸𝑖))))
31, 2fnmpti 6711 . . . . . 6 𝐽 Fn (1...𝑀)
4 fvelrnb 6968 . . . . . 6 (𝐽 Fn (1...𝑀) → ((𝐺𝐵) ∈ ran 𝐽 ↔ ∃𝑚 ∈ (1...𝑀)(𝐽𝑚) = (𝐺𝐵)))
53, 4ax-mp 5 . . . . 5 ((𝐺𝐵) ∈ ran 𝐽 ↔ ∃𝑚 ∈ (1...𝑀)(𝐽𝑚) = (𝐺𝐵))
6 vdwlem4.r . . . . . . . 8 (𝜑𝑅 ∈ Fin)
76adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝑅 ∈ Fin)
8 vdwlem7.k . . . . . . . . 9 (𝜑𝐾 ∈ (ℤ‘2))
9 eluz2nn 12921 . . . . . . . . 9 (𝐾 ∈ (ℤ‘2) → 𝐾 ∈ ℕ)
108, 9syl 17 . . . . . . . 8 (𝜑𝐾 ∈ ℕ)
1110adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝐾 ∈ ℕ)
12 vdwlem3.w . . . . . . . 8 (𝜑𝑊 ∈ ℕ)
1312adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝑊 ∈ ℕ)
14 vdwlem7.g . . . . . . . 8 (𝜑𝐺:(1...𝑊)⟶𝑅)
1514adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝐺:(1...𝑊)⟶𝑅)
16 vdwlem6.b . . . . . . . 8 (𝜑𝐵 ∈ ℕ)
1716adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝐵 ∈ ℕ)
18 vdwlem7.m . . . . . . . 8 (𝜑𝑀 ∈ ℕ)
1918adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝑀 ∈ ℕ)
20 vdwlem6.e . . . . . . . 8 (𝜑𝐸:(1...𝑀)⟶ℕ)
2120adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝐸:(1...𝑀)⟶ℕ)
22 vdwlem6.s . . . . . . . 8 (𝜑 → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
2322adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
24 simprl 771 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝑚 ∈ (1...𝑀))
25 simprr 773 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐽𝑚) = (𝐺𝐵))
26 fveq2 6906 . . . . . . . . . . . 12 (𝑖 = 𝑚 → (𝐸𝑖) = (𝐸𝑚))
2726oveq2d 7446 . . . . . . . . . . 11 (𝑖 = 𝑚 → (𝐵 + (𝐸𝑖)) = (𝐵 + (𝐸𝑚)))
2827fveq2d 6910 . . . . . . . . . 10 (𝑖 = 𝑚 → (𝐺‘(𝐵 + (𝐸𝑖))) = (𝐺‘(𝐵 + (𝐸𝑚))))
29 fvex 6919 . . . . . . . . . 10 (𝐺‘(𝐵 + (𝐸𝑚))) ∈ V
3028, 2, 29fvmpt 7015 . . . . . . . . 9 (𝑚 ∈ (1...𝑀) → (𝐽𝑚) = (𝐺‘(𝐵 + (𝐸𝑚))))
3124, 30syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐽𝑚) = (𝐺‘(𝐵 + (𝐸𝑚))))
3225, 31eqtr3d 2776 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐺𝐵) = (𝐺‘(𝐵 + (𝐸𝑚))))
337, 11, 13, 15, 17, 19, 21, 23, 24, 32vdwlem1 17014 . . . . . 6 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐾 + 1) MonoAP 𝐺)
3433rexlimdvaa 3153 . . . . 5 (𝜑 → (∃𝑚 ∈ (1...𝑀)(𝐽𝑚) = (𝐺𝐵) → (𝐾 + 1) MonoAP 𝐺))
355, 34biimtrid 242 . . . 4 (𝜑 → ((𝐺𝐵) ∈ ran 𝐽 → (𝐾 + 1) MonoAP 𝐺))
3635imp 406 . . 3 ((𝜑 ∧ (𝐺𝐵) ∈ ran 𝐽) → (𝐾 + 1) MonoAP 𝐺)
3736olcd 874 . 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 17018 . . . . . 6 (𝜑𝑇 ∈ ℕ)
4847adantr 480 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑇 ∈ ℕ)
49 0nn0 12538 . . . . . . . . . 10 0 ∈ ℕ0
5049a1i 11 . . . . . . . . 9 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 = (𝑀 + 1)) → 0 ∈ ℕ0)
51 nnuz 12918 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
5218, 51eleqtrdi 2848 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ (ℤ‘1))
5352adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑀 ∈ (ℤ‘1))
54 elfzp1 13610 . . . . . . . . . . . . . . 15 (𝑀 ∈ (ℤ‘1) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1))))
5553, 54syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1))))
5655biimpa 476 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1)))
5756ord 864 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 ∈ (1...𝑀) → 𝑗 = (𝑀 + 1)))
5857con1d 145 . . . . . . . . . . 11 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 = (𝑀 + 1) → 𝑗 ∈ (1...𝑀)))
5958imp 406 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → 𝑗 ∈ (1...𝑀))
6020ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → 𝐸:(1...𝑀)⟶ℕ)
6160ffvelcdmda 7103 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸𝑗) ∈ ℕ)
6261nnnn0d 12584 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸𝑗) ∈ ℕ0)
6359, 62syldan 591 . . . . . . . . 9 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → (𝐸𝑗) ∈ ℕ0)
6450, 63ifclda 4565 . . . . . . . 8 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) ∈ ℕ0)
6512, 42nnmulcld 12316 . . . . . . . . 9 (𝜑 → (𝑊 · 𝐷) ∈ ℕ)
6665ad2antrr 726 . . . . . . . 8 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑊 · 𝐷) ∈ ℕ)
67 nn0nnaddcl 12554 . . . . . . . 8 ((if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) ∈ ℕ0 ∧ (𝑊 · 𝐷) ∈ ℕ) → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
6864, 66, 67syl2anc 584 . . . . . . 7 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
6968, 46fmptd 7133 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑃:(1...(𝑀 + 1))⟶ℕ)
70 nnex 12269 . . . . . . 7 ℕ ∈ V
71 ovex 7463 . . . . . . 7 (1...(𝑀 + 1)) ∈ V
7270, 71elmap 8909 . . . . . 6 (𝑃 ∈ (ℕ ↑m (1...(𝑀 + 1))) ↔ 𝑃:(1...(𝑀 + 1))⟶ℕ)
7369, 72sylibr 234 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑃 ∈ (ℕ ↑m (1...(𝑀 + 1))))
74 elfzp1 13610 . . . . . . . . . 10 (𝑀 ∈ (ℤ‘1) → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1))))
7552, 74syl 17 . . . . . . . . 9 (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1))))
7616adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℕ)
7776nncnd 12279 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℂ)
7877adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ)
7920ffvelcdmda 7103 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐸𝑖) ∈ ℕ)
8079nncnd 12279 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐸𝑖) ∈ ℂ)
8180adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐸𝑖) ∈ ℂ)
8278, 81addcld 11277 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝐸𝑖)) ∈ ℂ)
83 nnm1nn0 12564 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ ℕ → (𝐴 − 1) ∈ ℕ0)
8441, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐴 − 1) ∈ ℕ0)
85 nn0nnaddcl 12554 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 − 1) ∈ ℕ0𝑉 ∈ ℕ) → ((𝐴 − 1) + 𝑉) ∈ ℕ)
8684, 38, 85syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℕ)
8712, 86nnmulcld 12316 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
8887nncnd 12279 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
8988ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
90 elfznn0 13656 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ (0...(𝐾 − 1)) → 𝑚 ∈ ℕ0)
9190adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℕ0)
9291nn0cnd 12586 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
9392adantlr 715 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
9493, 81mulcld 11278 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝐸𝑖)) ∈ ℂ)
9565nnnn0d 12584 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑊 · 𝐷) ∈ ℕ0)
9695adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℕ0)
9791, 96nn0mulcld 12589 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℕ0)
9897nn0cnd 12586 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
9998adantlr 715 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
10082, 89, 94, 99add4d 11487 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸𝑖)) + (𝑚 · (𝑊 · 𝐷)))) = (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
10165nncnd 12279 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑊 · 𝐷) ∈ ℂ)
102101ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℂ)
10393, 81, 102adddid 11282 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))) = ((𝑚 · (𝐸𝑖)) + (𝑚 · (𝑊 · 𝐷))))
104103oveq2d 7446 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸𝑖)) + (𝑚 · (𝑊 · 𝐷)))))
10512nncnd 12279 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑊 ∈ ℂ)
106105adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℂ)
10786nncnd 12279 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℂ)
108107adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 − 1) + 𝑉) ∈ ℂ)
10942nncnd 12279 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐷 ∈ ℂ)
110109adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐷 ∈ ℂ)
11192, 110mulcld 11278 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · 𝐷) ∈ ℂ)
112106, 108, 111adddid 11282 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
11341nncnd 12279 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐴 ∈ ℂ)
114113adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐴 ∈ ℂ)
115 1cnd 11253 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 1 ∈ ℂ)
116114, 111, 115addsubd 11638 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) − 1) = ((𝐴 − 1) + (𝑚 · 𝐷)))
117116oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉))
11884nn0cnd 12586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 − 1) ∈ ℂ)
119118adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 − 1) ∈ ℂ)
12038nncnd 12279 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑉 ∈ ℂ)
121120adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℂ)
122119, 111, 121add32d 11486 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
123117, 122eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
124123oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))))
12592, 106, 110mul12d 11467 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) = (𝑊 · (𝑚 · 𝐷)))
126125oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
127112, 124, 1263eqtr4d 2784 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
128127adantlr 715 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
129128oveq2d 7446 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
130100, 104, 1293eqtr4d 2784 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
13138ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
13212ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
13343adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴(AP‘𝐾)𝐷) ⊆ (𝐹 “ {𝐺}))
134 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))
135 oveq1 7437 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑚 → (𝑛 · 𝐷) = (𝑚 · 𝐷))
136135oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → (𝐴 + (𝑛 · 𝐷)) = (𝐴 + (𝑚 · 𝐷)))
137136rspceeqv 3644 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 ∈ (0...(𝐾 − 1)) ∧ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
138134, 137mpan2 691 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
13910nnnn0d 12584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐾 ∈ ℕ0)
140 vdwapval 17006 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
141139, 41, 42, 140syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
142141biimpar 477 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
143138, 142sylan2 593 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
144133, 143sseldd 3995 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺}))
14538, 12, 6, 39, 40vdwlem4 17017 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹:(1...𝑉)⟶(𝑅m (1...𝑊)))
146145ffnd 6737 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹 Fn (1...𝑉))
147 fniniseg 7079 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 Fn (1...𝑉) → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
148146, 147syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
149148biimpa 476 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺})) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
150144, 149syldan 591 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
151150simpld 494 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
152151adantlr 715 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
15322r19.21bi 3248 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
154153adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
155 eqid 2734 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))
156 oveq1 7437 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → (𝑛 · (𝐸𝑖)) = (𝑚 · (𝐸𝑖)))
157156oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑚 → ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))))
158157rspceeqv 3644 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚 ∈ (0...(𝐾 − 1)) ∧ ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖))))
159155, 158mpan2 691 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖))))
16010adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ)
161160nnnn0d 12584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ0)
16276, 79nnaddcld 12315 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ ℕ)
163 vdwapval 17006 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐾 ∈ ℕ0 ∧ (𝐵 + (𝐸𝑖)) ∈ ℕ ∧ (𝐸𝑖) ∈ ℕ) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖)))))
164161, 162, 79, 163syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖)))))
165164biimpar 477 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖 ∈ (1...𝑀)) ∧ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖)))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
166159, 165sylan2 593 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
167154, 166sseldd 3995 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
16814ffnd 6737 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐺 Fn (1...𝑊))
169168adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐺 Fn (1...𝑊))
170 fniniseg 7079 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 Fn (1...𝑊) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖))))))
171169, 170syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖))))))
172171biimpa 476 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))})) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
173167, 172syldan 591 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
174173simpld 494 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊))
175131, 132, 152, 174vdwlem3 17016 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
176130, 175eqeltrd 2838 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))))
177 fvoveq1 7453 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
178 eqid 2734 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
179 fvex 6919 . . . . . . . . . . . . . . . . . . . 20 (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
180177, 178, 179fvmpt 7015 . . . . . . . . . . . . . . . . . . 19 (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
181174, 180syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
182173simprd 495 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖))))
183150simprd 495 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)
184 oveq1 7437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑥 − 1) = ((𝐴 + (𝑚 · 𝐷)) − 1))
185184oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → ((𝑥 − 1) + 𝑉) = (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))
186185oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))
187186oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
188187fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
189188mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
190 ovex 7463 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1...𝑊) ∈ V
191190mptex 7242 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) ∈ V
192189, 40, 191fvmpt 7015 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
193151, 192syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
194183, 193eqtr3d 2776 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
195194adantlr 715 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
196195fveq1d 6908 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))))
197182, 196eqtr3d 2776 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘(𝐵 + (𝐸𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))))
198130fveq2d 6910 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
199181, 197, 1983eqtr4rd 2785 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖))))
200176, 199jca 511 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
201 eleq1 2826 . . . . . . . . . . . . . . . . 17 (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉)))))
202 fveqeq2 6915 . . . . . . . . . . . . . . . . 17 (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → ((𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))) ↔ (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
203201, 202anbi12d 632 . . . . . . . . . . . . . . . 16 (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → ((𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖)))) ↔ ((((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖))))))
204200, 203syl5ibrcom 247 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
205204rexlimdva 3152 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
20687adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
207162, 206nnaddcld 12315 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
20865adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℕ)
20979, 208nnaddcld 12315 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + (𝑊 · 𝐷)) ∈ ℕ)
210 vdwapval 17006 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℕ0 ∧ ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ ((𝐸𝑖) + (𝑊 · 𝐷)) ∈ ℕ) → (𝑥 ∈ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))))
211161, 207, 209, 210syl3anc 1370 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))))
21239ffnd 6737 . . . . . . . . . . . . . . . 16 (𝜑𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
213212adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
214 fniniseg 7079 . . . . . . . . . . . . . . 15 (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑥 ∈ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
215213, 214syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
216205, 211, 2153imtr4d 294 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) → 𝑥 ∈ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))})))
217216ssrdv 4000 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) ⊆ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
218 ssun1 4187 . . . . . . . . . . . . . . . . . . 19 (1...𝑀) ⊆ ((1...𝑀) ∪ {(𝑀 + 1)})
219 fzsuc 13607 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (ℤ‘1) → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
22052, 219syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
221218, 220sseqtrrid 4048 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1...𝑀) ⊆ (1...(𝑀 + 1)))
222221sselda 3994 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...(𝑀 + 1)))
223 eqeq1 2738 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝑗 = (𝑀 + 1) ↔ 𝑖 = (𝑀 + 1)))
224 fveq2 6906 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝐸𝑗) = (𝐸𝑖))
225223, 224ifbieq2d 4556 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) = if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)))
226225oveq1d 7445 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) = (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)))
227 ovex 7463 . . . . . . . . . . . . . . . . . 18 (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)) ∈ V
228226, 46, 227fvmpt 7015 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...(𝑀 + 1)) → (𝑃𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)))
229222, 228syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑃𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)))
23018nnred 12278 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑀 ∈ ℝ)
231230ltp1d 12195 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑀 < (𝑀 + 1))
232 peano2re 11431 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
233230, 232syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑀 + 1) ∈ ℝ)
234230, 233ltnled 11405 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀))
235231, 234mpbid 232 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀)
236 breq1 5150 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = (𝑀 + 1) → (𝑖𝑀 ↔ (𝑀 + 1) ≤ 𝑀))
237236notbid 318 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = (𝑀 + 1) → (¬ 𝑖𝑀 ↔ ¬ (𝑀 + 1) ≤ 𝑀))
238235, 237syl5ibrcom 247 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑖 = (𝑀 + 1) → ¬ 𝑖𝑀))
239238con2d 134 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑖𝑀 → ¬ 𝑖 = (𝑀 + 1)))
240 elfzle2 13564 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑀) → 𝑖𝑀)
241239, 240impel 505 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → ¬ 𝑖 = (𝑀 + 1))
242 iffalse 4539 . . . . . . . . . . . . . . . . . 18 𝑖 = (𝑀 + 1) → if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) = (𝐸𝑖))
243242oveq1d 7445 . . . . . . . . . . . . . . . . 17 𝑖 = (𝑀 + 1) → (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)) = ((𝐸𝑖) + (𝑊 · 𝐷)))
244241, 243syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)) = ((𝐸𝑖) + (𝑊 · 𝐷)))
245229, 244eqtrd 2774 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑃𝑖) = ((𝐸𝑖) + (𝑊 · 𝐷)))
246245oveq2d 7446 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃𝑖)) = (𝑇 + ((𝐸𝑖) + (𝑊 · 𝐷))))
24747nncnd 12279 . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ ℂ)
248247adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑇 ∈ ℂ)
249101adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℂ)
250248, 80, 249add12d 11485 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑇 + ((𝐸𝑖) + (𝑊 · 𝐷))) = ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))))
25145oveq1i 7440 . . . . . . . . . . . . . . . . . 18 (𝑇 + (𝑊 · 𝐷)) = ((𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1))) + (𝑊 · 𝐷))
25216nncnd 12279 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℂ)
253120, 109subcld 11617 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑉𝐷) ∈ ℂ)
254113, 253addcld 11277 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 + (𝑉𝐷)) ∈ ℂ)
255 ax-1cn 11210 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℂ
256 subcl 11504 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 + (𝑉𝐷)) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 + (𝑉𝐷)) − 1) ∈ ℂ)
257254, 255, 256sylancl 586 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 + (𝑉𝐷)) − 1) ∈ ℂ)
258105, 257mulcld 11278 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) ∈ ℂ)
259252, 258, 101addassd 11280 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷))))
260105, 257, 109adddid 11282 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑊 · (((𝐴 + (𝑉𝐷)) − 1) + 𝐷)) = ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷)))
261113, 253, 109addassd 11280 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 + (𝑉𝐷)) + 𝐷) = (𝐴 + ((𝑉𝐷) + 𝐷)))
262120, 109npcand 11621 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑉𝐷) + 𝐷) = 𝑉)
263262oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐴 + ((𝑉𝐷) + 𝐷)) = (𝐴 + 𝑉))
264261, 263eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐴 + (𝑉𝐷)) + 𝐷) = (𝐴 + 𝑉))
265264oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝐴 + (𝑉𝐷)) + 𝐷) − 1) = ((𝐴 + 𝑉) − 1))
266 1cnd 11253 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ∈ ℂ)
267254, 109, 266addsubd 11638 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝐴 + (𝑉𝐷)) + 𝐷) − 1) = (((𝐴 + (𝑉𝐷)) − 1) + 𝐷))
268113, 120, 266addsubd 11638 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 + 𝑉) − 1) = ((𝐴 − 1) + 𝑉))
269265, 267, 2683eqtr3d 2782 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐴 + (𝑉𝐷)) − 1) + 𝐷) = ((𝐴 − 1) + 𝑉))
270269oveq2d 7446 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑊 · (((𝐴 + (𝑉𝐷)) − 1) + 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
271260, 270eqtr3d 2776 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
272271oveq2d 7446 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵 + ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
273259, 272eqtrd 2774 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
274251, 273eqtrid 2786 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑇 + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
275274oveq2d 7446 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
276275adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
27788adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
27880, 77, 277addassd 11280 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐸𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐸𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
27980, 77addcomd 11460 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + 𝐵) = (𝐵 + (𝐸𝑖)))
280279oveq1d 7445 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐸𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
281276, 278, 2803eqtr2d 2780 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
282246, 250, 2813eqtrd 2778 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃𝑖)) = ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
283282, 245oveq12d 7448 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))))
284 cnvimass 6101 . . . . . . . . . . . . . . . . . . 19 (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ⊆ dom 𝐺
285284, 14fssdm 6755 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ⊆ (1...𝑊))
286285adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ⊆ (1...𝑊))
287 vdwapid1 17008 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ ℕ ∧ (𝐵 + (𝐸𝑖)) ∈ ℕ ∧ (𝐸𝑖) ∈ ℕ) → (𝐵 + (𝐸𝑖)) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
288160, 162, 79, 287syl3anc 1370 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
289153, 288sseldd 3995 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
290286, 289sseldd 3995 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ (1...𝑊))
291 fvoveq1 7453 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝐵 + (𝐸𝑖)) → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
292 eqid 2734 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
293 fvex 6919 . . . . . . . . . . . . . . . . 17 (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
294291, 292, 293fvmpt 7015 . . . . . . . . . . . . . . . 16 ((𝐵 + (𝐸𝑖)) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
295290, 294syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
296 vdwapid1 17008 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
29710, 41, 42, 296syl3anc 1370 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
29843, 297sseldd 3995 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ (𝐹 “ {𝐺}))
299 fniniseg 7079 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn (1...𝑉) → (𝐴 ∈ (𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹𝐴) = 𝐺)))
300146, 299syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐴 ∈ (𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹𝐴) = 𝐺)))
301298, 300mpbid 232 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 ∈ (1...𝑉) ∧ (𝐹𝐴) = 𝐺))
302301simprd 495 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹𝐴) = 𝐺)
303301simpld 494 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ (1...𝑉))
304 oveq1 7437 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝐴 → (𝑥 − 1) = (𝐴 − 1))
305304oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝐴 → ((𝑥 − 1) + 𝑉) = ((𝐴 − 1) + 𝑉))
306305oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝐴 → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
307306oveq2d 7446 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝐴 → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))
308307fveq2d 6910 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝐴 → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
309308mpteq2dv 5249 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝐴 → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
310190mptex 7242 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) ∈ V
311309, 40, 310fvmpt 7015 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ (1...𝑉) → (𝐹𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
312303, 311syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
313302, 312eqtr3d 2776 . . . . . . . . . . . . . . . . 17 (𝜑𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
314313fveq1d 6908 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐺‘(𝐵 + (𝐸𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))))
315314adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐵 + (𝐸𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))))
316282fveq2d 6910 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃𝑖))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
317295, 315, 3163eqtr4rd 2785 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃𝑖))) = (𝐺‘(𝐵 + (𝐸𝑖))))
318317sneqd 4642 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → {(𝐻‘(𝑇 + (𝑃𝑖)))} = {(𝐺‘(𝐵 + (𝐸𝑖)))})
319318imaeq2d 6079 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) = (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
320217, 283, 3193sstr4d 4042 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
321320ex 412 . . . . . . . . . 10 (𝜑 → (𝑖 ∈ (1...𝑀) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
322252adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ)
32388adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
324322, 323, 98addassd 11280 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
325127oveq2d 7446 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
326324, 325eqtr4d 2777 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
32738adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
32812adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
329 eluzfz1 13567 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ (ℤ‘1) → 1 ∈ (1...𝑀))
33052, 329syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ∈ (1...𝑀))
331330ne0d 4347 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑀) ≠ ∅)
332 elfzuz3 13557 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 + (𝐸𝑖)) ∈ (1...𝑊) → 𝑊 ∈ (ℤ‘(𝐵 + (𝐸𝑖))))
333290, 332syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ‘(𝐵 + (𝐸𝑖))))
33416nnzd 12637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐵 ∈ ℤ)
335 uzid 12890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵 ∈ ℤ → 𝐵 ∈ (ℤ𝐵))
336334, 335syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ∈ (ℤ𝐵))
337336adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵 ∈ (ℤ𝐵))
33879nnnn0d 12584 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐸𝑖) ∈ ℕ0)
339 uzaddcl 12943 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ∈ (ℤ𝐵) ∧ (𝐸𝑖) ∈ ℕ0) → (𝐵 + (𝐸𝑖)) ∈ (ℤ𝐵))
340337, 338, 339syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ (ℤ𝐵))
341 uztrn 12893 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑊 ∈ (ℤ‘(𝐵 + (𝐸𝑖))) ∧ (𝐵 + (𝐸𝑖)) ∈ (ℤ𝐵)) → 𝑊 ∈ (ℤ𝐵))
342333, 340, 341syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ𝐵))
343 eluzle 12888 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑊 ∈ (ℤ𝐵) → 𝐵𝑊)
344342, 343syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵𝑊)
345344ralrimiva 3143 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑖 ∈ (1...𝑀)𝐵𝑊)
346 r19.2z 4500 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...𝑀) ≠ ∅ ∧ ∀𝑖 ∈ (1...𝑀)𝐵𝑊) → ∃𝑖 ∈ (1...𝑀)𝐵𝑊)
347331, 345, 346syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∃𝑖 ∈ (1...𝑀)𝐵𝑊)
348 idd 24 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (1...𝑀) → (𝐵𝑊𝐵𝑊))
349348rexlimiv 3145 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑖 ∈ (1...𝑀)𝐵𝑊𝐵𝑊)
350347, 349syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵𝑊)
35112nnzd 12637 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑊 ∈ ℤ)
352 fznn 13628 . . . . . . . . . . . . . . . . . . . . . 22 (𝑊 ∈ ℤ → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵𝑊)))
353351, 352syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵𝑊)))
35416, 350, 353mpbir2and 713 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ (1...𝑊))
355354adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ (1...𝑊))
356327, 328, 151, 355vdwlem3 17016 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
357326, 356eqeltrd 2838 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))))
358 fvoveq1 7453 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
359 fvex 6919 . . . . . . . . . . . . . . . . . . . 20 (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
360358, 178, 359fvmpt 7015 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
361355, 360syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
362194fveq1d 6908 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐺𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵))
363326fveq2d 6910 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
364361, 362, 3633eqtr4rd 2785 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵))
365357, 364jca 511 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵)))
366 eleq1 2826 . . . . . . . . . . . . . . . . 17 (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉)))))
367 fveqeq2 6915 . . . . . . . . . . . . . . . . 17 (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝐻𝑧) = (𝐺𝐵) ↔ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵)))
368366, 367anbi12d 632 . . . . . . . . . . . . . . . 16 (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵)) ↔ (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵))))
369365, 368syl5ibrcom 247 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
370369rexlimdva 3152 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
37116, 87nnaddcld 12315 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
372 vdwapval 17006 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℕ0 ∧ (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ (𝑊 · 𝐷) ∈ ℕ) → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
373139, 371, 65, 372syl3anc 1370 . . . . . . . . . . . . . 14 (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
374 fniniseg 7079 . . . . . . . . . . . . . . 15 (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑧 ∈ (𝐻 “ {(𝐺𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
375212, 374syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑧 ∈ (𝐻 “ {(𝐺𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
376370, 373, 3753imtr4d 294 . . . . . . . . . . . . 13 (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) → 𝑧 ∈ (𝐻 “ {(𝐺𝐵)})))
377376ssrdv 4000 . . . . . . . . . . . 12 (𝜑 → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ⊆ (𝐻 “ {(𝐺𝐵)}))
37818peano2nnd 12280 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 + 1) ∈ ℕ)
379378, 51eleqtrdi 2848 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 + 1) ∈ (ℤ‘1))
380 eluzfz2 13568 . . . . . . . . . . . . . . . . 17 ((𝑀 + 1) ∈ (ℤ‘1) → (𝑀 + 1) ∈ (1...(𝑀 + 1)))
381 iftrue 4536 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑀 + 1) → if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) = 0)
382381oveq1d 7445 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑀 + 1) → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) = (0 + (𝑊 · 𝐷)))
383 ovex 7463 . . . . . . . . . . . . . . . . . 18 (0 + (𝑊 · 𝐷)) ∈ V
384382, 46, 383fvmpt 7015 . . . . . . . . . . . . . . . . 17 ((𝑀 + 1) ∈ (1...(𝑀 + 1)) → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
385379, 380, 3843syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
386101addlidd 11459 . . . . . . . . . . . . . . . 16 (𝜑 → (0 + (𝑊 · 𝐷)) = (𝑊 · 𝐷))
387385, 386eqtrd 2774 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃‘(𝑀 + 1)) = (𝑊 · 𝐷))
388387oveq2d 7446 . . . . . . . . . . . . . 14 (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝑇 + (𝑊 · 𝐷)))
389388, 274eqtrd 2774 . . . . . . . . . . . . 13 (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
390389, 387oveq12d 7448 . . . . . . . . . . . 12 (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)))
391 fvoveq1 7453 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
392 fvex 6919 . . . . . . . . . . . . . . . . 17 (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
393391, 292, 392fvmpt 7015 . . . . . . . . . . . . . . . 16 (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
394354, 393syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
395313fveq1d 6908 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵))
396389fveq2d 6910 . . . . . . . . . . . . . . 15 (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
397394, 395, 3963eqtr4rd 2785 . . . . . . . . . . . . . 14 (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐺𝐵))
398397sneqd 4642 . . . . . . . . . . . . 13 (𝜑 → {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))} = {(𝐺𝐵)})
399398imaeq2d 6079 . . . . . . . . . . . 12 (𝜑 → (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}) = (𝐻 “ {(𝐺𝐵)}))
400377, 390, 3993sstr4d 4042 . . . . . . . . . . 11 (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
401 fveq2 6906 . . . . . . . . . . . . . 14 (𝑖 = (𝑀 + 1) → (𝑃𝑖) = (𝑃‘(𝑀 + 1)))
402401oveq2d 7446 . . . . . . . . . . . . 13 (𝑖 = (𝑀 + 1) → (𝑇 + (𝑃𝑖)) = (𝑇 + (𝑃‘(𝑀 + 1))))
403402, 401oveq12d 7448 . . . . . . . . . . . 12 (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) = ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))))
404402fveq2d 6910 . . . . . . . . . . . . . 14 (𝑖 = (𝑀 + 1) → (𝐻‘(𝑇 + (𝑃𝑖))) = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
405404sneqd 4642 . . . . . . . . . . . . 13 (𝑖 = (𝑀 + 1) → {(𝐻‘(𝑇 + (𝑃𝑖)))} = {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})
406405imaeq2d 6079 . . . . . . . . . . . 12 (𝑖 = (𝑀 + 1) → (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) = (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
407403, 406sseq12d 4028 . . . . . . . . . . 11 (𝑖 = (𝑀 + 1) → (((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) ↔ ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})))
408400, 407syl5ibrcom 247 . . . . . . . . . 10 (𝜑 → (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
409321, 408jaod 859 . . . . . . . . 9 (𝜑 → ((𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
41075, 409sylbid 240 . . . . . . . 8 (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
411410ralrimiv 3142 . . . . . . 7 (𝜑 → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
412411adantr 480 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
413220rexeqdv 3324 . . . . . . . . . . . 12 (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ ∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))))
414 rexun 4205 . . . . . . . . . . . . 13 (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))))
415317eqeq2d 2745 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))))
416415rexbidva 3174 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))))
417 ovex 7463 . . . . . . . . . . . . . . . 16 (𝑀 + 1) ∈ V
418404eqeq2d 2745 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑀 + 1) → (𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))))
419417, 418rexsn 4686 . . . . . . . . . . . . . . 15 (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
420397eqeq2d 2745 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) ↔ 𝑥 = (𝐺𝐵)))
421419, 420bitrid 283 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐺𝐵)))
422416, 421orbi12d 918 . . . . . . . . . . . . 13 (𝜑 → ((∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))))
423414, 422bitrid 283 . . . . . . . . . . . 12 (𝜑 → (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))))
424413, 423bitrd 279 . . . . . . . . . . 11 (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))))
425424adantr 480 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))))
426425abbidv 2805 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))} = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))})
427 eqid 2734 . . . . . . . . . 10 (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))
428427rnmpt 5970 . . . . . . . . 9 ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))) = {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))}
4292rnmpt 5970 . . . . . . . . . . 11 ran 𝐽 = {𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))}
430 df-sn 4631 . . . . . . . . . . 11 {(𝐺𝐵)} = {𝑥𝑥 = (𝐺𝐵)}
431429, 430uneq12i 4175 . . . . . . . . . 10 (ran 𝐽 ∪ {(𝐺𝐵)}) = ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))} ∪ {𝑥𝑥 = (𝐺𝐵)})
432 unab 4313 . . . . . . . . . 10 ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))} ∪ {𝑥𝑥 = (𝐺𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))}
433431, 432eqtri 2762 . . . . . . . . 9 (ran 𝐽 ∪ {(𝐺𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))}
434426, 428, 4333eqtr4g 2799 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))) = (ran 𝐽 ∪ {(𝐺𝐵)}))
435434fveq2d 6910 . . . . . . 7 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (♯‘(ran 𝐽 ∪ {(𝐺𝐵)})))
436 fzfi 14009 . . . . . . . . . 10 (1...𝑀) ∈ Fin
437 dffn4 6826 . . . . . . . . . . 11 (𝐽 Fn (1...𝑀) ↔ 𝐽:(1...𝑀)–onto→ran 𝐽)
4383, 437mpbi 230 . . . . . . . . . 10 𝐽:(1...𝑀)–onto→ran 𝐽
439 fofi 9348 . . . . . . . . . 10 (((1...𝑀) ∈ Fin ∧ 𝐽:(1...𝑀)–onto→ran 𝐽) → ran 𝐽 ∈ Fin)
440436, 438, 439mp2an 692 . . . . . . . . 9 ran 𝐽 ∈ Fin
441440a1i 11 . . . . . . . 8 (𝜑 → ran 𝐽 ∈ Fin)
442 fvex 6919 . . . . . . . . 9 (𝐺𝐵) ∈ V
443 hashunsng 14427 . . . . . . . . 9 ((𝐺𝐵) ∈ V → ((ran 𝐽 ∈ Fin ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺𝐵)})) = ((♯‘ran 𝐽) + 1)))
444442, 443ax-mp 5 . . . . . . . 8 ((ran 𝐽 ∈ Fin ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺𝐵)})) = ((♯‘ran 𝐽) + 1))
445441, 444sylan 580 . . . . . . 7 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺𝐵)})) = ((♯‘ran 𝐽) + 1))
44644adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘ran 𝐽) = 𝑀)
447446oveq1d 7445 . . . . . . 7 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ((♯‘ran 𝐽) + 1) = (𝑀 + 1))
448435, 445, 4473eqtrd 2778 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1))
449412, 448jca 511 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1)))
450 oveq1 7437 . . . . . . . . . 10 (𝑎 = 𝑇 → (𝑎 + (𝑑𝑖)) = (𝑇 + (𝑑𝑖)))
451450oveq1d 7445 . . . . . . . . 9 (𝑎 = 𝑇 → ((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) = ((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)))
452 fvoveq1 7453 . . . . . . . . . . 11 (𝑎 = 𝑇 → (𝐻‘(𝑎 + (𝑑𝑖))) = (𝐻‘(𝑇 + (𝑑𝑖))))
453452sneqd 4642 . . . . . . . . . 10 (𝑎 = 𝑇 → {(𝐻‘(𝑎 + (𝑑𝑖)))} = {(𝐻‘(𝑇 + (𝑑𝑖)))})
454453imaeq2d 6079 . . . . . . . . 9 (𝑎 = 𝑇 → (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) = (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}))
455451, 454sseq12d 4028 . . . . . . . 8 (𝑎 = 𝑇 → (((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ↔ ((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))})))
456455ralbidv 3175 . . . . . . 7 (𝑎 = 𝑇 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))})))
457452mpteq2dv 5249 . . . . . . . . 9 (𝑎 = 𝑇 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))))
458457rneqd 5951 . . . . . . . 8 (𝑎 = 𝑇 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))))
459458fveqeq2d 6914 . . . . . . 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 6905 . . . . . . . . . . 11 (𝑑 = 𝑃 → (𝑑𝑖) = (𝑃𝑖))
462461oveq2d 7446 . . . . . . . . . 10 (𝑑 = 𝑃 → (𝑇 + (𝑑𝑖)) = (𝑇 + (𝑃𝑖)))
463462, 461oveq12d 7448 . . . . . . . . 9 (𝑑 = 𝑃 → ((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) = ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)))
464462fveq2d 6910 . . . . . . . . . . 11 (𝑑 = 𝑃 → (𝐻‘(𝑇 + (𝑑𝑖))) = (𝐻‘(𝑇 + (𝑃𝑖))))
465464sneqd 4642 . . . . . . . . . 10 (𝑑 = 𝑃 → {(𝐻‘(𝑇 + (𝑑𝑖)))} = {(𝐻‘(𝑇 + (𝑃𝑖)))})
466465imaeq2d 6079 . . . . . . . . 9 (𝑑 = 𝑃 → (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) = (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
467463, 466sseq12d 4028 . . . . . . . 8 (𝑑 = 𝑃 → (((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ↔ ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
468467ralbidv 3175 . . . . . . 7 (𝑑 = 𝑃 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
469464mpteq2dv 5249 . . . . . . . . 9 (𝑑 = 𝑃 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))))
470469rneqd 5951 . . . . . . . 8 (𝑑 = 𝑃 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))))
471470fveqeq2d 6914 . . . . . . 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 3634 . . . . 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 1370 . . . 4 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1)))
475 ovex 7463 . . . . 5 (1...(𝑊 · (2 · 𝑉))) ∈ V
47610adantr 480 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ)
477476nnnn0d 12584 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ0)
47839adantr 480 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
47918adantr 480 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑀 ∈ ℕ)
480479peano2nnd 12280 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (𝑀 + 1) ∈ ℕ)
481 eqid 2734 . . . . 5 (1...(𝑀 + 1)) = (1...(𝑀 + 1))
482475, 477, 478, 480, 481vdwpc 17013 . . . 4 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1))))
483474, 482mpbird 257 . . 3 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻)
484483orcd 873 . 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 206  wa 395  wo 847   = wceq 1536  wcel 2105  {cab 2711  wne 2937  wral 3058  wrex 3067  Vcvv 3477  cun 3960  wss 3962  c0 4338  ifcif 4530  {csn 4630  cop 4636   class class class wbr 5147  cmpt 5230  ccnv 5687  ran crn 5689  cima 5691   Fn wfn 6557  wf 6558  ontowfo 6560  cfv 6562  (class class class)co 7430  m cmap 8864  Fincfn 8983  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157   < clt 11292  cle 11293  cmin 11489  cn 12263  2c2 12318  0cn0 12523  cz 12610  cuz 12875  ...cfz 13543  chash 14365  APcvdwa 16998   MonoAP cvdwm 16999   PolyAP cvdwp 17000
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-oadd 8508  df-er 8743  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-dju 9938  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-n0 12524  df-z 12611  df-uz 12876  df-rp 13032  df-fz 13544  df-hash 14366  df-vdwap 17001  df-vdwmc 17002  df-vdwpc 17003
This theorem is referenced by:  vdwlem7  17020
  Copyright terms: Public domain W3C validator