mtest - Metamath Proof Explorer

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

Theorem mtest 26647

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.

Step	Hyp	Ref	Expression
1		mtest.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℤ)
2		mtest.d	. . . 4 ⊢ (𝜑 → seq𝑁( + , 𝑀) ∈ dom ⇝ )
3		mtest.z	. . . . 5 ⊢ 𝑍 = (ℤ_≥‘𝑁)
4	3	climcau 15762	. . . 4 ⊢ ((𝑁 ∈ ℤ ∧ seq𝑁( + , 𝑀) ∈ dom ⇝ ) → ∀𝑟 ∈ ℝ⁺ ∃𝑗 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟)
5	1, 2, 4	syl2anc 596	. . 3 ⊢ (𝜑 → ∀𝑟 ∈ ℝ⁺ ∃𝑗 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟)
6		seqfn 14081	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℤ → seq𝑁( ∘_f + , 𝐹) Fn (ℤ_≥‘𝑁))
7	1, 6	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → seq𝑁( ∘_f + , 𝐹) Fn (ℤ_≥‘𝑁))
8	3	fneq2i 6634	. . . . . . . . . . . . . . . . . 18 ⊢ (seq𝑁( ∘_f + , 𝐹) Fn 𝑍 ↔ seq𝑁( ∘_f + , 𝐹) Fn (ℤ_≥‘𝑁))
9	7, 8	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → seq𝑁( ∘_f + , 𝐹) Fn 𝑍)
10		mtest.s	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑆 ∈ 𝑉)
11	10	elexd 3476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑆 ∈ V)
12	11	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑆 ∈ V)
13		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍)
14	13, 3	eleqtrdi 2872	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ (ℤ_≥‘𝑁))
15		mtest.f	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑_m 𝑆))
16	15	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝐹:𝑍⟶(ℂ ↑_m 𝑆))
17		elfzuz 13578	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (𝑁...𝑖) → 𝑘 ∈ (ℤ_≥‘𝑁))
18	17, 3	eleqtrrdi 2873	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (𝑁...𝑖) → 𝑘 ∈ 𝑍)
19		ffvelcdm 7078	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹:𝑍⟶(ℂ ↑_m 𝑆) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ (ℂ ↑_m 𝑆))
20	16, 18, 19	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹‘𝑘) ∈ (ℂ ↑_m 𝑆))
21		elmapi 8852	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑘) ∈ (ℂ ↑_m 𝑆) → (𝐹‘𝑘):𝑆⟶ℂ)
22	20, 21	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹‘𝑘):𝑆⟶ℂ)
23	22	feqmptd 6950	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹‘𝑘) = (𝑧 ∈ 𝑆 ↦ ((𝐹‘𝑘)‘𝑧)))
24	18	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → 𝑘 ∈ 𝑍)
25		fveq2 6882	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
26	25	fveq1d 6884	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛)‘𝑧) = ((𝐹‘𝑘)‘𝑧))
27		eqid 2762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)) = (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧))
28		fvex 6895	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑘)‘𝑧) ∈ V
29	26, 27, 28	fvmpt 6990	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ 𝑍 → ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧))‘𝑘) = ((𝐹‘𝑘)‘𝑧))
30	24, 29	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧))‘𝑘) = ((𝐹‘𝑘)‘𝑧))
31	30	mpteq2dv 5203	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝑧 ∈ 𝑆 ↦ ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧))‘𝑘)) = (𝑧 ∈ 𝑆 ↦ ((𝐹‘𝑘)‘𝑧)))
32	23, 31	eqtr4d 2800	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹‘𝑘) = (𝑧 ∈ 𝑆 ↦ ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧))‘𝑘)))
33	12, 14, 32	seqof 14127	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (seq𝑁( ∘_f + , 𝐹)‘𝑖) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖)))
34	1	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → 𝑁 ∈ ℤ)
35	15	ffvelcdmda 7081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ (ℂ ↑_m 𝑆))
36		elmapi 8852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐹‘𝑛) ∈ (ℂ ↑_m 𝑆) → (𝐹‘𝑛):𝑆⟶ℂ)
37	35, 36	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):𝑆⟶ℂ)
38	37	ffvelcdmda 7081	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑛)‘𝑧) ∈ ℂ)
39	38	an32s 665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑧) ∈ ℂ)
40	39	fmpttd 7112	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)):𝑍⟶ℂ)
41	40	ffvelcdmda 7081	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑖 ∈ 𝑍) → ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧))‘𝑖) ∈ ℂ)
42	3, 34, 41	serf 14098	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧))):𝑍⟶ℂ)
43	42	ffvelcdmda 7081	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑆) ∧ 𝑖 ∈ 𝑍) → (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖) ∈ ℂ)
44	43	an32s 665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑧 ∈ 𝑆) → (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖) ∈ ℂ)
45	44	fmpttd 7112	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖)):𝑆⟶ℂ)
46		cnex 11209	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ ∈ V
47		elmapg 8842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂ ∈ V ∧ 𝑆 ∈ V) → ((𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖)) ∈ (ℂ ↑_m 𝑆) ↔ (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖)):𝑆⟶ℂ))
48	46, 12, 47	sylancr 599	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ((𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖)) ∈ (ℂ ↑_m 𝑆) ↔ (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖)):𝑆⟶ℂ))
49	45, 48	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖)) ∈ (ℂ ↑_m 𝑆))
50	33, 49	eqeltrd 2862	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (seq𝑁( ∘_f + , 𝐹)‘𝑖) ∈ (ℂ ↑_m 𝑆))
51	50	ralrimiva 3156	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑖 ∈ 𝑍 (seq𝑁( ∘_f + , 𝐹)‘𝑖) ∈ (ℂ ↑_m 𝑆))
52		ffnfv 7116	. . . . . . . . . . . . . . . . 17 ⊢ (seq𝑁( ∘_f + , 𝐹):𝑍⟶(ℂ ↑_m 𝑆) ↔ (seq𝑁( ∘_f + , 𝐹) Fn 𝑍 ∧ ∀𝑖 ∈ 𝑍 (seq𝑁( ∘_f + , 𝐹)‘𝑖) ∈ (ℂ ↑_m 𝑆)))
53	9, 51, 52	sylanbrc 595	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → seq𝑁( ∘_f + , 𝐹):𝑍⟶(ℂ ↑_m 𝑆))
54	53	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → seq𝑁( ∘_f + , 𝐹):𝑍⟶(ℂ ↑_m 𝑆))
55	3	uztrn2 12910	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → 𝑖 ∈ 𝑍)
56	55	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → 𝑖 ∈ 𝑍)
57	54, 56	ffvelcdmd 7082	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → (seq𝑁( ∘_f + , 𝐹)‘𝑖) ∈ (ℂ ↑_m 𝑆))
58		elmapi 8852	. . . . . . . . . . . . . 14 ⊢ ((seq𝑁( ∘_f + , 𝐹)‘𝑖) ∈ (ℂ ↑_m 𝑆) → (seq𝑁( ∘_f + , 𝐹)‘𝑖):𝑆⟶ℂ)
59	57, 58	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → (seq𝑁( ∘_f + , 𝐹)‘𝑖):𝑆⟶ℂ)
60	59	ffvelcdmda 7081	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → ((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) ∈ ℂ)
61		simprl 783	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → 𝑗 ∈ 𝑍)
62	54, 61	ffvelcdmd 7082	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → (seq𝑁( ∘_f + , 𝐹)‘𝑗) ∈ (ℂ ↑_m 𝑆))
63		elmapi 8852	. . . . . . . . . . . . . 14 ⊢ ((seq𝑁( ∘_f + , 𝐹)‘𝑗) ∈ (ℂ ↑_m 𝑆) → (seq𝑁( ∘_f + , 𝐹)‘𝑗):𝑆⟶ℂ)
64	62, 63	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → (seq𝑁( ∘_f + , 𝐹)‘𝑗):𝑆⟶ℂ)
65	64	ffvelcdmda 7081	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧) ∈ ℂ)
66	60, 65	subcld 11597	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧)) ∈ ℂ)
67	66	abscld 15530	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (abs‘(((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧))) ∈ ℝ)
68		fzfid 14041	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → ((𝑗 + 1)...𝑖) ∈ Fin)
69		ssun2 4128	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 + 1)...𝑖) ⊆ ((𝑁...𝑗) ∪ ((𝑗 + 1)...𝑖))
70	61, 3	eleqtrdi 2872	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → 𝑗 ∈ (ℤ_≥‘𝑁))
71		simprr 785	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → 𝑖 ∈ (ℤ_≥‘𝑗))
72		elfzuzb 13576	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (𝑁...𝑖) ↔ (𝑗 ∈ (ℤ_≥‘𝑁) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)))
73	70, 71, 72	sylanbrc 595	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → 𝑗 ∈ (𝑁...𝑖))
74		fzsplit 13609	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (𝑁...𝑖) → (𝑁...𝑖) = ((𝑁...𝑗) ∪ ((𝑗 + 1)...𝑖)))
75	73, 74	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → (𝑁...𝑖) = ((𝑁...𝑗) ∪ ((𝑗 + 1)...𝑖)))
76	69, 75	sseqtrrid 3977	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → ((𝑗 + 1)...𝑖) ⊆ (𝑁...𝑖))
77	76	sselda 3934	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 𝑘 ∈ (𝑁...𝑖))
78	77	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 𝑘 ∈ (𝑁...𝑖))
79	15	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → 𝐹:𝑍⟶(ℂ ↑_m 𝑆))
80	79, 18, 19	syl2an 608	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹‘𝑘) ∈ (ℂ ↑_m 𝑆))
81	80, 21	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝐹‘𝑘):𝑆⟶ℂ)
82	81	ffvelcdmda 7081	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑘)‘𝑧) ∈ ℂ)
83	82	an32s 665	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑘 ∈ (𝑁...𝑖)) → ((𝐹‘𝑘)‘𝑧) ∈ ℂ)
84	78, 83	syldan 603	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → ((𝐹‘𝑘)‘𝑧) ∈ ℂ)
85	84	abscld 15530	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (abs‘((𝐹‘𝑘)‘𝑧)) ∈ ℝ)
86	68, 85	fsumrecl 15824	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹‘𝑘)‘𝑧)) ∈ ℝ)
87		mtest.c	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑀‘𝑘) ∈ ℝ)
88	3, 1, 87	serfre 14099	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → seq𝑁( + , 𝑀):𝑍⟶ℝ)
89	88	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → seq𝑁( + , 𝑀):𝑍⟶ℝ)
90	89, 56	ffvelcdmd 7082	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → (seq𝑁( + , 𝑀)‘𝑖) ∈ ℝ)
91	89, 61	ffvelcdmd 7082	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → (seq𝑁( + , 𝑀)‘𝑗) ∈ ℝ)
92	90, 91	resubcld 11670	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → ((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗)) ∈ ℝ)
93	92	recnd 11265	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → ((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗)) ∈ ℂ)
94	93	abscld 15530	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∈ ℝ)
95	94	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∈ ℝ)
96	55, 33	sylan2 605	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → (seq𝑁( ∘_f + , 𝐹)‘𝑖) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖)))
97	96	adantlr 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → (seq𝑁( ∘_f + , 𝐹)‘𝑖) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖)))
98	97	fveq1d 6884	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → ((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) = ((𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖))‘𝑧))
99		fvex 6895	. . . . . . . . . . . . . . . 16 ⊢ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖) ∈ V
100		eqid 2762	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖)) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖))
101	100	fvmpt2 7002	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ 𝑆 ∧ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖) ∈ V) → ((𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖))‘𝑧) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖))
102	99, 101	mpan2 704	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑆 → ((𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖))‘𝑧) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖))
103	98, 102	sylan9eq 2817	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → ((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖))
104		fveq2 6882	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (seq𝑁( ∘_f + , 𝐹)‘𝑖) = (seq𝑁( ∘_f + , 𝐹)‘𝑗))
105		fveq2 6882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑗))
106	105	mpteq2dv 5203	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖)) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑗)))
107	104, 106	eqeq12d 2778	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → ((seq𝑁( ∘_f + , 𝐹)‘𝑖) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖)) ↔ (seq𝑁( ∘_f + , 𝐹)‘𝑗) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑗))))
108	33	ralrimiva 3156	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑖 ∈ 𝑍 (seq𝑁( ∘_f + , 𝐹)‘𝑖) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖)))
109	108	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → ∀𝑖 ∈ 𝑍 (seq𝑁( ∘_f + , 𝐹)‘𝑖) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖)))
110	107, 109, 61	rspcdva 3580	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → (seq𝑁( ∘_f + , 𝐹)‘𝑗) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑗)))
111	110	fveq1d 6884	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧) = ((𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑗))‘𝑧))
112		fvex 6895	. . . . . . . . . . . . . . . 16 ⊢ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑗) ∈ V
113		eqid 2762	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑗)) = (𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑗))
114	113	fvmpt2 7002	. . . . . . . . . . . . . . . 16 ⊢ ((𝑧 ∈ 𝑆 ∧ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑗) ∈ V) → ((𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑗))‘𝑧) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑗))
115	112, 114	mpan2 704	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑆 → ((𝑧 ∈ 𝑆 ↦ (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑗))‘𝑧) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑗))
116	111, 115	sylan9eq 2817	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑗))
117	103, 116	oveq12d 7435	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧)) = ((seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖) − (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑗)))
118	18	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑘 ∈ (𝑁...𝑖)) → 𝑘 ∈ 𝑍)
119	118, 29	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑘 ∈ (𝑁...𝑖)) → ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧))‘𝑘) = ((𝐹‘𝑘)‘𝑧))
120	56	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → 𝑖 ∈ 𝑍)
121	120, 3	eleqtrdi 2872	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → 𝑖 ∈ (ℤ_≥‘𝑁))
122	119, 121, 83	fsumser 15820	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → Σ𝑘 ∈ (𝑁...𝑖)((𝐹‘𝑘)‘𝑧) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖))
123		elfzuz 13578	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (𝑁...𝑗) → 𝑘 ∈ (ℤ_≥‘𝑁))
124	123, 3	eleqtrrdi 2873	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (𝑁...𝑗) → 𝑘 ∈ 𝑍)
125	124	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑘 ∈ (𝑁...𝑗)) → 𝑘 ∈ 𝑍)
126	125, 29	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑘 ∈ (𝑁...𝑗)) → ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧))‘𝑘) = ((𝐹‘𝑘)‘𝑧))
127	61	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → 𝑗 ∈ 𝑍)
128	127, 3	eleqtrdi 2872	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → 𝑗 ∈ (ℤ_≥‘𝑁))
129	79, 124, 19	syl2an 608	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝐹‘𝑘) ∈ (ℂ ↑_m 𝑆))
130	129, 21	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝐹‘𝑘):𝑆⟶ℂ)
131	130	ffvelcdmda 7081	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑘)‘𝑧) ∈ ℂ)
132	131	an32s 665	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑘 ∈ (𝑁...𝑗)) → ((𝐹‘𝑘)‘𝑧) ∈ ℂ)
133	126, 128, 132	fsumser 15820	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → Σ𝑘 ∈ (𝑁...𝑗)((𝐹‘𝑘)‘𝑧) = (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑗))
134	122, 133	oveq12d 7435	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (Σ𝑘 ∈ (𝑁...𝑖)((𝐹‘𝑘)‘𝑧) − Σ𝑘 ∈ (𝑁...𝑗)((𝐹‘𝑘)‘𝑧)) = ((seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑖) − (seq𝑁( + , (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑧)))‘𝑗)))
135		fzfid 14041	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (𝑁...𝑗) ∈ Fin)
136	135, 132	fsumcl 15823	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → Σ𝑘 ∈ (𝑁...𝑗)((𝐹‘𝑘)‘𝑧) ∈ ℂ)
137	68, 84	fsumcl 15823	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹‘𝑘)‘𝑧) ∈ ℂ)
138		eluzelre 12902	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (ℤ_≥‘𝑁) → 𝑗 ∈ ℝ)
139	70, 138	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → 𝑗 ∈ ℝ)
140	139	ltp1d 12173	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → 𝑗 < (𝑗 + 1))
141		fzdisj 13610	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 < (𝑗 + 1) → ((𝑁...𝑗) ∩ ((𝑗 + 1)...𝑖)) = ∅)
142	140, 141	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → ((𝑁...𝑗) ∩ ((𝑗 + 1)...𝑖)) = ∅)
143	142	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → ((𝑁...𝑗) ∩ ((𝑗 + 1)...𝑖)) = ∅)
144	75	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (𝑁...𝑖) = ((𝑁...𝑗) ∪ ((𝑗 + 1)...𝑖)))
145		fzfid 14041	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (𝑁...𝑖) ∈ Fin)
146	143, 144, 145, 83	fsumsplit 15831	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → Σ𝑘 ∈ (𝑁...𝑖)((𝐹‘𝑘)‘𝑧) = (Σ𝑘 ∈ (𝑁...𝑗)((𝐹‘𝑘)‘𝑧) + Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹‘𝑘)‘𝑧)))
147	136, 137, 146	mvrladdd 11655	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (Σ𝑘 ∈ (𝑁...𝑖)((𝐹‘𝑘)‘𝑧) − Σ𝑘 ∈ (𝑁...𝑗)((𝐹‘𝑘)‘𝑧)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹‘𝑘)‘𝑧))
148	117, 134, 147	3eqtr2d 2803	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹‘𝑘)‘𝑧))
149	148	fveq2d 6886	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (abs‘(((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧))) = (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹‘𝑘)‘𝑧)))
150	68, 84	fsumabs 15892	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)((𝐹‘𝑘)‘𝑧)) ≤ Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹‘𝑘)‘𝑧)))
151	149, 150	eqbrtrd 5131	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (abs‘(((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧))) ≤ Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹‘𝑘)‘𝑧)))
152		simpll 779	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → 𝜑)
153	152, 18, 87	syl2an 608	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝑀‘𝑘) ∈ ℝ)
154	77, 153	syldan 603	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (𝑀‘𝑘) ∈ ℝ)
155	154	adantlr 728	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (𝑀‘𝑘) ∈ ℝ)
156	78, 18	syl 18	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 𝑘 ∈ 𝑍)
157		mtest.l	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → (abs‘((𝐹‘𝑘)‘𝑧)) ≤ (𝑀‘𝑘))
158	157	ad4ant14 765	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → (abs‘((𝐹‘𝑘)‘𝑧)) ≤ (𝑀‘𝑘))
159	158	anass1rs 668	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑘 ∈ 𝑍) → (abs‘((𝐹‘𝑘)‘𝑧)) ≤ (𝑀‘𝑘))
160	156, 159	syldan 603	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (abs‘((𝐹‘𝑘)‘𝑧)) ≤ (𝑀‘𝑘))
161	68, 85, 155, 160	fsumle 15890	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹‘𝑘)‘𝑧)) ≤ Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀‘𝑘))
162		eqidd 2763	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝑀‘𝑘) = (𝑀‘𝑘))
163	56, 3	eleqtrdi 2872	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → 𝑖 ∈ (ℤ_≥‘𝑁))
164	153	recnd 11265	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑘 ∈ (𝑁...𝑖)) → (𝑀‘𝑘) ∈ ℂ)
165	162, 163, 164	fsumser 15820	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → Σ𝑘 ∈ (𝑁...𝑖)(𝑀‘𝑘) = (seq𝑁( + , 𝑀)‘𝑖))
166		eqidd 2763	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝑀‘𝑘) = (𝑀‘𝑘))
167	152, 124, 87	syl2an 608	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝑀‘𝑘) ∈ ℝ)
168	167	recnd 11265	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑘 ∈ (𝑁...𝑗)) → (𝑀‘𝑘) ∈ ℂ)
169	166, 70, 168	fsumser 15820	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → Σ𝑘 ∈ (𝑁...𝑗)(𝑀‘𝑘) = (seq𝑁( + , 𝑀)‘𝑗))
170	165, 169	oveq12d 7435	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → (Σ𝑘 ∈ (𝑁...𝑖)(𝑀‘𝑘) − Σ𝑘 ∈ (𝑁...𝑗)(𝑀‘𝑘)) = ((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗)))
171		fzfid 14041	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → (𝑁...𝑗) ∈ Fin)
172	171, 168	fsumcl 15823	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → Σ𝑘 ∈ (𝑁...𝑗)(𝑀‘𝑘) ∈ ℂ)
173		fzfid 14041	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → ((𝑗 + 1)...𝑖) ∈ Fin)
174	77, 164	syldan 603	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → (𝑀‘𝑘) ∈ ℂ)
175	173, 174	fsumcl 15823	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀‘𝑘) ∈ ℂ)
176		fzfid 14041	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → (𝑁...𝑖) ∈ Fin)
177	142, 75, 176, 164	fsumsplit 15831	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → Σ𝑘 ∈ (𝑁...𝑖)(𝑀‘𝑘) = (Σ𝑘 ∈ (𝑁...𝑗)(𝑀‘𝑘) + Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀‘𝑘)))
178	172, 175, 177	mvrladdd 11655	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → (Σ𝑘 ∈ (𝑁...𝑖)(𝑀‘𝑘) − Σ𝑘 ∈ (𝑁...𝑗)(𝑀‘𝑘)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀‘𝑘))
179	170, 178	eqtr3d 2799	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → ((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀‘𝑘))
180	179	fveq2d 6886	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) = (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀‘𝑘)))
181	180	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) = (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀‘𝑘)))
182	179, 92	eqeltrrd 2863	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀‘𝑘) ∈ ℝ)
183	182	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀‘𝑘) ∈ ℝ)
184		0red 11239	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 0 ∈ ℝ)
185	84	absge0d 15538	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 0 ≤ (abs‘((𝐹‘𝑘)‘𝑧)))
186	184, 85, 155, 185, 160	letrd 11395	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) ∧ 𝑘 ∈ ((𝑗 + 1)...𝑖)) → 0 ≤ (𝑀‘𝑘))
187	68, 155, 186	fsumge0 15886	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → 0 ≤ Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀‘𝑘))
188	183, 187	absidd 15514	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (abs‘Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀‘𝑘)) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀‘𝑘))
189	181, 188	eqtrd 2797	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) = Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(𝑀‘𝑘))
190	161, 189	breqtrrd 5137	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → Σ𝑘 ∈ ((𝑗 + 1)...𝑖)(abs‘((𝐹‘𝑘)‘𝑧)) ≤ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))))
191	67, 86, 95, 151, 190	letrd 11395	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (abs‘(((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧))) ≤ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))))
192		simpllr 788	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → 𝑟 ∈ ℝ⁺)
193	192	rpred 13090	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → 𝑟 ∈ ℝ)
194		lelttr 11328	. . . . . . . . . 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 + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
195	67, 95, 193, 194	syl3anc 1398	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → (((abs‘(((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧))) ≤ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) ∧ (abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟) → (abs‘(((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
196	191, 195	mpand 708	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) ∧ 𝑧 ∈ 𝑆) → ((abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → (abs‘(((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
197	196	ralrimdva 3164	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ (𝑗 ∈ 𝑍 ∧ 𝑖 ∈ (ℤ_≥‘𝑗))) → ((abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∀𝑧 ∈ 𝑆 (abs‘(((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
198	197	anassrs 473	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑗 ∈ 𝑍) ∧ 𝑖 ∈ (ℤ_≥‘𝑗)) → ((abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∀𝑧 ∈ 𝑆 (abs‘(((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
199	198	ralimdva 3176	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑗 ∈ 𝑍) → (∀𝑖 ∈ (ℤ_≥‘𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∀𝑖 ∈ (ℤ_≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
200	199	reximdva 3177	. . . 4 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ⁺) → (∃𝑗 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∃𝑗 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
201	200	ralimdva 3176	. . 3 ⊢ (𝜑 → (∀𝑟 ∈ ℝ⁺ ∃𝑗 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑗)(abs‘((seq𝑁( + , 𝑀)‘𝑖) − (seq𝑁( + , 𝑀)‘𝑗))) < 𝑟 → ∀𝑟 ∈ ℝ⁺ ∃𝑗 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
202	5, 201	mpd 16	. 2 ⊢ (𝜑 → ∀𝑟 ∈ ℝ⁺ ∃𝑗 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟)
203	3, 1, 10, 53	ulmcau 26638	. 2 ⊢ (𝜑 → (seq𝑁( ∘_f + , 𝐹) ∈ dom (⇝_𝑢‘𝑆) ↔ ∀𝑟 ∈ ℝ⁺ ∃𝑗 ∈ 𝑍 ∀𝑖 ∈ (ℤ_≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((seq𝑁( ∘_f + , 𝐹)‘𝑖)‘𝑧) − ((seq𝑁( ∘_f + , 𝐹)‘𝑗)‘𝑧))) < 𝑟))
204	202, 203	mpbird 260	1 ⊢ (𝜑 → seq𝑁( ∘_f + , 𝐹) ∈ dom (⇝_𝑢‘𝑆))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∀wral 3078 ∃wrex 3088 Vcvv 3453 ∪ cun 3900 ∩ cin 3901 ∅c0 4282 class class class wbr 5107 ↦ cmpt 5190 dom cdm 5659 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 (class class class)co 7417 ∘_f cof 7680 ↑_m cmap 8830 ℂcc 11126 ℝcr 11127 0cc0 11128 1c1 11129 + caddc 11131 < clt 11271 ≤ cle 11272 − cmin 11469 ℤcz 12619 ℤ_≥cuz 12891 ℝ⁺crp 13046 ...cfz 13565 seqcseq 14069 abscabs 15325 ⇝ cli 15575 Σcsu 15777 ⇝_𝑢culm 26619

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-inf2 9624 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205 ax-pre-sup 11206

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-of 7682 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-er 8700 df-map 8832 df-pm 8833 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-sup 9416 df-inf 9417 df-oi 9486 df-card 9948 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-div 11900 df-nn 12262 df-2 12331 df-3 12332 df-n0 12533 df-z 12620 df-uz 12892 df-rp 13047 df-ico 13408 df-fz 13566 df-fzo 13714 df-fl 13857 df-seq 14070 df-exp 14130 df-hash 14399 df-cj 15190 df-re 15191 df-im 15192 df-sqrt 15326 df-abs 15327 df-limsup 15562 df-clim 15579 df-rlim 15580 df-sum 15778 df-ulm 26620

This theorem is used by: pserulm 26665 lgamgulmlem6 27278 knoppcnlem6 37203

W3C validator