Step | Hyp | Ref
| Expression |
1 | | fvex 6681 |
. . . . . . 7
⊢ (𝐺‘(𝐵 + (𝐸‘𝑖))) ∈ V |
2 | | vdwlem6.j |
. . . . . . 7
⊢ 𝐽 = (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝐵 + (𝐸‘𝑖)))) |
3 | 1, 2 | fnmpti 6474 |
. . . . . 6
⊢ 𝐽 Fn (1...𝑀) |
4 | | fvelrnb 6724 |
. . . . . 6
⊢ (𝐽 Fn (1...𝑀) → ((𝐺‘𝐵) ∈ ran 𝐽 ↔ ∃𝑚 ∈ (1...𝑀)(𝐽‘𝑚) = (𝐺‘𝐵))) |
5 | 3, 4 | ax-mp 5 |
. . . . 5
⊢ ((𝐺‘𝐵) ∈ ran 𝐽 ↔ ∃𝑚 ∈ (1...𝑀)(𝐽‘𝑚) = (𝐺‘𝐵)) |
6 | | vdwlem4.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Fin) |
7 | 6 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝑅 ∈ Fin) |
8 | | vdwlem7.k |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈
(ℤ≥‘2)) |
9 | | eluz2nn 12359 |
. . . . . . . . 9
⊢ (𝐾 ∈
(ℤ≥‘2) → 𝐾 ∈ ℕ) |
10 | 8, 9 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℕ) |
11 | 10 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝐾 ∈ ℕ) |
12 | | vdwlem3.w |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ ℕ) |
13 | 12 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝑊 ∈ ℕ) |
14 | | vdwlem7.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺:(1...𝑊)⟶𝑅) |
15 | 14 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝐺:(1...𝑊)⟶𝑅) |
16 | | vdwlem6.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℕ) |
17 | 16 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝐵 ∈ ℕ) |
18 | | vdwlem7.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) |
19 | 18 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝑀 ∈ ℕ) |
20 | | vdwlem6.e |
. . . . . . . 8
⊢ (𝜑 → 𝐸:(1...𝑀)⟶ℕ) |
21 | 20 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝐸:(1...𝑀)⟶ℕ) |
22 | | vdwlem6.s |
. . . . . . . 8
⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))})) |
23 | 22 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))})) |
24 | | simprl 771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → 𝑚 ∈ (1...𝑀)) |
25 | | simprr 773 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐽‘𝑚) = (𝐺‘𝐵)) |
26 | | fveq2 6668 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑚 → (𝐸‘𝑖) = (𝐸‘𝑚)) |
27 | 26 | oveq2d 7180 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑚 → (𝐵 + (𝐸‘𝑖)) = (𝐵 + (𝐸‘𝑚))) |
28 | 27 | fveq2d 6672 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑚 → (𝐺‘(𝐵 + (𝐸‘𝑖))) = (𝐺‘(𝐵 + (𝐸‘𝑚)))) |
29 | | fvex 6681 |
. . . . . . . . . 10
⊢ (𝐺‘(𝐵 + (𝐸‘𝑚))) ∈ V |
30 | 28, 2, 29 | fvmpt 6769 |
. . . . . . . . 9
⊢ (𝑚 ∈ (1...𝑀) → (𝐽‘𝑚) = (𝐺‘(𝐵 + (𝐸‘𝑚)))) |
31 | 24, 30 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐽‘𝑚) = (𝐺‘(𝐵 + (𝐸‘𝑚)))) |
32 | 25, 31 | eqtr3d 2775 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐺‘𝐵) = (𝐺‘(𝐵 + (𝐸‘𝑚)))) |
33 | 7, 11, 13, 15, 17, 19, 21, 23, 24, 32 | vdwlem1 16410 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ (1...𝑀) ∧ (𝐽‘𝑚) = (𝐺‘𝐵))) → (𝐾 + 1) MonoAP 𝐺) |
34 | 33 | rexlimdvaa 3194 |
. . . . 5
⊢ (𝜑 → (∃𝑚 ∈ (1...𝑀)(𝐽‘𝑚) = (𝐺‘𝐵) → (𝐾 + 1) MonoAP 𝐺)) |
35 | 5, 34 | syl5bi 245 |
. . . 4
⊢ (𝜑 → ((𝐺‘𝐵) ∈ ran 𝐽 → (𝐾 + 1) MonoAP 𝐺)) |
36 | 35 | imp 410 |
. . 3
⊢ ((𝜑 ∧ (𝐺‘𝐵) ∈ ran 𝐽) → (𝐾 + 1) MonoAP 𝐺) |
37 | 36 | olcd 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, (𝐸‘𝑗)) + (𝑊 · 𝐷))) |
47 | 38, 12, 6, 39, 40, 18, 14, 8, 41, 42, 43, 16, 20, 22, 2, 44, 45, 46 | vdwlem5 16414 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ ℕ) |
48 | 47 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑇 ∈ ℕ) |
49 | | 0nn0 11984 |
. . . . . . . . . 10
⊢ 0 ∈
ℕ0 |
50 | 49 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 = (𝑀 + 1)) → 0 ∈
ℕ0) |
51 | | nnuz 12356 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ =
(ℤ≥‘1) |
52 | 18, 51 | eleqtrdi 2843 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
53 | 52 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑀 ∈
(ℤ≥‘1)) |
54 | | elfzp1 13041 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈
(ℤ≥‘1) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1)))) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (𝑗 ∈ (1...(𝑀 + 1)) ↔ (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1)))) |
56 | 55 | biimpa 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑗 ∈ (1...𝑀) ∨ 𝑗 = (𝑀 + 1))) |
57 | 56 | ord 863 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 ∈ (1...𝑀) → 𝑗 = (𝑀 + 1))) |
58 | 57 | con1d 147 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (¬ 𝑗 = (𝑀 + 1) → 𝑗 ∈ (1...𝑀))) |
59 | 58 | imp 410 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → 𝑗 ∈ (1...𝑀)) |
60 | 20 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → 𝐸:(1...𝑀)⟶ℕ) |
61 | 60 | ffvelrnda 6855 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸‘𝑗) ∈ ℕ) |
62 | 61 | nnnn0d 12029 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ 𝑗 ∈ (1...𝑀)) → (𝐸‘𝑗) ∈
ℕ0) |
63 | 59, 62 | syldan 594 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) ∧ ¬ 𝑗 = (𝑀 + 1)) → (𝐸‘𝑗) ∈
ℕ0) |
64 | 50, 63 | ifclda 4446 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) ∈
ℕ0) |
65 | 12, 42 | nnmulcld 11762 |
. . . . . . . . 9
⊢ (𝜑 → (𝑊 · 𝐷) ∈ ℕ) |
66 | 65 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (𝑊 · 𝐷) ∈ ℕ) |
67 | | nn0nnaddcl 12000 |
. . . . . . . 8
⊢
((if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) ∈ ℕ0 ∧ (𝑊 · 𝐷) ∈ ℕ) → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) ∈ ℕ) |
68 | 64, 66, 67 | syl2anc 587 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) ∧ 𝑗 ∈ (1...(𝑀 + 1))) → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) ∈ ℕ) |
69 | 68, 46 | fmptd 6882 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑃:(1...(𝑀 + 1))⟶ℕ) |
70 | | nnex 11715 |
. . . . . . 7
⊢ ℕ
∈ V |
71 | | ovex 7197 |
. . . . . . 7
⊢
(1...(𝑀 + 1)) ∈
V |
72 | 70, 71 | elmap 8474 |
. . . . . 6
⊢ (𝑃 ∈ (ℕ
↑m (1...(𝑀
+ 1))) ↔ 𝑃:(1...(𝑀 +
1))⟶ℕ) |
73 | 69, 72 | sylibr 237 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑃 ∈ (ℕ ↑m
(1...(𝑀 +
1)))) |
74 | | elfzp1 13041 |
. . . . . . . . . 10
⊢ (𝑀 ∈
(ℤ≥‘1) → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1)))) |
75 | 52, 74 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) ↔ (𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1)))) |
76 | 16 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℕ) |
77 | 76 | nncnd 11725 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ∈ ℂ) |
78 | 77 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ) |
79 | 20 | ffvelrnda 6855 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐸‘𝑖) ∈ ℕ) |
80 | 79 | nncnd 11725 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐸‘𝑖) ∈ ℂ) |
81 | 80 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐸‘𝑖) ∈ ℂ) |
82 | 78, 81 | addcld 10731 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝐸‘𝑖)) ∈ ℂ) |
83 | | nnm1nn0 12010 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ∈ ℕ → (𝐴 − 1) ∈
ℕ0) |
84 | 41, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐴 − 1) ∈
ℕ0) |
85 | | nn0nnaddcl 12000 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 − 1) ∈
ℕ0 ∧ 𝑉
∈ ℕ) → ((𝐴
− 1) + 𝑉) ∈
ℕ) |
86 | 84, 38, 85 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℕ) |
87 | 12, 86 | nnmulcld 11762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ) |
88 | 87 | nncnd 11725 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ) |
89 | 88 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ) |
90 | | elfznn0 13084 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 ∈ (0...(𝐾 − 1)) → 𝑚 ∈ ℕ0) |
91 | 90 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℕ0) |
92 | 91 | nn0cnd 12031 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ) |
93 | 92 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑚 ∈ ℂ) |
94 | 93, 81 | mulcld 10732 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝐸‘𝑖)) ∈ ℂ) |
95 | 65 | nnnn0d 12029 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑊 · 𝐷) ∈
ℕ0) |
96 | 95 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈
ℕ0) |
97 | 91, 96 | nn0mulcld 12034 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈
ℕ0) |
98 | 97 | nn0cnd 12031 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ) |
99 | 98 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) ∈ ℂ) |
100 | 82, 89, 94, 99 | add4d 10939 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸‘𝑖)) + (𝑚 · (𝑊 · 𝐷)))) = (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))) |
101 | 65 | nncnd 11725 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑊 · 𝐷) ∈ ℂ) |
102 | 101 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · 𝐷) ∈ ℂ) |
103 | 93, 81, 102 | adddid 10736 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))) = ((𝑚 · (𝐸‘𝑖)) + (𝑚 · (𝑊 · 𝐷)))) |
104 | 103 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + ((𝑚 · (𝐸‘𝑖)) + (𝑚 · (𝑊 · 𝐷))))) |
105 | 12 | nncnd 11725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑊 ∈ ℂ) |
106 | 105 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℂ) |
107 | 86 | nncnd 11725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℂ) |
108 | 107 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 − 1) + 𝑉) ∈ ℂ) |
109 | 42 | nncnd 11725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐷 ∈ ℂ) |
110 | 109 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐷 ∈ ℂ) |
111 | 92, 110 | mulcld 10732 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · 𝐷) ∈ ℂ) |
112 | 106, 108,
111 | adddid 10736 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷)))) |
113 | 41 | nncnd 11725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐴 ∈ ℂ) |
114 | 113 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐴 ∈ ℂ) |
115 | | 1cnd 10707 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 1 ∈
ℂ) |
116 | 114, 111,
115 | addsubd 11089 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) − 1) = ((𝐴 − 1) + (𝑚 · 𝐷))) |
117 | 116 | oveq1d 7179 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉)) |
118 | 84 | nn0cnd 12031 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐴 − 1) ∈ ℂ) |
119 | 118 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 − 1) ∈ ℂ) |
120 | 38 | nncnd 11725 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑉 ∈ ℂ) |
121 | 120 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℂ) |
122 | 119, 111,
121 | add32d 10938 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 − 1) + (𝑚 · 𝐷)) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))) |
123 | 117, 122 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉) = (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷))) |
124 | 123 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = (𝑊 · (((𝐴 − 1) + 𝑉) + (𝑚 · 𝐷)))) |
125 | 92, 106, 110 | mul12d 10920 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · (𝑊 · 𝐷)) = (𝑊 · (𝑚 · 𝐷))) |
126 | 125 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑊 · (𝑚 · 𝐷)))) |
127 | 112, 124,
126 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))) |
128 | 127 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) = ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷)))) |
129 | 128 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))) |
130 | 100, 104,
129 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) = (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) |
131 | 38 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ) |
132 | 12 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ) |
133 | 43 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴(AP‘𝐾)𝐷) ⊆ (◡𝐹 “ {𝐺})) |
134 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷)) |
135 | | oveq1 7171 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = 𝑚 → (𝑛 · 𝐷) = (𝑚 · 𝐷)) |
136 | 135 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = 𝑚 → (𝐴 + (𝑛 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))) |
137 | 136 | rspceeqv 3539 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑚 ∈ (0...(𝐾 − 1)) ∧ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))) |
138 | 134, 137 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))) |
139 | 10 | nnnn0d 12029 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
140 | | vdwapval 16402 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐾 ∈ ℕ0
∧ 𝐴 ∈ ℕ
∧ 𝐷 ∈ ℕ)
→ ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))) |
141 | 139, 41, 42, 140 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))) |
142 | 141 | biimpar 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷)) |
143 | 138, 142 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷)) |
144 | 133, 143 | sseldd 3876 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (◡𝐹 “ {𝐺})) |
145 | 38, 12, 6, 39, 40 | vdwlem4 16413 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐹:(1...𝑉)⟶(𝑅 ↑m (1...𝑊))) |
146 | 145 | ffnd 6499 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐹 Fn (1...𝑉)) |
147 | | fniniseg 6831 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹 Fn (1...𝑉) → ((𝐴 + (𝑚 · 𝐷)) ∈ (◡𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (◡𝐹 “ {𝐺}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺))) |
149 | 148 | biimpa 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝐴 + (𝑚 · 𝐷)) ∈ (◡𝐹 “ {𝐺})) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)) |
150 | 144, 149 | syldan 594 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) ∧ (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺)) |
151 | 150 | simpld 498 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉)) |
152 | 151 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉)) |
153 | 22 | r19.21bi 3120 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))})) |
154 | 153 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))})) |
155 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) |
156 | | oveq1 7171 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = 𝑚 → (𝑛 · (𝐸‘𝑖)) = (𝑚 · (𝐸‘𝑖))) |
157 | 156 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 = 𝑚 → ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) |
158 | 157 | rspceeqv 3539 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑚 ∈ (0...(𝐾 − 1)) ∧ ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖)))) |
159 | 155, 158 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖)))) |
160 | 10 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ) |
161 | 160 | nnnn0d 12029 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐾 ∈
ℕ0) |
162 | 76, 79 | nnaddcld 11761 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ ℕ) |
163 | | vdwapval 16402 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐾 ∈ ℕ0
∧ (𝐵 + (𝐸‘𝑖)) ∈ ℕ ∧ (𝐸‘𝑖) ∈ ℕ) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖))))) |
164 | 161, 162,
79, 163 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖))))) |
165 | 164 | biimpar 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ ∃𝑛 ∈ (0...(𝐾 − 1))((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) = ((𝐵 + (𝐸‘𝑖)) + (𝑛 · (𝐸‘𝑖)))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖))) |
166 | 159, 165 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖))) |
167 | 154, 166 | sseldd 3876 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))})) |
168 | 14 | ffnd 6499 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐺 Fn (1...𝑊)) |
169 | 168 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐺 Fn (1...𝑊)) |
170 | | fniniseg 6831 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺 Fn (1...𝑊) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))) |
171 | 169, 170 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))) |
172 | 171 | biimpa 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))})) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))) |
173 | 167, 172 | syldan 594 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) ∧ (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))) |
174 | 173 | simpld 498 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊)) |
175 | 131, 132,
152, 174 | vdwlem3 16412 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉)))) |
176 | 130, 175 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉)))) |
177 | | fvoveq1 7187 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = ((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) |
178 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) |
179 | | fvex 6681 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V |
180 | 177, 178,
179 | fvmpt 6769 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) |
181 | 174, 180 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) |
182 | 173 | simprd 499 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))) |
183 | 150 | simprd 499 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = 𝐺) |
184 | | oveq1 7171 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑥 − 1) = ((𝐴 + (𝑚 · 𝐷)) − 1)) |
185 | 184 | oveq1d 7179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → ((𝑥 − 1) + 𝑉) = (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)) |
186 | 185 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) |
187 | 186 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) |
188 | 187 | fveq2d 6672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) |
189 | 188 | mpteq2dv 5123 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))) |
190 | | ovex 7197 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(1...𝑊) ∈
V |
191 | 190 | mptex 6990 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) ∈ V |
192 | 189, 40, 191 | fvmpt 6769 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑉) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))) |
193 | 151, 192 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘(𝐴 + (𝑚 · 𝐷))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))) |
194 | 183, 193 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))) |
195 | 194 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))) |
196 | 195 | fveq1d 6670 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖)))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))))) |
197 | 182, 196 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘(𝐵 + (𝐸‘𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))))) |
198 | 130 | fveq2d 6672 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑚 · (𝐸‘𝑖))) + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) |
199 | 181, 197,
198 | 3eqtr4rd 2784 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))) |
200 | 176, 199 | jca 515 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))) |
201 | | eleq1 2820 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))))) |
202 | | fveqeq2 6677 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → ((𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖))) ↔ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖))))) |
203 | 201, 202 | anbi12d 634 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → ((𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖)))) ↔ ((((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘(((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷))))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))) |
204 | 200, 203 | syl5ibrcom 250 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))) |
205 | 204 | rexlimdva 3193 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))) → (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))) |
206 | 87 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ) |
207 | 162, 206 | nnaddcld 11761 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ) |
208 | 65 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℕ) |
209 | 79, 208 | nnaddcld 11761 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + (𝑊 · 𝐷)) ∈ ℕ) |
210 | | vdwapval 16402 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℕ0
∧ ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ ((𝐸‘𝑖) + (𝑊 · 𝐷)) ∈ ℕ) → (𝑥 ∈ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))))) |
211 | 161, 207,
209, 210 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · ((𝐸‘𝑖) + (𝑊 · 𝐷)))))) |
212 | 39 | ffnd 6499 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐻 Fn (1...(𝑊 · (2 · 𝑉)))) |
213 | 212 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐻 Fn (1...(𝑊 · (2 · 𝑉)))) |
214 | | fniniseg 6831 |
. . . . . . . . . . . . . . 15
⊢ (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑥 ∈ (◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))) |
215 | 213, 214 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ↔ (𝑥 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑥) = (𝐺‘(𝐵 + (𝐸‘𝑖)))))) |
216 | 205, 211,
215 | 3imtr4d 297 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 ∈ (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) → 𝑥 ∈ (◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))) |
217 | 216 | ssrdv 3881 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷))) ⊆ (◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))})) |
218 | | ssun1 4060 |
. . . . . . . . . . . . . . . . . . 19
⊢
(1...𝑀) ⊆
((1...𝑀) ∪ {(𝑀 + 1)}) |
219 | | fzsuc 13038 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈
(ℤ≥‘1) → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)})) |
220 | 52, 219 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1...(𝑀 + 1)) = ((1...𝑀) ∪ {(𝑀 + 1)})) |
221 | 218, 220 | sseqtrrid 3928 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1...𝑀) ⊆ (1...(𝑀 + 1))) |
222 | 221 | sselda 3875 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (1...(𝑀 + 1))) |
223 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑖 → (𝑗 = (𝑀 + 1) ↔ 𝑖 = (𝑀 + 1))) |
224 | | fveq2 6668 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑖 → (𝐸‘𝑗) = (𝐸‘𝑖)) |
225 | 223, 224 | ifbieq2d 4437 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑖 → if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) = if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖))) |
226 | 225 | oveq1d 7179 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑖 → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) = (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷))) |
227 | | ovex 7197 |
. . . . . . . . . . . . . . . . . 18
⊢ (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)) ∈ V |
228 | 226, 46, 227 | fvmpt 6769 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...(𝑀 + 1)) → (𝑃‘𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷))) |
229 | 222, 228 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑃‘𝑖) = (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷))) |
230 | 18 | nnred 11724 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑀 ∈ ℝ) |
231 | 230 | ltp1d 11641 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑀 < (𝑀 + 1)) |
232 | | peano2re 10884 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈
ℝ) |
233 | 230, 232 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑀 + 1) ∈ ℝ) |
234 | 230, 233 | ltnled 10858 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀)) |
235 | 231, 234 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀) |
236 | | breq1 5030 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = (𝑀 + 1) → (𝑖 ≤ 𝑀 ↔ (𝑀 + 1) ≤ 𝑀)) |
237 | 236 | notbid 321 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = (𝑀 + 1) → (¬ 𝑖 ≤ 𝑀 ↔ ¬ (𝑀 + 1) ≤ 𝑀)) |
238 | 235, 237 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑖 = (𝑀 + 1) → ¬ 𝑖 ≤ 𝑀)) |
239 | 238 | con2d 136 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑖 ≤ 𝑀 → ¬ 𝑖 = (𝑀 + 1))) |
240 | | elfzle2 12995 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ≤ 𝑀) |
241 | 239, 240 | impel 509 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ¬ 𝑖 = (𝑀 + 1)) |
242 | | iffalse 4420 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑖 = (𝑀 + 1) → if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) = (𝐸‘𝑖)) |
243 | 242 | oveq1d 7179 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑖 = (𝑀 + 1) → (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)) = ((𝐸‘𝑖) + (𝑊 · 𝐷))) |
244 | 241, 243 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (if(𝑖 = (𝑀 + 1), 0, (𝐸‘𝑖)) + (𝑊 · 𝐷)) = ((𝐸‘𝑖) + (𝑊 · 𝐷))) |
245 | 229, 244 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑃‘𝑖) = ((𝐸‘𝑖) + (𝑊 · 𝐷))) |
246 | 245 | oveq2d 7180 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃‘𝑖)) = (𝑇 + ((𝐸‘𝑖) + (𝑊 · 𝐷)))) |
247 | 47 | nncnd 11725 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑇 ∈ ℂ) |
248 | 247 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑇 ∈ ℂ) |
249 | 101 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · 𝐷) ∈ ℂ) |
250 | 248, 80, 249 | add12d 10937 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑇 + ((𝐸‘𝑖) + (𝑊 · 𝐷))) = ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷)))) |
251 | 45 | oveq1i 7174 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇 + (𝑊 · 𝐷)) = ((𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) + (𝑊 · 𝐷)) |
252 | 16 | nncnd 11725 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐵 ∈ ℂ) |
253 | 120, 109 | subcld 11068 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑉 − 𝐷) ∈ ℂ) |
254 | 113, 253 | addcld 10731 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐴 + (𝑉 − 𝐷)) ∈ ℂ) |
255 | | ax-1cn 10666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℂ |
256 | | subcl 10956 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 + (𝑉 − 𝐷)) ∈ ℂ ∧ 1 ∈ ℂ)
→ ((𝐴 + (𝑉 − 𝐷)) − 1) ∈
ℂ) |
257 | 254, 255,
256 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐴 + (𝑉 − 𝐷)) − 1) ∈
ℂ) |
258 | 105, 257 | mulcld 10732 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) ∈
ℂ) |
259 | 252, 258,
101 | addassd 10734 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷)))) |
260 | 105, 257,
109 | adddid 10736 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑊 · (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷)) = ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷))) |
261 | 113, 253,
109 | addassd 10734 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝐴 + (𝑉 − 𝐷)) + 𝐷) = (𝐴 + ((𝑉 − 𝐷) + 𝐷))) |
262 | 120, 109 | npcand 11072 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((𝑉 − 𝐷) + 𝐷) = 𝑉) |
263 | 262 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝐴 + ((𝑉 − 𝐷) + 𝐷)) = (𝐴 + 𝑉)) |
264 | 261, 263 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((𝐴 + (𝑉 − 𝐷)) + 𝐷) = (𝐴 + 𝑉)) |
265 | 264 | oveq1d 7179 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((𝐴 + (𝑉 − 𝐷)) + 𝐷) − 1) = ((𝐴 + 𝑉) − 1)) |
266 | | 1cnd 10707 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 1 ∈
ℂ) |
267 | 254, 109,
266 | addsubd 11089 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((𝐴 + (𝑉 − 𝐷)) + 𝐷) − 1) = (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷)) |
268 | 113, 120,
266 | addsubd 11089 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝐴 + 𝑉) − 1) = ((𝐴 − 1) + 𝑉)) |
269 | 265, 267,
268 | 3eqtr3d 2781 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷) = ((𝐴 − 1) + 𝑉)) |
270 | 269 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑊 · (((𝐴 + (𝑉 − 𝐷)) − 1) + 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉))) |
271 | 260, 270 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷)) = (𝑊 · ((𝐴 − 1) + 𝑉))) |
272 | 271 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐵 + ((𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) + (𝑊 · 𝐷))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))) |
273 | 259, 272 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))) |
274 | 251, 273 | syl5eq 2785 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑇 + (𝑊 · 𝐷)) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))) |
275 | 274 | oveq2d 7180 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸‘𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))) |
276 | 275 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐸‘𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))) |
277 | 88 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ) |
278 | 80, 77, 277 | addassd 10734 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐸‘𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐸‘𝑖) + (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))) |
279 | 80, 77 | addcomd 10913 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + 𝐵) = (𝐵 + (𝐸‘𝑖))) |
280 | 279 | oveq1d 7179 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐸‘𝑖) + 𝐵) + (𝑊 · ((𝐴 − 1) + 𝑉))) = ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))) |
281 | 276, 278,
280 | 3eqtr2d 2779 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐸‘𝑖) + (𝑇 + (𝑊 · 𝐷))) = ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))) |
282 | 246, 250,
281 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑇 + (𝑃‘𝑖)) = ((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))) |
283 | 282, 245 | oveq12d 7182 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) = (((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)((𝐸‘𝑖) + (𝑊 · 𝐷)))) |
284 | | cnvimass 5917 |
. . . . . . . . . . . . . . . . . . 19
⊢ (◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ⊆ dom 𝐺 |
285 | 284, 14 | fssdm 6518 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ⊆ (1...𝑊)) |
286 | 285 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) ⊆ (1...𝑊)) |
287 | | vdwapid1 16404 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ ℕ ∧ (𝐵 + (𝐸‘𝑖)) ∈ ℕ ∧ (𝐸‘𝑖) ∈ ℕ) → (𝐵 + (𝐸‘𝑖)) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖))) |
288 | 160, 162,
79, 287 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ ((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖))) |
289 | 153, 288 | sseldd 3876 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ (◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))})) |
290 | 286, 289 | sseldd 3876 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ (1...𝑊)) |
291 | | fvoveq1 7187 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝐵 + (𝐸‘𝑖)) → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))) |
292 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) |
293 | | fvex 6681 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V |
294 | 291, 292,
293 | fvmpt 6769 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 + (𝐸‘𝑖)) ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))) |
295 | 290, 294 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))) |
296 | | vdwapid1 16404 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷)) |
297 | 10, 41, 42, 296 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷)) |
298 | 43, 297 | sseldd 3876 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐴 ∈ (◡𝐹 “ {𝐺})) |
299 | | fniniseg 6831 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹 Fn (1...𝑉) → (𝐴 ∈ (◡𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹‘𝐴) = 𝐺))) |
300 | 146, 299 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐴 ∈ (◡𝐹 “ {𝐺}) ↔ (𝐴 ∈ (1...𝑉) ∧ (𝐹‘𝐴) = 𝐺))) |
301 | 298, 300 | mpbid 235 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐴 ∈ (1...𝑉) ∧ (𝐹‘𝐴) = 𝐺)) |
302 | 301 | simprd 499 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹‘𝐴) = 𝐺) |
303 | 301 | simpld 498 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ∈ (1...𝑉)) |
304 | | oveq1 7171 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝐴 → (𝑥 − 1) = (𝐴 − 1)) |
305 | 304 | oveq1d 7179 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝐴 → ((𝑥 − 1) + 𝑉) = ((𝐴 − 1) + 𝑉)) |
306 | 305 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝐴 → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · ((𝐴 − 1) + 𝑉))) |
307 | 306 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝐴 → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) |
308 | 307 | fveq2d 6672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝐴 → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) |
309 | 308 | mpteq2dv 5123 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝐴 → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))) |
310 | 190 | mptex 6990 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉))))) ∈ V |
311 | 309, 40, 310 | fvmpt 6769 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ (1...𝑉) → (𝐹‘𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))) |
312 | 303, 311 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹‘𝐴) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))) |
313 | 302, 312 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺 = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))) |
314 | 313 | fveq1d 6670 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺‘(𝐵 + (𝐸‘𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖)))) |
315 | 314 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐵 + (𝐸‘𝑖))) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘(𝐵 + (𝐸‘𝑖)))) |
316 | 282 | fveq2d 6672 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃‘𝑖))) = (𝐻‘((𝐵 + (𝐸‘𝑖)) + (𝑊 · ((𝐴 − 1) + 𝑉))))) |
317 | 295, 315,
316 | 3eqtr4rd 2784 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘(𝑇 + (𝑃‘𝑖))) = (𝐺‘(𝐵 + (𝐸‘𝑖)))) |
318 | 317 | sneqd 4525 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → {(𝐻‘(𝑇 + (𝑃‘𝑖)))} = {(𝐺‘(𝐵 + (𝐸‘𝑖)))}) |
319 | 318 | imaeq2d 5897 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) = (◡𝐻 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))})) |
320 | 217, 283,
319 | 3sstr4d 3922 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})) |
321 | 320 | ex 416 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑖 ∈ (1...𝑀) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))) |
322 | 252 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ ℂ) |
323 | 88 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℂ) |
324 | 322, 323,
98 | addassd 10734 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))) |
325 | 127 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) = (𝐵 + ((𝑊 · ((𝐴 − 1) + 𝑉)) + (𝑚 · (𝑊 · 𝐷))))) |
326 | 324, 325 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) = (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) |
327 | 38 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑉 ∈ ℕ) |
328 | 12 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℕ) |
329 | | eluzfz1 12998 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑀)) |
330 | 52, 329 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 1 ∈ (1...𝑀)) |
331 | 330 | ne0d 4222 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1...𝑀) ≠ ∅) |
332 | | elfzuz3 12988 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 + (𝐸‘𝑖)) ∈ (1...𝑊) → 𝑊 ∈ (ℤ≥‘(𝐵 + (𝐸‘𝑖)))) |
333 | 290, 332 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ≥‘(𝐵 + (𝐸‘𝑖)))) |
334 | 16 | nnzd 12160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝐵 ∈ ℤ) |
335 | | uzid 12332 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
(ℤ≥‘𝐵)) |
336 | 334, 335 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐵 ∈ (ℤ≥‘𝐵)) |
337 | 336 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ∈ (ℤ≥‘𝐵)) |
338 | 79 | nnnn0d 12029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐸‘𝑖) ∈
ℕ0) |
339 | | uzaddcl 12379 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 ∈
(ℤ≥‘𝐵) ∧ (𝐸‘𝑖) ∈ ℕ0) → (𝐵 + (𝐸‘𝑖)) ∈ (ℤ≥‘𝐵)) |
340 | 337, 338,
339 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐵 + (𝐸‘𝑖)) ∈ (ℤ≥‘𝐵)) |
341 | | uztrn 12335 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑊 ∈
(ℤ≥‘(𝐵 + (𝐸‘𝑖))) ∧ (𝐵 + (𝐸‘𝑖)) ∈ (ℤ≥‘𝐵)) → 𝑊 ∈ (ℤ≥‘𝐵)) |
342 | 333, 340,
341 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑊 ∈ (ℤ≥‘𝐵)) |
343 | | eluzle 12330 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑊 ∈
(ℤ≥‘𝐵) → 𝐵 ≤ 𝑊) |
344 | 342, 343 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐵 ≤ 𝑊) |
345 | 344 | ralrimiva 3096 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊) |
346 | | r19.2z 4378 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1...𝑀) ≠
∅ ∧ ∀𝑖
∈ (1...𝑀)𝐵 ≤ 𝑊) → ∃𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊) |
347 | 331, 345,
346 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ∃𝑖 ∈ (1...𝑀)𝐵 ≤ 𝑊) |
348 | | idd 24 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ (1...𝑀) → (𝐵 ≤ 𝑊 → 𝐵 ≤ 𝑊)) |
349 | 348 | rexlimiv 3189 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃𝑖 ∈
(1...𝑀)𝐵 ≤ 𝑊 → 𝐵 ≤ 𝑊) |
350 | 347, 349 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐵 ≤ 𝑊) |
351 | 12 | nnzd 12160 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑊 ∈ ℤ) |
352 | | fznn 13059 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑊 ∈ ℤ → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵 ≤ 𝑊))) |
353 | 351, 352 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐵 ∈ (1...𝑊) ↔ (𝐵 ∈ ℕ ∧ 𝐵 ≤ 𝑊))) |
354 | 16, 350, 353 | mpbir2and 713 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐵 ∈ (1...𝑊)) |
355 | 354 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐵 ∈ (1...𝑊)) |
356 | 327, 328,
151, 355 | vdwlem3 16412 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉)))) |
357 | 326, 356 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉)))) |
358 | | fvoveq1 7187 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) |
359 | | fvex 6681 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))) ∈ V |
360 | 358, 178,
359 | fvmpt 6769 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) |
361 | 355, 360 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) |
362 | 194 | fveq1d 6670 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉)))))‘𝐵)) |
363 | 326 | fveq2d 6672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐻‘(𝐵 + (𝑊 · (((𝐴 + (𝑚 · 𝐷)) − 1) + 𝑉))))) |
364 | 361, 362,
363 | 3eqtr4rd 2784 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵)) |
365 | 357, 364 | jca 515 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵))) |
366 | | eleq1 2820 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ↔ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))))) |
367 | | fveqeq2 6677 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝐻‘𝑧) = (𝐺‘𝐵) ↔ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵))) |
368 | 366, 367 | anbi12d 634 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → ((𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵)) ↔ (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷)))) = (𝐺‘𝐵)))) |
369 | 365, 368 | syl5ibrcom 250 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵)))) |
370 | 369 | rexlimdva 3193 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))) → (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵)))) |
371 | 16, 87 | nnaddcld 11761 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ) |
372 | | vdwapval 16402 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℕ0
∧ (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ ∧ (𝑊 · 𝐷) ∈ ℕ) → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))))) |
373 | 139, 371,
65, 372 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑧 = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) + (𝑚 · (𝑊 · 𝐷))))) |
374 | | fniniseg 6831 |
. . . . . . . . . . . . . . 15
⊢ (𝐻 Fn (1...(𝑊 · (2 · 𝑉))) → (𝑧 ∈ (◡𝐻 “ {(𝐺‘𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵)))) |
375 | 212, 374 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑧 ∈ (◡𝐻 “ {(𝐺‘𝐵)}) ↔ (𝑧 ∈ (1...(𝑊 · (2 · 𝑉))) ∧ (𝐻‘𝑧) = (𝐺‘𝐵)))) |
376 | 370, 373,
375 | 3imtr4d 297 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑧 ∈ ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) → 𝑧 ∈ (◡𝐻 “ {(𝐺‘𝐵)}))) |
377 | 376 | ssrdv 3881 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷)) ⊆ (◡𝐻 “ {(𝐺‘𝐵)})) |
378 | 18 | peano2nnd 11726 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀 + 1) ∈ ℕ) |
379 | 378, 51 | eleqtrdi 2843 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 + 1) ∈
(ℤ≥‘1)) |
380 | | eluzfz2 12999 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 + 1) ∈
(ℤ≥‘1) → (𝑀 + 1) ∈ (1...(𝑀 + 1))) |
381 | | iftrue 4417 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑀 + 1) → if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) = 0) |
382 | 381 | oveq1d 7179 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑀 + 1) → (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)) = (0 + (𝑊 · 𝐷))) |
383 | | ovex 7197 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 +
(𝑊 · 𝐷)) ∈ V |
384 | 382, 46, 383 | fvmpt 6769 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 + 1) ∈ (1...(𝑀 + 1)) → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷))) |
385 | 379, 380,
384 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃‘(𝑀 + 1)) = (0 + (𝑊 · 𝐷))) |
386 | 101 | addid2d 10912 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0 + (𝑊 · 𝐷)) = (𝑊 · 𝐷)) |
387 | 385, 386 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃‘(𝑀 + 1)) = (𝑊 · 𝐷)) |
388 | 387 | oveq2d 7180 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝑇 + (𝑊 · 𝐷))) |
389 | 388, 274 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑇 + (𝑃‘(𝑀 + 1))) = (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))) |
390 | 389, 387 | oveq12d 7182 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) = ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))(AP‘𝐾)(𝑊 · 𝐷))) |
391 | | fvoveq1 7187 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝐵 → (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))) |
392 | | fvex 6681 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉)))) ∈ V |
393 | 391, 292,
392 | fvmpt 6769 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ (1...𝑊) → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))) |
394 | 354, 393 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))) |
395 | 313 | fveq1d 6670 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺‘𝐵) = ((𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝐴 − 1) + 𝑉)))))‘𝐵)) |
396 | 389 | fveq2d 6672 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐻‘(𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))))) |
397 | 394, 395,
396 | 3eqtr4rd 2784 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) = (𝐺‘𝐵)) |
398 | 397 | sneqd 4525 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))} = {(𝐺‘𝐵)}) |
399 | 398 | imaeq2d 5897 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}) = (◡𝐻 “ {(𝐺‘𝐵)})) |
400 | 377, 390,
399 | 3sstr4d 3922 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})) |
401 | | fveq2 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑀 + 1) → (𝑃‘𝑖) = (𝑃‘(𝑀 + 1))) |
402 | 401 | oveq2d 7180 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑀 + 1) → (𝑇 + (𝑃‘𝑖)) = (𝑇 + (𝑃‘(𝑀 + 1)))) |
403 | 402, 401 | oveq12d 7182 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) = ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1)))) |
404 | 402 | fveq2d 6672 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑀 + 1) → (𝐻‘(𝑇 + (𝑃‘𝑖))) = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))) |
405 | 404 | sneqd 4525 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑀 + 1) → {(𝐻‘(𝑇 + (𝑃‘𝑖)))} = {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}) |
406 | 405 | imaeq2d 5897 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑀 + 1) → (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) = (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))})) |
407 | 403, 406 | sseq12d 3908 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑀 + 1) → (((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) ↔ ((𝑇 + (𝑃‘(𝑀 + 1)))(AP‘𝐾)(𝑃‘(𝑀 + 1))) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))}))) |
408 | 400, 407 | syl5ibrcom 250 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑖 = (𝑀 + 1) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))) |
409 | 321, 408 | jaod 858 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑖 ∈ (1...𝑀) ∨ 𝑖 = (𝑀 + 1)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))) |
410 | 75, 409 | sylbid 243 |
. . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ (1...(𝑀 + 1)) → ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))) |
411 | 410 | ralrimiv 3095 |
. . . . . . 7
⊢ (𝜑 → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})) |
412 | 411 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})) |
413 | 220 | rexeqdv 3316 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ ∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))))) |
414 | | rexun 4078 |
. . . . . . . . . . . . 13
⊢
(∃𝑖 ∈
((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))))) |
415 | 317 | eqeq2d 2749 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))))) |
416 | 415 | rexbidva 3205 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))))) |
417 | | ovex 7197 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 + 1) ∈ V |
418 | 404 | eqeq2d 2749 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑀 + 1) → (𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))))) |
419 | 417, 418 | rexsn 4570 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑖 ∈
{(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1))))) |
420 | 397 | eqeq2d 2749 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 = (𝐻‘(𝑇 + (𝑃‘(𝑀 + 1)))) ↔ 𝑥 = (𝐺‘𝐵))) |
421 | 419, 420 | syl5bb 286 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ 𝑥 = (𝐺‘𝐵))) |
422 | 416, 421 | orbi12d 918 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((∃𝑖 ∈ (1...𝑀)𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ∨ ∃𝑖 ∈ {(𝑀 + 1)}𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵)))) |
423 | 414, 422 | syl5bb 286 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∃𝑖 ∈ ((1...𝑀) ∪ {(𝑀 + 1)})𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵)))) |
424 | 413, 423 | bitrd 282 |
. . . . . . . . . . 11
⊢ (𝜑 → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵)))) |
425 | 424 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖))) ↔ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵)))) |
426 | 425 | abbidv 2802 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))} = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))}) |
427 | | eqid 2738 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))) |
428 | 427 | rnmpt 5792 |
. . . . . . . . 9
⊢ ran
(𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))) = {𝑥 ∣ ∃𝑖 ∈ (1...(𝑀 + 1))𝑥 = (𝐻‘(𝑇 + (𝑃‘𝑖)))} |
429 | 2 | rnmpt 5792 |
. . . . . . . . . . 11
⊢ ran 𝐽 = {𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))} |
430 | | df-sn 4514 |
. . . . . . . . . . 11
⊢ {(𝐺‘𝐵)} = {𝑥 ∣ 𝑥 = (𝐺‘𝐵)} |
431 | 429, 430 | uneq12i 4049 |
. . . . . . . . . 10
⊢ (ran
𝐽 ∪ {(𝐺‘𝐵)}) = ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))} ∪ {𝑥 ∣ 𝑥 = (𝐺‘𝐵)}) |
432 | | unab 4186 |
. . . . . . . . . 10
⊢ ({𝑥 ∣ ∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖)))} ∪ {𝑥 ∣ 𝑥 = (𝐺‘𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))} |
433 | 431, 432 | eqtri 2761 |
. . . . . . . . 9
⊢ (ran
𝐽 ∪ {(𝐺‘𝐵)}) = {𝑥 ∣ (∃𝑖 ∈ (1...𝑀)𝑥 = (𝐺‘(𝐵 + (𝐸‘𝑖))) ∨ 𝑥 = (𝐺‘𝐵))} |
434 | 426, 428,
433 | 3eqtr4g 2798 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖)))) = (ran 𝐽 ∪ {(𝐺‘𝐵)})) |
435 | 434 | fveq2d 6672 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (♯‘(ran 𝐽 ∪ {(𝐺‘𝐵)}))) |
436 | | fzfi 13424 |
. . . . . . . . . 10
⊢
(1...𝑀) ∈
Fin |
437 | | dffn4 6592 |
. . . . . . . . . . 11
⊢ (𝐽 Fn (1...𝑀) ↔ 𝐽:(1...𝑀)–onto→ran 𝐽) |
438 | 3, 437 | mpbi 233 |
. . . . . . . . . 10
⊢ 𝐽:(1...𝑀)–onto→ran 𝐽 |
439 | | fofi 8876 |
. . . . . . . . . 10
⊢
(((1...𝑀) ∈ Fin
∧ 𝐽:(1...𝑀)–onto→ran 𝐽) → ran 𝐽 ∈ Fin) |
440 | 436, 438,
439 | mp2an 692 |
. . . . . . . . 9
⊢ ran 𝐽 ∈ Fin |
441 | 440 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐽 ∈ Fin) |
442 | | fvex 6681 |
. . . . . . . . 9
⊢ (𝐺‘𝐵) ∈ V |
443 | | hashunsng 13838 |
. . . . . . . . 9
⊢ ((𝐺‘𝐵) ∈ V → ((ran 𝐽 ∈ Fin ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺‘𝐵)})) = ((♯‘ran 𝐽) + 1))) |
444 | 442, 443 | ax-mp 5 |
. . . . . . . 8
⊢ ((ran
𝐽 ∈ Fin ∧ ¬
(𝐺‘𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺‘𝐵)})) = ((♯‘ran 𝐽) + 1)) |
445 | 441, 444 | sylan 583 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘(ran 𝐽 ∪ {(𝐺‘𝐵)})) = ((♯‘ran 𝐽) + 1)) |
446 | 44 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘ran 𝐽) = 𝑀) |
447 | 446 | oveq1d 7179 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ((♯‘ran 𝐽) + 1) = (𝑀 + 1)) |
448 | 435, 445,
447 | 3eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1)) |
449 | 412, 448 | jca 515 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1))) |
450 | | oveq1 7171 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑇 → (𝑎 + (𝑑‘𝑖)) = (𝑇 + (𝑑‘𝑖))) |
451 | 450 | oveq1d 7179 |
. . . . . . . . 9
⊢ (𝑎 = 𝑇 → ((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) = ((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖))) |
452 | | fvoveq1 7187 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑇 → (𝐻‘(𝑎 + (𝑑‘𝑖))) = (𝐻‘(𝑇 + (𝑑‘𝑖)))) |
453 | 452 | sneqd 4525 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑇 → {(𝐻‘(𝑎 + (𝑑‘𝑖)))} = {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) |
454 | 453 | imaeq2d 5897 |
. . . . . . . . 9
⊢ (𝑎 = 𝑇 → (◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) = (◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))})) |
455 | 451, 454 | sseq12d 3908 |
. . . . . . . 8
⊢ (𝑎 = 𝑇 → (((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ↔ ((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}))) |
456 | 455 | ralbidv 3109 |
. . . . . . 7
⊢ (𝑎 = 𝑇 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}))) |
457 | 452 | mpteq2dv 5123 |
. . . . . . . . 9
⊢ (𝑎 = 𝑇 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) |
458 | 457 | rneqd 5775 |
. . . . . . . 8
⊢ (𝑎 = 𝑇 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) |
459 | 458 | fveqeq2d 6676 |
. . . . . . 7
⊢ (𝑎 = 𝑇 → ((♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1) ↔ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1))) |
460 | 456, 459 | anbi12d 634 |
. . . . . 6
⊢ (𝑎 = 𝑇 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1)))) |
461 | | fveq1 6667 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑃 → (𝑑‘𝑖) = (𝑃‘𝑖)) |
462 | 461 | oveq2d 7180 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑃 → (𝑇 + (𝑑‘𝑖)) = (𝑇 + (𝑃‘𝑖))) |
463 | 462, 461 | oveq12d 7182 |
. . . . . . . . 9
⊢ (𝑑 = 𝑃 → ((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) = ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖))) |
464 | 462 | fveq2d 6672 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑃 → (𝐻‘(𝑇 + (𝑑‘𝑖))) = (𝐻‘(𝑇 + (𝑃‘𝑖)))) |
465 | 464 | sneqd 4525 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑃 → {(𝐻‘(𝑇 + (𝑑‘𝑖)))} = {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) |
466 | 465 | imaeq2d 5897 |
. . . . . . . . 9
⊢ (𝑑 = 𝑃 → (◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) = (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))})) |
467 | 463, 466 | sseq12d 3908 |
. . . . . . . 8
⊢ (𝑑 = 𝑃 → (((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ↔ ((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))) |
468 | 467 | ralbidv 3109 |
. . . . . . 7
⊢ (𝑑 = 𝑃 → (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ↔ ∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}))) |
469 | 464 | mpteq2dv 5123 |
. . . . . . . . 9
⊢ (𝑑 = 𝑃 → (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))) = (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) |
470 | 469 | rneqd 5775 |
. . . . . . . 8
⊢ (𝑑 = 𝑃 → ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖)))) = ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) |
471 | 470 | fveqeq2d 6676 |
. . . . . . 7
⊢ (𝑑 = 𝑃 → ((♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1) ↔ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1))) |
472 | 468, 471 | anbi12d 634 |
. . . . . 6
⊢ (𝑑 = 𝑃 → ((∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑑‘𝑖))))) = (𝑀 + 1)) ↔ (∀𝑖 ∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1)))) |
473 | 460, 472 | rspc2ev 3536 |
. . . . 5
⊢ ((𝑇 ∈ ℕ ∧ 𝑃 ∈ (ℕ
↑m (1...(𝑀
+ 1))) ∧ (∀𝑖
∈ (1...(𝑀 + 1))((𝑇 + (𝑃‘𝑖))(AP‘𝐾)(𝑃‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑇 + (𝑃‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑇 + (𝑃‘𝑖))))) = (𝑀 + 1))) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m
(1...(𝑀 +
1)))(∀𝑖 ∈
(1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1))) |
474 | 48, 73, 449, 473 | syl3anc 1372 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m
(1...(𝑀 +
1)))(∀𝑖 ∈
(1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1))) |
475 | | ovex 7197 |
. . . . 5
⊢
(1...(𝑊 · (2
· 𝑉))) ∈
V |
476 | 10 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝐾 ∈ ℕ) |
477 | 476 | nnnn0d 12029 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝐾 ∈
ℕ0) |
478 | 39 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅) |
479 | 18 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 𝑀 ∈ ℕ) |
480 | 479 | peano2nnd 11726 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (𝑀 + 1) ∈ ℕ) |
481 | | eqid 2738 |
. . . . 5
⊢
(1...(𝑀 + 1)) =
(1...(𝑀 +
1)) |
482 | 475, 477,
478, 480, 481 | vdwpc 16409 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m
(1...(𝑀 +
1)))(∀𝑖 ∈
(1...(𝑀 + 1))((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐻 “ {(𝐻‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...(𝑀 + 1)) ↦ (𝐻‘(𝑎 + (𝑑‘𝑖))))) = (𝑀 + 1)))) |
483 | 474, 482 | mpbird 260 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → 〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻) |
484 | 483 | orcd 872 |
. 2
⊢ ((𝜑 ∧ ¬ (𝐺‘𝐵) ∈ ran 𝐽) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺)) |
485 | 37, 484 | pm2.61dan 813 |
1
⊢ (𝜑 → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺)) |