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

Theorem mtest 24978
 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 (𝜑𝐹:𝑍⟶(ℂ ↑m 𝑆))
mtest.m (𝜑𝑀𝑊)
mtest.c ((𝜑𝑘𝑍) → (𝑀𝑘) ∈ ℝ)
mtest.l ((𝜑 ∧ (𝑘𝑍𝑧𝑆)) → (abs‘((𝐹𝑘)‘𝑧)) ≤ (𝑀𝑘))
mtest.d (𝜑 → seq𝑁( + , 𝑀) ∈ dom ⇝ )
Assertion
Ref Expression
mtest (𝜑 → seq𝑁( ∘f + , 𝐹) ∈ 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 15007 . . . 4 ((𝑁 ∈ ℤ ∧ seq𝑁( + , 𝑀) ∈ dom ⇝ ) → ∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟)
51, 2, 4syl2anc 586 . . 3 (𝜑 → ∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟)
6 seqfn 13365 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℤ → seq𝑁( ∘f + , 𝐹) Fn (ℤ𝑁))
71, 6syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → seq𝑁( ∘f + , 𝐹) Fn (ℤ𝑁))
83fneq2i 6427 . . . . . . . . . . . . . . . . . 18 (seq𝑁( ∘f + , 𝐹) Fn 𝑍 ↔ seq𝑁( ∘f + , 𝐹) Fn (ℤ𝑁))
97, 8sylibr 236 . . . . . . . . . . . . . . . . 17 (𝜑 → seq𝑁( ∘f + , 𝐹) Fn 𝑍)
10 mtest.s . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑆𝑉)
1110elexd 3493 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑆 ∈ V)
1211adantr 483 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝑍) → 𝑆 ∈ V)
13 simpr 487 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝑍) → 𝑖𝑍)
1413, 3eleqtrdi 2921 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝑍) → 𝑖 ∈ (ℤ𝑁))
15 mtest.f . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹:𝑍⟶(ℂ ↑m 𝑆))
1615adantr 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑖𝑍) → 𝐹:𝑍⟶(ℂ ↑m 𝑆))
17 elfzuz 12888 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (𝑁...𝑖) → 𝑘 ∈ (ℤ𝑁))
1817, 3eleqtrrdi 2922 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (𝑁...𝑖) → 𝑘𝑍)
19 ffvelrn 6825 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹:𝑍⟶(ℂ ↑m 𝑆) ∧ 𝑘𝑍) → (𝐹𝑘) ∈ (ℂ ↑m 𝑆))
2016, 18, 19syl2an 597 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘) ∈ (ℂ ↑m 𝑆))
21 elmapi 8406 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑘) ∈ (ℂ ↑m 𝑆) → (𝐹𝑘):𝑆⟶ℂ)
2220, 21syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘):𝑆⟶ℂ)
2322feqmptd 6709 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘) = (𝑧𝑆 ↦ ((𝐹𝑘)‘𝑧)))
2418adantl 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → 𝑘𝑍)
25 fveq2 6646 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
2625fveq1d 6648 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑘 → ((𝐹𝑛)‘𝑧) = ((𝐹𝑘)‘𝑧))
27 eqid 2820 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)) = (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))
28 fvex 6659 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑘)‘𝑧) ∈ V
2926, 27, 28fvmpt 6744 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘𝑍 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘) = ((𝐹𝑘)‘𝑧))
3024, 29syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘) = ((𝐹𝑘)‘𝑧))
3130mpteq2dv 5138 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝑧𝑆 ↦ ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘)) = (𝑧𝑆 ↦ ((𝐹𝑘)‘𝑧)))
3223, 31eqtr4d 2858 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘) = (𝑧𝑆 ↦ ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘)))
3312, 14, 32seqof 13412 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝑍) → (seq𝑁( ∘f + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)))
341adantr 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑧𝑆) → 𝑁 ∈ ℤ)
3515ffvelrnda 6827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑛𝑍) → (𝐹𝑛) ∈ (ℂ ↑m 𝑆))
36 elmapi 8406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹𝑛) ∈ (ℂ ↑m 𝑆) → (𝐹𝑛):𝑆⟶ℂ)
3735, 36syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑛𝑍) → (𝐹𝑛):𝑆⟶ℂ)
3837ffvelrnda 6827 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑛𝑍) ∧ 𝑧𝑆) → ((𝐹𝑛)‘𝑧) ∈ ℂ)
3938an32s 650 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑧𝑆) ∧ 𝑛𝑍) → ((𝐹𝑛)‘𝑧) ∈ ℂ)
4039fmpttd 6855 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑧𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)):𝑍⟶ℂ)
4140ffvelrnda 6827 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑧𝑆) ∧ 𝑖𝑍) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑖) ∈ ℂ)
423, 34, 41serf 13383 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧𝑆) → seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))):𝑍⟶ℂ)
4342ffvelrnda 6827 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑧𝑆) ∧ 𝑖𝑍) → (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) ∈ ℂ)
4443an32s 650 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖𝑍) ∧ 𝑧𝑆) → (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) ∈ ℂ)
4544fmpttd 6855 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝑍) → (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)):𝑆⟶ℂ)
46 cnex 10596 . . . . . . . . . . . . . . . . . . . . 21 ℂ ∈ V
47 elmapg 8397 . . . . . . . . . . . . . . . . . . . . 21 ((ℂ ∈ V ∧ 𝑆 ∈ V) → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) ∈ (ℂ ↑m 𝑆) ↔ (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)):𝑆⟶ℂ))
4846, 12, 47sylancr 589 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝑍) → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) ∈ (ℂ ↑m 𝑆) ↔ (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)):𝑆⟶ℂ))
4945, 48mpbird 259 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝑍) → (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) ∈ (ℂ ↑m 𝑆))
5033, 49eqeltrd 2911 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖𝑍) → (seq𝑁( ∘f + , 𝐹)‘𝑖) ∈ (ℂ ↑m 𝑆))
5150ralrimiva 3169 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑖𝑍 (seq𝑁( ∘f + , 𝐹)‘𝑖) ∈ (ℂ ↑m 𝑆))
52 ffnfv 6858 . . . . . . . . . . . . . . . . 17 (seq𝑁( ∘f + , 𝐹):𝑍⟶(ℂ ↑m 𝑆) ↔ (seq𝑁( ∘f + , 𝐹) Fn 𝑍 ∧ ∀𝑖𝑍 (seq𝑁( ∘f + , 𝐹)‘𝑖) ∈ (ℂ ↑m 𝑆)))
539, 51, 52sylanbrc 585 . . . . . . . . . . . . . . . 16 (𝜑 → seq𝑁( ∘f + , 𝐹):𝑍⟶(ℂ ↑m 𝑆))
5453ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → seq𝑁( ∘f + , 𝐹):𝑍⟶(ℂ ↑m 𝑆))
553uztrn2 12241 . . . . . . . . . . . . . . . 16 ((𝑗𝑍𝑖 ∈ (ℤ𝑗)) → 𝑖𝑍)
5655adantl 484 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑖𝑍)
5754, 56ffvelrnd 6828 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘f + , 𝐹)‘𝑖) ∈ (ℂ ↑m 𝑆))
58 elmapi 8406 . . . . . . . . . . . . . 14 ((seq𝑁( ∘f + , 𝐹)‘𝑖) ∈ (ℂ ↑m 𝑆) → (seq𝑁( ∘f + , 𝐹)‘𝑖):𝑆⟶ℂ)
5957, 58syl 17 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘f + , 𝐹)‘𝑖):𝑆⟶ℂ)
6059ffvelrnda 6827 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) ∈ ℂ)
61 simprl 769 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑗𝑍)
6254, 61ffvelrnd 6828 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘f + , 𝐹)‘𝑗) ∈ (ℂ ↑m 𝑆))
63 elmapi 8406 . . . . . . . . . . . . . 14 ((seq𝑁( ∘f + , 𝐹)‘𝑗) ∈ (ℂ ↑m 𝑆) → (seq𝑁( ∘f + , 𝐹)‘𝑗):𝑆⟶ℂ)
6462, 63syl 17 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘f + , 𝐹)‘𝑗):𝑆⟶ℂ)
6564ffvelrnda 6827 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧) ∈ ℂ)
6660, 65subcld 10975 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧)) ∈ ℂ)
6766abscld 14776 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘(((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧))) ∈ ℝ)
68 fzfid 13325 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((𝑗 + 1)...𝑖) ∈ Fin)
69 ssun2 4128 . . . . . . . . . . . . . . . 16 ((𝑗 + 1)...𝑖) ⊆ ((𝑁...𝑗) ∪ ((𝑗 + 1)...𝑖))
7061, 3eleqtrdi 2921 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑗 ∈ (ℤ𝑁))
71 simprr 771 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑖 ∈ (ℤ𝑗))
72 elfzuzb 12886 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑁...𝑖) ↔ (𝑗 ∈ (ℤ𝑁) ∧ 𝑖 ∈ (ℤ𝑗)))
7370, 71, 72sylanbrc 585 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑗 ∈ (𝑁...𝑖))
74 fzsplit 12917 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑁...𝑖) → (𝑁...𝑖) = ((𝑁...𝑗) ∪ ((𝑗 + 1)...𝑖)))
7573, 74syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (𝑁...𝑖) = ((𝑁...𝑗) ∪ ((𝑗 + 1)...𝑖)))
7669, 75sseqtrrid 3999 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((𝑗 + 1)...𝑖) ⊆ (𝑁...𝑖))
7776sselda 3946 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 𝑘 ∈ (𝑁...𝑖))
7877adantlr 713 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 𝑘 ∈ (𝑁...𝑖))
7915ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝐹:𝑍⟶(ℂ ↑m 𝑆))
8079, 18, 19syl2an 597 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘) ∈ (ℂ ↑m 𝑆))
8180, 21syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹𝑘):𝑆⟶ℂ)
8281ffvelrnda 6827 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) ∧ 𝑧𝑆) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
8382an32s 650 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑖)) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
8478, 83syldan 593 . . . . . . . . . . . 12 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
8584abscld 14776 . . . . . . . . . . 11 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (abs‘((𝐹𝑘)‘𝑧)) ∈ ℝ)
8668, 85fsumrecl 15071 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹𝑘)‘𝑧)) ∈ ℝ)
87 mtest.c . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑍) → (𝑀𝑘) ∈ ℝ)
883, 1, 87serfre 13384 . . . . . . . . . . . . . . . 16 (𝜑 → seq𝑁( + , 𝑀):𝑍⟶ℝ)
8988ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → seq𝑁( + , 𝑀):𝑍⟶ℝ)
9089, 56ffvelrnd 6828 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( + , 𝑀)‘𝑖) ∈ ℝ)
9189, 61ffvelrnd 6828 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( + , 𝑀)‘𝑗) ∈ ℝ)
9290, 91resubcld 11046 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗)) ∈ ℝ)
9392recnd 10647 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗)) ∈ ℂ)
9493abscld 14776 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∈ ℝ)
9594adantr 483 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∈ ℝ)
9655, 33sylan2 594 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘f + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)))
9796adantlr 713 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘f + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)))
9897fveq1d 6648 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) = ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))‘𝑧))
99 fvex 6659 . . . . . . . . . . . . . . . 16 (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) ∈ V
100 eqid 2820 . . . . . . . . . . . . . . . . 17 (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))
101100fvmpt2 6755 . . . . . . . . . . . . . . . 16 ((𝑧𝑆 ∧ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) ∈ V) → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))
10299, 101mpan2 689 . . . . . . . . . . . . . . 15 (𝑧𝑆 → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))
10398, 102sylan9eq 2875 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))
104 fveq2 6646 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → (seq𝑁( ∘f + , 𝐹)‘𝑖) = (seq𝑁( ∘f + , 𝐹)‘𝑗))
105 fveq2 6646 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
106105mpteq2dv 5138 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗)))
107104, 106eqeq12d 2836 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → ((seq𝑁( ∘f + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)) ↔ (seq𝑁( ∘f + , 𝐹)‘𝑗) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))))
10833ralrimiva 3169 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑖𝑍 (seq𝑁( ∘f + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)))
109108ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ∀𝑖𝑍 (seq𝑁( ∘f + , 𝐹)‘𝑖) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖)))
110107, 109, 61rspcdva 3604 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (seq𝑁( ∘f + , 𝐹)‘𝑗) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗)))
111110fveq1d 6648 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧) = ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))‘𝑧))
112 fvex 6659 . . . . . . . . . . . . . . . 16 (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗) ∈ V
113 eqid 2820 . . . . . . . . . . . . . . . . 17 (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗)) = (𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
114113fvmpt2 6755 . . . . . . . . . . . . . . . 16 ((𝑧𝑆 ∧ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗) ∈ V) → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
115112, 114mpan2 689 . . . . . . . . . . . . . . 15 (𝑧𝑆 → ((𝑧𝑆 ↦ (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
116111, 115sylan9eq 2875 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
117103, 116oveq12d 7151 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧)) = ((seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) − (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗)))
11818adantl 484 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑖)) → 𝑘𝑍)
119118, 29syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑖)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘) = ((𝐹𝑘)‘𝑧))
12056adantr 483 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑖𝑍)
121120, 3eleqtrdi 2921 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑖 ∈ (ℤ𝑁))
122119, 121, 83fsumser 15067 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖))
123 elfzuz 12888 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (𝑁...𝑗) → 𝑘 ∈ (ℤ𝑁))
124123, 3eleqtrrdi 2922 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (𝑁...𝑗) → 𝑘𝑍)
125124adantl 484 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑗)) → 𝑘𝑍)
126125, 29syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑗)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧))‘𝑘) = ((𝐹𝑘)‘𝑧))
12761adantr 483 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑗𝑍)
128127, 3eleqtrdi 2921 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑗 ∈ (ℤ𝑁))
12979, 124, 19syl2an 597 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝐹𝑘) ∈ (ℂ ↑m 𝑆))
130129, 21syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝐹𝑘):𝑆⟶ℂ)
131130ffvelrnda 6827 . . . . . . . . . . . . . . . 16 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) ∧ 𝑧𝑆) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
132131an32s 650 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ (𝑁...𝑗)) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
133126, 128, 132fsumser 15067 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧) = (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗))
134122, 133oveq12d 7151 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧) − Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧)) = ((seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑖) − (seq𝑁( + , (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑧)))‘𝑗)))
135 fzfid 13325 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (𝑁...𝑗) ∈ Fin)
136135, 132fsumcl 15070 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧) ∈ ℂ)
13768, 84fsumcl 15070 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧) ∈ ℂ)
138 eluzelre 12233 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (ℤ𝑁) → 𝑗 ∈ ℝ)
13970, 138syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑗 ∈ ℝ)
140139ltp1d 11548 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑗 < (𝑗 + 1))
141 fzdisj 12918 . . . . . . . . . . . . . . . . 17 (𝑗 < (𝑗 + 1) → ((𝑁...𝑗) ∩ ((𝑗 + 1)...𝑖)) = ∅)
142140, 141syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((𝑁...𝑗) ∩ ((𝑗 + 1)...𝑖)) = ∅)
143142adantr 483 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((𝑁...𝑗) ∩ ((𝑗 + 1)...𝑖)) = ∅)
14475adantr 483 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (𝑁...𝑖) = ((𝑁...𝑗) ∪ ((𝑗 + 1)...𝑖)))
145 fzfid 13325 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (𝑁...𝑖) ∈ Fin)
146143, 144, 145, 83fsumsplit 15077 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧) = (Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧) + Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧)))
147136, 137, 146mvrladdd 11031 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (Σ𝑘 ∈ (𝑁...𝑖)((𝐹𝑘)‘𝑧) − Σ𝑘 ∈ (𝑁...𝑗)((𝐹𝑘)‘𝑧)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧))
148117, 134, 1473eqtr2d 2861 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧))
149148fveq2d 6650 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘(((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧))) = (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧)))
15068, 84fsumabs 15136 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹𝑘)‘𝑧)) ≤ Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹𝑘)‘𝑧)))
151149, 150eqbrtrd 5064 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘(((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧))) ≤ Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹𝑘)‘𝑧)))
152 simpll 765 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝜑)
153152, 18, 87syl2an 597 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝑀𝑘) ∈ ℝ)
15477, 153syldan 593 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (𝑀𝑘) ∈ ℝ)
155154adantlr 713 . . . . . . . . . . . 12 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (𝑀𝑘) ∈ ℝ)
15678, 18syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 𝑘𝑍)
157 mtest.l . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘𝑍𝑧𝑆)) → (abs‘((𝐹𝑘)‘𝑧)) ≤ (𝑀𝑘))
158157ad4ant14 750 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ (𝑘𝑍𝑧𝑆)) → (abs‘((𝐹𝑘)‘𝑧)) ≤ (𝑀𝑘))
159158anass1rs 653 . . . . . . . . . . . . 13 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘𝑍) → (abs‘((𝐹𝑘)‘𝑧)) ≤ (𝑀𝑘))
160156, 159syldan 593 . . . . . . . . . . . 12 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (abs‘((𝐹𝑘)‘𝑧)) ≤ (𝑀𝑘))
16168, 85, 155, 160fsumle 15134 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹𝑘)‘𝑧)) ≤ Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
162 eqidd 2821 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝑀𝑘) = (𝑀𝑘))
16356, 3eleqtrdi 2921 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → 𝑖 ∈ (ℤ𝑁))
164153recnd 10647 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝑀𝑘) ∈ ℂ)
165162, 163, 164fsumser 15067 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘) = (seq𝑁( + , 𝑀)‘𝑖))
166 eqidd 2821 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝑀𝑘) = (𝑀𝑘))
167152, 124, 87syl2an 597 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝑀𝑘) ∈ ℝ)
168167recnd 10647 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝑀𝑘) ∈ ℂ)
169166, 70, 168fsumser 15067 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘) = (seq𝑁( + , 𝑀)‘𝑗))
170165, 169oveq12d 7151 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘) − Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘)) = ((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗)))
171 fzfid 13325 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (𝑁...𝑗) ∈ Fin)
172171, 168fsumcl 15070 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘) ∈ ℂ)
173 fzfid 13325 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((𝑗 + 1)...𝑖) ∈ Fin)
17477, 164syldan 593 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (𝑀𝑘) ∈ ℂ)
175173, 174fsumcl 15070 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘) ∈ ℂ)
176 fzfid 13325 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (𝑁...𝑖) ∈ Fin)
177142, 75, 176, 164fsumsplit 15077 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘) = (Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘) + Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘)))
178172, 175, 177mvrladdd 11031 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (Σ𝑘 ∈ (𝑁...𝑖)(𝑀𝑘) − Σ𝑘 ∈ (𝑁...𝑗)(𝑀𝑘)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
179170, 178eqtr3d 2857 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
180179fveq2d 6650 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) = (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘)))
181180adantr 483 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) = (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘)))
182179, 92eqeltrrd 2912 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘) ∈ ℝ)
183182adantr 483 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘) ∈ ℝ)
184 0red 10622 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 0 ∈ ℝ)
18584absge0d 14784 . . . . . . . . . . . . . . 15 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 0 ≤ (abs‘((𝐹𝑘)‘𝑧)))
186184, 85, 155, 185, 160letrd 10775 . . . . . . . . . . . . . 14 (((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 0 ≤ (𝑀𝑘))
18768, 155, 186fsumge0 15130 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 0 ≤ Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
188183, 187absidd 14762 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
189181, 188eqtrd 2855 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀𝑘))
190161, 189breqtrrd 5070 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹𝑘)‘𝑧)) ≤ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))))
19167, 86, 95, 151, 190letrd 10775 . . . . . . . . 9 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (abs‘(((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧))) ≤ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))))
192 simpllr 774 . . . . . . . . . . 11 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑟 ∈ ℝ+)
193192rpred 12410 . . . . . . . . . 10 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → 𝑟 ∈ ℝ)
194 lelttr 10709 . . . . . . . . . 10 (((abs‘(((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧))) ∈ ℝ ∧ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∈ ℝ ∧ 𝑟 ∈ ℝ) → (((abs‘(((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧))) ≤ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∧ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟) → (abs‘(((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
19567, 95, 193, 194syl3anc 1367 . . . . . . . . 9 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → (((abs‘(((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧))) ≤ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∧ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟) → (abs‘(((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
196191, 195mpand 693 . . . . . . . 8 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) ∧ 𝑧𝑆) → ((abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → (abs‘(((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
197196ralrimdva 3176 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑖 ∈ (ℤ𝑗))) → ((abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∀𝑧𝑆 (abs‘(((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
198197anassrs 470 . . . . . 6 ((((𝜑𝑟 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑖 ∈ (ℤ𝑗)) → ((abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∀𝑧𝑆 (abs‘(((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
199198ralimdva 3164 . . . . 5 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑖 ∈ (ℤ𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∀𝑖 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
200199reximdva 3261 . . . 4 ((𝜑𝑟 ∈ ℝ+) → (∃𝑗𝑍𝑖 ∈ (ℤ𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∃𝑗𝑍𝑖 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
201200ralimdva 3164 . . 3 (𝜑 → (∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
2025, 201mpd 15 . 2 (𝜑 → ∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟)
2033, 1, 10, 53ulmcau 24969 . 2 (𝜑 → (seq𝑁( ∘f + , 𝐹) ∈ dom (⇝𝑢𝑆) ↔ ∀𝑟 ∈ ℝ+𝑗𝑍𝑖 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((seq𝑁( ∘f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
204202, 203mpbird 259 1 (𝜑 → seq𝑁( ∘f + , 𝐹) ∈ dom (⇝𝑢𝑆))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3125  ∃wrex 3126  Vcvv 3473   ∪ cun 3911   ∩ cin 3912  ∅c0 4269   class class class wbr 5042   ↦ cmpt 5122  dom cdm 5531   Fn wfn 6326  ⟶wf 6327  ‘cfv 6331  (class class class)co 7133   ∘f cof 7385   ↑m cmap 8384  ℂcc 10513  ℝcr 10514  0cc0 10515  1c1 10516   + caddc 10518   < clt 10653   ≤ cle 10654   − cmin 10848  ℤcz 11960  ℤ≥cuz 12222  ℝ+crp 12368  ...cfz 12876  seqcseq 13353  abscabs 14573   ⇝ cli 14821  Σcsu 15022  ⇝𝑢culm 24950 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-inf2 9082  ax-cnex 10571  ax-resscn 10572  ax-1cn 10573  ax-icn 10574  ax-addcl 10575  ax-addrcl 10576  ax-mulcl 10577  ax-mulrcl 10578  ax-mulcom 10579  ax-addass 10580  ax-mulass 10581  ax-distr 10582  ax-i2m1 10583  ax-1ne0 10584  ax-1rid 10585  ax-rnegex 10586  ax-rrecex 10587  ax-cnre 10588  ax-pre-lttri 10589  ax-pre-lttrn 10590  ax-pre-ltadd 10591  ax-pre-mulgt0 10592  ax-pre-sup 10593  ax-addf 10594  ax-mulf 10595 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-int 4853  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-se 5491  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-isom 6340  df-riota 7091  df-ov 7136  df-oprab 7137  df-mpo 7138  df-of 7387  df-om 7559  df-1st 7667  df-2nd 7668  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-1o 8080  df-oadd 8084  df-er 8267  df-map 8386  df-pm 8387  df-en 8488  df-dom 8489  df-sdom 8490  df-fin 8491  df-sup 8884  df-inf 8885  df-oi 8952  df-card 9346  df-pnf 10655  df-mnf 10656  df-xr 10657  df-ltxr 10658  df-le 10659  df-sub 10850  df-neg 10851  df-div 11276  df-nn 11617  df-2 11679  df-3 11680  df-n0 11877  df-z 11961  df-uz 12223  df-rp 12369  df-ico 12723  df-fz 12877  df-fzo 13018  df-fl 13146  df-seq 13354  df-exp 13415  df-hash 13676  df-cj 14438  df-re 14439  df-im 14440  df-sqrt 14574  df-abs 14575  df-limsup 14808  df-clim 14825  df-rlim 14826  df-sum 15023  df-ulm 24951 This theorem is referenced by:  pserulm  24996  lgamgulmlem6  25598  knoppcnlem6  33845
 Copyright terms: Public domain W3C validator