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

Theorem pserulm 25116
 Description: If 𝑆 is a region contained in a circle of radius 𝑀 < 𝑅, then the sequence of partial sums of the infinite series converges uniformly on 𝑆. (Contributed by Mario Carneiro, 26-Feb-2015.)
Hypotheses
Ref Expression
pserf.g 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
pserf.f 𝐹 = (𝑦𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗))
pserf.a (𝜑𝐴:ℕ0⟶ℂ)
pserf.r 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < )
pserulm.h 𝐻 = (𝑖 ∈ ℕ0 ↦ (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)))
pserulm.m (𝜑𝑀 ∈ ℝ)
pserulm.l (𝜑𝑀 < 𝑅)
pserulm.y (𝜑𝑆 ⊆ (abs “ (0[,]𝑀)))
Assertion
Ref Expression
pserulm (𝜑𝐻(⇝𝑢𝑆)𝐹)
Distinct variable groups:   𝑗,𝑛,𝑟,𝑥,𝑦,𝐴   𝑖,𝑗,𝑦,𝐻   𝑖,𝑀,𝑗,𝑦   𝑥,𝑖,𝑟   𝑖,𝐺,𝑗,𝑟,𝑦   𝑆,𝑖,𝑗,𝑦   𝜑,𝑖,𝑗,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑛,𝑟)   𝐴(𝑖)   𝑅(𝑥,𝑦,𝑖,𝑗,𝑛,𝑟)   𝑆(𝑥,𝑛,𝑟)   𝐹(𝑥,𝑦,𝑖,𝑗,𝑛,𝑟)   𝐺(𝑥,𝑛)   𝐻(𝑥,𝑛,𝑟)   𝑀(𝑥,𝑛,𝑟)

Proof of Theorem pserulm
Dummy variables 𝑘 𝑚 𝑤 𝑧 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pserulm.y . . . . . 6 (𝜑𝑆 ⊆ (abs “ (0[,]𝑀)))
21adantr 484 . . . . 5 ((𝜑𝑀 < 0) → 𝑆 ⊆ (abs “ (0[,]𝑀)))
3 0xr 10726 . . . . . . . . 9 0 ∈ ℝ*
4 pserulm.m . . . . . . . . . 10 (𝜑𝑀 ∈ ℝ)
54rexrd 10729 . . . . . . . . 9 (𝜑𝑀 ∈ ℝ*)
6 icc0 12827 . . . . . . . . 9 ((0 ∈ ℝ*𝑀 ∈ ℝ*) → ((0[,]𝑀) = ∅ ↔ 𝑀 < 0))
73, 5, 6sylancr 590 . . . . . . . 8 (𝜑 → ((0[,]𝑀) = ∅ ↔ 𝑀 < 0))
87biimpar 481 . . . . . . 7 ((𝜑𝑀 < 0) → (0[,]𝑀) = ∅)
98imaeq2d 5901 . . . . . 6 ((𝜑𝑀 < 0) → (abs “ (0[,]𝑀)) = (abs “ ∅))
10 ima0 5917 . . . . . 6 (abs “ ∅) = ∅
119, 10eqtrdi 2809 . . . . 5 ((𝜑𝑀 < 0) → (abs “ (0[,]𝑀)) = ∅)
122, 11sseqtrd 3932 . . . 4 ((𝜑𝑀 < 0) → 𝑆 ⊆ ∅)
13 ss0 4294 . . . 4 (𝑆 ⊆ ∅ → 𝑆 = ∅)
1412, 13syl 17 . . 3 ((𝜑𝑀 < 0) → 𝑆 = ∅)
15 nn0uz 12320 . . . 4 0 = (ℤ‘0)
16 0zd 12032 . . . 4 (𝜑 → 0 ∈ ℤ)
17 0zd 12032 . . . . . . . . . 10 ((𝜑𝑦𝑆) → 0 ∈ ℤ)
18 pserf.g . . . . . . . . . . . 12 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
19 pserf.a . . . . . . . . . . . . 13 (𝜑𝐴:ℕ0⟶ℂ)
2019adantr 484 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 𝐴:ℕ0⟶ℂ)
21 cnvimass 5921 . . . . . . . . . . . . . . 15 (abs “ (0[,]𝑀)) ⊆ dom abs
22 absf 14745 . . . . . . . . . . . . . . . 16 abs:ℂ⟶ℝ
2322fdmi 6509 . . . . . . . . . . . . . . 15 dom abs = ℂ
2421, 23sseqtri 3928 . . . . . . . . . . . . . 14 (abs “ (0[,]𝑀)) ⊆ ℂ
251, 24sstrdi 3904 . . . . . . . . . . . . 13 (𝜑𝑆 ⊆ ℂ)
2625sselda 3892 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 𝑦 ∈ ℂ)
2718, 20, 26psergf 25106 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → (𝐺𝑦):ℕ0⟶ℂ)
2827ffvelrnda 6842 . . . . . . . . . 10 (((𝜑𝑦𝑆) ∧ 𝑗 ∈ ℕ0) → ((𝐺𝑦)‘𝑗) ∈ ℂ)
2915, 17, 28serf 13448 . . . . . . . . 9 ((𝜑𝑦𝑆) → seq0( + , (𝐺𝑦)):ℕ0⟶ℂ)
3029ffvelrnda 6842 . . . . . . . 8 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (seq0( + , (𝐺𝑦))‘𝑖) ∈ ℂ)
3130an32s 651 . . . . . . 7 (((𝜑𝑖 ∈ ℕ0) ∧ 𝑦𝑆) → (seq0( + , (𝐺𝑦))‘𝑖) ∈ ℂ)
3231fmpttd 6870 . . . . . 6 ((𝜑𝑖 ∈ ℕ0) → (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)):𝑆⟶ℂ)
33 cnex 10656 . . . . . . 7 ℂ ∈ V
34 ssexg 5193 . . . . . . . . 9 ((𝑆 ⊆ ℂ ∧ ℂ ∈ V) → 𝑆 ∈ V)
3525, 33, 34sylancl 589 . . . . . . . 8 (𝜑𝑆 ∈ V)
3635adantr 484 . . . . . . 7 ((𝜑𝑖 ∈ ℕ0) → 𝑆 ∈ V)
37 elmapg 8429 . . . . . . 7 ((ℂ ∈ V ∧ 𝑆 ∈ V) → ((𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)) ∈ (ℂ ↑m 𝑆) ↔ (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)):𝑆⟶ℂ))
3833, 36, 37sylancr 590 . . . . . 6 ((𝜑𝑖 ∈ ℕ0) → ((𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)) ∈ (ℂ ↑m 𝑆) ↔ (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)):𝑆⟶ℂ))
3932, 38mpbird 260 . . . . 5 ((𝜑𝑖 ∈ ℕ0) → (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)) ∈ (ℂ ↑m 𝑆))
40 pserulm.h . . . . 5 𝐻 = (𝑖 ∈ ℕ0 ↦ (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)))
4139, 40fmptd 6869 . . . 4 (𝜑𝐻:ℕ0⟶(ℂ ↑m 𝑆))
42 eqidd 2759 . . . . . 6 (((𝜑𝑦𝑆) ∧ 𝑗 ∈ ℕ0) → ((𝐺𝑦)‘𝑗) = ((𝐺𝑦)‘𝑗))
43 pserf.r . . . . . . 7 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < )
441sselda 3892 . . . . . . . . . . . . 13 ((𝜑𝑦𝑆) → 𝑦 ∈ (abs “ (0[,]𝑀)))
45 ffn 6498 . . . . . . . . . . . . . 14 (abs:ℂ⟶ℝ → abs Fn ℂ)
46 elpreima 6819 . . . . . . . . . . . . . 14 (abs Fn ℂ → (𝑦 ∈ (abs “ (0[,]𝑀)) ↔ (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,]𝑀))))
4722, 45, 46mp2b 10 . . . . . . . . . . . . 13 (𝑦 ∈ (abs “ (0[,]𝑀)) ↔ (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,]𝑀)))
4844, 47sylib 221 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,]𝑀)))
4948simprd 499 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → (abs‘𝑦) ∈ (0[,]𝑀))
50 0re 10681 . . . . . . . . . . . 12 0 ∈ ℝ
514adantr 484 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 𝑀 ∈ ℝ)
52 elicc2 12844 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((abs‘𝑦) ∈ (0[,]𝑀) ↔ ((abs‘𝑦) ∈ ℝ ∧ 0 ≤ (abs‘𝑦) ∧ (abs‘𝑦) ≤ 𝑀)))
5350, 51, 52sylancr 590 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → ((abs‘𝑦) ∈ (0[,]𝑀) ↔ ((abs‘𝑦) ∈ ℝ ∧ 0 ≤ (abs‘𝑦) ∧ (abs‘𝑦) ≤ 𝑀)))
5449, 53mpbid 235 . . . . . . . . . 10 ((𝜑𝑦𝑆) → ((abs‘𝑦) ∈ ℝ ∧ 0 ≤ (abs‘𝑦) ∧ (abs‘𝑦) ≤ 𝑀))
5554simp1d 1139 . . . . . . . . 9 ((𝜑𝑦𝑆) → (abs‘𝑦) ∈ ℝ)
5655rexrd 10729 . . . . . . . 8 ((𝜑𝑦𝑆) → (abs‘𝑦) ∈ ℝ*)
575adantr 484 . . . . . . . 8 ((𝜑𝑦𝑆) → 𝑀 ∈ ℝ*)
58 iccssxr 12862 . . . . . . . . . 10 (0[,]+∞) ⊆ ℝ*
5918, 19, 43radcnvcl 25111 . . . . . . . . . 10 (𝜑𝑅 ∈ (0[,]+∞))
6058, 59sseldi 3890 . . . . . . . . 9 (𝜑𝑅 ∈ ℝ*)
6160adantr 484 . . . . . . . 8 ((𝜑𝑦𝑆) → 𝑅 ∈ ℝ*)
6254simp3d 1141 . . . . . . . 8 ((𝜑𝑦𝑆) → (abs‘𝑦) ≤ 𝑀)
63 pserulm.l . . . . . . . . 9 (𝜑𝑀 < 𝑅)
6463adantr 484 . . . . . . . 8 ((𝜑𝑦𝑆) → 𝑀 < 𝑅)
6556, 57, 61, 62, 64xrlelttrd 12594 . . . . . . 7 ((𝜑𝑦𝑆) → (abs‘𝑦) < 𝑅)
6618, 20, 43, 26, 65radcnvlt2 25113 . . . . . 6 ((𝜑𝑦𝑆) → seq0( + , (𝐺𝑦)) ∈ dom ⇝ )
6715, 17, 42, 28, 66isumcl 15164 . . . . 5 ((𝜑𝑦𝑆) → Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗) ∈ ℂ)
68 pserf.f . . . . 5 𝐹 = (𝑦𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗))
6967, 68fmptd 6869 . . . 4 (𝜑𝐹:𝑆⟶ℂ)
7015, 16, 41, 69ulm0 25085 . . 3 ((𝜑𝑆 = ∅) → 𝐻(⇝𝑢𝑆)𝐹)
7114, 70syldan 594 . 2 ((𝜑𝑀 < 0) → 𝐻(⇝𝑢𝑆)𝐹)
72 simpr 488 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
7372, 15eleqtrdi 2862 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ0) → 𝑖 ∈ (ℤ‘0))
74 eqid 2758 . . . . . . . . . 10 (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚))) = (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))
75 fveq2 6658 . . . . . . . . . . . . 13 (𝑤 = 𝑦 → (𝐺𝑤) = (𝐺𝑦))
7675fveq1d 6660 . . . . . . . . . . . 12 (𝑤 = 𝑦 → ((𝐺𝑤)‘𝑚) = ((𝐺𝑦)‘𝑚))
7776cbvmptv 5135 . . . . . . . . . . 11 (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)) = (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑚))
78 fveq2 6658 . . . . . . . . . . . 12 (𝑚 = 𝑘 → ((𝐺𝑦)‘𝑚) = ((𝐺𝑦)‘𝑘))
7978mpteq2dv 5128 . . . . . . . . . . 11 (𝑚 = 𝑘 → (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑚)) = (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘)))
8077, 79syl5eq 2805 . . . . . . . . . 10 (𝑚 = 𝑘 → (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)) = (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘)))
81 elfznn0 13049 . . . . . . . . . . 11 (𝑘 ∈ (0...𝑖) → 𝑘 ∈ ℕ0)
8281adantl 485 . . . . . . . . . 10 (((𝜑𝑖 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑖)) → 𝑘 ∈ ℕ0)
8335ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑖 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑖)) → 𝑆 ∈ V)
8483mptexd 6978 . . . . . . . . . 10 (((𝜑𝑖 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑖)) → (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘)) ∈ V)
8574, 80, 82, 84fvmptd3 6782 . . . . . . . . 9 (((𝜑𝑖 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑖)) → ((𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))‘𝑘) = (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘)))
8636, 73, 85seqof 13477 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ0) → (seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚))))‘𝑖) = (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)))
8786eqcomd 2764 . . . . . . 7 ((𝜑𝑖 ∈ ℕ0) → (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)) = (seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚))))‘𝑖))
8887mpteq2dva 5127 . . . . . 6 (𝜑 → (𝑖 ∈ ℕ0 ↦ (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖))) = (𝑖 ∈ ℕ0 ↦ (seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚))))‘𝑖)))
89 0z 12031 . . . . . . . . 9 0 ∈ ℤ
90 seqfn 13430 . . . . . . . . 9 (0 ∈ ℤ → seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) Fn (ℤ‘0))
9189, 90ax-mp 5 . . . . . . . 8 seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) Fn (ℤ‘0)
9215fneq2i 6432 . . . . . . . 8 (seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) Fn ℕ0 ↔ seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) Fn (ℤ‘0))
9391, 92mpbir 234 . . . . . . 7 seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) Fn ℕ0
94 dffn5 6712 . . . . . . 7 (seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) Fn ℕ0 ↔ seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) = (𝑖 ∈ ℕ0 ↦ (seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚))))‘𝑖)))
9593, 94mpbi 233 . . . . . 6 seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) = (𝑖 ∈ ℕ0 ↦ (seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚))))‘𝑖))
9688, 40, 953eqtr4g 2818 . . . . 5 (𝜑𝐻 = seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))))
9796adantr 484 . . . 4 ((𝜑 ∧ 0 ≤ 𝑀) → 𝐻 = seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))))
98 0zd 12032 . . . . 5 ((𝜑 ∧ 0 ≤ 𝑀) → 0 ∈ ℤ)
9935adantr 484 . . . . 5 ((𝜑 ∧ 0 ≤ 𝑀) → 𝑆 ∈ V)
10019adantr 484 . . . . . . . . . . . 12 ((𝜑𝑤𝑆) → 𝐴:ℕ0⟶ℂ)
10125sselda 3892 . . . . . . . . . . . 12 ((𝜑𝑤𝑆) → 𝑤 ∈ ℂ)
10218, 100, 101psergf 25106 . . . . . . . . . . 11 ((𝜑𝑤𝑆) → (𝐺𝑤):ℕ0⟶ℂ)
103102ffvelrnda 6842 . . . . . . . . . 10 (((𝜑𝑤𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝐺𝑤)‘𝑚) ∈ ℂ)
104103an32s 651 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑤𝑆) → ((𝐺𝑤)‘𝑚) ∈ ℂ)
105104fmpttd 6870 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ0) → (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)):𝑆⟶ℂ)
10635adantr 484 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ0) → 𝑆 ∈ V)
107 elmapg 8429 . . . . . . . . 9 ((ℂ ∈ V ∧ 𝑆 ∈ V) → ((𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)) ∈ (ℂ ↑m 𝑆) ↔ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)):𝑆⟶ℂ))
10833, 106, 107sylancr 590 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ0) → ((𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)) ∈ (ℂ ↑m 𝑆) ↔ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)):𝑆⟶ℂ))
109105, 108mpbird 260 . . . . . . 7 ((𝜑𝑚 ∈ ℕ0) → (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)) ∈ (ℂ ↑m 𝑆))
110109fmpttd 6870 . . . . . 6 (𝜑 → (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚))):ℕ0⟶(ℂ ↑m 𝑆))
111110adantr 484 . . . . 5 ((𝜑 ∧ 0 ≤ 𝑀) → (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚))):ℕ0⟶(ℂ ↑m 𝑆))
112 fex 6980 . . . . . . . 8 ((abs:ℂ⟶ℝ ∧ ℂ ∈ V) → abs ∈ V)
11322, 33, 112mp2an 691 . . . . . . 7 abs ∈ V
114 fvex 6671 . . . . . . 7 (𝐺𝑀) ∈ V
115113, 114coex 7640 . . . . . 6 (abs ∘ (𝐺𝑀)) ∈ V
116115a1i 11 . . . . 5 ((𝜑 ∧ 0 ≤ 𝑀) → (abs ∘ (𝐺𝑀)) ∈ V)
11719adantr 484 . . . . . . . 8 ((𝜑 ∧ 0 ≤ 𝑀) → 𝐴:ℕ0⟶ℂ)
1184adantr 484 . . . . . . . . 9 ((𝜑 ∧ 0 ≤ 𝑀) → 𝑀 ∈ ℝ)
119118recnd 10707 . . . . . . . 8 ((𝜑 ∧ 0 ≤ 𝑀) → 𝑀 ∈ ℂ)
12018, 117, 119psergf 25106 . . . . . . 7 ((𝜑 ∧ 0 ≤ 𝑀) → (𝐺𝑀):ℕ0⟶ℂ)
121 fco 6516 . . . . . . 7 ((abs:ℂ⟶ℝ ∧ (𝐺𝑀):ℕ0⟶ℂ) → (abs ∘ (𝐺𝑀)):ℕ0⟶ℝ)
12222, 120, 121sylancr 590 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝑀) → (abs ∘ (𝐺𝑀)):ℕ0⟶ℝ)
123122ffvelrnda 6842 . . . . 5 (((𝜑 ∧ 0 ≤ 𝑀) ∧ 𝑘 ∈ ℕ0) → ((abs ∘ (𝐺𝑀))‘𝑘) ∈ ℝ)
12425ad2antrr 725 . . . . . . . . . . 11 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 𝑆 ⊆ ℂ)
125 simprr 772 . . . . . . . . . . 11 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 𝑧𝑆)
126124, 125sseldd 3893 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 𝑧 ∈ ℂ)
127 simprl 770 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 𝑘 ∈ ℕ0)
128126, 127expcld 13560 . . . . . . . . 9 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (𝑧𝑘) ∈ ℂ)
129128abscld 14844 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(𝑧𝑘)) ∈ ℝ)
130119adantr 484 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 𝑀 ∈ ℂ)
131130, 127expcld 13560 . . . . . . . . 9 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (𝑀𝑘) ∈ ℂ)
132131abscld 14844 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(𝑀𝑘)) ∈ ℝ)
13319ad2antrr 725 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 𝐴:ℕ0⟶ℂ)
134133, 127ffvelrnd 6843 . . . . . . . . 9 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (𝐴𝑘) ∈ ℂ)
135134abscld 14844 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(𝐴𝑘)) ∈ ℝ)
136134absge0d 14852 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 0 ≤ (abs‘(𝐴𝑘)))
137126abscld 14844 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘𝑧) ∈ ℝ)
1384ad2antrr 725 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 𝑀 ∈ ℝ)
139126absge0d 14852 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 0 ≤ (abs‘𝑧))
140 fveq2 6658 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (abs‘𝑦) = (abs‘𝑧))
141140breq1d 5042 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((abs‘𝑦) ≤ 𝑀 ↔ (abs‘𝑧) ≤ 𝑀))
14262ralrimiva 3113 . . . . . . . . . . . 12 (𝜑 → ∀𝑦𝑆 (abs‘𝑦) ≤ 𝑀)
143142ad2antrr 725 . . . . . . . . . . 11 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ∀𝑦𝑆 (abs‘𝑦) ≤ 𝑀)
144141, 143, 125rspcdva 3543 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘𝑧) ≤ 𝑀)
145 leexp1a 13589 . . . . . . . . . 10 ((((abs‘𝑧) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (0 ≤ (abs‘𝑧) ∧ (abs‘𝑧) ≤ 𝑀)) → ((abs‘𝑧)↑𝑘) ≤ (𝑀𝑘))
146137, 138, 127, 139, 144, 145syl32anc 1375 . . . . . . . . 9 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((abs‘𝑧)↑𝑘) ≤ (𝑀𝑘))
147126, 127absexpd 14860 . . . . . . . . 9 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(𝑧𝑘)) = ((abs‘𝑧)↑𝑘))
148130, 127absexpd 14860 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(𝑀𝑘)) = ((abs‘𝑀)↑𝑘))
149 absid 14704 . . . . . . . . . . . . 13 ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → (abs‘𝑀) = 𝑀)
1504, 149sylan 583 . . . . . . . . . . . 12 ((𝜑 ∧ 0 ≤ 𝑀) → (abs‘𝑀) = 𝑀)
151150adantr 484 . . . . . . . . . . 11 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘𝑀) = 𝑀)
152151oveq1d 7165 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((abs‘𝑀)↑𝑘) = (𝑀𝑘))
153148, 152eqtrd 2793 . . . . . . . . 9 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(𝑀𝑘)) = (𝑀𝑘))
154146, 147, 1533brtr4d 5064 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(𝑧𝑘)) ≤ (abs‘(𝑀𝑘)))
155129, 132, 135, 136, 154lemul2ad 11618 . . . . . . 7 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((abs‘(𝐴𝑘)) · (abs‘(𝑧𝑘))) ≤ ((abs‘(𝐴𝑘)) · (abs‘(𝑀𝑘))))
156134, 128absmuld 14862 . . . . . . 7 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘((𝐴𝑘) · (𝑧𝑘))) = ((abs‘(𝐴𝑘)) · (abs‘(𝑧𝑘))))
157134, 131absmuld 14862 . . . . . . 7 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘((𝐴𝑘) · (𝑀𝑘))) = ((abs‘(𝐴𝑘)) · (abs‘(𝑀𝑘))))
158155, 156, 1573brtr4d 5064 . . . . . 6 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘((𝐴𝑘) · (𝑧𝑘))) ≤ (abs‘((𝐴𝑘) · (𝑀𝑘))))
15935ad2antrr 725 . . . . . . . . . . 11 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 𝑆 ∈ V)
160159mptexd 6978 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘)) ∈ V)
16174, 80, 127, 160fvmptd3 6782 . . . . . . . . 9 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))‘𝑘) = (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘)))
162161fveq1d 6660 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (((𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))‘𝑘)‘𝑧) = ((𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘))‘𝑧))
163 fveq2 6658 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝐺𝑦) = (𝐺𝑧))
164163fveq1d 6660 . . . . . . . . . 10 (𝑦 = 𝑧 → ((𝐺𝑦)‘𝑘) = ((𝐺𝑧)‘𝑘))
165 eqid 2758 . . . . . . . . . 10 (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘)) = (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘))
166 fvex 6671 . . . . . . . . . 10 ((𝐺𝑧)‘𝑘) ∈ V
167164, 165, 166fvmpt 6759 . . . . . . . . 9 (𝑧𝑆 → ((𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘))‘𝑧) = ((𝐺𝑧)‘𝑘))
168167ad2antll 728 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘))‘𝑧) = ((𝐺𝑧)‘𝑘))
16918pserval2 25105 . . . . . . . . 9 ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝐺𝑧)‘𝑘) = ((𝐴𝑘) · (𝑧𝑘)))
170126, 127, 169syl2anc 587 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((𝐺𝑧)‘𝑘) = ((𝐴𝑘) · (𝑧𝑘)))
171162, 168, 1703eqtrd 2797 . . . . . . 7 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (((𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))‘𝑘)‘𝑧) = ((𝐴𝑘) · (𝑧𝑘)))
172171fveq2d 6662 . . . . . 6 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(((𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))‘𝑘)‘𝑧)) = (abs‘((𝐴𝑘) · (𝑧𝑘))))
173120adantr 484 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (𝐺𝑀):ℕ0⟶ℂ)
174 fvco3 6751 . . . . . . . 8 (((𝐺𝑀):ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → ((abs ∘ (𝐺𝑀))‘𝑘) = (abs‘((𝐺𝑀)‘𝑘)))
175173, 127, 174syl2anc 587 . . . . . . 7 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((abs ∘ (𝐺𝑀))‘𝑘) = (abs‘((𝐺𝑀)‘𝑘)))
17618pserval2 25105 . . . . . . . . 9 ((𝑀 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝐺𝑀)‘𝑘) = ((𝐴𝑘) · (𝑀𝑘)))
177130, 127, 176syl2anc 587 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((𝐺𝑀)‘𝑘) = ((𝐴𝑘) · (𝑀𝑘)))
178177fveq2d 6662 . . . . . . 7 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘((𝐺𝑀)‘𝑘)) = (abs‘((𝐴𝑘) · (𝑀𝑘))))
179175, 178eqtrd 2793 . . . . . 6 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((abs ∘ (𝐺𝑀))‘𝑘) = (abs‘((𝐴𝑘) · (𝑀𝑘))))
180158, 172, 1793brtr4d 5064 . . . . 5 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(((𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))‘𝑘)‘𝑧)) ≤ ((abs ∘ (𝐺𝑀))‘𝑘))
18163adantr 484 . . . . . . . 8 ((𝜑 ∧ 0 ≤ 𝑀) → 𝑀 < 𝑅)
182150, 181eqbrtrd 5054 . . . . . . 7 ((𝜑 ∧ 0 ≤ 𝑀) → (abs‘𝑀) < 𝑅)
183 id 22 . . . . . . . . 9 (𝑖 = 𝑚𝑖 = 𝑚)
184 2fveq3 6663 . . . . . . . . 9 (𝑖 = 𝑚 → (abs‘((𝐺𝑀)‘𝑖)) = (abs‘((𝐺𝑀)‘𝑚)))
185183, 184oveq12d 7168 . . . . . . . 8 (𝑖 = 𝑚 → (𝑖 · (abs‘((𝐺𝑀)‘𝑖))) = (𝑚 · (abs‘((𝐺𝑀)‘𝑚))))
186185cbvmptv 5135 . . . . . . 7 (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺𝑀)‘𝑖)))) = (𝑚 ∈ ℕ0 ↦ (𝑚 · (abs‘((𝐺𝑀)‘𝑚))))
18718, 117, 43, 119, 182, 186radcnvlt1 25112 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝑀) → (seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺𝑀)‘𝑖))))) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (𝐺𝑀))) ∈ dom ⇝ ))
188187simprd 499 . . . . 5 ((𝜑 ∧ 0 ≤ 𝑀) → seq0( + , (abs ∘ (𝐺𝑀))) ∈ dom ⇝ )
18915, 98, 99, 111, 116, 123, 180, 188mtest 25098 . . . 4 ((𝜑 ∧ 0 ≤ 𝑀) → seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) ∈ dom (⇝𝑢𝑆))
19097, 189eqeltrd 2852 . . 3 ((𝜑 ∧ 0 ≤ 𝑀) → 𝐻 ∈ dom (⇝𝑢𝑆))
191 simpr 488 . . . . . . 7 ((𝜑𝐻(⇝𝑢𝑆)𝑓) → 𝐻(⇝𝑢𝑆)𝑓)
192 ulmcl 25075 . . . . . . . . . 10 (𝐻(⇝𝑢𝑆)𝑓𝑓:𝑆⟶ℂ)
193192adantl 485 . . . . . . . . 9 ((𝜑𝐻(⇝𝑢𝑆)𝑓) → 𝑓:𝑆⟶ℂ)
194193feqmptd 6721 . . . . . . . 8 ((𝜑𝐻(⇝𝑢𝑆)𝑓) → 𝑓 = (𝑦𝑆 ↦ (𝑓𝑦)))
195 0zd 12032 . . . . . . . . . . 11 (((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) → 0 ∈ ℤ)
196 eqidd 2759 . . . . . . . . . . 11 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑗 ∈ ℕ0) → ((𝐺𝑦)‘𝑗) = ((𝐺𝑦)‘𝑗))
19727adantlr 714 . . . . . . . . . . . 12 (((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) → (𝐺𝑦):ℕ0⟶ℂ)
198197ffvelrnda 6842 . . . . . . . . . . 11 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑗 ∈ ℕ0) → ((𝐺𝑦)‘𝑗) ∈ ℂ)
19941ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) → 𝐻:ℕ0⟶(ℂ ↑m 𝑆))
200 simpr 488 . . . . . . . . . . . 12 (((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) → 𝑦𝑆)
201 seqex 13420 . . . . . . . . . . . . 13 seq0( + , (𝐺𝑦)) ∈ V
202201a1i 11 . . . . . . . . . . . 12 (((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) → seq0( + , (𝐺𝑦)) ∈ V)
203 simpr 488 . . . . . . . . . . . . . . 15 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
20435ad3antrrr 729 . . . . . . . . . . . . . . . 16 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → 𝑆 ∈ V)
205204mptexd 6978 . . . . . . . . . . . . . . 15 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)) ∈ V)
20640fvmpt2 6770 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ℕ0 ∧ (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)) ∈ V) → (𝐻𝑖) = (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)))
207203, 205, 206syl2anc 587 . . . . . . . . . . . . . 14 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (𝐻𝑖) = (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)))
208207fveq1d 6660 . . . . . . . . . . . . 13 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝐻𝑖)‘𝑦) = ((𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖))‘𝑦))
209 simplr 768 . . . . . . . . . . . . . 14 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → 𝑦𝑆)
210 fvex 6671 . . . . . . . . . . . . . 14 (seq0( + , (𝐺𝑦))‘𝑖) ∈ V
211 eqid 2758 . . . . . . . . . . . . . . 15 (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)) = (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖))
212211fvmpt2 6770 . . . . . . . . . . . . . 14 ((𝑦𝑆 ∧ (seq0( + , (𝐺𝑦))‘𝑖) ∈ V) → ((𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖))‘𝑦) = (seq0( + , (𝐺𝑦))‘𝑖))
213209, 210, 212sylancl 589 . . . . . . . . . . . . 13 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖))‘𝑦) = (seq0( + , (𝐺𝑦))‘𝑖))
214208, 213eqtrd 2793 . . . . . . . . . . . 12 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝐻𝑖)‘𝑦) = (seq0( + , (𝐺𝑦))‘𝑖))
215 simplr 768 . . . . . . . . . . . 12 (((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) → 𝐻(⇝𝑢𝑆)𝑓)
21615, 195, 199, 200, 202, 214, 215ulmclm 25081 . . . . . . . . . . 11 (((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) → seq0( + , (𝐺𝑦)) ⇝ (𝑓𝑦))
21715, 195, 196, 198, 216isumclim 15160 . . . . . . . . . 10 (((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) → Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗) = (𝑓𝑦))
218217mpteq2dva 5127 . . . . . . . . 9 ((𝜑𝐻(⇝𝑢𝑆)𝑓) → (𝑦𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗)) = (𝑦𝑆 ↦ (𝑓𝑦)))
21968, 218syl5eq 2805 . . . . . . . 8 ((𝜑𝐻(⇝𝑢𝑆)𝑓) → 𝐹 = (𝑦𝑆 ↦ (𝑓𝑦)))
220194, 219eqtr4d 2796 . . . . . . 7 ((𝜑𝐻(⇝𝑢𝑆)𝑓) → 𝑓 = 𝐹)
221191, 220breqtrd 5058 . . . . . 6 ((𝜑𝐻(⇝𝑢𝑆)𝑓) → 𝐻(⇝𝑢𝑆)𝐹)
222221ex 416 . . . . 5 (𝜑 → (𝐻(⇝𝑢𝑆)𝑓𝐻(⇝𝑢𝑆)𝐹))
223222exlimdv 1934 . . . 4 (𝜑 → (∃𝑓 𝐻(⇝𝑢𝑆)𝑓𝐻(⇝𝑢𝑆)𝐹))
224 eldmg 5738 . . . . 5 (𝐻 ∈ dom (⇝𝑢𝑆) → (𝐻 ∈ dom (⇝𝑢𝑆) ↔ ∃𝑓 𝐻(⇝𝑢𝑆)𝑓))
225224ibi 270 . . . 4 (𝐻 ∈ dom (⇝𝑢𝑆) → ∃𝑓 𝐻(⇝𝑢𝑆)𝑓)
226223, 225impel 509 . . 3 ((𝜑𝐻 ∈ dom (⇝𝑢𝑆)) → 𝐻(⇝𝑢𝑆)𝐹)
227190, 226syldan 594 . 2 ((𝜑 ∧ 0 ≤ 𝑀) → 𝐻(⇝𝑢𝑆)𝐹)
228 0red 10682 . 2 (𝜑 → 0 ∈ ℝ)
22971, 227, 4, 228ltlecasei 10786 1 (𝜑𝐻(⇝𝑢𝑆)𝐹)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∀wral 3070  {crab 3074  Vcvv 3409   ⊆ wss 3858  ∅c0 4225   class class class wbr 5032   ↦ cmpt 5112  ◡ccnv 5523  dom cdm 5524   “ cima 5527   ∘ ccom 5528   Fn wfn 6330  ⟶wf 6331  ‘cfv 6335  (class class class)co 7150   ∘f cof 7403   ↑m cmap 8416  supcsup 8937  ℂcc 10573  ℝcr 10574  0cc0 10575   + caddc 10578   · cmul 10580  +∞cpnf 10710  ℝ*cxr 10712   < clt 10713   ≤ cle 10714  ℕ0cn0 11934  ℤcz 12020  ℤ≥cuz 12282  [,]cicc 12782  ...cfz 12939  seqcseq 13418  ↑cexp 13479  abscabs 14641   ⇝ cli 14889  Σcsu 15090  ⇝𝑢culm 25070 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-inf2 9137  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652  ax-pre-sup 10653  ax-addf 10654  ax-mulf 10655 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-int 4839  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-se 5484  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-isom 6344  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7405  df-om 7580  df-1st 7693  df-2nd 7694  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-er 8299  df-map 8418  df-pm 8419  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-sup 8939  df-inf 8940  df-oi 9007  df-card 9401  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-div 11336  df-nn 11675  df-2 11737  df-3 11738  df-n0 11935  df-z 12021  df-uz 12283  df-rp 12431  df-ico 12785  df-icc 12786  df-fz 12940  df-fzo 13083  df-fl 13211  df-seq 13419  df-exp 13480  df-hash 13741  df-cj 14506  df-re 14507  df-im 14508  df-sqrt 14642  df-abs 14643  df-limsup 14876  df-clim 14893  df-rlim 14894  df-sum 15091  df-ulm 25071 This theorem is referenced by:  psercn2  25117  pserdvlem2  25122
 Copyright terms: Public domain W3C validator