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

Theorem mtest 24096
Description: The Weierstrass M-test. If 𝐹 is a sequence of functions which are uniformly bounded by the convergent sequence 𝑀(𝑘), then the series generated by the sequence 𝐹 converges uniformly. (Contributed by Mario Carneiro, 3-Mar-2015.)
Hypotheses
Ref Expression
mtest.z 𝑍 = (ℤ𝑁)
mtest.n (𝜑𝑁 ∈ ℤ)
mtest.s (𝜑𝑆𝑉)
mtest.f (𝜑𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
mtest.m (𝜑𝑀𝑊)
mtest.c ((𝜑𝑘𝑍) → (𝑀𝑘) ∈ ℝ)
mtest.l ((𝜑 ∧ (𝑘𝑍𝑧𝑆)) → (abs‘((𝐹𝑘)‘𝑧)) ≤ (𝑀𝑘))
mtest.d (𝜑 → seq𝑁( + , 𝑀) ∈ dom ⇝ )
Assertion
Ref Expression
mtest (𝜑 → seq𝑁( ∘𝑓 + , 𝐹) ∈ dom (⇝𝑢𝑆))
Distinct variable groups:   𝑧,𝑘,𝐹   𝑘,𝑀,𝑧   𝑘,𝑁,𝑧   𝜑,𝑘,𝑧   𝑘,𝑍,𝑧   𝑆,𝑘,𝑧
Allowed substitution hints:   𝑉(𝑧,𝑘)   𝑊(𝑧,𝑘)

Proof of Theorem mtest
Dummy variables 𝑖 𝑗 𝑛 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mtest.n . . . 4 (𝜑𝑁 ∈ ℤ)
2 mtest.d . . . 4 (𝜑 → seq𝑁( + , 𝑀) ∈ dom ⇝ )
3 mtest.z . . . . 5 𝑍 = (ℤ𝑁)
43climcau 14351 . . . 4 ((𝑁 ∈ ℤ ∧ seq𝑁( + , 𝑀) ∈ dom ⇝ ) → ∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟)
51, 2, 4syl2anc 692 . . 3 (𝜑 → ∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟)
6 seqfn 12769 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℤ → seq𝑁( ∘𝑓 + , 𝐹) Fn (ℤ𝑁))
71, 6syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → seq𝑁( ∘𝑓 + , 𝐹) Fn (ℤ𝑁))
83fneq2i 5954 . . . . . . . . . . . . . . . . . 18 (seq𝑁( ∘𝑓 + , 𝐹) Fn 𝑍 ↔ seq𝑁( ∘𝑓 + , 𝐹) Fn (ℤ𝑁))
97, 8sylibr 224 . . . . . . . . . . . . . . . . 17 (𝜑 → seq𝑁( ∘𝑓 + , 𝐹) Fn 𝑍)
10 mtest.s . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑆𝑉)
11 elex 3202 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆𝑉𝑆 ∈ V)
1210, 11syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑆 ∈ V)
1312adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝑍) → 𝑆 ∈ V)
14 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝑍) → 𝑖𝑍)
1514, 3syl6eleq 2708 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝑍) → 𝑖 ∈ (ℤ𝑁))
16 mtest.f . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
1716adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖𝑍) → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
18 elfzuz 12296 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (𝑁...𝑖) → 𝑘 ∈ (ℤ𝑁))
1918, 3syl6eleqr 2709 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (𝑁...𝑖) → 𝑘𝑍)
20 ffvelrn 6323 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹:𝑍⟶(ℂ ↑𝑚 𝑆) ∧ 𝑘𝑍) → (𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆))
2117, 19, 20syl2an 494 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆))
22 elmapi 7839 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆) → (𝐹𝑘):𝑆⟶ℂ)
2321, 22syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘):𝑆⟶ℂ)
2423feqmptd 6216 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘) = (𝑧𝑆 ↦ ((𝐹𝑘)‘𝑧)))
2519adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → 𝑘𝑍)
26 fveq2 6158 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
2726fveq1d 6160 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑘 → ((𝐹𝑛)‘𝑧) = ((𝐹𝑘)‘𝑧))
28 eqid 2621 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)) = (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))
29 fvex 6168 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑘)‘𝑧) ∈ V
3027, 28, 29fvmpt 6249 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑍 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘) = ((𝐹𝑘)‘𝑧))
3125, 30syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘) = ((𝐹𝑘)‘𝑧))
3231mpteq2dv 4715 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝑧𝑆 ↦ ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘)) = (𝑧𝑆 ↦ ((𝐹𝑘)‘𝑧)))
3324, 32eqtr4d 2658 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘) = (𝑧𝑆 ↦ ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘)))
3413, 15, 33seqof 12814 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝑍) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)))
351adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧𝑆) → 𝑁 ∈ ℤ)
3616ffvelrnda 6325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑛𝑍) → (𝐹𝑛) ∈ (ℂ ↑𝑚 𝑆))
37 elmapi 7839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹𝑛) ∈ (ℂ ↑𝑚 𝑆) → (𝐹𝑛):𝑆⟶ℂ)
3836, 37syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑛𝑍) → (𝐹𝑛):𝑆⟶ℂ)
3938ffvelrnda 6325 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑛𝑍) ∧ 𝑧𝑆) → ((𝐹𝑛)‘𝑧) ∈ ℂ)
4039an32s 845 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ 𝑛𝑍) → ((𝐹𝑛)‘𝑧) ∈ ℂ)
4140, 28fmptd 6351 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)):𝑍⟶ℂ)
4241ffvelrnda 6325 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ 𝑖𝑍) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑖) ∈ ℂ)
433, 35, 42serf 12785 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧𝑆) → seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))):𝑍⟶ℂ)
4443ffvelrnda 6325 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ 𝑖𝑍) → (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) ∈ ℂ)
4544an32s 845 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝑍) ∧ 𝑧𝑆) → (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) ∈ ℂ)
46 eqid 2621 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))
4745, 46fmptd 6351 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝑍) → (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)):𝑆⟶ℂ)
48 cnex 9977 . . . . . . . . . . . . . . . . . . . . 21 ℂ ∈ V
49 elmapg 7830 . . . . . . . . . . . . . . . . . . . . 21 ((ℂ ∈ V ∧ 𝑆 ∈ V) → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) ∈ (ℂ ↑𝑚 𝑆) ↔ (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)):𝑆⟶ℂ))
5048, 13, 49sylancr 694 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝑍) → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) ∈ (ℂ ↑𝑚 𝑆) ↔ (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)):𝑆⟶ℂ))
5147, 50mpbird 247 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝑍) → (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) ∈ (ℂ ↑𝑚 𝑆))
5234, 51eqeltrd 2698 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖𝑍) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) ∈ (ℂ ↑𝑚 𝑆))
5352ralrimiva 2962 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑖𝑍 (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) ∈ (ℂ ↑𝑚 𝑆))
54 ffnfv 6354 . . . . . . . . . . . . . . . . 17 (seq𝑁( ∘𝑓 + , 𝐹):𝑍⟶(ℂ ↑𝑚 𝑆) ↔ (seq𝑁( ∘𝑓 + , 𝐹) Fn 𝑍 ∧ ∀𝑖𝑍 (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) ∈ (ℂ ↑𝑚 𝑆)))
559, 53, 54sylanbrc 697 . . . . . . . . . . . . . . . 16 (𝜑 → seq𝑁( ∘𝑓 + , 𝐹):𝑍⟶(ℂ ↑𝑚 𝑆))
5655ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → seq𝑁( ∘𝑓 + , 𝐹):𝑍⟶(ℂ ↑𝑚 𝑆))
573uztrn2 11665 . . . . . . . . . . . . . . . 16 ((𝑗𝑍𝑖 ∈ (ℤ𝑗)) → 𝑖𝑍)
5857adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑖𝑍)
5956, 58ffvelrnd 6326 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) ∈ (ℂ ↑𝑚 𝑆))
60 elmapi 7839 . . . . . . . . . . . . . 14 ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) ∈ (ℂ ↑𝑚 𝑆) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖):𝑆⟶ℂ)
6159, 60syl 17 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖):𝑆⟶ℂ)
6261ffvelrnda 6325 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) ∈ ℂ)
63 simprl 793 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑗𝑍)
6456, 63ffvelrnd 6326 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑗) ∈ (ℂ ↑𝑚 𝑆))
65 elmapi 7839 . . . . . . . . . . . . . 14 ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗) ∈ (ℂ ↑𝑚 𝑆) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑗):𝑆⟶ℂ)
6664, 65syl 17 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑗):𝑆⟶ℂ)
6766ffvelrnda 6325 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧) ∈ ℂ)
6862, 67subcld 10352 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧)) ∈ ℂ)
6968abscld 14125 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) ∈ ℝ)
70 fzfid 12728 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((𝑗 + 1)...𝑖) ∈ Fin)
71 ssun2 3761 . . . . . . . . . . . . . . . 16 ((𝑗 + 1)...𝑖) ⊆ ((𝑁...𝑗) ∪ ((𝑗 + 1)...𝑖))
7263, 3syl6eleq 2708 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑗 ∈ (ℤ𝑁))
73 simprr 795 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑖 ∈ (ℤ𝑗))
74 elfzuzb 12294 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑁...𝑖) ↔ (𝑗 ∈ (ℤ𝑁) ∧ 𝑖 ∈ (ℤ𝑗)))
7572, 73, 74sylanbrc 697 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑗 ∈ (𝑁...𝑖))
76 fzsplit 12325 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑁...𝑖) → (𝑁...𝑖) = ((𝑁...𝑗) ∪ ((𝑗 + 1)...𝑖)))
7775, 76syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (𝑁...𝑖) = ((𝑁...𝑗) ∪ ((𝑗 + 1)...𝑖)))
7871, 77syl5sseqr 3639 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((𝑗 + 1)...𝑖) ⊆ (𝑁...𝑖))
7978sselda 3588 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 𝑘 ∈ (𝑁...𝑖))
8079adantlr 750 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 𝑘 ∈ (𝑁...𝑖))
8116ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
8281, 19, 20syl2an 494 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆))
8382, 22syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘):𝑆⟶ℂ)
8483ffvelrnda 6325 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) ∧ 𝑧𝑆) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
8584an32s 845 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑖)) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
8680, 85syldan 487 . . . . . . . . . . . 12 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
8786abscld 14125 . . . . . . . . . . 11 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (abs‘((𝐹𝑘)‘𝑧)) ∈ ℝ)
8870, 87fsumrecl 14414 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹𝑘)‘𝑧)) ∈ ℝ)
89 mtest.c . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑍) → (𝑀𝑘) ∈ ℝ)
903, 1, 89serfre 12786 . . . . . . . . . . . . . . . 16 (𝜑 → seq𝑁( + , 𝑀):𝑍⟶ℝ)
9190ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → seq𝑁( + , 𝑀):𝑍⟶ℝ)
9291, 58ffvelrnd 6326 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( + , 𝑀)‘𝑖) ∈ ℝ)
9391, 63ffvelrnd 6326 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( + , 𝑀)‘𝑗) ∈ ℝ)
9492, 93resubcld 10418 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗)) ∈ ℝ)
9594recnd 10028 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗)) ∈ ℂ)
9695abscld 14125 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∈ ℝ)
9796adantr 481 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∈ ℝ)
9857, 34sylan2 491 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)))
9998adantlr 750 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)))
10099fveq1d 6160 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) = ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))‘𝑧))
101 fvex 6168 . . . . . . . . . . . . . . . 16 (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) ∈ V
10246fvmpt2 6258 . . . . . . . . . . . . . . . 16 ((𝑧𝑆 ∧ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) ∈ V) → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))
103101, 102mpan2 706 . . . . . . . . . . . . . . 15 (𝑧𝑆 → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))
104100, 103sylan9eq 2675 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))
10534ralrimiva 2962 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑖𝑍 (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)))
106105ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ∀𝑖𝑍 (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)))
107 fveq2 6158 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) = (seq𝑁( ∘𝑓 + , 𝐹)‘𝑗))
108 fveq2 6158 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
109108mpteq2dv 4715 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗)))
110107, 109eqeq12d 2636 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) ↔ (seq𝑁( ∘𝑓 + , 𝐹)‘𝑗) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))))
111110rspccv 3296 . . . . . . . . . . . . . . . . 17 (∀𝑖𝑍 (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) → (𝑗𝑍 → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑗) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))))
112106, 63, 111sylc 65 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑗) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗)))
113112fveq1d 6160 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧) = ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))‘𝑧))
114 fvex 6168 . . . . . . . . . . . . . . . 16 (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗) ∈ V
115 eqid 2621 . . . . . . . . . . . . . . . . 17 (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗)) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
116115fvmpt2 6258 . . . . . . . . . . . . . . . 16 ((𝑧𝑆 ∧ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗) ∈ V) → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
117114, 116mpan2 706 . . . . . . . . . . . . . . 15 (𝑧𝑆 → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
118113, 117sylan9eq 2675 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
119104, 118oveq12d 6633 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧)) = ((seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) − (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗)))
12019adantl 482 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑖)) → 𝑘𝑍)
121120, 30syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑖)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘) = ((𝐹𝑘)‘𝑧))
12258adantr 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑖𝑍)
123122, 3syl6eleq 2708 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑖 ∈ (ℤ𝑁))
124121, 123, 85fsumser 14410 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))
125 elfzuz 12296 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (𝑁...𝑗) → 𝑘 ∈ (ℤ𝑁))
126125, 3syl6eleqr 2709 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (𝑁...𝑗) → 𝑘𝑍)
127126adantl 482 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑗)) → 𝑘𝑍)
128127, 30syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑗)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘) = ((𝐹𝑘)‘𝑧))
12963adantr 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑗𝑍)
130129, 3syl6eleq 2708 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑗 ∈ (ℤ𝑁))
13181, 126, 20syl2an 494 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆))
132131, 22syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝐹𝑘):𝑆⟶ℂ)
133132ffvelrnda 6325 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) ∧ 𝑧𝑆) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
134133an32s 845 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑗)) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
135128, 130, 134fsumser 14410 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
136124, 135oveq12d 6633 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧) − Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧)) = ((seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) − (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗)))
137 eluzelre 11658 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (ℤ𝑁) → 𝑗 ∈ ℝ)
13872, 137syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑗 ∈ ℝ)
139138ltp1d 10914 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑗 < (𝑗 + 1))
140 fzdisj 12326 . . . . . . . . . . . . . . . . . 18 (𝑗 < (𝑗 + 1) → ((𝑁...𝑗) ∩ ((𝑗 + 1)...𝑖)) = ∅)
141139, 140syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((𝑁...𝑗) ∩ ((𝑗 + 1)...𝑖)) = ∅)
142141adantr 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((𝑁...𝑗) ∩ ((𝑗 + 1)...𝑖)) = ∅)
14377adantr 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (𝑁...𝑖) = ((𝑁...𝑗) ∪ ((𝑗 + 1)...𝑖)))
144 fzfid 12728 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (𝑁...𝑖) ∈ Fin)
145142, 143, 144, 85fsumsplit 14420 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧) = (Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧) + Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧)))
146145eqcomd 2627 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧) + Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧)) = Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧))
147144, 85fsumcl 14413 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧) ∈ ℂ)
148 fzfid 12728 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (𝑁...𝑗) ∈ Fin)
149148, 134fsumcl 14413 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧) ∈ ℂ)
15070, 86fsumcl 14413 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧) ∈ ℂ)
151147, 149, 150subaddd 10370 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧) − Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧) ↔ (Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧) + Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧)) = Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧)))
152146, 151mpbird 247 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧) − Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧))
153119, 136, 1523eqtr2d 2661 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧))
154153fveq2d 6162 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) = (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧)))
15570, 86fsumabs 14479 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧)) ≤ Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹𝑘)‘𝑧)))
156154, 155eqbrtrd 4645 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) ≤ Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹𝑘)‘𝑧)))
157 simpll 789 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝜑)
158157, 19, 89syl2an 494 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝑀𝑘) ∈ ℝ)
15979, 158syldan 487 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (𝑀𝑘) ∈ ℝ)
160159adantlr 750 . . . . . . . . . . . 12 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (𝑀𝑘) ∈ ℝ)
16180, 19syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 𝑘𝑍)
162 mtest.l . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘𝑍𝑧𝑆)) → (abs‘((𝐹𝑘)‘𝑧)) ≤ (𝑀𝑘))
163162adantlr 750 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑧𝑆)) → (abs‘((𝐹𝑘)‘𝑧)) ≤ (𝑀𝑘))
164163adantlr 750 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ (𝑘𝑍𝑧𝑆)) → (abs‘((𝐹𝑘)‘𝑧)) ≤ (𝑀𝑘))
165164anass1rs 848 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘𝑍) → (abs‘((𝐹𝑘)‘𝑧)) ≤ (𝑀𝑘))
166161, 165syldan 487 . . . . . . . . . . . 12 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (abs‘((𝐹𝑘)‘𝑧)) ≤ (𝑀𝑘))
16770, 87, 160, 166fsumle 14477 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹𝑘)‘𝑧)) ≤ Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
168 eqidd 2622 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝑀𝑘) = (𝑀𝑘))
16958, 3syl6eleq 2708 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑖 ∈ (ℤ𝑁))
170158recnd 10028 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝑀𝑘) ∈ ℂ)
171168, 169, 170fsumser 14410 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘) = (seq𝑁( + , 𝑀)‘𝑖))
172 eqidd 2622 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝑀𝑘) = (𝑀𝑘))
173157, 126, 89syl2an 494 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝑀𝑘) ∈ ℝ)
174173recnd 10028 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝑀𝑘) ∈ ℂ)
175172, 72, 174fsumser 14410 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘) = (seq𝑁( + , 𝑀)‘𝑗))
176171, 175oveq12d 6633 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘) − Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘)) = ((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗)))
177 fzfid 12728 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (𝑁...𝑖) ∈ Fin)
178141, 77, 177, 170fsumsplit 14420 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘) = (Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘) + Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘)))
179178eqcomd 2627 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘) + Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘)) = Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘))
180177, 170fsumcl 14413 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘) ∈ ℂ)
181 fzfid 12728 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (𝑁...𝑗) ∈ Fin)
182181, 174fsumcl 14413 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘) ∈ ℂ)
183 fzfid 12728 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((𝑗 + 1)...𝑖) ∈ Fin)
18479, 170syldan 487 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (𝑀𝑘) ∈ ℂ)
185183, 184fsumcl 14413 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘) ∈ ℂ)
186180, 182, 185subaddd 10370 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘) − Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘) ↔ (Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘) + Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘)) = Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘)))
187179, 186mpbird 247 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘) − Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
188176, 187eqtr3d 2657 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
189188fveq2d 6162 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) = (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘)))
190189adantr 481 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) = (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘)))
191188, 94eqeltrrd 2699 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘) ∈ ℝ)
192191adantr 481 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘) ∈ ℝ)
193 0red 10001 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 0 ∈ ℝ)
19486absge0d 14133 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 0 ≤ (abs‘((𝐹𝑘)‘𝑧)))
195193, 87, 160, 194, 166letrd 10154 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 0 ≤ (𝑀𝑘))
19670, 160, 195fsumge0 14473 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 0 ≤ Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
197192, 196absidd 14111 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
198190, 197eqtrd 2655 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
199167, 198breqtrrd 4651 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹𝑘)‘𝑧)) ≤ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))))
20069, 88, 97, 156, 199letrd 10154 . . . . . . . . 9 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) ≤ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))))
201 simpllr 798 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑟 ∈ ℝ+)
202201rpred 11832 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑟 ∈ ℝ)
203 lelttr 10088 . . . . . . . . . 10 (((abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) ∈ ℝ ∧ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∈ ℝ ∧ 𝑟 ∈ ℝ) → (((abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) ≤ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∧ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟) → (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
20469, 97, 202, 203syl3anc 1323 . . . . . . . . 9 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (((abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) ≤ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∧ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟) → (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
205200, 204mpand 710 . . . . . . . 8 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
206205ralrimdva 2965 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∀𝑧𝑆 (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
207206anassrs 679 . . . . . 6 ((((𝜑𝑟 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑖 ∈ (ℤ𝑗)) → ((abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∀𝑧𝑆 (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
208207ralimdva 2958 . . . . 5 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑖 ∈ (ℤ𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∀𝑖 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
209208reximdva 3013 . . . 4 ((𝜑𝑟 ∈ ℝ+) → (∃𝑗𝑍𝑖 ∈ (ℤ𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∃𝑗𝑍𝑖 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
210209ralimdva 2958 . . 3 (𝜑 → (∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
2115, 210mpd 15 . 2 (𝜑 → ∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟)
2123, 1, 10, 55ulmcau 24087 . 2 (𝜑 → (seq𝑁( ∘𝑓 + , 𝐹) ∈ dom (⇝𝑢𝑆) ↔ ∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
213211, 212mpbird 247 1 (𝜑 → seq𝑁( ∘𝑓 + , 𝐹) ∈ dom (⇝𝑢𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2908  wrex 2909  Vcvv 3190  cun 3558  cin 3559  c0 3897   class class class wbr 4623  cmpt 4683  dom cdm 5084   Fn wfn 5852  wf 5853  cfv 5857  (class class class)co 6615  𝑓 cof 6860  𝑚 cmap 7817  cc 9894  cr 9895  0cc0 9896  1c1 9897   + caddc 9899   < clt 10034  cle 10035  cmin 10226  cz 11337  cuz 11647  +crp 11792  ...cfz 12284  seqcseq 12757  abscabs 13924  cli 14165  Σcsu 14366  𝑢culm 24068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-inf2 8498  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974  ax-addf 9975  ax-mulf 9976
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-se 5044  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-isom 5866  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-of 6862  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-oadd 7524  df-er 7702  df-map 7819  df-pm 7820  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-sup 8308  df-inf 8309  df-oi 8375  df-card 8725  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-n0 11253  df-z 11338  df-uz 11648  df-rp 11793  df-ico 12139  df-fz 12285  df-fzo 12423  df-fl 12549  df-seq 12758  df-exp 12817  df-hash 13074  df-cj 13789  df-re 13790  df-im 13791  df-sqrt 13925  df-abs 13926  df-limsup 14152  df-clim 14169  df-rlim 14170  df-sum 14367  df-ulm 24069
This theorem is referenced by:  pserulm  24114  lgamgulmlem6  24694  knoppcnlem6  32183
  Copyright terms: Public domain W3C validator