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

Theorem vdwlem6 17033
Description: Lemma for vdw 17041. (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 6933 . . . . . . 7 (𝐺‘(𝐵 + (𝐸𝑖))) ∈ V
2 vdwlem6.j . . . . . . 7 𝐽 = (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝐵 + (𝐸𝑖))))
31, 2fnmpti 6723 . . . . . 6 𝐽 Fn (1...𝑀)
4 fvelrnb 6982 . . . . . 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 12949 . . . . . . . . 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 770 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → 𝑚 ∈ (1...𝑀))
25 simprr 772 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐽𝑚) = (𝐺𝐵))
26 fveq2 6920 . . . . . . . . . . . 12 (𝑖 = 𝑚 → (𝐸𝑖) = (𝐸𝑚))
2726oveq2d 7464 . . . . . . . . . . 11 (𝑖 = 𝑚 → (𝐵 + (𝐸𝑖)) = (𝐵 + (𝐸𝑚)))
2827fveq2d 6924 . . . . . . . . . 10 (𝑖 = 𝑚 → (𝐺‘(𝐵 + (𝐸𝑖))) = (𝐺‘(𝐵 + (𝐸𝑚))))
29 fvex 6933 . . . . . . . . . 10 (𝐺‘(𝐵 + (𝐸𝑚))) ∈ V
3028, 2, 29fvmpt 7029 . . . . . . . . 9 (𝑚 ∈ (1...𝑀) → (𝐽𝑚) = (𝐺‘(𝐵 + (𝐸𝑚))))
3124, 30syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐽𝑚) = (𝐺‘(𝐵 + (𝐸𝑚))))
3225, 31eqtr3d 2782 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐺𝐵) = (𝐺‘(𝐵 + (𝐸𝑚))))
337, 11, 13, 15, 17, 19, 21, 23, 24, 32vdwlem1 17028 . . . . . 6 ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽𝑚) = (𝐺𝐵))) → (𝐾 + 1) MonoAP 𝐺)
3433rexlimdvaa 3162 . . . . 5 (𝜑 → (∃𝑚 ∈ (1...𝑀)(𝐽𝑚) = (𝐺𝐵) → (𝐾 + 1) MonoAP 𝐺))
355, 34biimtrid 242 . . . 4 (𝜑 → ((𝐺𝐵) ∈ ran 𝐽 → (𝐾 + 1) MonoAP 𝐺))
3635imp 406 . . 3 ((𝜑 ∧ (𝐺𝐵) ∈ ran 𝐽) → (𝐾 + 1) MonoAP 𝐺)
3736olcd 873 . 2 ((𝜑 ∧ (𝐺𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))
38 vdwlem3.v . . . . . . 7 (𝜑𝑉 ∈ ℕ)
39 vdwlem4.h . . . . . . 7 (𝜑𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
40 vdwlem4.f . . . . . . 7 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))))
41 vdwlem7.a . . . . . . 7 (𝜑𝐴 ∈ ℕ)
42 vdwlem7.d . . . . . . 7 (𝜑𝐷 ∈ ℕ)
43 vdwlem7.s . . . . . . 7 (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (𝐹 “ {𝐺}))
44 vdwlem6.r . . . . . . 7 (𝜑 → (♯‘ran 𝐽) = 𝑀)
45 vdwlem6.t . . . . . . 7 𝑇 = (𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1)))
46 vdwlem6.p . . . . . . 7 𝑃 = (𝑗 ∈ (1...(𝑀 + 1)) ↦ (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)))
4738, 12, 6, 39, 40, 18, 14, 8, 41, 42, 43, 16, 20, 22, 2, 44, 45, 46vdwlem5 17032 . . . . . 6 (𝜑𝑇 ∈ ℕ)
4847adantr 480 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑇 ∈ ℕ)
49 0nn0 12568 . . . . . . . . . 10 0 ∈ ℕ0
5049a1i 11 . . . . . . . . 9 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 = (𝑀 + 1)) → 0 ∈ ℕ0)
51 nnuz 12946 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
5218, 51eleqtrdi 2854 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ (ℤ‘1))
5352adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑀 ∈ (ℤ‘1))
54 elfzp1 13634 . . . . . . . . . . . . . . 15 (𝑀 ∈ (ℤ‘1) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1))))
5553, 54syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1))))
5655biimpa 476 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1)))
5756ord 863 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 ∈ (1...𝑀) → 𝑗 = (𝑀 + 1)))
5857con1d 145 . . . . . . . . . . 11 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 = (𝑀 + 1) → 𝑗 ∈ (1...𝑀)))
5958imp 406 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → 𝑗 ∈ (1...𝑀))
6020ad2antrr 725 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → 𝐸:(1...𝑀)⟶ℕ)
6160ffvelcdmda 7118 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸𝑗) ∈ ℕ)
6261nnnn0d 12613 . . . . . . . . . 10 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸𝑗) ∈ ℕ0)
6359, 62syldan 590 . . . . . . . . 9 ((((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → (𝐸𝑗) ∈ ℕ0)
6450, 63ifclda 4583 . . . . . . . 8 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) ∈ ℕ0)
6512, 42nnmulcld 12346 . . . . . . . . 9 (𝜑 → (𝑊 · 𝐷) ∈ ℕ)
6665ad2antrr 725 . . . . . . . 8 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑊 · 𝐷) ∈ ℕ)
67 nn0nnaddcl 12584 . . . . . . . 8 ((if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) ∈ ℕ0 ∧ (𝑊 · 𝐷) ∈ ℕ) → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
6864, 66, 67syl2anc 583 . . . . . . 7 (((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) ∈ ℕ)
6968, 46fmptd 7148 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑃:(1...(𝑀 + 1))⟶ℕ)
70 nnex 12299 . . . . . . 7 ℕ ∈ V
71 ovex 7481 . . . . . . 7 (1...(𝑀 + 1)) ∈ V
7270, 71elmap 8929 . . . . . 6 (𝑃 ∈ (ℕ ↑m (1...(𝑀 + 1))) ↔ 𝑃:(1...(𝑀 + 1))⟶ℕ)
7369, 72sylibr 234 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑃 ∈ (ℕ ↑m (1...(𝑀 + 1))))
74 elfzp1 13634 . . . . . . . . . 10 (𝑀 ∈ (ℤ‘1) → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1))))
7552, 74syl 17 . . . . . . . . 9 (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1))))
7616adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℕ)
7776nncnd 12309 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℂ)
7877adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ)
7920ffvelcdmda 7118 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐸𝑖) ∈ ℕ)
8079nncnd 12309 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐸𝑖) ∈ ℂ)
8180adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐸𝑖) ∈ ℂ)
8278, 81addcld 11309 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝐸𝑖)) ∈ ℂ)
83 nnm1nn0 12594 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ ℕ → (𝐴 − 1) ∈ ℕ0)
8441, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐴 − 1) ∈ ℕ0)
85 nn0nnaddcl 12584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐴 − 1) ∈ ℕ0𝑉 ∈ ℕ) → ((𝐴 − 1) + 𝑉) ∈ ℕ)
8684, 38, 85syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℕ)
8712, 86nnmulcld 12346 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
8887nncnd 12309 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
8988ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
90 elfznn0 13677 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ (0...(𝐾 − 1)) → 𝑚 ∈ ℕ0)
9190adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℕ0)
9291nn0cnd 12615 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
9392adantlr 714 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ)
9493, 81mulcld 11310 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝐸𝑖)) ∈ ℂ)
9565nnnn0d 12613 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑊 · 𝐷) ∈ ℕ0)
9695adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℕ0)
9791, 96nn0mulcld 12618 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℕ0)
9897nn0cnd 12615 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
9998adantlr 714 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ)
10082, 89, 94, 99add4d 11518 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸𝑖)) + (𝑚 · (𝑊 · 𝐷)))) = (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
10165nncnd 12309 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑊 · 𝐷) ∈ ℂ)
102101ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℂ)
10393, 81, 102adddid 11314 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))) = ((𝑚 · (𝐸𝑖)) + (𝑚 · (𝑊 · 𝐷))))
104103oveq2d 7464 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸𝑖)) + (𝑚 · (𝑊 · 𝐷)))))
10512nncnd 12309 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑊 ∈ ℂ)
106105adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℂ)
10786nncnd 12309 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℂ)
108107adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 − 1) + 𝑉) ∈ ℂ)
10942nncnd 12309 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐷 ∈ ℂ)
110109adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐷 ∈ ℂ)
11192, 110mulcld 11310 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · 𝐷) ∈ ℂ)
112106, 108, 111adddid 11314 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
11341nncnd 12309 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐴 ∈ ℂ)
114113adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐴 ∈ ℂ)
115 1cnd 11285 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 1 ∈ ℂ)
116114, 111, 115addsubd 11668 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) − 1) = ((𝐴 − 1) + (𝑚 · 𝐷)))
117116oveq1d 7463 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉))
11884nn0cnd 12615 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 − 1) ∈ ℂ)
119118adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 − 1) ∈ ℂ)
12038nncnd 12309 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑉 ∈ ℂ)
121120adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℂ)
122119, 111, 121add32d 11517 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
123117, 122eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))
124123oveq2d 7464 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))))
12592, 106, 110mul12d 11499 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) = (𝑊 · (𝑚 · 𝐷)))
126125oveq2d 7464 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷))))
127112, 124, 1263eqtr4d 2790 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
128127adantlr 714 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))
129128oveq2d 7464 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
130100, 104, 1293eqtr4d 2790 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
13138ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
13212ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
13343adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴(AP‘𝐾)𝐷) ⊆ (𝐹 “ {𝐺}))
134 eqid 2740 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))
135 oveq1 7455 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = 𝑚 → (𝑛 · 𝐷) = (𝑚 · 𝐷))
136135oveq2d 7464 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → (𝐴 + (𝑛 · 𝐷)) = (𝐴 + (𝑚 · 𝐷)))
137136rspceeqv 3658 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 ∈ (0...(𝐾 − 1)) ∧ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
138134, 137mpan2 690 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))
13910nnnn0d 12613 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐾 ∈ ℕ0)
140 vdwapval 17020 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐾 ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
141139, 41, 42, 140syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))))
142141biimpar 477 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
143138, 142sylan2 592 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷))
144133, 143sseldd 4009 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺}))
14538, 12, 6, 39, 40vdwlem4 17031 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹:(1...𝑉)⟶(𝑅m (1...𝑊)))
146145ffnd 6748 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹 Fn (1...𝑉))
147 fniniseg 7093 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 Fn (1...𝑉) → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
148146, 147syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)))
149148biimpa 476 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝐴 + (𝑚 · 𝐷)) ∈ (𝐹 “ {𝐺})) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
150144, 149syldan 590 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))
151150simpld 494 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
152151adantlr 714 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉))
15322r19.21bi 3257 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
154153adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ⊆ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
155 eqid 2740 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))
156 oveq1 7455 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → (𝑛 · (𝐸𝑖)) = (𝑚 · (𝐸𝑖)))
157156oveq2d 7464 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑚 → ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))))
158157rspceeqv 3658 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚 ∈ (0...(𝐾 − 1)) ∧ ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖))))
159155, 158mpan2 690 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖))))
16010adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ)
161160nnnn0d 12613 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ0)
16276, 79nnaddcld 12345 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ ℕ)
163 vdwapval 17020 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐾 ∈ ℕ0 ∧ (𝐵 + (𝐸𝑖)) ∈ ℕ ∧ (𝐸𝑖) ∈ ℕ) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖)))))
164161, 162, 79, 163syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖)))))
165164biimpar 477 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖 ∈ (1...𝑀)) ∧ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) = ((𝐵 + (𝐸𝑖)) + (𝑛 · (𝐸𝑖)))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
166159, 165sylan2 592 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
167154, 166sseldd 4009 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
16814ffnd 6748 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐺 Fn (1...𝑊))
169168adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐺 Fn (1...𝑊))
170 fniniseg 7093 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 Fn (1...𝑊) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖))))))
171169, 170syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖))))))
172171biimpa 476 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (1...𝑀)) ∧ ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))})) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
173167, 172syldan 590 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
174173simpld 494 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) ∈ (1...𝑊))
175131, 132, 152, 174vdwlem3 17030 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
176130, 175eqeltrd 2844 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))))
177 fvoveq1 7471 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = ((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
178 eqid 2740 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
179 fvex 6933 . . . . . . . . . . . . . . . . . . . 20 (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
180177, 178, 179fvmpt 7029 . . . . . . . . . . . . . . . . . . 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 7455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑥 − 1) = ((𝐴 + (𝑚 · 𝐷)) − 1))
185184oveq1d 7463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → ((𝑥 − 1) + 𝑉) = (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))
186185oveq2d 7464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))
187186oveq2d 7464 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
188187fveq2d 6924 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
189188mpteq2dv 5268 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
190 ovex 7481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1...𝑊) ∈ V
191190mptex 7260 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) ∈ V
192189, 40, 191fvmpt 7029 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
193151, 192syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
194183, 193eqtr3d 2782 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
195194adantlr 714 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))))
196195fveq1d 6922 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))))
197182, 196eqtr3d 2782 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘(𝐵 + (𝐸𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖)))))
198130fveq2d 6924 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑚 · (𝐸𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
199181, 197, 1983eqtr4rd 2791 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖))))
200176, 199jca 511 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
201 eleq1 2832 . . . . . . . . . . . . . . . . 17 (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉)))))
202 fveqeq2 6929 . . . . . . . . . . . . . . . . 17 (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → ((𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))) ↔ (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖)))))
203201, 202anbi12d 631 . . . . . . . . . . . . . . . 16 (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → ((𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖)))) ↔ ((((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸𝑖))))))
204200, 203syl5ibrcom 247 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
205204rexlimdva 3161 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
20687adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ)
207162, 206nnaddcld 12345 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
20865adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℕ)
20979, 208nnaddcld 12345 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + (𝑊 · 𝐷)) ∈ ℕ)
210 vdwapval 17020 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℕ0 ∧ ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ ((𝐸𝑖) + (𝑊 · 𝐷)) ∈ ℕ) → (𝑥 ∈ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))))
211161, 207, 209, 210syl3anc 1371 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸𝑖) + (𝑊 · 𝐷))))))
21239ffnd 6748 . . . . . . . . . . . . . . . 16 (𝜑𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
213212adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐻 Fn (1...(𝑊 · (2 · 𝑉))))
214 fniniseg 7093 . . . . . . . . . . . . . . 15 (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑥 ∈ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
215213, 214syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑥) = (𝐺‘(𝐵 + (𝐸𝑖))))))
216205, 211, 2153imtr4d 294 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) → 𝑥 ∈ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))})))
217216ssrdv 4014 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))) ⊆ (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
218 ssun1 4201 . . . . . . . . . . . . . . . . . . 19 (1...𝑀) ⊆ ((1...𝑀) ∪ {(𝑀 + 1)})
219 fzsuc 13631 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (ℤ‘1) → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
22052, 219syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)}))
221218, 220sseqtrrid 4062 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1...𝑀) ⊆ (1...(𝑀 + 1)))
222221sselda 4008 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...(𝑀 + 1)))
223 eqeq1 2744 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝑗 = (𝑀 + 1) ↔ 𝑖 = (𝑀 + 1)))
224 fveq2 6920 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝐸𝑗) = (𝐸𝑖))
225223, 224ifbieq2d 4574 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) = if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)))
226225oveq1d 7463 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) = (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)))
227 ovex 7481 . . . . . . . . . . . . . . . . . 18 (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)) ∈ V
228226, 46, 227fvmpt 7029 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (1...(𝑀 + 1)) → (𝑃𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)))
229222, 228syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑃𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)))
23018nnred 12308 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑀 ∈ ℝ)
231230ltp1d 12225 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑀 < (𝑀 + 1))
232 peano2re 11463 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
233230, 232syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑀 + 1) ∈ ℝ)
234230, 233ltnled 11437 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀))
235231, 234mpbid 232 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀)
236 breq1 5169 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = (𝑀 + 1) → (𝑖𝑀 ↔ (𝑀 + 1) ≤ 𝑀))
237236notbid 318 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = (𝑀 + 1) → (¬ 𝑖𝑀 ↔ ¬ (𝑀 + 1) ≤ 𝑀))
238235, 237syl5ibrcom 247 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑖 = (𝑀 + 1) → ¬ 𝑖𝑀))
239238con2d 134 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑖𝑀 → ¬ 𝑖 = (𝑀 + 1)))
240 elfzle2 13588 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑀) → 𝑖𝑀)
241239, 240impel 505 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → ¬ 𝑖 = (𝑀 + 1))
242 iffalse 4557 . . . . . . . . . . . . . . . . . 18 𝑖 = (𝑀 + 1) → if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) = (𝐸𝑖))
243242oveq1d 7463 . . . . . . . . . . . . . . . . 17 𝑖 = (𝑀 + 1) → (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)) = ((𝐸𝑖) + (𝑊 · 𝐷)))
244241, 243syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (if(𝑖 = (𝑀 + 1), 0, (𝐸𝑖)) + (𝑊 · 𝐷)) = ((𝐸𝑖) + (𝑊 · 𝐷)))
245229, 244eqtrd 2780 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑃𝑖) = ((𝐸𝑖) + (𝑊 · 𝐷)))
246245oveq2d 7464 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃𝑖)) = (𝑇 + ((𝐸𝑖) + (𝑊 · 𝐷))))
24747nncnd 12309 . . . . . . . . . . . . . . . 16 (𝜑𝑇 ∈ ℂ)
248247adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑇 ∈ ℂ)
249101adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℂ)
250248, 80, 249add12d 11516 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑇 + ((𝐸𝑖) + (𝑊 · 𝐷))) = ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))))
25145oveq1i 7458 . . . . . . . . . . . . . . . . . 18 (𝑇 + (𝑊 · 𝐷)) = ((𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1))) + (𝑊 · 𝐷))
25216nncnd 12309 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℂ)
253120, 109subcld 11647 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑉𝐷) ∈ ℂ)
254113, 253addcld 11309 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐴 + (𝑉𝐷)) ∈ ℂ)
255 ax-1cn 11242 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℂ
256 subcl 11535 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴 + (𝑉𝐷)) ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 + (𝑉𝐷)) − 1) ∈ ℂ)
257254, 255, 256sylancl 585 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴 + (𝑉𝐷)) − 1) ∈ ℂ)
258105, 257mulcld 11310 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) ∈ ℂ)
259252, 258, 101addassd 11312 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷))))
260105, 257, 109adddid 11314 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑊 · (((𝐴 + (𝑉𝐷)) − 1) + 𝐷)) = ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷)))
261113, 253, 109addassd 11312 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 + (𝑉𝐷)) + 𝐷) = (𝐴 + ((𝑉𝐷) + 𝐷)))
262120, 109npcand 11651 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑉𝐷) + 𝐷) = 𝑉)
263262oveq2d 7464 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐴 + ((𝑉𝐷) + 𝐷)) = (𝐴 + 𝑉))
264261, 263eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐴 + (𝑉𝐷)) + 𝐷) = (𝐴 + 𝑉))
265264oveq1d 7463 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝐴 + (𝑉𝐷)) + 𝐷) − 1) = ((𝐴 + 𝑉) − 1))
266 1cnd 11285 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ∈ ℂ)
267254, 109, 266addsubd 11668 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝐴 + (𝑉𝐷)) + 𝐷) − 1) = (((𝐴 + (𝑉𝐷)) − 1) + 𝐷))
268113, 120, 266addsubd 11668 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐴 + 𝑉) − 1) = ((𝐴 − 1) + 𝑉))
269265, 267, 2683eqtr3d 2788 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐴 + (𝑉𝐷)) − 1) + 𝐷) = ((𝐴 − 1) + 𝑉))
270269oveq2d 7464 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑊 · (((𝐴 + (𝑉𝐷)) − 1) + 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
271260, 270eqtr3d 2782 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
272271oveq2d 7464 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵 + ((𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) + (𝑊 · 𝐷))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
273259, 272eqtrd 2780 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
274251, 273eqtrid 2792 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑇 + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
275274oveq2d 7464 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
276275adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
27788adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
27880, 77, 277addassd 11312 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐸𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐸𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
27980, 77addcomd 11492 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + 𝐵) = (𝐵 + (𝐸𝑖)))
280279oveq1d 7463 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (((𝐸𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
281276, 278, 2803eqtr2d 2786 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝐸𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
282246, 250, 2813eqtrd 2784 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃𝑖)) = ((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))
283282, 245oveq12d 7466 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) = (((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸𝑖) + (𝑊 · 𝐷))))
284 cnvimass 6111 . . . . . . . . . . . . . . . . . . 19 (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ⊆ dom 𝐺
285284, 14fssdm 6766 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ⊆ (1...𝑊))
286285adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}) ⊆ (1...𝑊))
287 vdwapid1 17022 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ ℕ ∧ (𝐵 + (𝐸𝑖)) ∈ ℕ ∧ (𝐸𝑖) ∈ ℕ) → (𝐵 + (𝐸𝑖)) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
288160, 162, 79, 287syl3anc 1371 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ ((𝐵 + (𝐸𝑖))(AP‘𝐾)(𝐸𝑖)))
289153, 288sseldd 4009 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ (𝐺 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
290286, 289sseldd 4009 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ (1...𝑊))
291 fvoveq1 7471 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝐵 + (𝐸𝑖)) → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
292 eqid 2740 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
293 fvex 6933 . . . . . . . . . . . . . . . . 17 (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
294291, 292, 293fvmpt 7029 . . . . . . . . . . . . . . . 16 ((𝐵 + (𝐸𝑖)) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
295290, 294syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
296 vdwapid1 17022 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
29710, 41, 42, 296syl3anc 1371 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
29843, 297sseldd 4009 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ (𝐹 “ {𝐺}))
299 fniniseg 7093 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn (1...𝑉) → (𝐴 ∈ (𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹𝐴) = 𝐺)))
300146, 299syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐴 ∈ (𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹𝐴) = 𝐺)))
301298, 300mpbid 232 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 ∈ (1...𝑉) ∧ (𝐹𝐴) = 𝐺))
302301simprd 495 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹𝐴) = 𝐺)
303301simpld 494 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ (1...𝑉))
304 oveq1 7455 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝐴 → (𝑥 − 1) = (𝐴 − 1))
305304oveq1d 7463 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝐴 → ((𝑥 − 1) + 𝑉) = ((𝐴 − 1) + 𝑉))
306305oveq2d 7464 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝐴 → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · ((𝐴 − 1) + 𝑉)))
307306oveq2d 7464 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝐴 → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))
308307fveq2d 6924 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝐴 → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
309308mpteq2dv 5268 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝐴 → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
310190mptex 7260 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) ∈ V
311309, 40, 310fvmpt 7029 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ (1...𝑉) → (𝐹𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
312303, 311syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
313302, 312eqtr3d 2782 . . . . . . . . . . . . . . . . 17 (𝜑𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))))
314313fveq1d 6922 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐺‘(𝐵 + (𝐸𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))))
315314adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐵 + (𝐸𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸𝑖))))
316282fveq2d 6924 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃𝑖))) = (𝐻‘((𝐵 + (𝐸𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))))
317295, 315, 3163eqtr4rd 2791 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃𝑖))) = (𝐺‘(𝐵 + (𝐸𝑖))))
318317sneqd 4660 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (1...𝑀)) → {(𝐻‘(𝑇 + (𝑃𝑖)))} = {(𝐺‘(𝐵 + (𝐸𝑖)))})
319318imaeq2d 6089 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) = (𝐻 “ {(𝐺‘(𝐵 + (𝐸𝑖)))}))
320217, 283, 3193sstr4d 4056 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
321320ex 412 . . . . . . . . . 10 (𝜑 → (𝑖 ∈ (1...𝑀) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
322252adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ)
32388adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ)
324322, 323, 98addassd 11312 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
325127oveq2d 7464 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))))
326324, 325eqtr4d 2783 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))
32738adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ)
32812adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ)
329 eluzfz1 13591 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ (ℤ‘1) → 1 ∈ (1...𝑀))
33052, 329syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ∈ (1...𝑀))
331330ne0d 4365 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑀) ≠ ∅)
332 elfzuz3 13581 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 + (𝐸𝑖)) ∈ (1...𝑊) → 𝑊 ∈ (ℤ‘(𝐵 + (𝐸𝑖))))
333290, 332syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ‘(𝐵 + (𝐸𝑖))))
33416nnzd 12666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐵 ∈ ℤ)
335 uzid 12918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵 ∈ ℤ → 𝐵 ∈ (ℤ𝐵))
336334, 335syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ∈ (ℤ𝐵))
337336adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵 ∈ (ℤ𝐵))
33879nnnn0d 12613 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐸𝑖) ∈ ℕ0)
339 uzaddcl 12969 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ∈ (ℤ𝐵) ∧ (𝐸𝑖) ∈ ℕ0) → (𝐵 + (𝐸𝑖)) ∈ (ℤ𝐵))
340337, 338, 339syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸𝑖)) ∈ (ℤ𝐵))
341 uztrn 12921 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑊 ∈ (ℤ‘(𝐵 + (𝐸𝑖))) ∧ (𝐵 + (𝐸𝑖)) ∈ (ℤ𝐵)) → 𝑊 ∈ (ℤ𝐵))
342333, 340, 341syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ𝐵))
343 eluzle 12916 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑊 ∈ (ℤ𝐵) → 𝐵𝑊)
344342, 343syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖 ∈ (1...𝑀)) → 𝐵𝑊)
345344ralrimiva 3152 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑖 ∈ (1...𝑀)𝐵𝑊)
346 r19.2z 4518 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...𝑀) ≠ ∅ ∧ ∀𝑖 ∈ (1...𝑀)𝐵𝑊) → ∃𝑖 ∈ (1...𝑀)𝐵𝑊)
347331, 345, 346syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∃𝑖 ∈ (1...𝑀)𝐵𝑊)
348 idd 24 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (1...𝑀) → (𝐵𝑊𝐵𝑊))
349348rexlimiv 3154 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑖 ∈ (1...𝑀)𝐵𝑊𝐵𝑊)
350347, 349syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵𝑊)
35112nnzd 12666 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑊 ∈ ℤ)
352 fznn 13652 . . . . . . . . . . . . . . . . . . . . . 22 (𝑊 ∈ ℤ → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵𝑊)))
353351, 352syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵𝑊)))
35416, 350, 353mpbir2and 712 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ (1...𝑊))
355354adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ (1...𝑊))
356327, 328, 151, 355vdwlem3 17030 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
357326, 356eqeltrd 2844 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))))
358 fvoveq1 7471 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
359 fvex 6933 . . . . . . . . . . . . . . . . . . . 20 (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V
360358, 178, 359fvmpt 7029 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
361355, 360syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
362194fveq1d 6922 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐺𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵))
363326fveq2d 6924 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))
364361, 362, 3633eqtr4rd 2791 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵))
365357, 364jca 511 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵)))
366 eleq1 2832 . . . . . . . . . . . . . . . . 17 (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉)))))
367 fveqeq2 6929 . . . . . . . . . . . . . . . . 17 (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝐻𝑧) = (𝐺𝐵) ↔ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵)))
368366, 367anbi12d 631 . . . . . . . . . . . . . . . 16 (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵)) ↔ (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺𝐵))))
369365, 368syl5ibrcom 247 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (0...(𝐾 − 1))) → (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
370369rexlimdva 3161 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
37116, 87nnaddcld 12345 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ)
372 vdwapval 17020 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℕ0 ∧ (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ (𝑊 · 𝐷) ∈ ℕ) → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
373139, 371, 65, 372syl3anc 1371 . . . . . . . . . . . . . 14 (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))))
374 fniniseg 7093 . . . . . . . . . . . . . . 15 (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑧 ∈ (𝐻 “ {(𝐺𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
375212, 374syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑧 ∈ (𝐻 “ {(𝐺𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻𝑧) = (𝐺𝐵))))
376370, 373, 3753imtr4d 294 . . . . . . . . . . . . 13 (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) → 𝑧 ∈ (𝐻 “ {(𝐺𝐵)})))
377376ssrdv 4014 . . . . . . . . . . . 12 (𝜑 → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ⊆ (𝐻 “ {(𝐺𝐵)}))
37818peano2nnd 12310 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 + 1) ∈ ℕ)
379378, 51eleqtrdi 2854 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 + 1) ∈ (ℤ‘1))
380 eluzfz2 13592 . . . . . . . . . . . . . . . . 17 ((𝑀 + 1) ∈ (ℤ‘1) → (𝑀 + 1) ∈ (1...(𝑀 + 1)))
381 iftrue 4554 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑀 + 1) → if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) = 0)
382381oveq1d 7463 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑀 + 1) → (if(𝑗 = (𝑀 + 1), 0, (𝐸𝑗)) + (𝑊 · 𝐷)) = (0 + (𝑊 · 𝐷)))
383 ovex 7481 . . . . . . . . . . . . . . . . . 18 (0 + (𝑊 · 𝐷)) ∈ V
384382, 46, 383fvmpt 7029 . . . . . . . . . . . . . . . . 17 ((𝑀 + 1) ∈ (1...(𝑀 + 1)) → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
385379, 380, 3843syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷)))
386101addlidd 11491 . . . . . . . . . . . . . . . 16 (𝜑 → (0 + (𝑊 · 𝐷)) = (𝑊 · 𝐷))
387385, 386eqtrd 2780 . . . . . . . . . . . . . . 15 (𝜑 → (𝑃‘(𝑀 + 1)) = (𝑊 · 𝐷))
388387oveq2d 7464 . . . . . . . . . . . . . 14 (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝑇 + (𝑊 · 𝐷)))
389388, 274eqtrd 2780 . . . . . . . . . . . . 13 (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))
390389, 387oveq12d 7466 . . . . . . . . . . . 12 (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)))
391 fvoveq1 7471 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
392 fvex 6933 . . . . . . . . . . . . . . . . 17 (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V
393391, 292, 392fvmpt 7029 . . . . . . . . . . . . . . . 16 (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
394354, 393syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
395313fveq1d 6922 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵))
396389fveq2d 6924 . . . . . . . . . . . . . . 15 (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))))
397394, 395, 3963eqtr4rd 2791 . . . . . . . . . . . . . 14 (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐺𝐵))
398397sneqd 4660 . . . . . . . . . . . . 13 (𝜑 → {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))} = {(𝐺𝐵)})
399398imaeq2d 6089 . . . . . . . . . . . 12 (𝜑 → (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}) = (𝐻 “ {(𝐺𝐵)}))
400377, 390, 3993sstr4d 4056 . . . . . . . . . . 11 (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
401 fveq2 6920 . . . . . . . . . . . . . 14 (𝑖 = (𝑀 + 1) → (𝑃𝑖) = (𝑃‘(𝑀 + 1)))
402401oveq2d 7464 . . . . . . . . . . . . 13 (𝑖 = (𝑀 + 1) → (𝑇 + (𝑃𝑖)) = (𝑇 + (𝑃‘(𝑀 + 1))))
403402, 401oveq12d 7466 . . . . . . . . . . . 12 (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) = ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))))
404402fveq2d 6924 . . . . . . . . . . . . . 14 (𝑖 = (𝑀 + 1) → (𝐻‘(𝑇 + (𝑃𝑖))) = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
405404sneqd 4660 . . . . . . . . . . . . 13 (𝑖 = (𝑀 + 1) → {(𝐻‘(𝑇 + (𝑃𝑖)))} = {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})
406405imaeq2d 6089 . . . . . . . . . . . 12 (𝑖 = (𝑀 + 1) → (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) = (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))
407403, 406sseq12d 4042 . . . . . . . . . . 11 (𝑖 = (𝑀 + 1) → (((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) ↔ ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})))
408400, 407syl5ibrcom 247 . . . . . . . . . 10 (𝜑 → (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
409321, 408jaod 858 . . . . . . . . 9 (𝜑 → ((𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
41075, 409sylbid 240 . . . . . . . 8 (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) → ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
411410ralrimiv 3151 . . . . . . 7 (𝜑 → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
412411adantr 480 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
413220rexeqdv 3335 . . . . . . . . . . . 12 (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ ∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))))
414 rexun 4219 . . . . . . . . . . . . 13 (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))))
415317eqeq2d 2751 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑀)) → (𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))))
416415rexbidva 3183 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))))
417 ovex 7481 . . . . . . . . . . . . . . . 16 (𝑀 + 1) ∈ V
418404eqeq2d 2751 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑀 + 1) → (𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))))
419417, 418rexsn 4706 . . . . . . . . . . . . . . 15 (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))
420397eqeq2d 2751 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) ↔ 𝑥 = (𝐺𝐵)))
421419, 420bitrid 283 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃𝑖))) ↔ 𝑥 = (𝐺𝐵)))
422416, 421orbi12d 917 . . . . . . . . . . . . 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 2811 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))} = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))})
427 eqid 2740 . . . . . . . . . 10 (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))
428427rnmpt 5980 . . . . . . . . 9 ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))) = {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃𝑖)))}
4292rnmpt 5980 . . . . . . . . . . 11 ran 𝐽 = {𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))}
430 df-sn 4649 . . . . . . . . . . 11 {(𝐺𝐵)} = {𝑥𝑥 = (𝐺𝐵)}
431429, 430uneq12i 4189 . . . . . . . . . 10 (ran 𝐽 ∪ {(𝐺𝐵)}) = ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))} ∪ {𝑥𝑥 = (𝐺𝐵)})
432 unab 4327 . . . . . . . . . 10 ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖)))} ∪ {𝑥𝑥 = (𝐺𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))}
433431, 432eqtri 2768 . . . . . . . . 9 (ran 𝐽 ∪ {(𝐺𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸𝑖))) ∨ 𝑥 = (𝐺𝐵))}
434426, 428, 4333eqtr4g 2805 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))) = (ran 𝐽 ∪ {(𝐺𝐵)}))
435434fveq2d 6924 . . . . . . 7 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (♯‘(ran 𝐽 ∪ {(𝐺𝐵)})))
436 fzfi 14023 . . . . . . . . . 10 (1...𝑀) ∈ Fin
437 dffn4 6840 . . . . . . . . . . 11 (𝐽 Fn (1...𝑀) ↔ 𝐽:(1...𝑀)–onto→ran 𝐽)
4383, 437mpbi 230 . . . . . . . . . 10 𝐽:(1...𝑀)–onto→ran 𝐽
439 fofi 9379 . . . . . . . . . 10 (((1...𝑀) ∈ Fin ∧ 𝐽:(1...𝑀)–onto→ran 𝐽) → ran 𝐽 ∈ Fin)
440436, 438, 439mp2an 691 . . . . . . . . 9 ran 𝐽 ∈ Fin
441440a1i 11 . . . . . . . 8 (𝜑 → ran 𝐽 ∈ Fin)
442 fvex 6933 . . . . . . . . 9 (𝐺𝐵) ∈ V
443 hashunsng 14441 . . . . . . . . 9 ((𝐺𝐵) ∈ V → ((ran 𝐽 ∈ Fin ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺𝐵)})) = ((♯‘ran 𝐽) + 1)))
444442, 443ax-mp 5 . . . . . . . 8 ((ran 𝐽 ∈ Fin ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺𝐵)})) = ((♯‘ran 𝐽) + 1))
445441, 444sylan 579 . . . . . . 7 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺𝐵)})) = ((♯‘ran 𝐽) + 1))
44644adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘ran 𝐽) = 𝑀)
447446oveq1d 7463 . . . . . . 7 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ((♯‘ran 𝐽) + 1) = (𝑀 + 1))
448435, 445, 4473eqtrd 2784 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1))
449412, 448jca 511 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1)))
450 oveq1 7455 . . . . . . . . . 10 (𝑎 = 𝑇 → (𝑎 + (𝑑𝑖)) = (𝑇 + (𝑑𝑖)))
451450oveq1d 7463 . . . . . . . . 9 (𝑎 = 𝑇 → ((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) = ((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)))
452 fvoveq1 7471 . . . . . . . . . . 11 (𝑎 = 𝑇 → (𝐻‘(𝑎 + (𝑑𝑖))) = (𝐻‘(𝑇 + (𝑑𝑖))))
453452sneqd 4660 . . . . . . . . . 10 (𝑎 = 𝑇 → {(𝐻‘(𝑎 + (𝑑𝑖)))} = {(𝐻‘(𝑇 + (𝑑𝑖)))})
454453imaeq2d 6089 . . . . . . . . 9 (𝑎 = 𝑇 → (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) = (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}))
455451, 454sseq12d 4042 . . . . . . . 8 (𝑎 = 𝑇 → (((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ↔ ((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))})))
456455ralbidv 3184 . . . . . . 7 (𝑎 = 𝑇 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))})))
457452mpteq2dv 5268 . . . . . . . . 9 (𝑎 = 𝑇 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))))
458457rneqd 5963 . . . . . . . 8 (𝑎 = 𝑇 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))))
459458fveqeq2d 6928 . . . . . . 7 (𝑎 = 𝑇 → ((♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1) ↔ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))) = (𝑀 + 1)))
460456, 459anbi12d 631 . . . . . 6 (𝑎 = 𝑇 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))) = (𝑀 + 1))))
461 fveq1 6919 . . . . . . . . . . 11 (𝑑 = 𝑃 → (𝑑𝑖) = (𝑃𝑖))
462461oveq2d 7464 . . . . . . . . . 10 (𝑑 = 𝑃 → (𝑇 + (𝑑𝑖)) = (𝑇 + (𝑃𝑖)))
463462, 461oveq12d 7466 . . . . . . . . 9 (𝑑 = 𝑃 → ((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) = ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)))
464462fveq2d 6924 . . . . . . . . . . 11 (𝑑 = 𝑃 → (𝐻‘(𝑇 + (𝑑𝑖))) = (𝐻‘(𝑇 + (𝑃𝑖))))
465464sneqd 4660 . . . . . . . . . 10 (𝑑 = 𝑃 → {(𝐻‘(𝑇 + (𝑑𝑖)))} = {(𝐻‘(𝑇 + (𝑃𝑖)))})
466465imaeq2d 6089 . . . . . . . . 9 (𝑑 = 𝑃 → (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) = (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}))
467463, 466sseq12d 4042 . . . . . . . 8 (𝑑 = 𝑃 → (((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ↔ ((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
468467ralbidv 3184 . . . . . . 7 (𝑑 = 𝑃 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))})))
469464mpteq2dv 5268 . . . . . . . . 9 (𝑑 = 𝑃 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))))
470469rneqd 5963 . . . . . . . 8 (𝑑 = 𝑃 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖)))))
471470fveqeq2d 6928 . . . . . . 7 (𝑑 = 𝑃 → ((♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))) = (𝑀 + 1) ↔ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1)))
472468, 471anbi12d 631 . . . . . 6 (𝑑 = 𝑃 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃𝑖))(AP‘𝐾)(𝑃𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑇 + (𝑃𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃𝑖))))) = (𝑀 + 1))))
473460, 472rspc2ev 3648 . . . . 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 1371 . . . 4 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1)))
475 ovex 7481 . . . . 5 (1...(𝑊 · (2 · 𝑉))) ∈ V
47610adantr 480 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ)
477476nnnn0d 12613 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ0)
47839adantr 480 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
47918adantr 480 . . . . . 6 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → 𝑀 ∈ ℕ)
480479peano2nnd 12310 . . . . 5 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (𝑀 + 1) ∈ ℕ)
481 eqid 2740 . . . . 5 (1...(𝑀 + 1)) = (1...(𝑀 + 1))
482475, 477, 478, 480, 481vdwpc 17027 . . . 4 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m (1...(𝑀 + 1)))(∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑𝑖))(AP‘𝐾)(𝑑𝑖)) ⊆ (𝐻 “ {(𝐻‘(𝑎 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑𝑖))))) = (𝑀 + 1))))
483474, 482mpbird 257 . . 3 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → ⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻)
484483orcd 872 . 2 ((𝜑 ∧ ¬ (𝐺𝐵) ∈ ran 𝐽) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))
48537, 484pm2.61dan 812 1 (𝜑 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 846   = wceq 1537  wcel 2108  {cab 2717  wne 2946  wral 3067  wrex 3076  Vcvv 3488  cun 3974  wss 3976  c0 4352  ifcif 4548  {csn 4648  cop 4654   class class class wbr 5166  cmpt 5249  ccnv 5699  ran crn 5701  cima 5703   Fn wfn 6568  wf 6569  ontowfo 6571  cfv 6573  (class class class)co 7448  m cmap 8884  Fincfn 9003  cc 11182  cr 11183  0cc0 11184  1c1 11185   + caddc 11187   · cmul 11189   < clt 11324  cle 11325  cmin 11520  cn 12293  2c2 12348  0cn0 12553  cz 12639  cuz 12903  ...cfz 13567  chash 14379  APcvdwa 17012   MonoAP cvdwm 17013   PolyAP cvdwp 17014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-oadd 8526  df-er 8763  df-map 8886  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-dju 9970  df-card 10008  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-nn 12294  df-2 12356  df-n0 12554  df-z 12640  df-uz 12904  df-rp 13058  df-fz 13568  df-hash 14380  df-vdwap 17015  df-vdwmc 17016  df-vdwpc 17017
This theorem is referenced by:  vdwlem7  17034
  Copyright terms: Public domain W3C validator