Metamath Proof Explorer

Theorem pserdvlem2

Description: Lemma for pserdv . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses pserf.g ⊒ 𝐺 = ( π‘₯ ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) )
pserf.f ⊒ 𝐹 = ( 𝑦 ∈ 𝑆 ↦ Ξ£ 𝑗 ∈ β„•0 ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑗 ) )
pserf.a ⊒ ( πœ‘ β†’ 𝐴 : β„•0 ⟢ β„‚ )
pserf.r ⊒ 𝑅 = sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝐺 β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < )
psercn.s ⊒ 𝑆 = ( β—‘ abs β€œ ( 0 [,) 𝑅 ) )
psercn.m ⊒ 𝑀 = if ( 𝑅 ∈ ℝ , ( ( ( abs β€˜ π‘Ž ) + 𝑅 ) / 2 ) , ( ( abs β€˜ π‘Ž ) + 1 ) )
pserdv.b ⊒ 𝐡 = ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) )
Assertion pserdvlem2 ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( β„‚ D ( 𝐹 β†Ύ 𝐡 ) ) = ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) )

Proof

Step Hyp Ref Expression
1 pserf.g ⊒ 𝐺 = ( π‘₯ ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) )
2 pserf.f ⊒ 𝐹 = ( 𝑦 ∈ 𝑆 ↦ Ξ£ 𝑗 ∈ β„•0 ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑗 ) )
3 pserf.a ⊒ ( πœ‘ β†’ 𝐴 : β„•0 ⟢ β„‚ )
4 pserf.r ⊒ 𝑅 = sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝐺 β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < )
5 psercn.s ⊒ 𝑆 = ( β—‘ abs β€œ ( 0 [,) 𝑅 ) )
6 psercn.m ⊒ 𝑀 = if ( 𝑅 ∈ ℝ , ( ( ( abs β€˜ π‘Ž ) + 𝑅 ) / 2 ) , ( ( abs β€˜ π‘Ž ) + 1 ) )
7 pserdv.b ⊒ 𝐡 = ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) )
8 nn0uz ⊒ β„•0 = ( β„€β‰₯ β€˜ 0 )
9 cnelprrecn ⊒ β„‚ ∈ { ℝ , β„‚ }
10 9 a1i ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ β„‚ ∈ { ℝ , β„‚ } )
11 0zd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 0 ∈ β„€ )
12 fzfid ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘˜ ∈ β„•0 ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( 0 ... π‘˜ ) ∈ Fin )
13 3 ad3antrrr ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘˜ ∈ β„•0 ) ∧ 𝑦 ∈ 𝐡 ) β†’ 𝐴 : β„•0 ⟢ β„‚ )
14 cnxmet ⊒ ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ )
15 0cnd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 0 ∈ β„‚ )
16 1 2 3 4 5 6 pserdvlem1 ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ∈ ℝ+ ∧ ( abs β€˜ π‘Ž ) < ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ∧ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) < 𝑅 ) )
17 16 simp1d ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ∈ ℝ+ )
18 17 rpxrd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ∈ ℝ* )
19 blssm ⊒ ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ 0 ∈ β„‚ ∧ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ∈ ℝ* ) β†’ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) βŠ† β„‚ )
20 14 15 18 19 mp3an2i ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) βŠ† β„‚ )
21 7 20 eqsstrid ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝐡 βŠ† β„‚ )
22 21 adantr ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘˜ ∈ β„•0 ) β†’ 𝐡 βŠ† β„‚ )
23 22 sselda ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘˜ ∈ β„•0 ) ∧ 𝑦 ∈ 𝐡 ) β†’ 𝑦 ∈ β„‚ )
24 1 13 23 psergf ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘˜ ∈ β„•0 ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( 𝐺 β€˜ 𝑦 ) : β„•0 ⟢ β„‚ )
25 elfznn0 ⊒ ( 𝑖 ∈ ( 0 ... π‘˜ ) β†’ 𝑖 ∈ β„•0 )
26 ffvelcdm ⊒ ( ( ( 𝐺 β€˜ 𝑦 ) : β„•0 ⟢ β„‚ ∧ 𝑖 ∈ β„•0 ) β†’ ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ∈ β„‚ )
27 24 25 26 syl2an ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘˜ ∈ β„•0 ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ ( 0 ... π‘˜ ) ) β†’ ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ∈ β„‚ )
28 12 27 fsumcl ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘˜ ∈ β„•0 ) ∧ 𝑦 ∈ 𝐡 ) β†’ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ∈ β„‚ )
29 28 fmpttd ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘˜ ∈ β„•0 ) β†’ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) : 𝐡 ⟢ β„‚ )
30 cnex ⊒ β„‚ ∈ V
31 7 ovexi ⊒ 𝐡 ∈ V
32 30 31 elmap ⊒ ( ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ∈ ( β„‚ ↑m 𝐡 ) ↔ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) : 𝐡 ⟢ β„‚ )
33 29 32 sylibr ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘˜ ∈ β„•0 ) β†’ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ∈ ( β„‚ ↑m 𝐡 ) )
34 33 fmpttd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( π‘˜ ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) : β„•0 ⟢ ( β„‚ ↑m 𝐡 ) )
35 1 2 3 4 5 6 psercn ⊒ ( πœ‘ β†’ 𝐹 ∈ ( 𝑆 –cnβ†’ β„‚ ) )
36 cncff ⊒ ( 𝐹 ∈ ( 𝑆 –cnβ†’ β„‚ ) β†’ 𝐹 : 𝑆 ⟢ β„‚ )
37 35 36 syl ⊒ ( πœ‘ β†’ 𝐹 : 𝑆 ⟢ β„‚ )
38 37 adantr ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝐹 : 𝑆 ⟢ β„‚ )
39 1 2 3 4 5 16 psercnlem2 ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( π‘Ž ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) ∧ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) βŠ† ( β—‘ abs β€œ ( 0 [,] ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) ) ∧ ( β—‘ abs β€œ ( 0 [,] ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) ) βŠ† 𝑆 ) )
40 39 simp2d ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) βŠ† ( β—‘ abs β€œ ( 0 [,] ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) ) )
41 7 40 eqsstrid ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝐡 βŠ† ( β—‘ abs β€œ ( 0 [,] ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) ) )
42 39 simp3d ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( β—‘ abs β€œ ( 0 [,] ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) ) βŠ† 𝑆 )
43 41 42 sstrd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝐡 βŠ† 𝑆 )
44 38 43 fssresd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( 𝐹 β†Ύ 𝐡 ) : 𝐡 ⟢ β„‚ )
45 0zd ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ 0 ∈ β„€ )
46 eqidd ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) ∧ 𝑗 ∈ β„•0 ) β†’ ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑗 ) = ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑗 ) )
47 3 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ 𝐴 : β„•0 ⟢ β„‚ )
48 21 sselda ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ 𝑧 ∈ β„‚ )
49 1 47 48 psergf ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( 𝐺 β€˜ 𝑧 ) : β„•0 ⟢ β„‚ )
50 49 ffvelcdmda ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) ∧ 𝑗 ∈ β„•0 ) β†’ ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑗 ) ∈ β„‚ )
51 48 abscld ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( abs β€˜ 𝑧 ) ∈ ℝ )
52 51 rexrd ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( abs β€˜ 𝑧 ) ∈ ℝ* )
53 18 adantr ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ∈ ℝ* )
54 iccssxr ⊒ ( 0 [,] +∞ ) βŠ† ℝ*
55 1 3 4 radcnvcl ⊒ ( πœ‘ β†’ 𝑅 ∈ ( 0 [,] +∞ ) )
56 54 55 sselid ⊒ ( πœ‘ β†’ 𝑅 ∈ ℝ* )
57 56 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ 𝑅 ∈ ℝ* )
58 0cn ⊒ 0 ∈ β„‚
59 eqid ⊒ ( abs ∘ βˆ’ ) = ( abs ∘ βˆ’ )
60 59 cnmetdval ⊒ ( ( 𝑧 ∈ β„‚ ∧ 0 ∈ β„‚ ) β†’ ( 𝑧 ( abs ∘ βˆ’ ) 0 ) = ( abs β€˜ ( 𝑧 βˆ’ 0 ) ) )
61 48 58 60 sylancl ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( 𝑧 ( abs ∘ βˆ’ ) 0 ) = ( abs β€˜ ( 𝑧 βˆ’ 0 ) ) )
62 48 subid1d ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( 𝑧 βˆ’ 0 ) = 𝑧 )
63 62 fveq2d ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( abs β€˜ ( 𝑧 βˆ’ 0 ) ) = ( abs β€˜ 𝑧 ) )
64 61 63 eqtrd ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( 𝑧 ( abs ∘ βˆ’ ) 0 ) = ( abs β€˜ 𝑧 ) )
65 simpr ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ 𝑧 ∈ 𝐡 )
66 65 7 eleqtrdi ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ 𝑧 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) )
67 14 a1i ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) )
68 0cnd ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ 0 ∈ β„‚ )
69 elbl3 ⊒ ( ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ∈ ℝ* ) ∧ ( 0 ∈ β„‚ ∧ 𝑧 ∈ β„‚ ) ) β†’ ( 𝑧 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) ↔ ( 𝑧 ( abs ∘ βˆ’ ) 0 ) < ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) )
70 67 53 68 48 69 syl22anc ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( 𝑧 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) ↔ ( 𝑧 ( abs ∘ βˆ’ ) 0 ) < ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) )
71 66 70 mpbid ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( 𝑧 ( abs ∘ βˆ’ ) 0 ) < ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) )
72 64 71 eqbrtrrd ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( abs β€˜ 𝑧 ) < ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) )
73 16 simp3d ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) < 𝑅 )
74 73 adantr ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) < 𝑅 )
75 52 53 57 72 74 xrlttrd ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( abs β€˜ 𝑧 ) < 𝑅 )
76 1 47 4 48 75 radcnvlt2 ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ seq 0 ( + , ( 𝐺 β€˜ 𝑧 ) ) ∈ dom ⇝ )
77 8 45 46 50 76 isumclim2 ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ seq 0 ( + , ( 𝐺 β€˜ 𝑧 ) ) ⇝ Ξ£ 𝑗 ∈ β„•0 ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑗 ) )
78 43 sselda ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ 𝑧 ∈ 𝑆 )
79 fveq2 ⊒ ( 𝑦 = 𝑧 β†’ ( 𝐺 β€˜ 𝑦 ) = ( 𝐺 β€˜ 𝑧 ) )
80 79 fveq1d ⊒ ( 𝑦 = 𝑧 β†’ ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑗 ) = ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑗 ) )
81 80 sumeq2sdv ⊒ ( 𝑦 = 𝑧 β†’ Ξ£ 𝑗 ∈ β„•0 ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑗 ) = Ξ£ 𝑗 ∈ β„•0 ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑗 ) )
82 sumex ⊒ Ξ£ 𝑗 ∈ β„•0 ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑗 ) ∈ V
83 81 2 82 fvmpt ⊒ ( 𝑧 ∈ 𝑆 β†’ ( 𝐹 β€˜ 𝑧 ) = Ξ£ 𝑗 ∈ β„•0 ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑗 ) )
84 78 83 syl ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( 𝐹 β€˜ 𝑧 ) = Ξ£ 𝑗 ∈ β„•0 ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑗 ) )
85 77 84 breqtrrd ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ seq 0 ( + , ( 𝐺 β€˜ 𝑧 ) ) ⇝ ( 𝐹 β€˜ 𝑧 ) )
86 oveq2 ⊒ ( π‘˜ = π‘š β†’ ( 0 ... π‘˜ ) = ( 0 ... π‘š ) )
87 86 sumeq1d ⊒ ( π‘˜ = π‘š β†’ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) = Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) )
88 87 mpteq2dv ⊒ ( π‘˜ = π‘š β†’ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) = ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) )
89 eqid ⊒ ( π‘˜ ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) = ( π‘˜ ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) )
90 31 mptex ⊒ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ∈ V
91 88 89 90 fvmpt ⊒ ( π‘š ∈ β„•0 β†’ ( ( π‘˜ ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) β€˜ π‘š ) = ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) )
92 91 adantl ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) ∧ π‘š ∈ β„•0 ) β†’ ( ( π‘˜ ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) β€˜ π‘š ) = ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) )
93 92 fveq1d ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) ∧ π‘š ∈ β„•0 ) β†’ ( ( ( π‘˜ ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) β€˜ π‘š ) β€˜ 𝑧 ) = ( ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) β€˜ 𝑧 ) )
94 79 fveq1d ⊒ ( 𝑦 = 𝑧 β†’ ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) = ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑖 ) )
95 94 sumeq2sdv ⊒ ( 𝑦 = 𝑧 β†’ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) = Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑖 ) )
96 eqid ⊒ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) = ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) )
97 sumex ⊒ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑖 ) ∈ V
98 95 96 97 fvmpt ⊒ ( 𝑧 ∈ 𝐡 β†’ ( ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) β€˜ 𝑧 ) = Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑖 ) )
99 98 ad2antlr ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) ∧ π‘š ∈ β„•0 ) β†’ ( ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) β€˜ 𝑧 ) = Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑖 ) )
100 eqidd ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) β†’ ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑖 ) = ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑖 ) )
101 simpr ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) ∧ π‘š ∈ β„•0 ) β†’ π‘š ∈ β„•0 )
102 101 8 eleqtrdi ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) ∧ π‘š ∈ β„•0 ) β†’ π‘š ∈ ( β„€β‰₯ β€˜ 0 ) )
103 49 adantr ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) ∧ π‘š ∈ β„•0 ) β†’ ( 𝐺 β€˜ 𝑧 ) : β„•0 ⟢ β„‚ )
104 elfznn0 ⊒ ( 𝑖 ∈ ( 0 ... π‘š ) β†’ 𝑖 ∈ β„•0 )
105 ffvelcdm ⊒ ( ( ( 𝐺 β€˜ 𝑧 ) : β„•0 ⟢ β„‚ ∧ 𝑖 ∈ β„•0 ) β†’ ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑖 ) ∈ β„‚ )
106 103 104 105 syl2an ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) β†’ ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑖 ) ∈ β„‚ )
107 100 102 106 fsumser ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) ∧ π‘š ∈ β„•0 ) β†’ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑧 ) β€˜ 𝑖 ) = ( seq 0 ( + , ( 𝐺 β€˜ 𝑧 ) ) β€˜ π‘š ) )
108 93 99 107 3eqtrd ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) ∧ π‘š ∈ β„•0 ) β†’ ( ( ( π‘˜ ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) β€˜ π‘š ) β€˜ 𝑧 ) = ( seq 0 ( + , ( 𝐺 β€˜ 𝑧 ) ) β€˜ π‘š ) )
109 108 mpteq2dva ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( π‘š ∈ β„•0 ↦ ( ( ( π‘˜ ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) β€˜ π‘š ) β€˜ 𝑧 ) ) = ( π‘š ∈ β„•0 ↦ ( seq 0 ( + , ( 𝐺 β€˜ 𝑧 ) ) β€˜ π‘š ) ) )
110 0z ⊒ 0 ∈ β„€
111 seqfn ⊒ ( 0 ∈ β„€ β†’ seq 0 ( + , ( 𝐺 β€˜ 𝑧 ) ) Fn ( β„€β‰₯ β€˜ 0 ) )
112 110 111 ax-mp ⊒ seq 0 ( + , ( 𝐺 β€˜ 𝑧 ) ) Fn ( β„€β‰₯ β€˜ 0 )
113 8 fneq2i ⊒ ( seq 0 ( + , ( 𝐺 β€˜ 𝑧 ) ) Fn β„•0 ↔ seq 0 ( + , ( 𝐺 β€˜ 𝑧 ) ) Fn ( β„€β‰₯ β€˜ 0 ) )
114 112 113 mpbir ⊒ seq 0 ( + , ( 𝐺 β€˜ 𝑧 ) ) Fn β„•0
115 dffn5 ⊒ ( seq 0 ( + , ( 𝐺 β€˜ 𝑧 ) ) Fn β„•0 ↔ seq 0 ( + , ( 𝐺 β€˜ 𝑧 ) ) = ( π‘š ∈ β„•0 ↦ ( seq 0 ( + , ( 𝐺 β€˜ 𝑧 ) ) β€˜ π‘š ) ) )
116 114 115 mpbi ⊒ seq 0 ( + , ( 𝐺 β€˜ 𝑧 ) ) = ( π‘š ∈ β„•0 ↦ ( seq 0 ( + , ( 𝐺 β€˜ 𝑧 ) ) β€˜ π‘š ) )
117 109 116 eqtr4di ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( π‘š ∈ β„•0 ↦ ( ( ( π‘˜ ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) β€˜ π‘š ) β€˜ 𝑧 ) ) = seq 0 ( + , ( 𝐺 β€˜ 𝑧 ) ) )
118 fvres ⊒ ( 𝑧 ∈ 𝐡 β†’ ( ( 𝐹 β†Ύ 𝐡 ) β€˜ 𝑧 ) = ( 𝐹 β€˜ 𝑧 ) )
119 118 adantl ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( ( 𝐹 β†Ύ 𝐡 ) β€˜ 𝑧 ) = ( 𝐹 β€˜ 𝑧 ) )
120 85 117 119 3brtr4d ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑧 ∈ 𝐡 ) β†’ ( π‘š ∈ β„•0 ↦ ( ( ( π‘˜ ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) β€˜ π‘š ) β€˜ 𝑧 ) ) ⇝ ( ( 𝐹 β†Ύ 𝐡 ) β€˜ 𝑧 ) )
121 91 adantl ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) β†’ ( ( π‘˜ ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) β€˜ π‘š ) = ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) )
122 121 oveq2d ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) β†’ ( β„‚ D ( ( π‘˜ ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) β€˜ π‘š ) ) = ( β„‚ D ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) )
123 eqid ⊒ ( TopOpen β€˜ β„‚fld ) = ( TopOpen β€˜ β„‚fld )
124 123 cnfldtopon ⊒ ( TopOpen β€˜ β„‚fld ) ∈ ( TopOn β€˜ β„‚ )
125 124 toponrestid ⊒ ( TopOpen β€˜ β„‚fld ) = ( ( TopOpen β€˜ β„‚fld ) β†Ύt β„‚ )
126 9 a1i ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) β†’ β„‚ ∈ { ℝ , β„‚ } )
127 123 cnfldtopn ⊒ ( TopOpen β€˜ β„‚fld ) = ( MetOpen β€˜ ( abs ∘ βˆ’ ) )
128 127 blopn ⊒ ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ 0 ∈ β„‚ ∧ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ∈ ℝ* ) β†’ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) ∈ ( TopOpen β€˜ β„‚fld ) )
129 14 15 18 128 mp3an2i ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ) ∈ ( TopOpen β€˜ β„‚fld ) )
130 7 129 eqeltrid ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝐡 ∈ ( TopOpen β€˜ β„‚fld ) )
131 130 adantr ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) β†’ 𝐡 ∈ ( TopOpen β€˜ β„‚fld ) )
132 fzfid ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) β†’ ( 0 ... π‘š ) ∈ Fin )
133 3 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) β†’ 𝐴 : β„•0 ⟢ β„‚ )
134 133 3ad2ant1 ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ∧ 𝑦 ∈ 𝐡 ) β†’ 𝐴 : β„•0 ⟢ β„‚ )
135 21 adantr ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) β†’ 𝐡 βŠ† β„‚ )
136 135 sselda ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑦 ∈ 𝐡 ) β†’ 𝑦 ∈ β„‚ )
137 136 3adant2 ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ∧ 𝑦 ∈ 𝐡 ) β†’ 𝑦 ∈ β„‚ )
138 1 134 137 psergf ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( 𝐺 β€˜ 𝑦 ) : β„•0 ⟢ β„‚ )
139 104 3ad2ant2 ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ∧ 𝑦 ∈ 𝐡 ) β†’ 𝑖 ∈ β„•0 )
140 138 139 ffvelcdmd ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ∈ β„‚ )
141 9 a1i ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) β†’ β„‚ ∈ { ℝ , β„‚ } )
142 ffvelcdm ⊒ ( ( 𝐴 : β„•0 ⟢ β„‚ ∧ 𝑖 ∈ β„•0 ) β†’ ( 𝐴 β€˜ 𝑖 ) ∈ β„‚ )
143 133 104 142 syl2an ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) β†’ ( 𝐴 β€˜ 𝑖 ) ∈ β„‚ )
144 143 adantr ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( 𝐴 β€˜ 𝑖 ) ∈ β„‚ )
145 136 adantlr ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) ∧ 𝑦 ∈ 𝐡 ) β†’ 𝑦 ∈ β„‚ )
146 id ⊒ ( 𝑦 ∈ β„‚ β†’ 𝑦 ∈ β„‚ )
147 104 adantl ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) β†’ 𝑖 ∈ β„•0 )
148 expcl ⊒ ( ( 𝑦 ∈ β„‚ ∧ 𝑖 ∈ β„•0 ) β†’ ( 𝑦 ↑ 𝑖 ) ∈ β„‚ )
149 146 147 148 syl2anr ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) ∧ 𝑦 ∈ β„‚ ) β†’ ( 𝑦 ↑ 𝑖 ) ∈ β„‚ )
150 145 149 syldan ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( 𝑦 ↑ 𝑖 ) ∈ β„‚ )
151 144 150 mulcld ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( ( 𝐴 β€˜ 𝑖 ) Β· ( 𝑦 ↑ 𝑖 ) ) ∈ β„‚ )
152 ovexd ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ∈ V )
153 c0ex ⊒ 0 ∈ V
154 ovex ⊒ ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ∈ V
155 153 154 ifex ⊒ if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ∈ V
156 155 a1i ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) ∧ 𝑦 ∈ 𝐡 ) β†’ if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ∈ V )
157 155 a1i ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) ∧ 𝑦 ∈ β„‚ ) β†’ if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ∈ V )
158 dvexp2 ⊒ ( 𝑖 ∈ β„•0 β†’ ( β„‚ D ( 𝑦 ∈ β„‚ ↦ ( 𝑦 ↑ 𝑖 ) ) ) = ( 𝑦 ∈ β„‚ ↦ if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) )
159 147 158 syl ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) β†’ ( β„‚ D ( 𝑦 ∈ β„‚ ↦ ( 𝑦 ↑ 𝑖 ) ) ) = ( 𝑦 ∈ β„‚ ↦ if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) )
160 21 ad2antrr ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) β†’ 𝐡 βŠ† β„‚ )
161 130 ad2antrr ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) β†’ 𝐡 ∈ ( TopOpen β€˜ β„‚fld ) )
162 141 149 157 159 160 125 123 161 dvmptres ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) β†’ ( β„‚ D ( 𝑦 ∈ 𝐡 ↦ ( 𝑦 ↑ 𝑖 ) ) ) = ( 𝑦 ∈ 𝐡 ↦ if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) )
163 141 150 156 162 143 dvmptcmul ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) β†’ ( β„‚ D ( 𝑦 ∈ 𝐡 ↦ ( ( 𝐴 β€˜ 𝑖 ) Β· ( 𝑦 ↑ 𝑖 ) ) ) ) = ( 𝑦 ∈ 𝐡 ↦ ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) )
164 141 151 152 163 dvmptcl ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ∈ β„‚ )
165 164 3impa ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ∈ β„‚ )
166 104 ad2antlr ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) ∧ 𝑦 ∈ 𝐡 ) β†’ 𝑖 ∈ β„•0 )
167 1 pserval2 ⊒ ( ( 𝑦 ∈ β„‚ ∧ 𝑖 ∈ β„•0 ) β†’ ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) = ( ( 𝐴 β€˜ 𝑖 ) Β· ( 𝑦 ↑ 𝑖 ) ) )
168 145 166 167 syl2anc ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) = ( ( 𝐴 β€˜ 𝑖 ) Β· ( 𝑦 ↑ 𝑖 ) ) )
169 168 mpteq2dva ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) β†’ ( 𝑦 ∈ 𝐡 ↦ ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) = ( 𝑦 ∈ 𝐡 ↦ ( ( 𝐴 β€˜ 𝑖 ) Β· ( 𝑦 ↑ 𝑖 ) ) ) )
170 169 oveq2d ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) β†’ ( β„‚ D ( 𝑦 ∈ 𝐡 ↦ ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) = ( β„‚ D ( 𝑦 ∈ 𝐡 ↦ ( ( 𝐴 β€˜ 𝑖 ) Β· ( 𝑦 ↑ 𝑖 ) ) ) ) )
171 170 163 eqtrd ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) β†’ ( β„‚ D ( 𝑦 ∈ 𝐡 ↦ ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) = ( 𝑦 ∈ 𝐡 ↦ ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) )
172 125 123 126 131 132 140 165 171 dvmptfsum ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) β†’ ( β„‚ D ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) = ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) )
173 122 172 eqtrd ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) β†’ ( β„‚ D ( ( π‘˜ ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) β€˜ π‘š ) ) = ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) )
174 173 mpteq2dva ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( π‘š ∈ β„•0 ↦ ( β„‚ D ( ( π‘˜ ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) β€˜ π‘š ) ) ) = ( π‘š ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) ) )
175 nnssnn0 ⊒ β„• βŠ† β„•0
176 resmpt ⊒ ( β„• βŠ† β„•0 β†’ ( ( π‘š ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) ) β†Ύ β„• ) = ( π‘š ∈ β„• ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) ) )
177 175 176 ax-mp ⊒ ( ( π‘š ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) ) β†Ύ β„• ) = ( π‘š ∈ β„• ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) )
178 oveq1 ⊒ ( π‘Ž = π‘₯ β†’ ( π‘Ž ↑ 𝑖 ) = ( π‘₯ ↑ 𝑖 ) )
179 178 oveq2d ⊒ ( π‘Ž = π‘₯ β†’ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) = ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘₯ ↑ 𝑖 ) ) )
180 179 mpteq2dv ⊒ ( π‘Ž = π‘₯ β†’ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) = ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘₯ ↑ 𝑖 ) ) ) )
181 oveq1 ⊒ ( 𝑖 = 𝑛 β†’ ( 𝑖 + 1 ) = ( 𝑛 + 1 ) )
182 fvoveq1 ⊒ ( 𝑖 = 𝑛 β†’ ( 𝐴 β€˜ ( 𝑖 + 1 ) ) = ( 𝐴 β€˜ ( 𝑛 + 1 ) ) )
183 181 182 oveq12d ⊒ ( 𝑖 = 𝑛 β†’ ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) = ( ( 𝑛 + 1 ) Β· ( 𝐴 β€˜ ( 𝑛 + 1 ) ) ) )
184 oveq2 ⊒ ( 𝑖 = 𝑛 β†’ ( π‘₯ ↑ 𝑖 ) = ( π‘₯ ↑ 𝑛 ) )
185 183 184 oveq12d ⊒ ( 𝑖 = 𝑛 β†’ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘₯ ↑ 𝑖 ) ) = ( ( ( 𝑛 + 1 ) Β· ( 𝐴 β€˜ ( 𝑛 + 1 ) ) ) Β· ( π‘₯ ↑ 𝑛 ) ) )
186 185 cbvmptv ⊒ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘₯ ↑ 𝑖 ) ) ) = ( 𝑛 ∈ β„•0 ↦ ( ( ( 𝑛 + 1 ) Β· ( 𝐴 β€˜ ( 𝑛 + 1 ) ) ) Β· ( π‘₯ ↑ 𝑛 ) ) )
187 oveq1 ⊒ ( π‘š = 𝑛 β†’ ( π‘š + 1 ) = ( 𝑛 + 1 ) )
188 fvoveq1 ⊒ ( π‘š = 𝑛 β†’ ( 𝐴 β€˜ ( π‘š + 1 ) ) = ( 𝐴 β€˜ ( 𝑛 + 1 ) ) )
189 187 188 oveq12d ⊒ ( π‘š = 𝑛 β†’ ( ( π‘š + 1 ) Β· ( 𝐴 β€˜ ( π‘š + 1 ) ) ) = ( ( 𝑛 + 1 ) Β· ( 𝐴 β€˜ ( 𝑛 + 1 ) ) ) )
190 eqid ⊒ ( π‘š ∈ β„•0 ↦ ( ( π‘š + 1 ) Β· ( 𝐴 β€˜ ( π‘š + 1 ) ) ) ) = ( π‘š ∈ β„•0 ↦ ( ( π‘š + 1 ) Β· ( 𝐴 β€˜ ( π‘š + 1 ) ) ) )
191 ovex ⊒ ( ( 𝑛 + 1 ) Β· ( 𝐴 β€˜ ( 𝑛 + 1 ) ) ) ∈ V
192 189 190 191 fvmpt ⊒ ( 𝑛 ∈ β„•0 β†’ ( ( π‘š ∈ β„•0 ↦ ( ( π‘š + 1 ) Β· ( 𝐴 β€˜ ( π‘š + 1 ) ) ) ) β€˜ 𝑛 ) = ( ( 𝑛 + 1 ) Β· ( 𝐴 β€˜ ( 𝑛 + 1 ) ) ) )
193 192 oveq1d ⊒ ( 𝑛 ∈ β„•0 β†’ ( ( ( π‘š ∈ β„•0 ↦ ( ( π‘š + 1 ) Β· ( 𝐴 β€˜ ( π‘š + 1 ) ) ) ) β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) = ( ( ( 𝑛 + 1 ) Β· ( 𝐴 β€˜ ( 𝑛 + 1 ) ) ) Β· ( π‘₯ ↑ 𝑛 ) ) )
194 193 mpteq2ia ⊒ ( 𝑛 ∈ β„•0 ↦ ( ( ( π‘š ∈ β„•0 ↦ ( ( π‘š + 1 ) Β· ( 𝐴 β€˜ ( π‘š + 1 ) ) ) ) β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) = ( 𝑛 ∈ β„•0 ↦ ( ( ( 𝑛 + 1 ) Β· ( 𝐴 β€˜ ( 𝑛 + 1 ) ) ) Β· ( π‘₯ ↑ 𝑛 ) ) )
195 186 194 eqtr4i ⊒ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘₯ ↑ 𝑖 ) ) ) = ( 𝑛 ∈ β„•0 ↦ ( ( ( π‘š ∈ β„•0 ↦ ( ( π‘š + 1 ) Β· ( 𝐴 β€˜ ( π‘š + 1 ) ) ) ) β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) )
196 180 195 eqtrdi ⊒ ( π‘Ž = π‘₯ β†’ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) = ( 𝑛 ∈ β„•0 ↦ ( ( ( π‘š ∈ β„•0 ↦ ( ( π‘š + 1 ) Β· ( 𝐴 β€˜ ( π‘š + 1 ) ) ) ) β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) )
197 196 cbvmptv ⊒ ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) = ( π‘₯ ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( ( π‘š ∈ β„•0 ↦ ( ( π‘š + 1 ) Β· ( 𝐴 β€˜ ( π‘š + 1 ) ) ) ) β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) )
198 fveq2 ⊒ ( 𝑦 = 𝑧 β†’ ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) = ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑧 ) )
199 198 fveq1d ⊒ ( 𝑦 = 𝑧 β†’ ( ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) β€˜ π‘˜ ) = ( ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑧 ) β€˜ π‘˜ ) )
200 199 sumeq2sdv ⊒ ( 𝑦 = 𝑧 β†’ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) β€˜ π‘˜ ) = Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑧 ) β€˜ π‘˜ ) )
201 200 cbvmptv ⊒ ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) β€˜ π‘˜ ) ) = ( 𝑧 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑧 ) β€˜ π‘˜ ) )
202 peano2nn0 ⊒ ( π‘š ∈ β„•0 β†’ ( π‘š + 1 ) ∈ β„•0 )
203 202 adantl ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) β†’ ( π‘š + 1 ) ∈ β„•0 )
204 203 nn0cnd ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) β†’ ( π‘š + 1 ) ∈ β„‚ )
205 133 203 ffvelcdmd ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) β†’ ( 𝐴 β€˜ ( π‘š + 1 ) ) ∈ β„‚ )
206 204 205 mulcld ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) β†’ ( ( π‘š + 1 ) Β· ( 𝐴 β€˜ ( π‘š + 1 ) ) ) ∈ β„‚ )
207 206 fmpttd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( π‘š ∈ β„•0 ↦ ( ( π‘š + 1 ) Β· ( 𝐴 β€˜ ( π‘š + 1 ) ) ) ) : β„•0 ⟢ β„‚ )
208 fveq2 ⊒ ( π‘Ÿ = 𝑗 β†’ ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ π‘Ÿ ) = ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑗 ) )
209 208 seqeq3d ⊒ ( π‘Ÿ = 𝑗 β†’ seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ π‘Ÿ ) ) = seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑗 ) ) )
210 209 eleq1d ⊒ ( π‘Ÿ = 𝑗 β†’ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑗 ) ) ∈ dom ⇝ ) )
211 210 cbvrabv ⊒ { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } = { 𝑗 ∈ ℝ ∣ seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑗 ) ) ∈ dom ⇝ }
212 211 supeq1i ⊒ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) = sup ( { 𝑗 ∈ ℝ ∣ seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑗 ) ) ∈ dom ⇝ } , ℝ* , < )
213 198 seqeq3d ⊒ ( 𝑦 = 𝑧 β†’ seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) = seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑧 ) ) )
214 213 fveq1d ⊒ ( 𝑦 = 𝑧 β†’ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) = ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑧 ) ) β€˜ 𝑗 ) )
215 214 cbvmptv ⊒ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) = ( 𝑧 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑧 ) ) β€˜ 𝑗 ) )
216 fveq2 ⊒ ( 𝑗 = π‘š β†’ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑧 ) ) β€˜ 𝑗 ) = ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑧 ) ) β€˜ π‘š ) )
217 216 mpteq2dv ⊒ ( 𝑗 = π‘š β†’ ( 𝑧 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑧 ) ) β€˜ 𝑗 ) ) = ( 𝑧 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑧 ) ) β€˜ π‘š ) ) )
218 215 217 eqtrid ⊒ ( 𝑗 = π‘š β†’ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) = ( 𝑧 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑧 ) ) β€˜ π‘š ) ) )
219 218 cbvmptv ⊒ ( 𝑗 ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) ) = ( π‘š ∈ β„•0 ↦ ( 𝑧 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑧 ) ) β€˜ π‘š ) ) )
220 17 rpred ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) ∈ ℝ )
221 1 2 3 4 5 6 psercnlem1 ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( 𝑀 ∈ ℝ+ ∧ ( abs β€˜ π‘Ž ) < 𝑀 ∧ 𝑀 < 𝑅 ) )
222 221 simp1d ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝑀 ∈ ℝ+ )
223 222 rpxrd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝑀 ∈ ℝ* )
224 197 207 212 radcnvcl ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
225 54 224 sselid ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* )
226 221 simp2d ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( abs β€˜ π‘Ž ) < 𝑀 )
227 cnvimass ⊒ ( β—‘ abs β€œ ( 0 [,) 𝑅 ) ) βŠ† dom abs
228 absf ⊒ abs : β„‚ ⟢ ℝ
229 228 fdmi ⊒ dom abs = β„‚
230 227 229 sseqtri ⊒ ( β—‘ abs β€œ ( 0 [,) 𝑅 ) ) βŠ† β„‚
231 5 230 eqsstri ⊒ 𝑆 βŠ† β„‚
232 231 a1i ⊒ ( πœ‘ β†’ 𝑆 βŠ† β„‚ )
233 232 sselda ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ π‘Ž ∈ β„‚ )
234 233 abscld ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( abs β€˜ π‘Ž ) ∈ ℝ )
235 222 rpred ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝑀 ∈ ℝ )
236 avglt2 ⊒ ( ( ( abs β€˜ π‘Ž ) ∈ ℝ ∧ 𝑀 ∈ ℝ ) β†’ ( ( abs β€˜ π‘Ž ) < 𝑀 ↔ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) < 𝑀 ) )
237 234 235 236 syl2anc ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( abs β€˜ π‘Ž ) < 𝑀 ↔ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) < 𝑀 ) )
238 226 237 mpbid ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) < 𝑀 )
239 222 rpge0d ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 0 ≀ 𝑀 )
240 235 239 absidd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( abs β€˜ 𝑀 ) = 𝑀 )
241 222 rpcnd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝑀 ∈ β„‚ )
242 oveq1 ⊒ ( 𝑀 = 𝑀 β†’ ( 𝑀 ↑ 𝑖 ) = ( 𝑀 ↑ 𝑖 ) )
243 242 oveq2d ⊒ ( 𝑀 = 𝑀 β†’ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑀 ↑ 𝑖 ) ) = ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑀 ↑ 𝑖 ) ) )
244 243 mpteq2dv ⊒ ( 𝑀 = 𝑀 β†’ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑀 ↑ 𝑖 ) ) ) = ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑀 ↑ 𝑖 ) ) ) )
245 oveq1 ⊒ ( π‘Ž = 𝑀 β†’ ( π‘Ž ↑ 𝑖 ) = ( 𝑀 ↑ 𝑖 ) )
246 245 oveq2d ⊒ ( π‘Ž = 𝑀 β†’ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) = ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑀 ↑ 𝑖 ) ) )
247 246 mpteq2dv ⊒ ( π‘Ž = 𝑀 β†’ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) = ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑀 ↑ 𝑖 ) ) ) )
248 247 cbvmptv ⊒ ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) = ( 𝑀 ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑀 ↑ 𝑖 ) ) ) )
249 nn0ex ⊒ β„•0 ∈ V
250 249 mptex ⊒ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑀 ↑ 𝑖 ) ) ) ∈ V
251 244 248 250 fvmpt ⊒ ( 𝑀 ∈ β„‚ β†’ ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑀 ) = ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑀 ↑ 𝑖 ) ) ) )
252 241 251 syl ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑀 ) = ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑀 ↑ 𝑖 ) ) ) )
253 252 seqeq3d ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑀 ) ) = seq 0 ( + , ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑀 ↑ 𝑖 ) ) ) ) )
254 fveq2 ⊒ ( 𝑛 = 𝑖 β†’ ( 𝐴 β€˜ 𝑛 ) = ( 𝐴 β€˜ 𝑖 ) )
255 oveq2 ⊒ ( 𝑛 = 𝑖 β†’ ( π‘₯ ↑ 𝑛 ) = ( π‘₯ ↑ 𝑖 ) )
256 254 255 oveq12d ⊒ ( 𝑛 = 𝑖 β†’ ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) = ( ( 𝐴 β€˜ 𝑖 ) Β· ( π‘₯ ↑ 𝑖 ) ) )
257 256 cbvmptv ⊒ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) = ( 𝑖 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑖 ) Β· ( π‘₯ ↑ 𝑖 ) ) )
258 oveq1 ⊒ ( π‘₯ = 𝑦 β†’ ( π‘₯ ↑ 𝑖 ) = ( 𝑦 ↑ 𝑖 ) )
259 258 oveq2d ⊒ ( π‘₯ = 𝑦 β†’ ( ( 𝐴 β€˜ 𝑖 ) Β· ( π‘₯ ↑ 𝑖 ) ) = ( ( 𝐴 β€˜ 𝑖 ) Β· ( 𝑦 ↑ 𝑖 ) ) )
260 259 mpteq2dv ⊒ ( π‘₯ = 𝑦 β†’ ( 𝑖 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑖 ) Β· ( π‘₯ ↑ 𝑖 ) ) ) = ( 𝑖 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑖 ) Β· ( 𝑦 ↑ 𝑖 ) ) ) )
261 257 260 eqtrid ⊒ ( π‘₯ = 𝑦 β†’ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) = ( 𝑖 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑖 ) Β· ( 𝑦 ↑ 𝑖 ) ) ) )
262 261 cbvmptv ⊒ ( π‘₯ ∈ β„‚ ↦ ( 𝑛 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑛 ) Β· ( π‘₯ ↑ 𝑛 ) ) ) ) = ( 𝑦 ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑖 ) Β· ( 𝑦 ↑ 𝑖 ) ) ) )
263 1 262 eqtri ⊒ 𝐺 = ( 𝑦 ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( 𝐴 β€˜ 𝑖 ) Β· ( 𝑦 ↑ 𝑖 ) ) ) )
264 fveq2 ⊒ ( π‘Ÿ = 𝑠 β†’ ( 𝐺 β€˜ π‘Ÿ ) = ( 𝐺 β€˜ 𝑠 ) )
265 264 seqeq3d ⊒ ( π‘Ÿ = 𝑠 β†’ seq 0 ( + , ( 𝐺 β€˜ π‘Ÿ ) ) = seq 0 ( + , ( 𝐺 β€˜ 𝑠 ) ) )
266 265 eleq1d ⊒ ( π‘Ÿ = 𝑠 β†’ ( seq 0 ( + , ( 𝐺 β€˜ π‘Ÿ ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( 𝐺 β€˜ 𝑠 ) ) ∈ dom ⇝ ) )
267 266 cbvrabv ⊒ { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝐺 β€˜ π‘Ÿ ) ) ∈ dom ⇝ } = { 𝑠 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 β€˜ 𝑠 ) ) ∈ dom ⇝ }
268 267 supeq1i ⊒ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝐺 β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) = sup ( { 𝑠 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 β€˜ 𝑠 ) ) ∈ dom ⇝ } , ℝ* , < )
269 4 268 eqtri ⊒ 𝑅 = sup ( { 𝑠 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 β€˜ 𝑠 ) ) ∈ dom ⇝ } , ℝ* , < )
270 eqid ⊒ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑀 ↑ 𝑖 ) ) ) = ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑀 ↑ 𝑖 ) ) )
271 3 adantr ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝐴 : β„•0 ⟢ β„‚ )
272 221 simp3d ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝑀 < 𝑅 )
273 240 272 eqbrtrd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( abs β€˜ 𝑀 ) < 𝑅 )
274 263 269 270 271 241 273 dvradcnv ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ seq 0 ( + , ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑀 ↑ 𝑖 ) ) ) ) ∈ dom ⇝ )
275 253 274 eqeltrd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑀 ) ) ∈ dom ⇝ )
276 197 207 212 241 275 radcnvle ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( abs β€˜ 𝑀 ) ≀ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) )
277 240 276 eqbrtrrd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 𝑀 ≀ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) )
278 18 223 225 238 277 xrltletrd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( ( abs β€˜ π‘Ž ) + 𝑀 ) / 2 ) < sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < ) )
279 197 201 207 212 219 220 278 41 pserulm ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( 𝑗 ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) ) ( ⇝𝑒 β€˜ 𝐡 ) ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) β€˜ π‘˜ ) ) )
280 21 sselda ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) β†’ 𝑦 ∈ β„‚ )
281 oveq1 ⊒ ( π‘Ž = 𝑦 β†’ ( π‘Ž ↑ 𝑖 ) = ( 𝑦 ↑ 𝑖 ) )
282 281 oveq2d ⊒ ( π‘Ž = 𝑦 β†’ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) = ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑦 ↑ 𝑖 ) ) )
283 282 mpteq2dv ⊒ ( π‘Ž = 𝑦 β†’ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) = ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑦 ↑ 𝑖 ) ) ) )
284 eqid ⊒ ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) = ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) )
285 249 mptex ⊒ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑦 ↑ 𝑖 ) ) ) ∈ V
286 283 284 285 fvmpt ⊒ ( 𝑦 ∈ β„‚ β†’ ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) = ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑦 ↑ 𝑖 ) ) ) )
287 280 286 syl ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) = ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑦 ↑ 𝑖 ) ) ) )
288 287 adantr ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ β„•0 ) β†’ ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) = ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑦 ↑ 𝑖 ) ) ) )
289 288 fveq1d ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ β„•0 ) β†’ ( ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) β€˜ π‘˜ ) = ( ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑦 ↑ 𝑖 ) ) ) β€˜ π‘˜ ) )
290 oveq1 ⊒ ( 𝑖 = π‘˜ β†’ ( 𝑖 + 1 ) = ( π‘˜ + 1 ) )
291 fvoveq1 ⊒ ( 𝑖 = π‘˜ β†’ ( 𝐴 β€˜ ( 𝑖 + 1 ) ) = ( 𝐴 β€˜ ( π‘˜ + 1 ) ) )
292 290 291 oveq12d ⊒ ( 𝑖 = π‘˜ β†’ ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) = ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) )
293 oveq2 ⊒ ( 𝑖 = π‘˜ β†’ ( 𝑦 ↑ 𝑖 ) = ( 𝑦 ↑ π‘˜ ) )
294 292 293 oveq12d ⊒ ( 𝑖 = π‘˜ β†’ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑦 ↑ 𝑖 ) ) = ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) )
295 eqid ⊒ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑦 ↑ 𝑖 ) ) ) = ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑦 ↑ 𝑖 ) ) )
296 ovex ⊒ ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ∈ V
297 294 295 296 fvmpt ⊒ ( π‘˜ ∈ β„•0 β†’ ( ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑦 ↑ 𝑖 ) ) ) β€˜ π‘˜ ) = ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) )
298 297 adantl ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ β„•0 ) β†’ ( ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑦 ↑ 𝑖 ) ) ) β€˜ π‘˜ ) = ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) )
299 289 298 eqtrd ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ β„•0 ) β†’ ( ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) β€˜ π‘˜ ) = ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) )
300 299 sumeq2dv ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) β†’ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) β€˜ π‘˜ ) = Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) )
301 300 mpteq2dva ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) β€˜ π‘˜ ) ) = ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) )
302 279 301 breqtrd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( 𝑗 ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) ) ( ⇝𝑒 β€˜ 𝐡 ) ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) )
303 nnuz ⊒ β„• = ( β„€β‰₯ β€˜ 1 )
304 1e0p1 ⊒ 1 = ( 0 + 1 )
305 304 fveq2i ⊒ ( β„€β‰₯ β€˜ 1 ) = ( β„€β‰₯ β€˜ ( 0 + 1 ) )
306 303 305 eqtri ⊒ β„• = ( β„€β‰₯ β€˜ ( 0 + 1 ) )
307 1zzd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 1 ∈ β„€ )
308 0zd ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) β†’ 0 ∈ β„€ )
309 peano2nn0 ⊒ ( 𝑖 ∈ β„•0 β†’ ( 𝑖 + 1 ) ∈ β„•0 )
310 309 nn0cnd ⊒ ( 𝑖 ∈ β„•0 β†’ ( 𝑖 + 1 ) ∈ β„‚ )
311 310 adantl ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ β„•0 ) β†’ ( 𝑖 + 1 ) ∈ β„‚ )
312 3 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) β†’ 𝐴 : β„•0 ⟢ β„‚ )
313 ffvelcdm ⊒ ( ( 𝐴 : β„•0 ⟢ β„‚ ∧ ( 𝑖 + 1 ) ∈ β„•0 ) β†’ ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ∈ β„‚ )
314 312 309 313 syl2an ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ β„•0 ) β†’ ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ∈ β„‚ )
315 311 314 mulcld ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ β„•0 ) β†’ ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) ∈ β„‚ )
316 280 148 sylan ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ β„•0 ) β†’ ( 𝑦 ↑ 𝑖 ) ∈ β„‚ )
317 315 316 mulcld ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ β„•0 ) β†’ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑦 ↑ 𝑖 ) ) ∈ β„‚ )
318 287 317 fmpt3d ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) : β„•0 ⟢ β„‚ )
319 318 ffvelcdmda ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘š ∈ β„•0 ) β†’ ( ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) β€˜ π‘š ) ∈ β„‚ )
320 8 308 319 serf ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) β†’ seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) : β„•0 ⟢ β„‚ )
321 320 ffvelcdmda ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑗 ∈ β„•0 ) β†’ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ∈ β„‚ )
322 321 an32s ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑗 ∈ β„•0 ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ∈ β„‚ )
323 322 fmpttd ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑗 ∈ β„•0 ) β†’ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) : 𝐡 ⟢ β„‚ )
324 30 31 elmap ⊒ ( ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) ∈ ( β„‚ ↑m 𝐡 ) ↔ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) : 𝐡 ⟢ β„‚ )
325 323 324 sylibr ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ 𝑗 ∈ β„•0 ) β†’ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) ∈ ( β„‚ ↑m 𝐡 ) )
326 325 fmpttd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( 𝑗 ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) ) : β„•0 ⟢ ( β„‚ ↑m 𝐡 ) )
327 elfznn ⊒ ( 𝑖 ∈ ( 1 ... π‘š ) β†’ 𝑖 ∈ β„• )
328 327 nnne0d ⊒ ( 𝑖 ∈ ( 1 ... π‘š ) β†’ 𝑖 β‰  0 )
329 328 neneqd ⊒ ( 𝑖 ∈ ( 1 ... π‘š ) β†’ Β¬ 𝑖 = 0 )
330 329 iffalsed ⊒ ( 𝑖 ∈ ( 1 ... π‘š ) β†’ if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) = ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) )
331 330 oveq2d ⊒ ( 𝑖 ∈ ( 1 ... π‘š ) β†’ ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) = ( ( 𝐴 β€˜ 𝑖 ) Β· ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) )
332 331 sumeq2i ⊒ Ξ£ 𝑖 ∈ ( 1 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) = Ξ£ 𝑖 ∈ ( 1 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) )
333 1zzd ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) β†’ 1 ∈ β„€ )
334 nnz ⊒ ( π‘š ∈ β„• β†’ π‘š ∈ β„€ )
335 334 ad2antlr ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) β†’ π‘š ∈ β„€ )
336 271 ad2antrr ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) β†’ 𝐴 : β„•0 ⟢ β„‚ )
337 327 nnnn0d ⊒ ( 𝑖 ∈ ( 1 ... π‘š ) β†’ 𝑖 ∈ β„•0 )
338 336 337 142 syl2an ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ ( 1 ... π‘š ) ) β†’ ( 𝐴 β€˜ 𝑖 ) ∈ β„‚ )
339 327 adantl ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ ( 1 ... π‘š ) ) β†’ 𝑖 ∈ β„• )
340 339 nncnd ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ ( 1 ... π‘š ) ) β†’ 𝑖 ∈ β„‚ )
341 280 adantlr ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) β†’ 𝑦 ∈ β„‚ )
342 nnm1nn0 ⊒ ( 𝑖 ∈ β„• β†’ ( 𝑖 βˆ’ 1 ) ∈ β„•0 )
343 327 342 syl ⊒ ( 𝑖 ∈ ( 1 ... π‘š ) β†’ ( 𝑖 βˆ’ 1 ) ∈ β„•0 )
344 expcl ⊒ ( ( 𝑦 ∈ β„‚ ∧ ( 𝑖 βˆ’ 1 ) ∈ β„•0 ) β†’ ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ∈ β„‚ )
345 341 343 344 syl2an ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ ( 1 ... π‘š ) ) β†’ ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ∈ β„‚ )
346 340 345 mulcld ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ ( 1 ... π‘š ) ) β†’ ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ∈ β„‚ )
347 338 346 mulcld ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ ( 1 ... π‘š ) ) β†’ ( ( 𝐴 β€˜ 𝑖 ) Β· ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ∈ β„‚ )
348 fveq2 ⊒ ( 𝑖 = ( π‘˜ + 1 ) β†’ ( 𝐴 β€˜ 𝑖 ) = ( 𝐴 β€˜ ( π‘˜ + 1 ) ) )
349 id ⊒ ( 𝑖 = ( π‘˜ + 1 ) β†’ 𝑖 = ( π‘˜ + 1 ) )
350 oveq1 ⊒ ( 𝑖 = ( π‘˜ + 1 ) β†’ ( 𝑖 βˆ’ 1 ) = ( ( π‘˜ + 1 ) βˆ’ 1 ) )
351 350 oveq2d ⊒ ( 𝑖 = ( π‘˜ + 1 ) β†’ ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) = ( 𝑦 ↑ ( ( π‘˜ + 1 ) βˆ’ 1 ) ) )
352 349 351 oveq12d ⊒ ( 𝑖 = ( π‘˜ + 1 ) β†’ ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) = ( ( π‘˜ + 1 ) Β· ( 𝑦 ↑ ( ( π‘˜ + 1 ) βˆ’ 1 ) ) ) )
353 348 352 oveq12d ⊒ ( 𝑖 = ( π‘˜ + 1 ) β†’ ( ( 𝐴 β€˜ 𝑖 ) Β· ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) = ( ( 𝐴 β€˜ ( π‘˜ + 1 ) ) Β· ( ( π‘˜ + 1 ) Β· ( 𝑦 ↑ ( ( π‘˜ + 1 ) βˆ’ 1 ) ) ) ) )
354 333 333 335 347 353 fsumshftm ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) β†’ Ξ£ 𝑖 ∈ ( 1 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) = Ξ£ π‘˜ ∈ ( ( 1 βˆ’ 1 ) ... ( π‘š βˆ’ 1 ) ) ( ( 𝐴 β€˜ ( π‘˜ + 1 ) ) Β· ( ( π‘˜ + 1 ) Β· ( 𝑦 ↑ ( ( π‘˜ + 1 ) βˆ’ 1 ) ) ) ) )
355 332 354 eqtrid ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) β†’ Ξ£ 𝑖 ∈ ( 1 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) = Ξ£ π‘˜ ∈ ( ( 1 βˆ’ 1 ) ... ( π‘š βˆ’ 1 ) ) ( ( 𝐴 β€˜ ( π‘˜ + 1 ) ) Β· ( ( π‘˜ + 1 ) Β· ( 𝑦 ↑ ( ( π‘˜ + 1 ) βˆ’ 1 ) ) ) ) )
356 fz1ssfz0 ⊒ ( 1 ... π‘š ) βŠ† ( 0 ... π‘š )
357 356 a1i ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( 1 ... π‘š ) βŠ† ( 0 ... π‘š ) )
358 331 adantl ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ ( 1 ... π‘š ) ) β†’ ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) = ( ( 𝐴 β€˜ 𝑖 ) Β· ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) )
359 358 347 eqeltrd ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ ( 1 ... π‘š ) ) β†’ ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ∈ β„‚ )
360 eldif ⊒ ( 𝑖 ∈ ( ( 0 ... π‘š ) βˆ– ( ( 0 + 1 ) ... π‘š ) ) ↔ ( 𝑖 ∈ ( 0 ... π‘š ) ∧ Β¬ 𝑖 ∈ ( ( 0 + 1 ) ... π‘š ) ) )
361 elfzuz2 ⊒ ( 𝑖 ∈ ( 0 ... π‘š ) β†’ π‘š ∈ ( β„€β‰₯ β€˜ 0 ) )
362 elfzp12 ⊒ ( π‘š ∈ ( β„€β‰₯ β€˜ 0 ) β†’ ( 𝑖 ∈ ( 0 ... π‘š ) ↔ ( 𝑖 = 0 ∨ 𝑖 ∈ ( ( 0 + 1 ) ... π‘š ) ) ) )
363 361 362 syl ⊒ ( 𝑖 ∈ ( 0 ... π‘š ) β†’ ( 𝑖 ∈ ( 0 ... π‘š ) ↔ ( 𝑖 = 0 ∨ 𝑖 ∈ ( ( 0 + 1 ) ... π‘š ) ) ) )
364 363 ibi ⊒ ( 𝑖 ∈ ( 0 ... π‘š ) β†’ ( 𝑖 = 0 ∨ 𝑖 ∈ ( ( 0 + 1 ) ... π‘š ) ) )
365 364 ord ⊒ ( 𝑖 ∈ ( 0 ... π‘š ) β†’ ( Β¬ 𝑖 = 0 β†’ 𝑖 ∈ ( ( 0 + 1 ) ... π‘š ) ) )
366 365 con1d ⊒ ( 𝑖 ∈ ( 0 ... π‘š ) β†’ ( Β¬ 𝑖 ∈ ( ( 0 + 1 ) ... π‘š ) β†’ 𝑖 = 0 ) )
367 366 imp ⊒ ( ( 𝑖 ∈ ( 0 ... π‘š ) ∧ Β¬ 𝑖 ∈ ( ( 0 + 1 ) ... π‘š ) ) β†’ 𝑖 = 0 )
368 360 367 sylbi ⊒ ( 𝑖 ∈ ( ( 0 ... π‘š ) βˆ– ( ( 0 + 1 ) ... π‘š ) ) β†’ 𝑖 = 0 )
369 304 oveq1i ⊒ ( 1 ... π‘š ) = ( ( 0 + 1 ) ... π‘š )
370 369 difeq2i ⊒ ( ( 0 ... π‘š ) βˆ– ( 1 ... π‘š ) ) = ( ( 0 ... π‘š ) βˆ– ( ( 0 + 1 ) ... π‘š ) )
371 368 370 eleq2s ⊒ ( 𝑖 ∈ ( ( 0 ... π‘š ) βˆ– ( 1 ... π‘š ) ) β†’ 𝑖 = 0 )
372 371 adantl ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ ( ( 0 ... π‘š ) βˆ– ( 1 ... π‘š ) ) ) β†’ 𝑖 = 0 )
373 372 iftrued ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ ( ( 0 ... π‘š ) βˆ– ( 1 ... π‘š ) ) ) β†’ if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) = 0 )
374 373 oveq2d ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ ( ( 0 ... π‘š ) βˆ– ( 1 ... π‘š ) ) ) β†’ ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) = ( ( 𝐴 β€˜ 𝑖 ) Β· 0 ) )
375 eldifi ⊒ ( 𝑖 ∈ ( ( 0 ... π‘š ) βˆ– ( 1 ... π‘š ) ) β†’ 𝑖 ∈ ( 0 ... π‘š ) )
376 375 104 syl ⊒ ( 𝑖 ∈ ( ( 0 ... π‘š ) βˆ– ( 1 ... π‘š ) ) β†’ 𝑖 ∈ β„•0 )
377 336 376 142 syl2an ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ ( ( 0 ... π‘š ) βˆ– ( 1 ... π‘š ) ) ) β†’ ( 𝐴 β€˜ 𝑖 ) ∈ β„‚ )
378 377 mul01d ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ ( ( 0 ... π‘š ) βˆ– ( 1 ... π‘š ) ) ) β†’ ( ( 𝐴 β€˜ 𝑖 ) Β· 0 ) = 0 )
379 374 378 eqtrd ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ ( ( 0 ... π‘š ) βˆ– ( 1 ... π‘š ) ) ) β†’ ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) = 0 )
380 fzfid ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( 0 ... π‘š ) ∈ Fin )
381 357 359 379 380 fsumss ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) β†’ Ξ£ 𝑖 ∈ ( 1 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) = Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) )
382 1m1e0 ⊒ ( 1 βˆ’ 1 ) = 0
383 382 oveq1i ⊒ ( ( 1 βˆ’ 1 ) ... ( π‘š βˆ’ 1 ) ) = ( 0 ... ( π‘š βˆ’ 1 ) )
384 383 sumeq1i ⊒ Ξ£ π‘˜ ∈ ( ( 1 βˆ’ 1 ) ... ( π‘š βˆ’ 1 ) ) ( ( 𝐴 β€˜ ( π‘˜ + 1 ) ) Β· ( ( π‘˜ + 1 ) Β· ( 𝑦 ↑ ( ( π‘˜ + 1 ) βˆ’ 1 ) ) ) ) = Ξ£ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ( ( 𝐴 β€˜ ( π‘˜ + 1 ) ) Β· ( ( π‘˜ + 1 ) Β· ( 𝑦 ↑ ( ( π‘˜ + 1 ) βˆ’ 1 ) ) ) )
385 elfznn0 ⊒ ( π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) β†’ π‘˜ ∈ β„•0 )
386 385 adantl ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ π‘˜ ∈ β„•0 )
387 386 297 syl ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑦 ↑ 𝑖 ) ) ) β€˜ π‘˜ ) = ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) )
388 341 adantr ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ 𝑦 ∈ β„‚ )
389 388 286 syl ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) = ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑦 ↑ 𝑖 ) ) ) )
390 389 fveq1d ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) β€˜ π‘˜ ) = ( ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( 𝑦 ↑ 𝑖 ) ) ) β€˜ π‘˜ ) )
391 336 adantr ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ 𝐴 : β„•0 ⟢ β„‚ )
392 peano2nn0 ⊒ ( π‘˜ ∈ β„•0 β†’ ( π‘˜ + 1 ) ∈ β„•0 )
393 386 392 syl ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( π‘˜ + 1 ) ∈ β„•0 )
394 391 393 ffvelcdmd ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ∈ β„‚ )
395 393 nn0cnd ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( π‘˜ + 1 ) ∈ β„‚ )
396 expcl ⊒ ( ( 𝑦 ∈ β„‚ ∧ π‘˜ ∈ β„•0 ) β†’ ( 𝑦 ↑ π‘˜ ) ∈ β„‚ )
397 341 385 396 syl2an ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( 𝑦 ↑ π‘˜ ) ∈ β„‚ )
398 394 395 397 mul12d ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( ( 𝐴 β€˜ ( π‘˜ + 1 ) ) Β· ( ( π‘˜ + 1 ) Β· ( 𝑦 ↑ π‘˜ ) ) ) = ( ( π‘˜ + 1 ) Β· ( ( 𝐴 β€˜ ( π‘˜ + 1 ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) )
399 386 nn0cnd ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ π‘˜ ∈ β„‚ )
400 ax-1cn ⊒ 1 ∈ β„‚
401 pncan ⊒ ( ( π‘˜ ∈ β„‚ ∧ 1 ∈ β„‚ ) β†’ ( ( π‘˜ + 1 ) βˆ’ 1 ) = π‘˜ )
402 399 400 401 sylancl ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( ( π‘˜ + 1 ) βˆ’ 1 ) = π‘˜ )
403 402 oveq2d ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( 𝑦 ↑ ( ( π‘˜ + 1 ) βˆ’ 1 ) ) = ( 𝑦 ↑ π‘˜ ) )
404 403 oveq2d ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( ( π‘˜ + 1 ) Β· ( 𝑦 ↑ ( ( π‘˜ + 1 ) βˆ’ 1 ) ) ) = ( ( π‘˜ + 1 ) Β· ( 𝑦 ↑ π‘˜ ) ) )
405 404 oveq2d ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( ( 𝐴 β€˜ ( π‘˜ + 1 ) ) Β· ( ( π‘˜ + 1 ) Β· ( 𝑦 ↑ ( ( π‘˜ + 1 ) βˆ’ 1 ) ) ) ) = ( ( 𝐴 β€˜ ( π‘˜ + 1 ) ) Β· ( ( π‘˜ + 1 ) Β· ( 𝑦 ↑ π‘˜ ) ) ) )
406 395 394 397 mulassd ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) = ( ( π‘˜ + 1 ) Β· ( ( 𝐴 β€˜ ( π‘˜ + 1 ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) )
407 398 405 406 3eqtr4d ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( ( 𝐴 β€˜ ( π‘˜ + 1 ) ) Β· ( ( π‘˜ + 1 ) Β· ( 𝑦 ↑ ( ( π‘˜ + 1 ) βˆ’ 1 ) ) ) ) = ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) )
408 387 390 407 3eqtr4d ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) β€˜ π‘˜ ) = ( ( 𝐴 β€˜ ( π‘˜ + 1 ) ) Β· ( ( π‘˜ + 1 ) Β· ( 𝑦 ↑ ( ( π‘˜ + 1 ) βˆ’ 1 ) ) ) ) )
409 nnm1nn0 ⊒ ( π‘š ∈ β„• β†’ ( π‘š βˆ’ 1 ) ∈ β„•0 )
410 409 adantl ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) β†’ ( π‘š βˆ’ 1 ) ∈ β„•0 )
411 410 adantr ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( π‘š βˆ’ 1 ) ∈ β„•0 )
412 411 8 eleqtrdi ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( π‘š βˆ’ 1 ) ∈ ( β„€β‰₯ β€˜ 0 ) )
413 403 397 eqeltrd ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( 𝑦 ↑ ( ( π‘˜ + 1 ) βˆ’ 1 ) ) ∈ β„‚ )
414 395 413 mulcld ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( ( π‘˜ + 1 ) Β· ( 𝑦 ↑ ( ( π‘˜ + 1 ) βˆ’ 1 ) ) ) ∈ β„‚ )
415 394 414 mulcld ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) ∧ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ) β†’ ( ( 𝐴 β€˜ ( π‘˜ + 1 ) ) Β· ( ( π‘˜ + 1 ) Β· ( 𝑦 ↑ ( ( π‘˜ + 1 ) βˆ’ 1 ) ) ) ) ∈ β„‚ )
416 408 412 415 fsumser ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) β†’ Ξ£ π‘˜ ∈ ( 0 ... ( π‘š βˆ’ 1 ) ) ( ( 𝐴 β€˜ ( π‘˜ + 1 ) ) Β· ( ( π‘˜ + 1 ) Β· ( 𝑦 ↑ ( ( π‘˜ + 1 ) βˆ’ 1 ) ) ) ) = ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ ( π‘š βˆ’ 1 ) ) )
417 384 416 eqtrid ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) β†’ Ξ£ π‘˜ ∈ ( ( 1 βˆ’ 1 ) ... ( π‘š βˆ’ 1 ) ) ( ( 𝐴 β€˜ ( π‘˜ + 1 ) ) Β· ( ( π‘˜ + 1 ) Β· ( 𝑦 ↑ ( ( π‘˜ + 1 ) βˆ’ 1 ) ) ) ) = ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ ( π‘š βˆ’ 1 ) ) )
418 355 381 417 3eqtr3d ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) ∧ 𝑦 ∈ 𝐡 ) β†’ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) = ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ ( π‘š βˆ’ 1 ) ) )
419 418 mpteq2dva ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) β†’ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) = ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ ( π‘š βˆ’ 1 ) ) ) )
420 fveq2 ⊒ ( 𝑗 = ( π‘š βˆ’ 1 ) β†’ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) = ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ ( π‘š βˆ’ 1 ) ) )
421 420 mpteq2dv ⊒ ( 𝑗 = ( π‘š βˆ’ 1 ) β†’ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) = ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ ( π‘š βˆ’ 1 ) ) ) )
422 eqid ⊒ ( 𝑗 ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) ) = ( 𝑗 ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) )
423 31 mptex ⊒ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ ( π‘š βˆ’ 1 ) ) ) ∈ V
424 421 422 423 fvmpt ⊒ ( ( π‘š βˆ’ 1 ) ∈ β„•0 β†’ ( ( 𝑗 ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) ) β€˜ ( π‘š βˆ’ 1 ) ) = ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ ( π‘š βˆ’ 1 ) ) ) )
425 410 424 syl ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) β†’ ( ( 𝑗 ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) ) β€˜ ( π‘š βˆ’ 1 ) ) = ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ ( π‘š βˆ’ 1 ) ) ) )
426 419 425 eqtr4d ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„• ) β†’ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) = ( ( 𝑗 ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) ) β€˜ ( π‘š βˆ’ 1 ) ) )
427 426 mpteq2dva ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( π‘š ∈ β„• ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) ) = ( π‘š ∈ β„• ↦ ( ( 𝑗 ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) ) β€˜ ( π‘š βˆ’ 1 ) ) ) )
428 8 306 11 307 326 427 ulmshft ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( 𝑗 ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ ( seq 0 ( + , ( ( π‘Ž ∈ β„‚ ↦ ( 𝑖 ∈ β„•0 ↦ ( ( ( 𝑖 + 1 ) Β· ( 𝐴 β€˜ ( 𝑖 + 1 ) ) ) Β· ( π‘Ž ↑ 𝑖 ) ) ) ) β€˜ 𝑦 ) ) β€˜ 𝑗 ) ) ) ( ⇝𝑒 β€˜ 𝐡 ) ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) ↔ ( π‘š ∈ β„• ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) ) ( ⇝𝑒 β€˜ 𝐡 ) ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) ) )
429 302 428 mpbid ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( π‘š ∈ β„• ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) ) ( ⇝𝑒 β€˜ 𝐡 ) ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) )
430 177 429 eqbrtrid ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( π‘š ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) ) β†Ύ β„• ) ( ⇝𝑒 β€˜ 𝐡 ) ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) )
431 1nn0 ⊒ 1 ∈ β„•0
432 431 a1i ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ 1 ∈ β„•0 )
433 fzfid ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( 0 ... π‘š ) ∈ Fin )
434 164 an32s ⊒ ( ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑦 ∈ 𝐡 ) ∧ 𝑖 ∈ ( 0 ... π‘š ) ) β†’ ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ∈ β„‚ )
435 433 434 fsumcl ⊒ ( ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) ∧ 𝑦 ∈ 𝐡 ) β†’ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ∈ β„‚ )
436 435 fmpttd ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) β†’ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) : 𝐡 ⟢ β„‚ )
437 30 31 elmap ⊒ ( ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) ∈ ( β„‚ ↑m 𝐡 ) ↔ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) : 𝐡 ⟢ β„‚ )
438 436 437 sylibr ⊒ ( ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) ∧ π‘š ∈ β„•0 ) β†’ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) ∈ ( β„‚ ↑m 𝐡 ) )
439 438 fmpttd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( π‘š ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) ) : β„•0 ⟢ ( β„‚ ↑m 𝐡 ) )
440 8 303 432 439 ulmres ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( ( π‘š ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) ) ( ⇝𝑒 β€˜ 𝐡 ) ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) ↔ ( ( π‘š ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) ) β†Ύ β„• ) ( ⇝𝑒 β€˜ 𝐡 ) ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) ) )
441 430 440 mpbird ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( π‘š ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘š ) ( ( 𝐴 β€˜ 𝑖 ) Β· if ( 𝑖 = 0 , 0 , ( 𝑖 Β· ( 𝑦 ↑ ( 𝑖 βˆ’ 1 ) ) ) ) ) ) ) ( ⇝𝑒 β€˜ 𝐡 ) ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) )
442 174 441 eqbrtrd ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( π‘š ∈ β„•0 ↦ ( β„‚ D ( ( π‘˜ ∈ β„•0 ↦ ( 𝑦 ∈ 𝐡 ↦ Ξ£ 𝑖 ∈ ( 0 ... π‘˜ ) ( ( 𝐺 β€˜ 𝑦 ) β€˜ 𝑖 ) ) ) β€˜ π‘š ) ) ) ( ⇝𝑒 β€˜ 𝐡 ) ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) )
443 8 10 11 34 44 120 442 ulmdv ⊒ ( ( πœ‘ ∧ π‘Ž ∈ 𝑆 ) β†’ ( β„‚ D ( 𝐹 β†Ύ 𝐡 ) ) = ( 𝑦 ∈ 𝐡 ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘˜ + 1 ) Β· ( 𝐴 β€˜ ( π‘˜ + 1 ) ) ) Β· ( 𝑦 ↑ π‘˜ ) ) ) )