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