Metamath Proof Explorer

Theorem vdwlem5

Description: Lemma for vdw . (Contributed by Mario Carneiro, 12-Sep-2014)

Ref Expression
Hypotheses vdwlem3.v ⊢ ( 𝜑 → 𝑉 ∈ ℕ )
vdwlem3.w ⊢ ( 𝜑 → 𝑊 ∈ ℕ )
vdwlem4.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
vdwlem4.h ⊢ ( 𝜑 → 𝐻 : ( 1 ... ( 𝑊 · ( 2 · 𝑉 ) ) ) ⟶ 𝑅 )
vdwlem4.f ⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... 𝑉 ) ↦ ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) ) )
vdwlem7.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
vdwlem7.g ⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑊 ) ⟶ 𝑅 )
vdwlem7.k ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
vdwlem7.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
vdwlem7.d ⊢ ( 𝜑 → 𝐷 ∈ ℕ )
vdwlem7.s ⊢ ( 𝜑 → ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) ⊆ ( ◡ 𝐹 “ { 𝐺 } ) )
vdwlem6.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
vdwlem6.e ⊢ ( 𝜑 → 𝐸 : ( 1 ... 𝑀 ) ⟶ ℕ )
vdwlem6.s ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐵 + ( 𝐸 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝐸 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝐵 + ( 𝐸 ‘ 𝑖 ) ) ) } ) )
vdwlem6.j ⊢ 𝐽 = ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝐵 + ( 𝐸 ‘ 𝑖 ) ) ) )
vdwlem6.r ⊢ ( 𝜑 → ( ♯ ‘ ran 𝐽 ) = 𝑀 )
vdwlem6.t ⊢ 𝑇 = ( 𝐵 + ( 𝑊 · ( ( 𝐴 + ( 𝑉 − 𝐷 ) ) − 1 ) ) )
vdwlem6.p ⊢ 𝑃 = ( 𝑗 ∈ ( 1 ... ( 𝑀 + 1 ) ) ↦ ( if ( 𝑗 = ( 𝑀 + 1 ) , 0 , ( 𝐸 ‘ 𝑗 ) ) + ( 𝑊 · 𝐷 ) ) )
Assertion vdwlem5 ( 𝜑 → 𝑇 ∈ ℕ )

Proof

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 2 nnnn0d ⊢ ( 𝜑 → 𝑊 ∈ ℕ0 )
20 1 nncnd ⊢ ( 𝜑 → 𝑉 ∈ ℂ )
21 10 nncnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
22 20 21 subcld ⊢ ( 𝜑 → ( 𝑉 − 𝐷 ) ∈ ℂ )
23 9 nncnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
24 22 23 npcand ⊢ ( 𝜑 → ( ( ( 𝑉 − 𝐷 ) − 𝐴 ) + 𝐴 ) = ( 𝑉 − 𝐷 ) )
25 20 21 23 subsub4d ⊢ ( 𝜑 → ( ( 𝑉 − 𝐷 ) − 𝐴 ) = ( 𝑉 − ( 𝐷 + 𝐴 ) ) )
26 21 23 addcomd ⊢ ( 𝜑 → ( 𝐷 + 𝐴 ) = ( 𝐴 + 𝐷 ) )
27 26 oveq2d ⊢ ( 𝜑 → ( 𝑉 − ( 𝐷 + 𝐴 ) ) = ( 𝑉 − ( 𝐴 + 𝐷 ) ) )
28 25 27 eqtrd ⊢ ( 𝜑 → ( ( 𝑉 − 𝐷 ) − 𝐴 ) = ( 𝑉 − ( 𝐴 + 𝐷 ) ) )
29 cnvimass ⊢ ( ◡ 𝐹 “ { 𝐺 } ) ⊆ dom 𝐹
30 1 2 3 4 5 vdwlem4 ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑉 ) ⟶ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) )
31 29 30 fssdm ⊢ ( 𝜑 → ( ◡ 𝐹 “ { 𝐺 } ) ⊆ ( 1 ... 𝑉 ) )
32 ssun2 ⊢ ( ( 𝐴 + 𝐷 ) ( AP ‘ ( 𝐾 − 1 ) ) 𝐷 ) ⊆ ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ ( 𝐾 − 1 ) ) 𝐷 ) )
33 uz2m1nn ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐾 − 1 ) ∈ ℕ )
34 8 33 syl ⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℕ )
35 9 10 nnaddcld ⊢ ( 𝜑 → ( 𝐴 + 𝐷 ) ∈ ℕ )
36 vdwapid1 ⊢ ( ( ( 𝐾 − 1 ) ∈ ℕ ∧ ( 𝐴 + 𝐷 ) ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 + 𝐷 ) ∈ ( ( 𝐴 + 𝐷 ) ( AP ‘ ( 𝐾 − 1 ) ) 𝐷 ) )
37 34 35 10 36 syl3anc ⊢ ( 𝜑 → ( 𝐴 + 𝐷 ) ∈ ( ( 𝐴 + 𝐷 ) ( AP ‘ ( 𝐾 − 1 ) ) 𝐷 ) )
38 32 37 sseldi ⊢ ( 𝜑 → ( 𝐴 + 𝐷 ) ∈ ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ ( 𝐾 − 1 ) ) 𝐷 ) ) )
39 eluz2nn ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → 𝐾 ∈ ℕ )
40 8 39 syl ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
41 40 nncnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
42 ax-1cn ⊢ 1 ∈ ℂ
43 npcan ⊢ ( ( 𝐾 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
44 41 42 43 sylancl ⊢ ( 𝜑 → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
45 44 fveq2d ⊢ ( 𝜑 → ( AP ‘ ( ( 𝐾 − 1 ) + 1 ) ) = ( AP ‘ 𝐾 ) )
46 45 oveqd ⊢ ( 𝜑 → ( 𝐴 ( AP ‘ ( ( 𝐾 − 1 ) + 1 ) ) 𝐷 ) = ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) )
47 nnm1nn0 ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 − 1 ) ∈ ℕ0 )
48 40 47 syl ⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℕ0 )
49 vdwapun ⊢ ( ( ( 𝐾 − 1 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( AP ‘ ( ( 𝐾 − 1 ) + 1 ) ) 𝐷 ) = ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ ( 𝐾 − 1 ) ) 𝐷 ) ) )
50 48 9 10 49 syl3anc ⊢ ( 𝜑 → ( 𝐴 ( AP ‘ ( ( 𝐾 − 1 ) + 1 ) ) 𝐷 ) = ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ ( 𝐾 − 1 ) ) 𝐷 ) ) )
51 46 50 eqtr3d ⊢ ( 𝜑 → ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) = ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ ( 𝐾 − 1 ) ) 𝐷 ) ) )
52 38 51 eleqtrrd ⊢ ( 𝜑 → ( 𝐴 + 𝐷 ) ∈ ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) )
53 11 52 sseldd ⊢ ( 𝜑 → ( 𝐴 + 𝐷 ) ∈ ( ◡ 𝐹 “ { 𝐺 } ) )
54 31 53 sseldd ⊢ ( 𝜑 → ( 𝐴 + 𝐷 ) ∈ ( 1 ... 𝑉 ) )
55 elfzuz3 ⊢ ( ( 𝐴 + 𝐷 ) ∈ ( 1 ... 𝑉 ) → 𝑉 ∈ ( ℤ≥ ‘ ( 𝐴 + 𝐷 ) ) )
56 54 55 syl ⊢ ( 𝜑 → 𝑉 ∈ ( ℤ≥ ‘ ( 𝐴 + 𝐷 ) ) )
57 uznn0sub ⊢ ( 𝑉 ∈ ( ℤ≥ ‘ ( 𝐴 + 𝐷 ) ) → ( 𝑉 − ( 𝐴 + 𝐷 ) ) ∈ ℕ0 )
58 56 57 syl ⊢ ( 𝜑 → ( 𝑉 − ( 𝐴 + 𝐷 ) ) ∈ ℕ0 )
59 28 58 eqeltrd ⊢ ( 𝜑 → ( ( 𝑉 − 𝐷 ) − 𝐴 ) ∈ ℕ0 )
60 nn0nnaddcl ⊢ ( ( ( ( 𝑉 − 𝐷 ) − 𝐴 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ ) → ( ( ( 𝑉 − 𝐷 ) − 𝐴 ) + 𝐴 ) ∈ ℕ )
61 59 9 60 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑉 − 𝐷 ) − 𝐴 ) + 𝐴 ) ∈ ℕ )
62 24 61 eqeltrrd ⊢ ( 𝜑 → ( 𝑉 − 𝐷 ) ∈ ℕ )
63 9 62 nnaddcld ⊢ ( 𝜑 → ( 𝐴 + ( 𝑉 − 𝐷 ) ) ∈ ℕ )
64 nnm1nn0 ⊢ ( ( 𝐴 + ( 𝑉 − 𝐷 ) ) ∈ ℕ → ( ( 𝐴 + ( 𝑉 − 𝐷 ) ) − 1 ) ∈ ℕ0 )
65 63 64 syl ⊢ ( 𝜑 → ( ( 𝐴 + ( 𝑉 − 𝐷 ) ) − 1 ) ∈ ℕ0 )
66 19 65 nn0mulcld ⊢ ( 𝜑 → ( 𝑊 · ( ( 𝐴 + ( 𝑉 − 𝐷 ) ) − 1 ) ) ∈ ℕ0 )
67 nnnn0addcl ⊢ ( ( 𝐵 ∈ ℕ ∧ ( 𝑊 · ( ( 𝐴 + ( 𝑉 − 𝐷 ) ) − 1 ) ) ∈ ℕ0 ) → ( 𝐵 + ( 𝑊 · ( ( 𝐴 + ( 𝑉 − 𝐷 ) ) − 1 ) ) ) ∈ ℕ )
68 12 66 67 syl2anc ⊢ ( 𝜑 → ( 𝐵 + ( 𝑊 · ( ( 𝐴 + ( 𝑉 − 𝐷 ) ) − 1 ) ) ) ∈ ℕ )
69 17 68 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℕ )