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

Theorem seqcoll2 14470
Description: The function 𝐹 contains a sparse set of nonzero values to be summed. The function 𝐺 is an order isomorphism from the set of nonzero values of 𝐹 to a 1-based finite sequence, and 𝐻 collects these nonzero values together. Under these conditions, the sum over the values in 𝐻 yields the same result as the sum over the original set 𝐹. (Contributed by Mario Carneiro, 13-Dec-2014.)
Hypotheses
Ref Expression
seqcoll2.1 ((𝜑𝑘𝑆) → (𝑍 + 𝑘) = 𝑘)
seqcoll2.1b ((𝜑𝑘𝑆) → (𝑘 + 𝑍) = 𝑘)
seqcoll2.c ((𝜑 ∧ (𝑘𝑆𝑛𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
seqcoll2.a (𝜑𝑍𝑆)
seqcoll2.2 (𝜑𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
seqcoll2.3 (𝜑𝐴 ≠ ∅)
seqcoll2.5 (𝜑𝐴 ⊆ (𝑀...𝑁))
seqcoll2.6 ((𝜑𝑘 ∈ (𝑀...𝑁)) → (𝐹𝑘) ∈ 𝑆)
seqcoll2.7 ((𝜑𝑘 ∈ ((𝑀...𝑁) ∖ 𝐴)) → (𝐹𝑘) = 𝑍)
seqcoll2.8 ((𝜑𝑛 ∈ (1...(♯‘𝐴))) → (𝐻𝑛) = (𝐹‘(𝐺𝑛)))
Assertion
Ref Expression
seqcoll2 (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq1( + , 𝐻)‘(♯‘𝐴)))
Distinct variable groups:   𝑘,𝑛,𝐴   𝑘,𝐹,𝑛   𝑘,𝐺,𝑛   𝑛,𝐻   𝑘,𝑀,𝑛   𝜑,𝑘,𝑛   𝑘,𝑁   + ,𝑘,𝑛   𝑆,𝑘,𝑛   𝑘,𝑍
Allowed substitution hints:   𝐻(𝑘)   𝑁(𝑛)   𝑍(𝑛)

Proof of Theorem seqcoll2
StepHypRef Expression
1 seqcoll2.1b . . 3 ((𝜑𝑘𝑆) → (𝑘 + 𝑍) = 𝑘)
2 fzssuz 13582 . . . 4 (𝑀...𝑁) ⊆ (ℤ𝑀)
3 seqcoll2.5 . . . . 5 (𝜑𝐴 ⊆ (𝑀...𝑁))
4 seqcoll2.2 . . . . . . . 8 (𝜑𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
5 isof1o 7330 . . . . . . . 8 (𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) → 𝐺:(1...(♯‘𝐴))–1-1-onto𝐴)
64, 5syl 17 . . . . . . 7 (𝜑𝐺:(1...(♯‘𝐴))–1-1-onto𝐴)
7 f1of 6838 . . . . . . 7 (𝐺:(1...(♯‘𝐴))–1-1-onto𝐴𝐺:(1...(♯‘𝐴))⟶𝐴)
86, 7syl 17 . . . . . 6 (𝜑𝐺:(1...(♯‘𝐴))⟶𝐴)
9 seqcoll2.3 . . . . . . . . . 10 (𝜑𝐴 ≠ ∅)
10 fzfi 13978 . . . . . . . . . . . . 13 (𝑀...𝑁) ∈ Fin
11 ssfi 9201 . . . . . . . . . . . . 13 (((𝑀...𝑁) ∈ Fin ∧ 𝐴 ⊆ (𝑀...𝑁)) → 𝐴 ∈ Fin)
1210, 3, 11sylancr 585 . . . . . . . . . . . 12 (𝜑𝐴 ∈ Fin)
13 hasheq0 14366 . . . . . . . . . . . 12 (𝐴 ∈ Fin → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅))
1412, 13syl 17 . . . . . . . . . . 11 (𝜑 → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅))
1514necon3bbid 2967 . . . . . . . . . 10 (𝜑 → (¬ (♯‘𝐴) = 0 ↔ 𝐴 ≠ ∅))
169, 15mpbird 256 . . . . . . . . 9 (𝜑 → ¬ (♯‘𝐴) = 0)
17 hashcl 14359 . . . . . . . . . . . 12 (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)
1812, 17syl 17 . . . . . . . . . . 11 (𝜑 → (♯‘𝐴) ∈ ℕ0)
19 elnn0 12512 . . . . . . . . . . 11 ((♯‘𝐴) ∈ ℕ0 ↔ ((♯‘𝐴) ∈ ℕ ∨ (♯‘𝐴) = 0))
2018, 19sylib 217 . . . . . . . . . 10 (𝜑 → ((♯‘𝐴) ∈ ℕ ∨ (♯‘𝐴) = 0))
2120ord 862 . . . . . . . . 9 (𝜑 → (¬ (♯‘𝐴) ∈ ℕ → (♯‘𝐴) = 0))
2216, 21mt3d 148 . . . . . . . 8 (𝜑 → (♯‘𝐴) ∈ ℕ)
23 nnuz 12903 . . . . . . . 8 ℕ = (ℤ‘1)
2422, 23eleqtrdi 2835 . . . . . . 7 (𝜑 → (♯‘𝐴) ∈ (ℤ‘1))
25 eluzfz2 13549 . . . . . . 7 ((♯‘𝐴) ∈ (ℤ‘1) → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
2624, 25syl 17 . . . . . 6 (𝜑 → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
278, 26ffvelcdmd 7094 . . . . 5 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ 𝐴)
283, 27sseldd 3977 . . . 4 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ (𝑀...𝑁))
292, 28sselid 3974 . . 3 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ (ℤ𝑀))
30 elfzuz3 13538 . . . 4 ((𝐺‘(♯‘𝐴)) ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ‘(𝐺‘(♯‘𝐴))))
3128, 30syl 17 . . 3 (𝜑𝑁 ∈ (ℤ‘(𝐺‘(♯‘𝐴))))
32 fzss2 13581 . . . . . . 7 (𝑁 ∈ (ℤ‘(𝐺‘(♯‘𝐴))) → (𝑀...(𝐺‘(♯‘𝐴))) ⊆ (𝑀...𝑁))
3331, 32syl 17 . . . . . 6 (𝜑 → (𝑀...(𝐺‘(♯‘𝐴))) ⊆ (𝑀...𝑁))
3433sselda 3976 . . . . 5 ((𝜑𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴)))) → 𝑘 ∈ (𝑀...𝑁))
35 seqcoll2.6 . . . . 5 ((𝜑𝑘 ∈ (𝑀...𝑁)) → (𝐹𝑘) ∈ 𝑆)
3634, 35syldan 589 . . . 4 ((𝜑𝑘 ∈ (𝑀...(𝐺‘(♯‘𝐴)))) → (𝐹𝑘) ∈ 𝑆)
37 seqcoll2.c . . . 4 ((𝜑 ∧ (𝑘𝑆𝑛𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)
3829, 36, 37seqcl 14028 . . 3 (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘(♯‘𝐴))) ∈ 𝑆)
39 peano2uz 12923 . . . . . . . 8 ((𝐺‘(♯‘𝐴)) ∈ (ℤ𝑀) → ((𝐺‘(♯‘𝐴)) + 1) ∈ (ℤ𝑀))
4029, 39syl 17 . . . . . . 7 (𝜑 → ((𝐺‘(♯‘𝐴)) + 1) ∈ (ℤ𝑀))
41 fzss1 13580 . . . . . . 7 (((𝐺‘(♯‘𝐴)) + 1) ∈ (ℤ𝑀) → (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ⊆ (𝑀...𝑁))
4240, 41syl 17 . . . . . 6 (𝜑 → (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ⊆ (𝑀...𝑁))
4342sselda 3976 . . . . 5 ((𝜑𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → 𝑘 ∈ (𝑀...𝑁))
44 eluzelre 12871 . . . . . . . . 9 ((𝐺‘(♯‘𝐴)) ∈ (ℤ𝑀) → (𝐺‘(♯‘𝐴)) ∈ ℝ)
4529, 44syl 17 . . . . . . . 8 (𝜑 → (𝐺‘(♯‘𝐴)) ∈ ℝ)
4645adantr 479 . . . . . . 7 ((𝜑𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → (𝐺‘(♯‘𝐴)) ∈ ℝ)
47 peano2re 11424 . . . . . . . 8 ((𝐺‘(♯‘𝐴)) ∈ ℝ → ((𝐺‘(♯‘𝐴)) + 1) ∈ ℝ)
4846, 47syl 17 . . . . . . 7 ((𝜑𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → ((𝐺‘(♯‘𝐴)) + 1) ∈ ℝ)
49 elfzelz 13541 . . . . . . . . 9 (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) → 𝑘 ∈ ℤ)
5049zred 12704 . . . . . . . 8 (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) → 𝑘 ∈ ℝ)
5150adantl 480 . . . . . . 7 ((𝜑𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → 𝑘 ∈ ℝ)
5246ltp1d 12182 . . . . . . 7 ((𝜑𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → (𝐺‘(♯‘𝐴)) < ((𝐺‘(♯‘𝐴)) + 1))
53 elfzle1 13544 . . . . . . . 8 (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) → ((𝐺‘(♯‘𝐴)) + 1) ≤ 𝑘)
5453adantl 480 . . . . . . 7 ((𝜑𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → ((𝐺‘(♯‘𝐴)) + 1) ≤ 𝑘)
5546, 48, 51, 52, 54ltletrd 11411 . . . . . 6 ((𝜑𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → (𝐺‘(♯‘𝐴)) < 𝑘)
566adantr 479 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → 𝐺:(1...(♯‘𝐴))–1-1-onto𝐴)
57 f1ocnv 6850 . . . . . . . . . . . . . 14 (𝐺:(1...(♯‘𝐴))–1-1-onto𝐴𝐺:𝐴1-1-onto→(1...(♯‘𝐴)))
5856, 57syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → 𝐺:𝐴1-1-onto→(1...(♯‘𝐴)))
59 f1of 6838 . . . . . . . . . . . . 13 (𝐺:𝐴1-1-onto→(1...(♯‘𝐴)) → 𝐺:𝐴⟶(1...(♯‘𝐴)))
6058, 59syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → 𝐺:𝐴⟶(1...(♯‘𝐴)))
61 simprr 771 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → 𝑘𝐴)
6260, 61ffvelcdmd 7094 . . . . . . . . . . 11 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → (𝐺𝑘) ∈ (1...(♯‘𝐴)))
6362elfzelzd 13542 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → (𝐺𝑘) ∈ ℤ)
6463zred 12704 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → (𝐺𝑘) ∈ ℝ)
6518adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → (♯‘𝐴) ∈ ℕ0)
6665nn0red 12571 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → (♯‘𝐴) ∈ ℝ)
67 elfzle2 13545 . . . . . . . . . 10 ((𝐺𝑘) ∈ (1...(♯‘𝐴)) → (𝐺𝑘) ≤ (♯‘𝐴))
6862, 67syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → (𝐺𝑘) ≤ (♯‘𝐴))
6964, 66, 68lensymd 11402 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → ¬ (♯‘𝐴) < (𝐺𝑘))
704adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))
7126adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → (♯‘𝐴) ∈ (1...(♯‘𝐴)))
72 isorel 7333 . . . . . . . . . 10 ((𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴) ∧ ((♯‘𝐴) ∈ (1...(♯‘𝐴)) ∧ (𝐺𝑘) ∈ (1...(♯‘𝐴)))) → ((♯‘𝐴) < (𝐺𝑘) ↔ (𝐺‘(♯‘𝐴)) < (𝐺‘(𝐺𝑘))))
7370, 71, 62, 72syl12anc 835 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → ((♯‘𝐴) < (𝐺𝑘) ↔ (𝐺‘(♯‘𝐴)) < (𝐺‘(𝐺𝑘))))
74 f1ocnvfv2 7286 . . . . . . . . . . 11 ((𝐺:(1...(♯‘𝐴))–1-1-onto𝐴𝑘𝐴) → (𝐺‘(𝐺𝑘)) = 𝑘)
7556, 61, 74syl2anc 582 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → (𝐺‘(𝐺𝑘)) = 𝑘)
7675breq2d 5161 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → ((𝐺‘(♯‘𝐴)) < (𝐺‘(𝐺𝑘)) ↔ (𝐺‘(♯‘𝐴)) < 𝑘))
7773, 76bitrd 278 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → ((♯‘𝐴) < (𝐺𝑘) ↔ (𝐺‘(♯‘𝐴)) < 𝑘))
7869, 77mtbid 323 . . . . . . 7 ((𝜑 ∧ (𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁) ∧ 𝑘𝐴)) → ¬ (𝐺‘(♯‘𝐴)) < 𝑘)
7978expr 455 . . . . . 6 ((𝜑𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → (𝑘𝐴 → ¬ (𝐺‘(♯‘𝐴)) < 𝑘))
8055, 79mt2d 136 . . . . 5 ((𝜑𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → ¬ 𝑘𝐴)
8143, 80eldifd 3955 . . . 4 ((𝜑𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → 𝑘 ∈ ((𝑀...𝑁) ∖ 𝐴))
82 seqcoll2.7 . . . 4 ((𝜑𝑘 ∈ ((𝑀...𝑁) ∖ 𝐴)) → (𝐹𝑘) = 𝑍)
8381, 82syldan 589 . . 3 ((𝜑𝑘 ∈ (((𝐺‘(♯‘𝐴)) + 1)...𝑁)) → (𝐹𝑘) = 𝑍)
841, 29, 31, 38, 83seqid2 14054 . 2 (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘(♯‘𝐴))) = (seq𝑀( + , 𝐹)‘𝑁))
85 seqcoll2.1 . . 3 ((𝜑𝑘𝑆) → (𝑍 + 𝑘) = 𝑘)
86 seqcoll2.a . . 3 (𝜑𝑍𝑆)
873, 2sstrdi 3989 . . 3 (𝜑𝐴 ⊆ (ℤ𝑀))
8833ssdifd 4137 . . . . 5 (𝜑 → ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴) ⊆ ((𝑀...𝑁) ∖ 𝐴))
8988sselda 3976 . . . 4 ((𝜑𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → 𝑘 ∈ ((𝑀...𝑁) ∖ 𝐴))
9089, 82syldan 589 . . 3 ((𝜑𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹𝑘) = 𝑍)
91 seqcoll2.8 . . 3 ((𝜑𝑛 ∈ (1...(♯‘𝐴))) → (𝐻𝑛) = (𝐹‘(𝐺𝑛)))
9285, 1, 37, 86, 4, 26, 87, 36, 90, 91seqcoll 14469 . 2 (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘(♯‘𝐴))) = (seq1( + , 𝐻)‘(♯‘𝐴)))
9384, 92eqtr3d 2767 1 (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq1( + , 𝐻)‘(♯‘𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 845   = wceq 1533  wcel 2098  wne 2929  cdif 3941  wss 3944  c0 4322   class class class wbr 5149  ccnv 5677  wf 6545  1-1-ontowf1o 6548  cfv 6549   Isom wiso 6550  (class class class)co 7419  Fincfn 8964  cr 11144  0cc0 11145  1c1 11146   + caddc 11148   < clt 11285  cle 11286  cn 12250  0cn0 12510  cuz 12860  ...cfz 13524  seqcseq 14007  chash 14333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11201  ax-resscn 11202  ax-1cn 11203  ax-icn 11204  ax-addcl 11205  ax-addrcl 11206  ax-mulcl 11207  ax-mulrcl 11208  ax-mulcom 11209  ax-addass 11210  ax-mulass 11211  ax-distr 11212  ax-i2m1 11213  ax-1ne0 11214  ax-1rid 11215  ax-rnegex 11216  ax-rrecex 11217  ax-cnre 11218  ax-pre-lttri 11219  ax-pre-lttrn 11220  ax-pre-ltadd 11221  ax-pre-mulgt0 11222
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-card 9969  df-pnf 11287  df-mnf 11288  df-xr 11289  df-ltxr 11290  df-le 11291  df-sub 11483  df-neg 11484  df-nn 12251  df-n0 12511  df-z 12597  df-uz 12861  df-fz 13525  df-seq 14008  df-hash 14334
This theorem is referenced by:  isercolllem3  15657  gsumval3  19891
  Copyright terms: Public domain W3C validator