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

Theorem mtest 25779
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 15562 . . . 4 ((𝑁 ∈ β„€ ∧ seq𝑁( + , 𝑀) ∈ dom ⇝ ) β†’ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘— ∈ 𝑍 βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—))) < π‘Ÿ)
51, 2, 4syl2anc 585 . . 3 (πœ‘ β†’ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘— ∈ 𝑍 βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—))) < π‘Ÿ)
6 seqfn 13925 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ β„€ β†’ seq𝑁( ∘f + , 𝐹) Fn (β„€β‰₯β€˜π‘))
71, 6syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ seq𝑁( ∘f + , 𝐹) Fn (β„€β‰₯β€˜π‘))
83fneq2i 6605 . . . . . . . . . . . . . . . . . 18 (seq𝑁( ∘f + , 𝐹) Fn 𝑍 ↔ seq𝑁( ∘f + , 𝐹) Fn (β„€β‰₯β€˜π‘))
97, 8sylibr 233 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ seq𝑁( ∘f + , 𝐹) Fn 𝑍)
10 mtest.s . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝑆 ∈ 𝑉)
1110elexd 3468 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝑆 ∈ V)
1211adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑖 ∈ 𝑍) β†’ 𝑆 ∈ V)
13 simpr 486 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑖 ∈ 𝑍) β†’ 𝑖 ∈ 𝑍)
1413, 3eleqtrdi 2848 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑖 ∈ 𝑍) β†’ 𝑖 ∈ (β„€β‰₯β€˜π‘))
15 mtest.f . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝐹:π‘βŸΆ(β„‚ ↑m 𝑆))
1615adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑖 ∈ 𝑍) β†’ 𝐹:π‘βŸΆ(β„‚ ↑m 𝑆))
17 elfzuz 13444 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘˜ ∈ (𝑁...𝑖) β†’ π‘˜ ∈ (β„€β‰₯β€˜π‘))
1817, 3eleqtrrdi 2849 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ ∈ (𝑁...𝑖) β†’ π‘˜ ∈ 𝑍)
19 ffvelcdm 7037 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹:π‘βŸΆ(β„‚ ↑m 𝑆) ∧ π‘˜ ∈ 𝑍) β†’ (πΉβ€˜π‘˜) ∈ (β„‚ ↑m 𝑆))
2016, 18, 19syl2an 597 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑖 ∈ 𝑍) ∧ π‘˜ ∈ (𝑁...𝑖)) β†’ (πΉβ€˜π‘˜) ∈ (β„‚ ↑m 𝑆))
21 elmapi 8794 . . . . . . . . . . . . . . . . . . . . . . 23 ((πΉβ€˜π‘˜) ∈ (β„‚ ↑m 𝑆) β†’ (πΉβ€˜π‘˜):π‘†βŸΆβ„‚)
2220, 21syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑖 ∈ 𝑍) ∧ π‘˜ ∈ (𝑁...𝑖)) β†’ (πΉβ€˜π‘˜):π‘†βŸΆβ„‚)
2322feqmptd 6915 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑖 ∈ 𝑍) ∧ π‘˜ ∈ (𝑁...𝑖)) β†’ (πΉβ€˜π‘˜) = (𝑧 ∈ 𝑆 ↦ ((πΉβ€˜π‘˜)β€˜π‘§)))
2418adantl 483 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑖 ∈ 𝑍) ∧ π‘˜ ∈ (𝑁...𝑖)) β†’ π‘˜ ∈ 𝑍)
25 fveq2 6847 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = π‘˜ β†’ (πΉβ€˜π‘›) = (πΉβ€˜π‘˜))
2625fveq1d 6849 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = π‘˜ β†’ ((πΉβ€˜π‘›)β€˜π‘§) = ((πΉβ€˜π‘˜)β€˜π‘§))
27 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)) = (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§))
28 fvex 6860 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πΉβ€˜π‘˜)β€˜π‘§) ∈ V
2926, 27, 28fvmpt 6953 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘˜ ∈ 𝑍 β†’ ((𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§))β€˜π‘˜) = ((πΉβ€˜π‘˜)β€˜π‘§))
3024, 29syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑖 ∈ 𝑍) ∧ π‘˜ ∈ (𝑁...𝑖)) β†’ ((𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§))β€˜π‘˜) = ((πΉβ€˜π‘˜)β€˜π‘§))
3130mpteq2dv 5212 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑖 ∈ 𝑍) ∧ π‘˜ ∈ (𝑁...𝑖)) β†’ (𝑧 ∈ 𝑆 ↦ ((𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§))β€˜π‘˜)) = (𝑧 ∈ 𝑆 ↦ ((πΉβ€˜π‘˜)β€˜π‘§)))
3223, 31eqtr4d 2780 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑖 ∈ 𝑍) ∧ π‘˜ ∈ (𝑁...𝑖)) β†’ (πΉβ€˜π‘˜) = (𝑧 ∈ 𝑆 ↦ ((𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§))β€˜π‘˜)))
3312, 14, 32seqof 13972 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑖 ∈ 𝑍) β†’ (seq𝑁( ∘f + , 𝐹)β€˜π‘–) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–)))
341adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑧 ∈ 𝑆) β†’ 𝑁 ∈ β„€)
3515ffvelcdmda 7040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (πΉβ€˜π‘›) ∈ (β„‚ ↑m 𝑆))
36 elmapi 8794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πΉβ€˜π‘›) ∈ (β„‚ ↑m 𝑆) β†’ (πΉβ€˜π‘›):π‘†βŸΆβ„‚)
3735, 36syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (πΉβ€˜π‘›):π‘†βŸΆβ„‚)
3837ffvelcdmda 7040 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ 𝑛 ∈ 𝑍) ∧ 𝑧 ∈ 𝑆) β†’ ((πΉβ€˜π‘›)β€˜π‘§) ∈ β„‚)
3938an32s 651 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑧 ∈ 𝑆) ∧ 𝑛 ∈ 𝑍) β†’ ((πΉβ€˜π‘›)β€˜π‘§) ∈ β„‚)
4039fmpttd 7068 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑧 ∈ 𝑆) β†’ (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)):π‘βŸΆβ„‚)
4140ffvelcdmda 7040 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑧 ∈ 𝑆) ∧ 𝑖 ∈ 𝑍) β†’ ((𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§))β€˜π‘–) ∈ β„‚)
423, 34, 41serf 13943 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑧 ∈ 𝑆) β†’ seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§))):π‘βŸΆβ„‚)
4342ffvelcdmda 7040 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑧 ∈ 𝑆) ∧ 𝑖 ∈ 𝑍) β†’ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–) ∈ β„‚)
4443an32s 651 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑖 ∈ 𝑍) ∧ 𝑧 ∈ 𝑆) β†’ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–) ∈ β„‚)
4544fmpttd 7068 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑖 ∈ 𝑍) β†’ (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–)):π‘†βŸΆβ„‚)
46 cnex 11139 . . . . . . . . . . . . . . . . . . . . 21 β„‚ ∈ V
47 elmapg 8785 . . . . . . . . . . . . . . . . . . . . 21 ((β„‚ ∈ V ∧ 𝑆 ∈ V) β†’ ((𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–)) ∈ (β„‚ ↑m 𝑆) ↔ (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–)):π‘†βŸΆβ„‚))
4846, 12, 47sylancr 588 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑖 ∈ 𝑍) β†’ ((𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–)) ∈ (β„‚ ↑m 𝑆) ↔ (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–)):π‘†βŸΆβ„‚))
4945, 48mpbird 257 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑖 ∈ 𝑍) β†’ (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–)) ∈ (β„‚ ↑m 𝑆))
5033, 49eqeltrd 2838 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑖 ∈ 𝑍) β†’ (seq𝑁( ∘f + , 𝐹)β€˜π‘–) ∈ (β„‚ ↑m 𝑆))
5150ralrimiva 3144 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ βˆ€π‘– ∈ 𝑍 (seq𝑁( ∘f + , 𝐹)β€˜π‘–) ∈ (β„‚ ↑m 𝑆))
52 ffnfv 7071 . . . . . . . . . . . . . . . . 17 (seq𝑁( ∘f + , 𝐹):π‘βŸΆ(β„‚ ↑m 𝑆) ↔ (seq𝑁( ∘f + , 𝐹) Fn 𝑍 ∧ βˆ€π‘– ∈ 𝑍 (seq𝑁( ∘f + , 𝐹)β€˜π‘–) ∈ (β„‚ ↑m 𝑆)))
539, 51, 52sylanbrc 584 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ seq𝑁( ∘f + , 𝐹):π‘βŸΆ(β„‚ ↑m 𝑆))
5453ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ seq𝑁( ∘f + , 𝐹):π‘βŸΆ(β„‚ ↑m 𝑆))
553uztrn2 12789 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—)) β†’ 𝑖 ∈ 𝑍)
5655adantl 483 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ 𝑖 ∈ 𝑍)
5754, 56ffvelcdmd 7041 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ (seq𝑁( ∘f + , 𝐹)β€˜π‘–) ∈ (β„‚ ↑m 𝑆))
58 elmapi 8794 . . . . . . . . . . . . . 14 ((seq𝑁( ∘f + , 𝐹)β€˜π‘–) ∈ (β„‚ ↑m 𝑆) β†’ (seq𝑁( ∘f + , 𝐹)β€˜π‘–):π‘†βŸΆβ„‚)
5957, 58syl 17 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ (seq𝑁( ∘f + , 𝐹)β€˜π‘–):π‘†βŸΆβ„‚)
6059ffvelcdmda 7040 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) ∈ β„‚)
61 simprl 770 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ 𝑗 ∈ 𝑍)
6254, 61ffvelcdmd 7041 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ (seq𝑁( ∘f + , 𝐹)β€˜π‘—) ∈ (β„‚ ↑m 𝑆))
63 elmapi 8794 . . . . . . . . . . . . . 14 ((seq𝑁( ∘f + , 𝐹)β€˜π‘—) ∈ (β„‚ ↑m 𝑆) β†’ (seq𝑁( ∘f + , 𝐹)β€˜π‘—):π‘†βŸΆβ„‚)
6462, 63syl 17 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ (seq𝑁( ∘f + , 𝐹)β€˜π‘—):π‘†βŸΆβ„‚)
6564ffvelcdmda 7040 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§) ∈ β„‚)
6660, 65subcld 11519 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) βˆ’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§)) ∈ β„‚)
6766abscld 15328 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (absβ€˜(((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) βˆ’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§))) ∈ ℝ)
68 fzfid 13885 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ ((𝑗 + 1)...𝑖) ∈ Fin)
69 ssun2 4138 . . . . . . . . . . . . . . . 16 ((𝑗 + 1)...𝑖) βŠ† ((𝑁...𝑗) βˆͺ ((𝑗 + 1)...𝑖))
7061, 3eleqtrdi 2848 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ 𝑗 ∈ (β„€β‰₯β€˜π‘))
71 simprr 772 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ 𝑖 ∈ (β„€β‰₯β€˜π‘—))
72 elfzuzb 13442 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑁...𝑖) ↔ (𝑗 ∈ (β„€β‰₯β€˜π‘) ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—)))
7370, 71, 72sylanbrc 584 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ 𝑗 ∈ (𝑁...𝑖))
74 fzsplit 13474 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑁...𝑖) β†’ (𝑁...𝑖) = ((𝑁...𝑗) βˆͺ ((𝑗 + 1)...𝑖)))
7573, 74syl 17 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ (𝑁...𝑖) = ((𝑁...𝑗) βˆͺ ((𝑗 + 1)...𝑖)))
7669, 75sseqtrrid 4002 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ ((𝑗 + 1)...𝑖) βŠ† (𝑁...𝑖))
7776sselda 3949 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ π‘˜ ∈ ((𝑗 + 1)...𝑖)) β†’ π‘˜ ∈ (𝑁...𝑖))
7877adantlr 714 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) ∧ π‘˜ ∈ ((𝑗 + 1)...𝑖)) β†’ π‘˜ ∈ (𝑁...𝑖))
7915ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ 𝐹:π‘βŸΆ(β„‚ ↑m 𝑆))
8079, 18, 19syl2an 597 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ π‘˜ ∈ (𝑁...𝑖)) β†’ (πΉβ€˜π‘˜) ∈ (β„‚ ↑m 𝑆))
8180, 21syl 17 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ π‘˜ ∈ (𝑁...𝑖)) β†’ (πΉβ€˜π‘˜):π‘†βŸΆβ„‚)
8281ffvelcdmda 7040 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ π‘˜ ∈ (𝑁...𝑖)) ∧ 𝑧 ∈ 𝑆) β†’ ((πΉβ€˜π‘˜)β€˜π‘§) ∈ β„‚)
8382an32s 651 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) ∧ π‘˜ ∈ (𝑁...𝑖)) β†’ ((πΉβ€˜π‘˜)β€˜π‘§) ∈ β„‚)
8478, 83syldan 592 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) ∧ π‘˜ ∈ ((𝑗 + 1)...𝑖)) β†’ ((πΉβ€˜π‘˜)β€˜π‘§) ∈ β„‚)
8584abscld 15328 . . . . . . . . . . 11 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) ∧ π‘˜ ∈ ((𝑗 + 1)...𝑖)) β†’ (absβ€˜((πΉβ€˜π‘˜)β€˜π‘§)) ∈ ℝ)
8668, 85fsumrecl 15626 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(absβ€˜((πΉβ€˜π‘˜)β€˜π‘§)) ∈ ℝ)
87 mtest.c . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (π‘€β€˜π‘˜) ∈ ℝ)
883, 1, 87serfre 13944 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ seq𝑁( + , 𝑀):π‘βŸΆβ„)
8988ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ seq𝑁( + , 𝑀):π‘βŸΆβ„)
9089, 56ffvelcdmd 7041 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ (seq𝑁( + , 𝑀)β€˜π‘–) ∈ ℝ)
9189, 61ffvelcdmd 7041 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ (seq𝑁( + , 𝑀)β€˜π‘—) ∈ ℝ)
9290, 91resubcld 11590 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ ((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—)) ∈ ℝ)
9392recnd 11190 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ ((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—)) ∈ β„‚)
9493abscld 15328 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ (absβ€˜((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—))) ∈ ℝ)
9594adantr 482 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (absβ€˜((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—))) ∈ ℝ)
9655, 33sylan2 594 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ (seq𝑁( ∘f + , 𝐹)β€˜π‘–) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–)))
9796adantlr 714 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ (seq𝑁( ∘f + , 𝐹)β€˜π‘–) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–)))
9897fveq1d 6849 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) = ((𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–))β€˜π‘§))
99 fvex 6860 . . . . . . . . . . . . . . . 16 (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–) ∈ V
100 eqid 2737 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–)) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–))
101100fvmpt2 6964 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ 𝑆 ∧ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–) ∈ V) β†’ ((𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–))β€˜π‘§) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–))
10299, 101mpan2 690 . . . . . . . . . . . . . . 15 (𝑧 ∈ 𝑆 β†’ ((𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–))β€˜π‘§) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–))
10398, 102sylan9eq 2797 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–))
104 fveq2 6847 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 β†’ (seq𝑁( ∘f + , 𝐹)β€˜π‘–) = (seq𝑁( ∘f + , 𝐹)β€˜π‘—))
105 fveq2 6847 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 β†’ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘—))
106105mpteq2dv 5212 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 β†’ (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–)) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘—)))
107104, 106eqeq12d 2753 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 β†’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘–) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–)) ↔ (seq𝑁( ∘f + , 𝐹)β€˜π‘—) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘—))))
10833ralrimiva 3144 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ βˆ€π‘– ∈ 𝑍 (seq𝑁( ∘f + , 𝐹)β€˜π‘–) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–)))
109108ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ βˆ€π‘– ∈ 𝑍 (seq𝑁( ∘f + , 𝐹)β€˜π‘–) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–)))
110107, 109, 61rspcdva 3585 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ (seq𝑁( ∘f + , 𝐹)β€˜π‘—) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘—)))
111110fveq1d 6849 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§) = ((𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘—))β€˜π‘§))
112 fvex 6860 . . . . . . . . . . . . . . . 16 (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘—) ∈ V
113 eqid 2737 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘—)) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘—))
114113fvmpt2 6964 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ 𝑆 ∧ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘—) ∈ V) β†’ ((𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘—))β€˜π‘§) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘—))
115112, 114mpan2 690 . . . . . . . . . . . . . . 15 (𝑧 ∈ 𝑆 β†’ ((𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘—))β€˜π‘§) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘—))
116111, 115sylan9eq 2797 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘—))
117103, 116oveq12d 7380 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) βˆ’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§)) = ((seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–) βˆ’ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘—)))
11818adantl 483 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) ∧ π‘˜ ∈ (𝑁...𝑖)) β†’ π‘˜ ∈ 𝑍)
119118, 29syl 17 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) ∧ π‘˜ ∈ (𝑁...𝑖)) β†’ ((𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§))β€˜π‘˜) = ((πΉβ€˜π‘˜)β€˜π‘§))
12056adantr 482 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ 𝑖 ∈ 𝑍)
121120, 3eleqtrdi 2848 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ 𝑖 ∈ (β„€β‰₯β€˜π‘))
122119, 121, 83fsumser 15622 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ Ξ£π‘˜ ∈ (𝑁...𝑖)((πΉβ€˜π‘˜)β€˜π‘§) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–))
123 elfzuz 13444 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ (𝑁...𝑗) β†’ π‘˜ ∈ (β„€β‰₯β€˜π‘))
124123, 3eleqtrrdi 2849 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ (𝑁...𝑗) β†’ π‘˜ ∈ 𝑍)
125124adantl 483 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) ∧ π‘˜ ∈ (𝑁...𝑗)) β†’ π‘˜ ∈ 𝑍)
126125, 29syl 17 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) ∧ π‘˜ ∈ (𝑁...𝑗)) β†’ ((𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§))β€˜π‘˜) = ((πΉβ€˜π‘˜)β€˜π‘§))
12761adantr 482 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ 𝑗 ∈ 𝑍)
128127, 3eleqtrdi 2848 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ 𝑗 ∈ (β„€β‰₯β€˜π‘))
12979, 124, 19syl2an 597 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ π‘˜ ∈ (𝑁...𝑗)) β†’ (πΉβ€˜π‘˜) ∈ (β„‚ ↑m 𝑆))
130129, 21syl 17 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ π‘˜ ∈ (𝑁...𝑗)) β†’ (πΉβ€˜π‘˜):π‘†βŸΆβ„‚)
131130ffvelcdmda 7040 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ π‘˜ ∈ (𝑁...𝑗)) ∧ 𝑧 ∈ 𝑆) β†’ ((πΉβ€˜π‘˜)β€˜π‘§) ∈ β„‚)
132131an32s 651 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) ∧ π‘˜ ∈ (𝑁...𝑗)) β†’ ((πΉβ€˜π‘˜)β€˜π‘§) ∈ β„‚)
133126, 128, 132fsumser 15622 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ Ξ£π‘˜ ∈ (𝑁...𝑗)((πΉβ€˜π‘˜)β€˜π‘§) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘—))
134122, 133oveq12d 7380 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (Ξ£π‘˜ ∈ (𝑁...𝑖)((πΉβ€˜π‘˜)β€˜π‘§) βˆ’ Ξ£π‘˜ ∈ (𝑁...𝑗)((πΉβ€˜π‘˜)β€˜π‘§)) = ((seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘–) βˆ’ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)β€˜π‘§)))β€˜π‘—)))
135 fzfid 13885 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (𝑁...𝑗) ∈ Fin)
136135, 132fsumcl 15625 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ Ξ£π‘˜ ∈ (𝑁...𝑗)((πΉβ€˜π‘˜)β€˜π‘§) ∈ β„‚)
13768, 84fsumcl 15625 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)((πΉβ€˜π‘˜)β€˜π‘§) ∈ β„‚)
138 eluzelre 12781 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (β„€β‰₯β€˜π‘) β†’ 𝑗 ∈ ℝ)
13970, 138syl 17 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ 𝑗 ∈ ℝ)
140139ltp1d 12092 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ 𝑗 < (𝑗 + 1))
141 fzdisj 13475 . . . . . . . . . . . . . . . . 17 (𝑗 < (𝑗 + 1) β†’ ((𝑁...𝑗) ∩ ((𝑗 + 1)...𝑖)) = βˆ…)
142140, 141syl 17 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ ((𝑁...𝑗) ∩ ((𝑗 + 1)...𝑖)) = βˆ…)
143142adantr 482 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ ((𝑁...𝑗) ∩ ((𝑗 + 1)...𝑖)) = βˆ…)
14475adantr 482 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (𝑁...𝑖) = ((𝑁...𝑗) βˆͺ ((𝑗 + 1)...𝑖)))
145 fzfid 13885 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (𝑁...𝑖) ∈ Fin)
146143, 144, 145, 83fsumsplit 15633 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ Ξ£π‘˜ ∈ (𝑁...𝑖)((πΉβ€˜π‘˜)β€˜π‘§) = (Ξ£π‘˜ ∈ (𝑁...𝑗)((πΉβ€˜π‘˜)β€˜π‘§) + Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)((πΉβ€˜π‘˜)β€˜π‘§)))
147136, 137, 146mvrladdd 11575 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (Ξ£π‘˜ ∈ (𝑁...𝑖)((πΉβ€˜π‘˜)β€˜π‘§) βˆ’ Ξ£π‘˜ ∈ (𝑁...𝑗)((πΉβ€˜π‘˜)β€˜π‘§)) = Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)((πΉβ€˜π‘˜)β€˜π‘§))
148117, 134, 1473eqtr2d 2783 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) βˆ’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§)) = Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)((πΉβ€˜π‘˜)β€˜π‘§))
149148fveq2d 6851 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (absβ€˜(((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) βˆ’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§))) = (absβ€˜Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)((πΉβ€˜π‘˜)β€˜π‘§)))
15068, 84fsumabs 15693 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (absβ€˜Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)((πΉβ€˜π‘˜)β€˜π‘§)) ≀ Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(absβ€˜((πΉβ€˜π‘˜)β€˜π‘§)))
151149, 150eqbrtrd 5132 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (absβ€˜(((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) βˆ’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§))) ≀ Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(absβ€˜((πΉβ€˜π‘˜)β€˜π‘§)))
152 simpll 766 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ πœ‘)
153152, 18, 87syl2an 597 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ π‘˜ ∈ (𝑁...𝑖)) β†’ (π‘€β€˜π‘˜) ∈ ℝ)
15477, 153syldan 592 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ π‘˜ ∈ ((𝑗 + 1)...𝑖)) β†’ (π‘€β€˜π‘˜) ∈ ℝ)
155154adantlr 714 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) ∧ π‘˜ ∈ ((𝑗 + 1)...𝑖)) β†’ (π‘€β€˜π‘˜) ∈ ℝ)
15678, 18syl 17 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) ∧ π‘˜ ∈ ((𝑗 + 1)...𝑖)) β†’ π‘˜ ∈ 𝑍)
157 mtest.l . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘˜ ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) β†’ (absβ€˜((πΉβ€˜π‘˜)β€˜π‘§)) ≀ (π‘€β€˜π‘˜))
158157ad4ant14 751 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ (π‘˜ ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) β†’ (absβ€˜((πΉβ€˜π‘˜)β€˜π‘§)) ≀ (π‘€β€˜π‘˜))
159158anass1rs 654 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) ∧ π‘˜ ∈ 𝑍) β†’ (absβ€˜((πΉβ€˜π‘˜)β€˜π‘§)) ≀ (π‘€β€˜π‘˜))
160156, 159syldan 592 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) ∧ π‘˜ ∈ ((𝑗 + 1)...𝑖)) β†’ (absβ€˜((πΉβ€˜π‘˜)β€˜π‘§)) ≀ (π‘€β€˜π‘˜))
16168, 85, 155, 160fsumle 15691 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(absβ€˜((πΉβ€˜π‘˜)β€˜π‘§)) ≀ Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(π‘€β€˜π‘˜))
162 eqidd 2738 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ π‘˜ ∈ (𝑁...𝑖)) β†’ (π‘€β€˜π‘˜) = (π‘€β€˜π‘˜))
16356, 3eleqtrdi 2848 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ 𝑖 ∈ (β„€β‰₯β€˜π‘))
164153recnd 11190 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ π‘˜ ∈ (𝑁...𝑖)) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
165162, 163, 164fsumser 15622 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ Ξ£π‘˜ ∈ (𝑁...𝑖)(π‘€β€˜π‘˜) = (seq𝑁( + , 𝑀)β€˜π‘–))
166 eqidd 2738 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ π‘˜ ∈ (𝑁...𝑗)) β†’ (π‘€β€˜π‘˜) = (π‘€β€˜π‘˜))
167152, 124, 87syl2an 597 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ π‘˜ ∈ (𝑁...𝑗)) β†’ (π‘€β€˜π‘˜) ∈ ℝ)
168167recnd 11190 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ π‘˜ ∈ (𝑁...𝑗)) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
169166, 70, 168fsumser 15622 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ Ξ£π‘˜ ∈ (𝑁...𝑗)(π‘€β€˜π‘˜) = (seq𝑁( + , 𝑀)β€˜π‘—))
170165, 169oveq12d 7380 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ (Ξ£π‘˜ ∈ (𝑁...𝑖)(π‘€β€˜π‘˜) βˆ’ Ξ£π‘˜ ∈ (𝑁...𝑗)(π‘€β€˜π‘˜)) = ((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—)))
171 fzfid 13885 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ (𝑁...𝑗) ∈ Fin)
172171, 168fsumcl 15625 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ Ξ£π‘˜ ∈ (𝑁...𝑗)(π‘€β€˜π‘˜) ∈ β„‚)
173 fzfid 13885 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ ((𝑗 + 1)...𝑖) ∈ Fin)
17477, 164syldan 592 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ π‘˜ ∈ ((𝑗 + 1)...𝑖)) β†’ (π‘€β€˜π‘˜) ∈ β„‚)
175173, 174fsumcl 15625 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(π‘€β€˜π‘˜) ∈ β„‚)
176 fzfid 13885 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ (𝑁...𝑖) ∈ Fin)
177142, 75, 176, 164fsumsplit 15633 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ Ξ£π‘˜ ∈ (𝑁...𝑖)(π‘€β€˜π‘˜) = (Ξ£π‘˜ ∈ (𝑁...𝑗)(π‘€β€˜π‘˜) + Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(π‘€β€˜π‘˜)))
178172, 175, 177mvrladdd 11575 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ (Ξ£π‘˜ ∈ (𝑁...𝑖)(π‘€β€˜π‘˜) βˆ’ Ξ£π‘˜ ∈ (𝑁...𝑗)(π‘€β€˜π‘˜)) = Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(π‘€β€˜π‘˜))
179170, 178eqtr3d 2779 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ ((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—)) = Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(π‘€β€˜π‘˜))
180179fveq2d 6851 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ (absβ€˜((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—))) = (absβ€˜Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(π‘€β€˜π‘˜)))
181180adantr 482 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (absβ€˜((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—))) = (absβ€˜Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(π‘€β€˜π‘˜)))
182179, 92eqeltrrd 2839 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(π‘€β€˜π‘˜) ∈ ℝ)
183182adantr 482 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(π‘€β€˜π‘˜) ∈ ℝ)
184 0red 11165 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) ∧ π‘˜ ∈ ((𝑗 + 1)...𝑖)) β†’ 0 ∈ ℝ)
18584absge0d 15336 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) ∧ π‘˜ ∈ ((𝑗 + 1)...𝑖)) β†’ 0 ≀ (absβ€˜((πΉβ€˜π‘˜)β€˜π‘§)))
186184, 85, 155, 185, 160letrd 11319 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) ∧ π‘˜ ∈ ((𝑗 + 1)...𝑖)) β†’ 0 ≀ (π‘€β€˜π‘˜))
18768, 155, 186fsumge0 15687 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ 0 ≀ Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(π‘€β€˜π‘˜))
188183, 187absidd 15314 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (absβ€˜Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(π‘€β€˜π‘˜)) = Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(π‘€β€˜π‘˜))
189181, 188eqtrd 2777 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (absβ€˜((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—))) = Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(π‘€β€˜π‘˜))
190161, 189breqtrrd 5138 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ Ξ£π‘˜ ∈ ((𝑗 + 1)...𝑖)(absβ€˜((πΉβ€˜π‘˜)β€˜π‘§)) ≀ (absβ€˜((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—))))
19167, 86, 95, 151, 190letrd 11319 . . . . . . . . 9 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (absβ€˜(((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) βˆ’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§))) ≀ (absβ€˜((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—))))
192 simpllr 775 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ π‘Ÿ ∈ ℝ+)
193192rpred 12964 . . . . . . . . . 10 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ π‘Ÿ ∈ ℝ)
194 lelttr 11252 . . . . . . . . . 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 1372 . . . . . . . . 9 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ (((absβ€˜(((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) βˆ’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§))) ≀ (absβ€˜((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—))) ∧ (absβ€˜((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—))) < π‘Ÿ) β†’ (absβ€˜(((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) βˆ’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§))) < π‘Ÿ))
196191, 195mpand 694 . . . . . . . 8 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) ∧ 𝑧 ∈ 𝑆) β†’ ((absβ€˜((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—))) < π‘Ÿ β†’ (absβ€˜(((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) βˆ’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§))) < π‘Ÿ))
197196ralrimdva 3152 . . . . . . 7 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—))) β†’ ((absβ€˜((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—))) < π‘Ÿ β†’ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) βˆ’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§))) < π‘Ÿ))
198197anassrs 469 . . . . . 6 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘—)) β†’ ((absβ€˜((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—))) < π‘Ÿ β†’ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) βˆ’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§))) < π‘Ÿ))
199198ralimdva 3165 . . . . 5 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) β†’ (βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—))) < π‘Ÿ β†’ βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑆 (absβ€˜(((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) βˆ’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§))) < π‘Ÿ))
200199reximdva 3166 . . . 4 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ (βˆƒπ‘— ∈ 𝑍 βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—))) < π‘Ÿ β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑆 (absβ€˜(((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) βˆ’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§))) < π‘Ÿ))
201200ralimdva 3165 . . 3 (πœ‘ β†’ (βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘— ∈ 𝑍 βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq𝑁( + , 𝑀)β€˜π‘–) βˆ’ (seq𝑁( + , 𝑀)β€˜π‘—))) < π‘Ÿ β†’ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘— ∈ 𝑍 βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑆 (absβ€˜(((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) βˆ’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§))) < π‘Ÿ))
2025, 201mpd 15 . 2 (πœ‘ β†’ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘— ∈ 𝑍 βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑆 (absβ€˜(((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) βˆ’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§))) < π‘Ÿ)
2033, 1, 10, 53ulmcau 25770 . 2 (πœ‘ β†’ (seq𝑁( ∘f + , 𝐹) ∈ dom (β‡π‘’β€˜π‘†) ↔ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘— ∈ 𝑍 βˆ€π‘– ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑆 (absβ€˜(((seq𝑁( ∘f + , 𝐹)β€˜π‘–)β€˜π‘§) βˆ’ ((seq𝑁( ∘f + , 𝐹)β€˜π‘—)β€˜π‘§))) < π‘Ÿ))
204202, 203mpbird 257 1 (πœ‘ β†’ seq𝑁( ∘f + , 𝐹) ∈ dom (β‡π‘’β€˜π‘†))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3065  βˆƒwrex 3074  Vcvv 3448   βˆͺ cun 3913   ∩ cin 3914  βˆ…c0 4287   class class class wbr 5110   ↦ cmpt 5193  dom cdm 5638   Fn wfn 6496  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362   ∘f cof 7620   ↑m cmap 8772  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392  β„€cz 12506  β„€β‰₯cuz 12770  β„+crp 12922  ...cfz 13431  seqcseq 13913  abscabs 15126   ⇝ cli 15373  Ξ£csu 15577  β‡π‘’culm 25751
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-map 8774  df-pm 8775  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-inf 9386  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-z 12507  df-uz 12771  df-rp 12923  df-ico 13277  df-fz 13432  df-fzo 13575  df-fl 13704  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-sum 15578  df-ulm 25752
This theorem is referenced by:  pserulm  25797  lgamgulmlem6  26399  knoppcnlem6  34990
  Copyright terms: Public domain W3C validator