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

Theorem pserulm 24927
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 481 . . . . 5 ((𝜑𝑀 < 0) → 𝑆 ⊆ (abs “ (0[,]𝑀)))
3 0xr 10680 . . . . . . . . 9 0 ∈ ℝ*
4 pserulm.m . . . . . . . . . 10 (𝜑𝑀 ∈ ℝ)
54rexrd 10683 . . . . . . . . 9 (𝜑𝑀 ∈ ℝ*)
6 icc0 12779 . . . . . . . . 9 ((0 ∈ ℝ*𝑀 ∈ ℝ*) → ((0[,]𝑀) = ∅ ↔ 𝑀 < 0))
73, 5, 6sylancr 587 . . . . . . . 8 (𝜑 → ((0[,]𝑀) = ∅ ↔ 𝑀 < 0))
87biimpar 478 . . . . . . 7 ((𝜑𝑀 < 0) → (0[,]𝑀) = ∅)
98imaeq2d 5926 . . . . . 6 ((𝜑𝑀 < 0) → (abs “ (0[,]𝑀)) = (abs “ ∅))
10 ima0 5942 . . . . . 6 (abs “ ∅) = ∅
119, 10syl6eq 2876 . . . . 5 ((𝜑𝑀 < 0) → (abs “ (0[,]𝑀)) = ∅)
122, 11sseqtrd 4010 . . . 4 ((𝜑𝑀 < 0) → 𝑆 ⊆ ∅)
13 ss0 4355 . . . 4 (𝑆 ⊆ ∅ → 𝑆 = ∅)
1412, 13syl 17 . . 3 ((𝜑𝑀 < 0) → 𝑆 = ∅)
15 nn0uz 12272 . . . 4 0 = (ℤ‘0)
16 0zd 11985 . . . 4 (𝜑 → 0 ∈ ℤ)
17 0zd 11985 . . . . . . . . . 10 ((𝜑𝑦𝑆) → 0 ∈ ℤ)
18 pserf.g . . . . . . . . . . . 12 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
19 pserf.a . . . . . . . . . . . . 13 (𝜑𝐴:ℕ0⟶ℂ)
2019adantr 481 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 𝐴:ℕ0⟶ℂ)
21 cnvimass 5946 . . . . . . . . . . . . . . 15 (abs “ (0[,]𝑀)) ⊆ dom abs
22 absf 14690 . . . . . . . . . . . . . . . 16 abs:ℂ⟶ℝ
2322fdmi 6520 . . . . . . . . . . . . . . 15 dom abs = ℂ
2421, 23sseqtri 4006 . . . . . . . . . . . . . 14 (abs “ (0[,]𝑀)) ⊆ ℂ
251, 24syl6ss 3982 . . . . . . . . . . . . 13 (𝜑𝑆 ⊆ ℂ)
2625sselda 3970 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 𝑦 ∈ ℂ)
2718, 20, 26psergf 24917 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → (𝐺𝑦):ℕ0⟶ℂ)
2827ffvelrnda 6846 . . . . . . . . . 10 (((𝜑𝑦𝑆) ∧ 𝑗 ∈ ℕ0) → ((𝐺𝑦)‘𝑗) ∈ ℂ)
2915, 17, 28serf 13391 . . . . . . . . 9 ((𝜑𝑦𝑆) → seq0( + , (𝐺𝑦)):ℕ0⟶ℂ)
3029ffvelrnda 6846 . . . . . . . 8 (((𝜑𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (seq0( + , (𝐺𝑦))‘𝑖) ∈ ℂ)
3130an32s 648 . . . . . . 7 (((𝜑𝑖 ∈ ℕ0) ∧ 𝑦𝑆) → (seq0( + , (𝐺𝑦))‘𝑖) ∈ ℂ)
3231fmpttd 6874 . . . . . 6 ((𝜑𝑖 ∈ ℕ0) → (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)):𝑆⟶ℂ)
33 cnex 10610 . . . . . . 7 ℂ ∈ V
34 ssexg 5223 . . . . . . . . 9 ((𝑆 ⊆ ℂ ∧ ℂ ∈ V) → 𝑆 ∈ V)
3525, 33, 34sylancl 586 . . . . . . . 8 (𝜑𝑆 ∈ V)
3635adantr 481 . . . . . . 7 ((𝜑𝑖 ∈ ℕ0) → 𝑆 ∈ V)
37 elmapg 8412 . . . . . . 7 ((ℂ ∈ V ∧ 𝑆 ∈ V) → ((𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)) ∈ (ℂ ↑m 𝑆) ↔ (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)):𝑆⟶ℂ))
3833, 36, 37sylancr 587 . . . . . 6 ((𝜑𝑖 ∈ ℕ0) → ((𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)) ∈ (ℂ ↑m 𝑆) ↔ (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)):𝑆⟶ℂ))
3932, 38mpbird 258 . . . . 5 ((𝜑𝑖 ∈ ℕ0) → (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)) ∈ (ℂ ↑m 𝑆))
40 pserulm.h . . . . 5 𝐻 = (𝑖 ∈ ℕ0 ↦ (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)))
4139, 40fmptd 6873 . . . 4 (𝜑𝐻:ℕ0⟶(ℂ ↑m 𝑆))
42 eqidd 2826 . . . . . 6 (((𝜑𝑦𝑆) ∧ 𝑗 ∈ ℕ0) → ((𝐺𝑦)‘𝑗) = ((𝐺𝑦)‘𝑗))
43 pserf.r . . . . . . 7 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < )
441sselda 3970 . . . . . . . . . . . . 13 ((𝜑𝑦𝑆) → 𝑦 ∈ (abs “ (0[,]𝑀)))
45 ffn 6510 . . . . . . . . . . . . . 14 (abs:ℂ⟶ℝ → abs Fn ℂ)
46 elpreima 6823 . . . . . . . . . . . . . 14 (abs Fn ℂ → (𝑦 ∈ (abs “ (0[,]𝑀)) ↔ (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,]𝑀))))
4722, 45, 46mp2b 10 . . . . . . . . . . . . 13 (𝑦 ∈ (abs “ (0[,]𝑀)) ↔ (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,]𝑀)))
4844, 47sylib 219 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,]𝑀)))
4948simprd 496 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → (abs‘𝑦) ∈ (0[,]𝑀))
50 0re 10635 . . . . . . . . . . . 12 0 ∈ ℝ
514adantr 481 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 𝑀 ∈ ℝ)
52 elicc2 12794 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((abs‘𝑦) ∈ (0[,]𝑀) ↔ ((abs‘𝑦) ∈ ℝ ∧ 0 ≤ (abs‘𝑦) ∧ (abs‘𝑦) ≤ 𝑀)))
5350, 51, 52sylancr 587 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → ((abs‘𝑦) ∈ (0[,]𝑀) ↔ ((abs‘𝑦) ∈ ℝ ∧ 0 ≤ (abs‘𝑦) ∧ (abs‘𝑦) ≤ 𝑀)))
5449, 53mpbid 233 . . . . . . . . . 10 ((𝜑𝑦𝑆) → ((abs‘𝑦) ∈ ℝ ∧ 0 ≤ (abs‘𝑦) ∧ (abs‘𝑦) ≤ 𝑀))
5554simp1d 1136 . . . . . . . . 9 ((𝜑𝑦𝑆) → (abs‘𝑦) ∈ ℝ)
5655rexrd 10683 . . . . . . . 8 ((𝜑𝑦𝑆) → (abs‘𝑦) ∈ ℝ*)
575adantr 481 . . . . . . . 8 ((𝜑𝑦𝑆) → 𝑀 ∈ ℝ*)
58 iccssxr 12812 . . . . . . . . . 10 (0[,]+∞) ⊆ ℝ*
5918, 19, 43radcnvcl 24922 . . . . . . . . . 10 (𝜑𝑅 ∈ (0[,]+∞))
6058, 59sseldi 3968 . . . . . . . . 9 (𝜑𝑅 ∈ ℝ*)
6160adantr 481 . . . . . . . 8 ((𝜑𝑦𝑆) → 𝑅 ∈ ℝ*)
6254simp3d 1138 . . . . . . . 8 ((𝜑𝑦𝑆) → (abs‘𝑦) ≤ 𝑀)
63 pserulm.l . . . . . . . . 9 (𝜑𝑀 < 𝑅)
6463adantr 481 . . . . . . . 8 ((𝜑𝑦𝑆) → 𝑀 < 𝑅)
6556, 57, 61, 62, 64xrlelttrd 12546 . . . . . . 7 ((𝜑𝑦𝑆) → (abs‘𝑦) < 𝑅)
6618, 20, 43, 26, 65radcnvlt2 24924 . . . . . 6 ((𝜑𝑦𝑆) → seq0( + , (𝐺𝑦)) ∈ dom ⇝ )
6715, 17, 42, 28, 66isumcl 15108 . . . . 5 ((𝜑𝑦𝑆) → Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗) ∈ ℂ)
68 pserf.f . . . . 5 𝐹 = (𝑦𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗))
6967, 68fmptd 6873 . . . 4 (𝜑𝐹:𝑆⟶ℂ)
7015, 16, 41, 69ulm0 24896 . . 3 ((𝜑𝑆 = ∅) → 𝐻(⇝𝑢𝑆)𝐹)
7114, 70syldan 591 . 2 ((𝜑𝑀 < 0) → 𝐻(⇝𝑢𝑆)𝐹)
72 simpr 485 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
7372, 15syl6eleq 2927 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ0) → 𝑖 ∈ (ℤ‘0))
74 eqid 2825 . . . . . . . . . 10 (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚))) = (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))
75 fveq2 6666 . . . . . . . . . . . . 13 (𝑤 = 𝑦 → (𝐺𝑤) = (𝐺𝑦))
7675fveq1d 6668 . . . . . . . . . . . 12 (𝑤 = 𝑦 → ((𝐺𝑤)‘𝑚) = ((𝐺𝑦)‘𝑚))
7776cbvmptv 5165 . . . . . . . . . . 11 (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)) = (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑚))
78 fveq2 6666 . . . . . . . . . . . 12 (𝑚 = 𝑘 → ((𝐺𝑦)‘𝑚) = ((𝐺𝑦)‘𝑘))
7978mpteq2dv 5158 . . . . . . . . . . 11 (𝑚 = 𝑘 → (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑚)) = (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘)))
8077, 79syl5eq 2872 . . . . . . . . . 10 (𝑚 = 𝑘 → (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)) = (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘)))
81 elfznn0 12993 . . . . . . . . . . 11 (𝑘 ∈ (0...𝑖) → 𝑘 ∈ ℕ0)
8281adantl 482 . . . . . . . . . 10 (((𝜑𝑖 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑖)) → 𝑘 ∈ ℕ0)
8335ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑖 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑖)) → 𝑆 ∈ V)
8483mptexd 6985 . . . . . . . . . 10 (((𝜑𝑖 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑖)) → (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘)) ∈ V)
8574, 80, 82, 84fvmptd3 6786 . . . . . . . . 9 (((𝜑𝑖 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑖)) → ((𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))‘𝑘) = (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘)))
8636, 73, 85seqof 13420 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ0) → (seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚))))‘𝑖) = (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)))
8786eqcomd 2831 . . . . . . 7 ((𝜑𝑖 ∈ ℕ0) → (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)) = (seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚))))‘𝑖))
8887mpteq2dva 5157 . . . . . 6 (𝜑 → (𝑖 ∈ ℕ0 ↦ (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖))) = (𝑖 ∈ ℕ0 ↦ (seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚))))‘𝑖)))
89 0z 11984 . . . . . . . . 9 0 ∈ ℤ
90 seqfn 13374 . . . . . . . . 9 (0 ∈ ℤ → seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) Fn (ℤ‘0))
9189, 90ax-mp 5 . . . . . . . 8 seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) Fn (ℤ‘0)
9215fneq2i 6447 . . . . . . . 8 (seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) Fn ℕ0 ↔ seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) Fn (ℤ‘0))
9391, 92mpbir 232 . . . . . . 7 seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) Fn ℕ0
94 dffn5 6720 . . . . . . 7 (seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) Fn ℕ0 ↔ seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) = (𝑖 ∈ ℕ0 ↦ (seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚))))‘𝑖)))
9593, 94mpbi 231 . . . . . 6 seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) = (𝑖 ∈ ℕ0 ↦ (seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚))))‘𝑖))
9688, 40, 953eqtr4g 2885 . . . . 5 (𝜑𝐻 = seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))))
9796adantr 481 . . . 4 ((𝜑 ∧ 0 ≤ 𝑀) → 𝐻 = seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))))
98 0zd 11985 . . . . 5 ((𝜑 ∧ 0 ≤ 𝑀) → 0 ∈ ℤ)
9935adantr 481 . . . . 5 ((𝜑 ∧ 0 ≤ 𝑀) → 𝑆 ∈ V)
10019adantr 481 . . . . . . . . . . . 12 ((𝜑𝑤𝑆) → 𝐴:ℕ0⟶ℂ)
10125sselda 3970 . . . . . . . . . . . 12 ((𝜑𝑤𝑆) → 𝑤 ∈ ℂ)
10218, 100, 101psergf 24917 . . . . . . . . . . 11 ((𝜑𝑤𝑆) → (𝐺𝑤):ℕ0⟶ℂ)
103102ffvelrnda 6846 . . . . . . . . . 10 (((𝜑𝑤𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝐺𝑤)‘𝑚) ∈ ℂ)
104103an32s 648 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑤𝑆) → ((𝐺𝑤)‘𝑚) ∈ ℂ)
105104fmpttd 6874 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ0) → (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)):𝑆⟶ℂ)
10635adantr 481 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ0) → 𝑆 ∈ V)
107 elmapg 8412 . . . . . . . . 9 ((ℂ ∈ V ∧ 𝑆 ∈ V) → ((𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)) ∈ (ℂ ↑m 𝑆) ↔ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)):𝑆⟶ℂ))
10833, 106, 107sylancr 587 . . . . . . . 8 ((𝜑𝑚 ∈ ℕ0) → ((𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)) ∈ (ℂ ↑m 𝑆) ↔ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)):𝑆⟶ℂ))
109105, 108mpbird 258 . . . . . . 7 ((𝜑𝑚 ∈ ℕ0) → (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)) ∈ (ℂ ↑m 𝑆))
110109fmpttd 6874 . . . . . 6 (𝜑 → (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚))):ℕ0⟶(ℂ ↑m 𝑆))
111110adantr 481 . . . . 5 ((𝜑 ∧ 0 ≤ 𝑀) → (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚))):ℕ0⟶(ℂ ↑m 𝑆))
112 fex 6987 . . . . . . . 8 ((abs:ℂ⟶ℝ ∧ ℂ ∈ V) → abs ∈ V)
11322, 33, 112mp2an 688 . . . . . . 7 abs ∈ V
114 fvex 6679 . . . . . . 7 (𝐺𝑀) ∈ V
115113, 114coex 7626 . . . . . 6 (abs ∘ (𝐺𝑀)) ∈ V
116115a1i 11 . . . . 5 ((𝜑 ∧ 0 ≤ 𝑀) → (abs ∘ (𝐺𝑀)) ∈ V)
11719adantr 481 . . . . . . . 8 ((𝜑 ∧ 0 ≤ 𝑀) → 𝐴:ℕ0⟶ℂ)
1184adantr 481 . . . . . . . . 9 ((𝜑 ∧ 0 ≤ 𝑀) → 𝑀 ∈ ℝ)
119118recnd 10661 . . . . . . . 8 ((𝜑 ∧ 0 ≤ 𝑀) → 𝑀 ∈ ℂ)
12018, 117, 119psergf 24917 . . . . . . 7 ((𝜑 ∧ 0 ≤ 𝑀) → (𝐺𝑀):ℕ0⟶ℂ)
121 fco 6527 . . . . . . 7 ((abs:ℂ⟶ℝ ∧ (𝐺𝑀):ℕ0⟶ℂ) → (abs ∘ (𝐺𝑀)):ℕ0⟶ℝ)
12222, 120, 121sylancr 587 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝑀) → (abs ∘ (𝐺𝑀)):ℕ0⟶ℝ)
123122ffvelrnda 6846 . . . . 5 (((𝜑 ∧ 0 ≤ 𝑀) ∧ 𝑘 ∈ ℕ0) → ((abs ∘ (𝐺𝑀))‘𝑘) ∈ ℝ)
12425ad2antrr 722 . . . . . . . . . . 11 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 𝑆 ⊆ ℂ)
125 simprr 769 . . . . . . . . . . 11 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 𝑧𝑆)
126124, 125sseldd 3971 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 𝑧 ∈ ℂ)
127 simprl 767 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 𝑘 ∈ ℕ0)
128126, 127expcld 13503 . . . . . . . . 9 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (𝑧𝑘) ∈ ℂ)
129128abscld 14789 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(𝑧𝑘)) ∈ ℝ)
130119adantr 481 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 𝑀 ∈ ℂ)
131130, 127expcld 13503 . . . . . . . . 9 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (𝑀𝑘) ∈ ℂ)
132131abscld 14789 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(𝑀𝑘)) ∈ ℝ)
13319ad2antrr 722 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 𝐴:ℕ0⟶ℂ)
134133, 127ffvelrnd 6847 . . . . . . . . 9 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (𝐴𝑘) ∈ ℂ)
135134abscld 14789 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(𝐴𝑘)) ∈ ℝ)
136134absge0d 14797 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 0 ≤ (abs‘(𝐴𝑘)))
137126abscld 14789 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘𝑧) ∈ ℝ)
1384ad2antrr 722 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 𝑀 ∈ ℝ)
139126absge0d 14797 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 0 ≤ (abs‘𝑧))
140 fveq2 6666 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (abs‘𝑦) = (abs‘𝑧))
141140breq1d 5072 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((abs‘𝑦) ≤ 𝑀 ↔ (abs‘𝑧) ≤ 𝑀))
14262ralrimiva 3186 . . . . . . . . . . . 12 (𝜑 → ∀𝑦𝑆 (abs‘𝑦) ≤ 𝑀)
143142ad2antrr 722 . . . . . . . . . . 11 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ∀𝑦𝑆 (abs‘𝑦) ≤ 𝑀)
144141, 143, 125rspcdva 3628 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘𝑧) ≤ 𝑀)
145 leexp1a 13532 . . . . . . . . . 10 ((((abs‘𝑧) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℕ0) ∧ (0 ≤ (abs‘𝑧) ∧ (abs‘𝑧) ≤ 𝑀)) → ((abs‘𝑧)↑𝑘) ≤ (𝑀𝑘))
146137, 138, 127, 139, 144, 145syl32anc 1372 . . . . . . . . 9 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((abs‘𝑧)↑𝑘) ≤ (𝑀𝑘))
147126, 127absexpd 14805 . . . . . . . . 9 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(𝑧𝑘)) = ((abs‘𝑧)↑𝑘))
148130, 127absexpd 14805 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(𝑀𝑘)) = ((abs‘𝑀)↑𝑘))
149 absid 14649 . . . . . . . . . . . . 13 ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → (abs‘𝑀) = 𝑀)
1504, 149sylan 580 . . . . . . . . . . . 12 ((𝜑 ∧ 0 ≤ 𝑀) → (abs‘𝑀) = 𝑀)
151150adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘𝑀) = 𝑀)
152151oveq1d 7166 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((abs‘𝑀)↑𝑘) = (𝑀𝑘))
153148, 152eqtrd 2860 . . . . . . . . 9 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(𝑀𝑘)) = (𝑀𝑘))
154146, 147, 1533brtr4d 5094 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(𝑧𝑘)) ≤ (abs‘(𝑀𝑘)))
155129, 132, 135, 136, 154lemul2ad 11572 . . . . . . 7 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((abs‘(𝐴𝑘)) · (abs‘(𝑧𝑘))) ≤ ((abs‘(𝐴𝑘)) · (abs‘(𝑀𝑘))))
156134, 128absmuld 14807 . . . . . . 7 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘((𝐴𝑘) · (𝑧𝑘))) = ((abs‘(𝐴𝑘)) · (abs‘(𝑧𝑘))))
157134, 131absmuld 14807 . . . . . . 7 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘((𝐴𝑘) · (𝑀𝑘))) = ((abs‘(𝐴𝑘)) · (abs‘(𝑀𝑘))))
158155, 156, 1573brtr4d 5094 . . . . . 6 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘((𝐴𝑘) · (𝑧𝑘))) ≤ (abs‘((𝐴𝑘) · (𝑀𝑘))))
15935ad2antrr 722 . . . . . . . . . . 11 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → 𝑆 ∈ V)
160159mptexd 6985 . . . . . . . . . 10 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘)) ∈ V)
16174, 80, 127, 160fvmptd3 6786 . . . . . . . . 9 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))‘𝑘) = (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘)))
162161fveq1d 6668 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (((𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))‘𝑘)‘𝑧) = ((𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘))‘𝑧))
163 fveq2 6666 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝐺𝑦) = (𝐺𝑧))
164163fveq1d 6668 . . . . . . . . . 10 (𝑦 = 𝑧 → ((𝐺𝑦)‘𝑘) = ((𝐺𝑧)‘𝑘))
165 eqid 2825 . . . . . . . . . 10 (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘)) = (𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘))
166 fvex 6679 . . . . . . . . . 10 ((𝐺𝑧)‘𝑘) ∈ V
167164, 165, 166fvmpt 6764 . . . . . . . . 9 (𝑧𝑆 → ((𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘))‘𝑧) = ((𝐺𝑧)‘𝑘))
168167ad2antll 725 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((𝑦𝑆 ↦ ((𝐺𝑦)‘𝑘))‘𝑧) = ((𝐺𝑧)‘𝑘))
16918pserval2 24916 . . . . . . . . 9 ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝐺𝑧)‘𝑘) = ((𝐴𝑘) · (𝑧𝑘)))
170126, 127, 169syl2anc 584 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((𝐺𝑧)‘𝑘) = ((𝐴𝑘) · (𝑧𝑘)))
171162, 168, 1703eqtrd 2864 . . . . . . 7 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (((𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))‘𝑘)‘𝑧) = ((𝐴𝑘) · (𝑧𝑘)))
172171fveq2d 6670 . . . . . 6 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(((𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))‘𝑘)‘𝑧)) = (abs‘((𝐴𝑘) · (𝑧𝑘))))
173120adantr 481 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (𝐺𝑀):ℕ0⟶ℂ)
174 fvco3 6756 . . . . . . . 8 (((𝐺𝑀):ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → ((abs ∘ (𝐺𝑀))‘𝑘) = (abs‘((𝐺𝑀)‘𝑘)))
175173, 127, 174syl2anc 584 . . . . . . 7 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((abs ∘ (𝐺𝑀))‘𝑘) = (abs‘((𝐺𝑀)‘𝑘)))
17618pserval2 24916 . . . . . . . . 9 ((𝑀 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝐺𝑀)‘𝑘) = ((𝐴𝑘) · (𝑀𝑘)))
177130, 127, 176syl2anc 584 . . . . . . . 8 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((𝐺𝑀)‘𝑘) = ((𝐴𝑘) · (𝑀𝑘)))
178177fveq2d 6670 . . . . . . 7 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘((𝐺𝑀)‘𝑘)) = (abs‘((𝐴𝑘) · (𝑀𝑘))))
179175, 178eqtrd 2860 . . . . . 6 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → ((abs ∘ (𝐺𝑀))‘𝑘) = (abs‘((𝐴𝑘) · (𝑀𝑘))))
180158, 172, 1793brtr4d 5094 . . . . 5 (((𝜑 ∧ 0 ≤ 𝑀) ∧ (𝑘 ∈ ℕ0𝑧𝑆)) → (abs‘(((𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))‘𝑘)‘𝑧)) ≤ ((abs ∘ (𝐺𝑀))‘𝑘))
18163adantr 481 . . . . . . . 8 ((𝜑 ∧ 0 ≤ 𝑀) → 𝑀 < 𝑅)
182150, 181eqbrtrd 5084 . . . . . . 7 ((𝜑 ∧ 0 ≤ 𝑀) → (abs‘𝑀) < 𝑅)
183 id 22 . . . . . . . . 9 (𝑖 = 𝑚𝑖 = 𝑚)
184 2fveq3 6671 . . . . . . . . 9 (𝑖 = 𝑚 → (abs‘((𝐺𝑀)‘𝑖)) = (abs‘((𝐺𝑀)‘𝑚)))
185183, 184oveq12d 7169 . . . . . . . 8 (𝑖 = 𝑚 → (𝑖 · (abs‘((𝐺𝑀)‘𝑖))) = (𝑚 · (abs‘((𝐺𝑀)‘𝑚))))
186185cbvmptv 5165 . . . . . . 7 (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺𝑀)‘𝑖)))) = (𝑚 ∈ ℕ0 ↦ (𝑚 · (abs‘((𝐺𝑀)‘𝑚))))
18718, 117, 43, 119, 182, 186radcnvlt1 24923 . . . . . 6 ((𝜑 ∧ 0 ≤ 𝑀) → (seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺𝑀)‘𝑖))))) ∈ dom ⇝ ∧ seq0( + , (abs ∘ (𝐺𝑀))) ∈ dom ⇝ ))
188187simprd 496 . . . . 5 ((𝜑 ∧ 0 ≤ 𝑀) → seq0( + , (abs ∘ (𝐺𝑀))) ∈ dom ⇝ )
18915, 98, 99, 111, 116, 123, 180, 188mtest 24909 . . . 4 ((𝜑 ∧ 0 ≤ 𝑀) → seq0( ∘f + , (𝑚 ∈ ℕ0 ↦ (𝑤𝑆 ↦ ((𝐺𝑤)‘𝑚)))) ∈ dom (⇝𝑢𝑆))
19097, 189eqeltrd 2917 . . 3 ((𝜑 ∧ 0 ≤ 𝑀) → 𝐻 ∈ dom (⇝𝑢𝑆))
191 simpr 485 . . . . . . 7 ((𝜑𝐻(⇝𝑢𝑆)𝑓) → 𝐻(⇝𝑢𝑆)𝑓)
192 ulmcl 24886 . . . . . . . . . 10 (𝐻(⇝𝑢𝑆)𝑓𝑓:𝑆⟶ℂ)
193192adantl 482 . . . . . . . . 9 ((𝜑𝐻(⇝𝑢𝑆)𝑓) → 𝑓:𝑆⟶ℂ)
194193feqmptd 6729 . . . . . . . 8 ((𝜑𝐻(⇝𝑢𝑆)𝑓) → 𝑓 = (𝑦𝑆 ↦ (𝑓𝑦)))
195 0zd 11985 . . . . . . . . . . 11 (((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) → 0 ∈ ℤ)
196 eqidd 2826 . . . . . . . . . . 11 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑗 ∈ ℕ0) → ((𝐺𝑦)‘𝑗) = ((𝐺𝑦)‘𝑗))
19727adantlr 711 . . . . . . . . . . . 12 (((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) → (𝐺𝑦):ℕ0⟶ℂ)
198197ffvelrnda 6846 . . . . . . . . . . 11 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑗 ∈ ℕ0) → ((𝐺𝑦)‘𝑗) ∈ ℂ)
19941ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) → 𝐻:ℕ0⟶(ℂ ↑m 𝑆))
200 simpr 485 . . . . . . . . . . . 12 (((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) → 𝑦𝑆)
201 seqex 13364 . . . . . . . . . . . . 13 seq0( + , (𝐺𝑦)) ∈ V
202201a1i 11 . . . . . . . . . . . 12 (((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) → seq0( + , (𝐺𝑦)) ∈ V)
203 simpr 485 . . . . . . . . . . . . . . 15 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
20435ad3antrrr 726 . . . . . . . . . . . . . . . 16 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → 𝑆 ∈ V)
205204mptexd 6985 . . . . . . . . . . . . . . 15 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)) ∈ V)
20640fvmpt2 6774 . . . . . . . . . . . . . . 15 ((𝑖 ∈ ℕ0 ∧ (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)) ∈ V) → (𝐻𝑖) = (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)))
207203, 205, 206syl2anc 584 . . . . . . . . . . . . . 14 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → (𝐻𝑖) = (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)))
208207fveq1d 6668 . . . . . . . . . . . . 13 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝐻𝑖)‘𝑦) = ((𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖))‘𝑦))
209 simplr 765 . . . . . . . . . . . . . 14 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → 𝑦𝑆)
210 fvex 6679 . . . . . . . . . . . . . 14 (seq0( + , (𝐺𝑦))‘𝑖) ∈ V
211 eqid 2825 . . . . . . . . . . . . . . 15 (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖)) = (𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖))
212211fvmpt2 6774 . . . . . . . . . . . . . 14 ((𝑦𝑆 ∧ (seq0( + , (𝐺𝑦))‘𝑖) ∈ V) → ((𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖))‘𝑦) = (seq0( + , (𝐺𝑦))‘𝑖))
213209, 210, 212sylancl 586 . . . . . . . . . . . . 13 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝑦𝑆 ↦ (seq0( + , (𝐺𝑦))‘𝑖))‘𝑦) = (seq0( + , (𝐺𝑦))‘𝑖))
214208, 213eqtrd 2860 . . . . . . . . . . . 12 ((((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) ∧ 𝑖 ∈ ℕ0) → ((𝐻𝑖)‘𝑦) = (seq0( + , (𝐺𝑦))‘𝑖))
215 simplr 765 . . . . . . . . . . . 12 (((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) → 𝐻(⇝𝑢𝑆)𝑓)
21615, 195, 199, 200, 202, 214, 215ulmclm 24892 . . . . . . . . . . 11 (((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) → seq0( + , (𝐺𝑦)) ⇝ (𝑓𝑦))
21715, 195, 196, 198, 216isumclim 15104 . . . . . . . . . 10 (((𝜑𝐻(⇝𝑢𝑆)𝑓) ∧ 𝑦𝑆) → Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗) = (𝑓𝑦))
218217mpteq2dva 5157 . . . . . . . . 9 ((𝜑𝐻(⇝𝑢𝑆)𝑓) → (𝑦𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗)) = (𝑦𝑆 ↦ (𝑓𝑦)))
21968, 218syl5eq 2872 . . . . . . . 8 ((𝜑𝐻(⇝𝑢𝑆)𝑓) → 𝐹 = (𝑦𝑆 ↦ (𝑓𝑦)))
220194, 219eqtr4d 2863 . . . . . . 7 ((𝜑𝐻(⇝𝑢𝑆)𝑓) → 𝑓 = 𝐹)
221191, 220breqtrd 5088 . . . . . 6 ((𝜑𝐻(⇝𝑢𝑆)𝑓) → 𝐻(⇝𝑢𝑆)𝐹)
222221ex 413 . . . . 5 (𝜑 → (𝐻(⇝𝑢𝑆)𝑓𝐻(⇝𝑢𝑆)𝐹))
223222exlimdv 1927 . . . 4 (𝜑 → (∃𝑓 𝐻(⇝𝑢𝑆)𝑓𝐻(⇝𝑢𝑆)𝐹))
224 eldmg 5765 . . . . 5 (𝐻 ∈ dom (⇝𝑢𝑆) → (𝐻 ∈ dom (⇝𝑢𝑆) ↔ ∃𝑓 𝐻(⇝𝑢𝑆)𝑓))
225224ibi 268 . . . 4 (𝐻 ∈ dom (⇝𝑢𝑆) → ∃𝑓 𝐻(⇝𝑢𝑆)𝑓)
226223, 225impel 506 . . 3 ((𝜑𝐻 ∈ dom (⇝𝑢𝑆)) → 𝐻(⇝𝑢𝑆)𝐹)
227190, 226syldan 591 . 2 ((𝜑 ∧ 0 ≤ 𝑀) → 𝐻(⇝𝑢𝑆)𝐹)
228 0red 10636 . 2 (𝜑 → 0 ∈ ℝ)
22971, 227, 4, 228ltlecasei 10740 1 (𝜑𝐻(⇝𝑢𝑆)𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wex 1773  wcel 2107  wral 3142  {crab 3146  Vcvv 3499  wss 3939  c0 4294   class class class wbr 5062  cmpt 5142  ccnv 5552  dom cdm 5553  cima 5556  ccom 5557   Fn wfn 6346  wf 6347  cfv 6351  (class class class)co 7151  f cof 7400  m cmap 8399  supcsup 8896  cc 10527  cr 10528  0cc0 10529   + caddc 10532   · cmul 10534  +∞cpnf 10664  *cxr 10666   < clt 10667  cle 10668  0cn0 11889  cz 11973  cuz 12235  [,]cicc 12734  ...cfz 12885  seqcseq 13362  cexp 13422  abscabs 14586  cli 14834  Σcsu 15035  𝑢culm 24881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-inf2 9096  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-se 5513  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-isom 6360  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7402  df-om 7572  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8282  df-map 8401  df-pm 8402  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-sup 8898  df-inf 8899  df-oi 8966  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-n0 11890  df-z 11974  df-uz 12236  df-rp 12383  df-ico 12737  df-icc 12738  df-fz 12886  df-fzo 13027  df-fl 13155  df-seq 13363  df-exp 13423  df-hash 13684  df-cj 14451  df-re 14452  df-im 14453  df-sqrt 14587  df-abs 14588  df-limsup 14821  df-clim 14838  df-rlim 14839  df-sum 15036  df-ulm 24882
This theorem is referenced by:  psercn2  24928  pserdvlem2  24933
  Copyright terms: Public domain W3C validator