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

Theorem mtest 23962
 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 14249 . . . 4 ((𝑁 ∈ ℤ ∧ seq𝑁( + , 𝑀) ∈ dom ⇝ ) → ∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟)
51, 2, 4syl2anc 691 . . 3 (𝜑 → ∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟)
6 seqfn 12675 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℤ → seq𝑁( ∘𝑓 + , 𝐹) Fn (ℤ𝑁))
71, 6syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → seq𝑁( ∘𝑓 + , 𝐹) Fn (ℤ𝑁))
83fneq2i 5900 . . . . . . . . . . . . . . . . . 18 (seq𝑁( ∘𝑓 + , 𝐹) Fn 𝑍 ↔ seq𝑁( ∘𝑓 + , 𝐹) Fn (ℤ𝑁))
97, 8sylibr 223 . . . . . . . . . . . . . . . . 17 (𝜑 → seq𝑁( ∘𝑓 + , 𝐹) Fn 𝑍)
10 mtest.s . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑆𝑉)
11 elex 3185 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆𝑉𝑆 ∈ V)
1210, 11syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑆 ∈ V)
1312adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝑍) → 𝑆 ∈ V)
14 simpr 476 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝑍) → 𝑖𝑍)
1514, 3syl6eleq 2698 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝑍) → 𝑖 ∈ (ℤ𝑁))
16 mtest.f . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
1716adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖𝑍) → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
18 elfzuz 12209 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (𝑁...𝑖) → 𝑘 ∈ (ℤ𝑁))
1918, 3syl6eleqr 2699 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (𝑁...𝑖) → 𝑘𝑍)
20 ffvelrn 6265 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹:𝑍⟶(ℂ ↑𝑚 𝑆) ∧ 𝑘𝑍) → (𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆))
2117, 19, 20syl2an 493 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆))
22 elmapi 7765 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆) → (𝐹𝑘):𝑆⟶ℂ)
2321, 22syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘):𝑆⟶ℂ)
2423feqmptd 6159 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘) = (𝑧𝑆 ↦ ((𝐹𝑘)‘𝑧)))
2519adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → 𝑘𝑍)
26 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
2726fveq1d 6105 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑘 → ((𝐹𝑛)‘𝑧) = ((𝐹𝑘)‘𝑧))
28 eqid 2610 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)) = (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))
29 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑘)‘𝑧) ∈ V
3027, 28, 29fvmpt 6191 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑍 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘) = ((𝐹𝑘)‘𝑧))
3125, 30syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘) = ((𝐹𝑘)‘𝑧))
3231mpteq2dv 4673 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝑧𝑆 ↦ ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘)) = (𝑧𝑆 ↦ ((𝐹𝑘)‘𝑧)))
3324, 32eqtr4d 2647 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘) = (𝑧𝑆 ↦ ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘)))
3413, 15, 33seqof 12720 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝑍) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)))
351adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧𝑆) → 𝑁 ∈ ℤ)
3616ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑛𝑍) → (𝐹𝑛) ∈ (ℂ ↑𝑚 𝑆))
37 elmapi 7765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹𝑛) ∈ (ℂ ↑𝑚 𝑆) → (𝐹𝑛):𝑆⟶ℂ)
3836, 37syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑛𝑍) → (𝐹𝑛):𝑆⟶ℂ)
3938ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑛𝑍) ∧ 𝑧𝑆) → ((𝐹𝑛)‘𝑧) ∈ ℂ)
4039an32s 842 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ 𝑛𝑍) → ((𝐹𝑛)‘𝑧) ∈ ℂ)
4140, 28fmptd 6292 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)):𝑍⟶ℂ)
4241ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ 𝑖𝑍) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑖) ∈ ℂ)
433, 35, 42serf 12691 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧𝑆) → seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))):𝑍⟶ℂ)
4443ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ 𝑖𝑍) → (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) ∈ ℂ)
4544an32s 842 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝑍) ∧ 𝑧𝑆) → (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) ∈ ℂ)
46 eqid 2610 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))
4745, 46fmptd 6292 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝑍) → (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)):𝑆⟶ℂ)
48 cnex 9896 . . . . . . . . . . . . . . . . . . . . 21 ℂ ∈ V
49 elmapg 7757 . . . . . . . . . . . . . . . . . . . . 21 ((ℂ ∈ V ∧ 𝑆 ∈ V) → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) ∈ (ℂ ↑𝑚 𝑆) ↔ (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)):𝑆⟶ℂ))
5048, 13, 49sylancr 694 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝑍) → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) ∈ (ℂ ↑𝑚 𝑆) ↔ (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)):𝑆⟶ℂ))
5147, 50mpbird 246 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝑍) → (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) ∈ (ℂ ↑𝑚 𝑆))
5234, 51eqeltrd 2688 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖𝑍) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) ∈ (ℂ ↑𝑚 𝑆))
5352ralrimiva 2949 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑖𝑍 (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) ∈ (ℂ ↑𝑚 𝑆))
54 ffnfv 6295 . . . . . . . . . . . . . . . . 17 (seq𝑁( ∘𝑓 + , 𝐹):𝑍⟶(ℂ ↑𝑚 𝑆) ↔ (seq𝑁( ∘𝑓 + , 𝐹) Fn 𝑍 ∧ ∀𝑖𝑍 (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) ∈ (ℂ ↑𝑚 𝑆)))
559, 53, 54sylanbrc 695 . . . . . . . . . . . . . . . 16 (𝜑 → seq𝑁( ∘𝑓 + , 𝐹):𝑍⟶(ℂ ↑𝑚 𝑆))
5655ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → seq𝑁( ∘𝑓 + , 𝐹):𝑍⟶(ℂ ↑𝑚 𝑆))
573uztrn2 11581 . . . . . . . . . . . . . . . 16 ((𝑗𝑍𝑖 ∈ (ℤ𝑗)) → 𝑖𝑍)
5857adantl 481 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑖𝑍)
5956, 58ffvelrnd 6268 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) ∈ (ℂ ↑𝑚 𝑆))
60 elmapi 7765 . . . . . . . . . . . . . 14 ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) ∈ (ℂ ↑𝑚 𝑆) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖):𝑆⟶ℂ)
6159, 60syl 17 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖):𝑆⟶ℂ)
6261ffvelrnda 6267 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) ∈ ℂ)
63 simprl 790 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑗𝑍)
6456, 63ffvelrnd 6268 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑗) ∈ (ℂ ↑𝑚 𝑆))
65 elmapi 7765 . . . . . . . . . . . . . 14 ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗) ∈ (ℂ ↑𝑚 𝑆) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑗):𝑆⟶ℂ)
6664, 65syl 17 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑗):𝑆⟶ℂ)
6766ffvelrnda 6267 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧) ∈ ℂ)
6862, 67subcld 10271 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧)) ∈ ℂ)
6968abscld 14023 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) ∈ ℝ)
70 fzfid 12634 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((𝑗 + 1)...𝑖) ∈ Fin)
71 ssun2 3739 . . . . . . . . . . . . . . . 16 ((𝑗 + 1)...𝑖) ⊆ ((𝑁...𝑗) ∪ ((𝑗 + 1)...𝑖))
7263, 3syl6eleq 2698 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑗 ∈ (ℤ𝑁))
73 simprr 792 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑖 ∈ (ℤ𝑗))
74 elfzuzb 12207 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑁...𝑖) ↔ (𝑗 ∈ (ℤ𝑁) ∧ 𝑖 ∈ (ℤ𝑗)))
7572, 73, 74sylanbrc 695 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑗 ∈ (𝑁...𝑖))
76 fzsplit 12238 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑁...𝑖) → (𝑁...𝑖) = ((𝑁...𝑗) ∪ ((𝑗 + 1)...𝑖)))
7775, 76syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (𝑁...𝑖) = ((𝑁...𝑗) ∪ ((𝑗 + 1)...𝑖)))
7871, 77syl5sseqr 3617 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((𝑗 + 1)...𝑖) ⊆ (𝑁...𝑖))
7978sselda 3568 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 𝑘 ∈ (𝑁...𝑖))
8079adantlr 747 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 𝑘 ∈ (𝑁...𝑖))
8116ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
8281, 19, 20syl2an 493 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆))
8382, 22syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘):𝑆⟶ℂ)
8483ffvelrnda 6267 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) ∧ 𝑧𝑆) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
8584an32s 842 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑖)) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
8680, 85syldan 486 . . . . . . . . . . . 12 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
8786abscld 14023 . . . . . . . . . . 11 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (abs‘((𝐹𝑘)‘𝑧)) ∈ ℝ)
8870, 87fsumrecl 14312 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹𝑘)‘𝑧)) ∈ ℝ)
89 mtest.c . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑍) → (𝑀𝑘) ∈ ℝ)
903, 1, 89serfre 12692 . . . . . . . . . . . . . . . 16 (𝜑 → seq𝑁( + , 𝑀):𝑍⟶ℝ)
9190ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → seq𝑁( + , 𝑀):𝑍⟶ℝ)
9291, 58ffvelrnd 6268 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( + , 𝑀)‘𝑖) ∈ ℝ)
9391, 63ffvelrnd 6268 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( + , 𝑀)‘𝑗) ∈ ℝ)
9492, 93resubcld 10337 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗)) ∈ ℝ)
9594recnd 9947 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗)) ∈ ℂ)
9695abscld 14023 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∈ ℝ)
9796adantr 480 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∈ ℝ)
9857, 34sylan2 490 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)))
9998adantlr 747 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)))
10099fveq1d 6105 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) = ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))‘𝑧))
101 fvex 6113 . . . . . . . . . . . . . . . 16 (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) ∈ V
10246fvmpt2 6200 . . . . . . . . . . . . . . . 16 ((𝑧𝑆 ∧ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) ∈ V) → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))
103101, 102mpan2 703 . . . . . . . . . . . . . . 15 (𝑧𝑆 → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))
104100, 103sylan9eq 2664 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))
10534ralrimiva 2949 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑖𝑍 (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)))
106105ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ∀𝑖𝑍 (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)))
107 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) = (seq𝑁( ∘𝑓 + , 𝐹)‘𝑗))
108 fveq2 6103 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑗 → (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
109108mpteq2dv 4673 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗)))
110107, 109eqeq12d 2625 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) ↔ (seq𝑁( ∘𝑓 + , 𝐹)‘𝑗) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))))
111110rspccv 3279 . . . . . . . . . . . . . . . . 17 (∀𝑖𝑍 (seq𝑁( ∘𝑓 + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) → (𝑗𝑍 → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑗) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))))
112106, 63, 111sylc 63 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘𝑓 + , 𝐹)‘𝑗) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗)))
113112fveq1d 6105 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧) = ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))‘𝑧))
114 fvex 6113 . . . . . . . . . . . . . . . 16 (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗) ∈ V
115 eqid 2610 . . . . . . . . . . . . . . . . 17 (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗)) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
116115fvmpt2 6200 . . . . . . . . . . . . . . . 16 ((𝑧𝑆 ∧ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗) ∈ V) → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
117114, 116mpan2 703 . . . . . . . . . . . . . . 15 (𝑧𝑆 → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
118113, 117sylan9eq 2664 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
119104, 118oveq12d 6567 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧)) = ((seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) − (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗)))
12019adantl 481 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑖)) → 𝑘𝑍)
121120, 30syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑖)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘) = ((𝐹𝑘)‘𝑧))
12258adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑖𝑍)
123122, 3syl6eleq 2698 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑖 ∈ (ℤ𝑁))
124121, 123, 85fsumser 14308 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))
125 elfzuz 12209 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (𝑁...𝑗) → 𝑘 ∈ (ℤ𝑁))
126125, 3syl6eleqr 2699 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (𝑁...𝑗) → 𝑘𝑍)
127126adantl 481 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑗)) → 𝑘𝑍)
128127, 30syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑗)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘) = ((𝐹𝑘)‘𝑧))
12963adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑗𝑍)
130129, 3syl6eleq 2698 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑗 ∈ (ℤ𝑁))
13181, 126, 20syl2an 493 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆))
132131, 22syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝐹𝑘):𝑆⟶ℂ)
133132ffvelrnda 6267 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) ∧ 𝑧𝑆) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
134133an32s 842 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑗)) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
135128, 130, 134fsumser 14308 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
136124, 135oveq12d 6567 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧) − Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧)) = ((seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) − (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗)))
137 eluzelre 11574 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (ℤ𝑁) → 𝑗 ∈ ℝ)
13872, 137syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑗 ∈ ℝ)
139138ltp1d 10833 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑗 < (𝑗 + 1))
140 fzdisj 12239 . . . . . . . . . . . . . . . . . 18 (𝑗 < (𝑗 + 1) → ((𝑁...𝑗) ∩ ((𝑗 + 1)...𝑖)) = ∅)
141139, 140syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((𝑁...𝑗) ∩ ((𝑗 + 1)...𝑖)) = ∅)
142141adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((𝑁...𝑗) ∩ ((𝑗 + 1)...𝑖)) = ∅)
14377adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (𝑁...𝑖) = ((𝑁...𝑗) ∪ ((𝑗 + 1)...𝑖)))
144 fzfid 12634 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (𝑁...𝑖) ∈ Fin)
145142, 143, 144, 85fsumsplit 14318 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧) = (Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧) + Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧)))
146145eqcomd 2616 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧) + Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧)) = Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧))
147144, 85fsumcl 14311 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧) ∈ ℂ)
148 fzfid 12634 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (𝑁...𝑗) ∈ Fin)
149148, 134fsumcl 14311 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧) ∈ ℂ)
15070, 86fsumcl 14311 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧) ∈ ℂ)
151147, 149, 150subaddd 10289 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧) − Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧) ↔ (Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧) + Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧)) = Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧)))
152146, 151mpbird 246 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧) − Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧))
153119, 136, 1523eqtr2d 2650 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧))
154153fveq2d 6107 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) = (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧)))
15570, 86fsumabs 14374 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧)) ≤ Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹𝑘)‘𝑧)))
156154, 155eqbrtrd 4605 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) ≤ Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹𝑘)‘𝑧)))
157 simpll 786 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝜑)
158157, 19, 89syl2an 493 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝑀𝑘) ∈ ℝ)
15979, 158syldan 486 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (𝑀𝑘) ∈ ℝ)
160159adantlr 747 . . . . . . . . . . . 12 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (𝑀𝑘) ∈ ℝ)
16180, 19syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 𝑘𝑍)
162 mtest.l . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑘𝑍𝑧𝑆)) → (abs‘((𝐹𝑘)‘𝑧)) ≤ (𝑀𝑘))
163162adantlr 747 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑧𝑆)) → (abs‘((𝐹𝑘)‘𝑧)) ≤ (𝑀𝑘))
164163adantlr 747 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ (𝑘𝑍𝑧𝑆)) → (abs‘((𝐹𝑘)‘𝑧)) ≤ (𝑀𝑘))
165164anass1rs 845 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘𝑍) → (abs‘((𝐹𝑘)‘𝑧)) ≤ (𝑀𝑘))
166161, 165syldan 486 . . . . . . . . . . . 12 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (abs‘((𝐹𝑘)‘𝑧)) ≤ (𝑀𝑘))
16770, 87, 160, 166fsumle 14372 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹𝑘)‘𝑧)) ≤ Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
168 eqidd 2611 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝑀𝑘) = (𝑀𝑘))
16958, 3syl6eleq 2698 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑖 ∈ (ℤ𝑁))
170158recnd 9947 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝑀𝑘) ∈ ℂ)
171168, 169, 170fsumser 14308 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘) = (seq𝑁( + , 𝑀)‘𝑖))
172 eqidd 2611 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝑀𝑘) = (𝑀𝑘))
173157, 126, 89syl2an 493 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝑀𝑘) ∈ ℝ)
174173recnd 9947 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝑀𝑘) ∈ ℂ)
175172, 72, 174fsumser 14308 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘) = (seq𝑁( + , 𝑀)‘𝑗))
176171, 175oveq12d 6567 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘) − Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘)) = ((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗)))
177 fzfid 12634 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (𝑁...𝑖) ∈ Fin)
178141, 77, 177, 170fsumsplit 14318 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘) = (Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘) + Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘)))
179178eqcomd 2616 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘) + Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘)) = Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘))
180177, 170fsumcl 14311 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘) ∈ ℂ)
181 fzfid 12634 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (𝑁...𝑗) ∈ Fin)
182181, 174fsumcl 14311 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘) ∈ ℂ)
183 fzfid 12634 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((𝑗 + 1)...𝑖) ∈ Fin)
18479, 170syldan 486 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (𝑀𝑘) ∈ ℂ)
185183, 184fsumcl 14311 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘) ∈ ℂ)
186180, 182, 185subaddd 10289 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘) − Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘) ↔ (Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘) + Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘)) = Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘)))
187179, 186mpbird 246 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘) − Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
188176, 187eqtr3d 2646 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
189188fveq2d 6107 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) = (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘)))
190189adantr 480 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) = (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘)))
191188, 94eqeltrrd 2689 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘) ∈ ℝ)
192191adantr 480 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘) ∈ ℝ)
193 0red 9920 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 0 ∈ ℝ)
19486absge0d 14031 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 0 ≤ (abs‘((𝐹𝑘)‘𝑧)))
195193, 87, 160, 194, 166letrd 10073 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 0 ≤ (𝑀𝑘))
19670, 160, 195fsumge0 14368 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 0 ≤ Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
197192, 196absidd 14009 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
198190, 197eqtrd 2644 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
199167, 198breqtrrd 4611 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹𝑘)‘𝑧)) ≤ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))))
20069, 88, 97, 156, 199letrd 10073 . . . . . . . . 9 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) ≤ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))))
201 simpllr 795 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑟 ∈ ℝ+)
202201rpred 11748 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑟 ∈ ℝ)
203 lelttr 10007 . . . . . . . . . 10 (((abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) ∈ ℝ ∧ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∈ ℝ ∧ 𝑟 ∈ ℝ) → (((abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) ≤ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∧ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟) → (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
20469, 97, 202, 203syl3anc 1318 . . . . . . . . 9 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (((abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) ≤ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∧ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟) → (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
205200, 204mpand 707 . . . . . . . 8 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
206205ralrimdva 2952 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∀𝑧𝑆 (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
207206anassrs 678 . . . . . 6 ((((𝜑𝑟 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑖 ∈ (ℤ𝑗)) → ((abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∀𝑧𝑆 (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
208207ralimdva 2945 . . . . 5 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑖 ∈ (ℤ𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∀𝑖 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
209208reximdva 3000 . . . 4 ((𝜑𝑟 ∈ ℝ+) → (∃𝑗𝑍𝑖 ∈ (ℤ𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∃𝑗𝑍𝑖 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
210209ralimdva 2945 . . 3 (𝜑 → (∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
2115, 210mpd 15 . 2 (𝜑 → ∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟)
2123, 1, 10, 55ulmcau 23953 . 2 (𝜑 → (seq𝑁( ∘𝑓 + , 𝐹) ∈ dom (⇝𝑢𝑆) ↔ ∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((seq𝑁( ∘𝑓 + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘𝑓 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
213211, 212mpbird 246 1 (𝜑 → seq𝑁( ∘𝑓 + , 𝐹) ∈ dom (⇝𝑢𝑆))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∪ cun 3538   ∩ cin 3539  ∅c0 3874   class class class wbr 4583   ↦ cmpt 4643  dom cdm 5038   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ∘𝑓 cof 6793   ↑𝑚 cmap 7744  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   < clt 9953   ≤ cle 9954   − cmin 10145  ℤcz 11254  ℤ≥cuz 11563  ℝ+crp 11708  ...cfz 12197  seqcseq 12663  abscabs 13822   ⇝ cli 14063  Σcsu 14264  ⇝𝑢culm 23934 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-ico 12052  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-limsup 14050  df-clim 14067  df-rlim 14068  df-sum 14265  df-ulm 23935 This theorem is referenced by:  pserulm  23980  lgamgulmlem6  24560  knoppcnlem6  31658
 Copyright terms: Public domain W3C validator