This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eftlub

Description: An upper bound on the absolute value of the infinite tail of the series expansion of the exponential function on the closed unit disk. (Contributed by Paul Chapman, 19-Jan-2008) (Proof shortened by Mario Carneiro, 29-Apr-2014)

Ref Expression
Hypotheses eftl.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
eftl.2 ⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
eftl.3 ⊢ 𝐻 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑛 ) ) )
eftl.4 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
eftl.5 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
eftl.6 ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ≤ 1 )
Assertion eftlub ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) · ( ( 𝑀 + 1 ) / ( ( ! ‘ 𝑀 ) · 𝑀 ) ) ) )

Proof

Step Hyp Ref Expression
1 eftl.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
2 eftl.2 ⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
3 eftl.3 ⊢ 𝐻 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑛 ) ) )
4 eftl.4 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
5 eftl.5 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
6 eftl.6 ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ≤ 1 )
7 4 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
8 1 eftlcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
9 5 7 8 syl2anc ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
10 9 abscld ⊢ ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
11 5 abscld ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ∈ ℝ )
12 2 reeftlcl ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
13 11 7 12 syl2anc ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
14 11 7 reexpcld ⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ∈ ℝ )
15 peano2nn0 ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ0 )
16 7 15 syl ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℕ0 )
17 16 nn0red ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℝ )
18 7 faccld ⊢ ( 𝜑 → ( ! ‘ 𝑀 ) ∈ ℕ )
19 18 4 nnmulcld ⊢ ( 𝜑 → ( ( ! ‘ 𝑀 ) · 𝑀 ) ∈ ℕ )
20 17 19 nndivred ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) / ( ( ! ‘ 𝑀 ) · 𝑀 ) ) ∈ ℝ )
21 14 20 remulcld ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) · ( ( 𝑀 + 1 ) / ( ( ! ‘ 𝑀 ) · 𝑀 ) ) ) ∈ ℝ )
22 eqid ⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
23 4 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
24 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
25 eluznn0 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ0 )
26 7 25 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ0 )
27 1 eftval ⊢ ( 𝑘 ∈ ℕ0 → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
29 eftcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
30 5 29 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
31 28 30 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
32 26 31 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
33 1 eftlcvg ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
34 5 7 33 syl2anc ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
35 22 23 24 32 34 isumclim2 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) )
36 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
37 2 eftval ⊢ ( 𝑘 ∈ ℕ0 → ( 𝐺 ‘ 𝑘 ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
39 reeftcl ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
40 11 39 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
41 38 40 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
42 26 41 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
43 42 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
44 11 recnd ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ∈ ℂ )
45 2 eftlcvg ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → seq 𝑀 ( + , 𝐺 ) ∈ dom ⇝ )
46 44 7 45 syl2anc ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ dom ⇝ )
47 22 23 36 43 46 isumclim2 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ⇝ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐺 ‘ 𝑘 ) )
48 eftabs ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
49 5 48 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
50 28 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = ( abs ‘ ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) )
51 49 50 38 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
52 26 51 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐺 ‘ 𝑘 ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
53 22 35 47 23 32 52 iserabs ⊢ ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) ) ≤ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐺 ‘ 𝑘 ) )
54 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
55 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
56 4 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
57 nn0cn ⊢ ( 𝑗 ∈ ℕ0 → 𝑗 ∈ ℂ )
58 nn0ex ⊢ ℕ0 ∈ V
59 58 mptex ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ∈ V
60 2 59 eqeltri ⊢ 𝐺 ∈ V
61 60 shftval4 ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( ( 𝐺 shift - 𝑀 ) ‘ 𝑗 ) = ( 𝐺 ‘ ( 𝑀 + 𝑗 ) ) )
62 56 57 61 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐺 shift - 𝑀 ) ‘ 𝑗 ) = ( 𝐺 ‘ ( 𝑀 + 𝑗 ) ) )
63 nn0addcl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ) → ( 𝑀 + 𝑗 ) ∈ ℕ0 )
64 7 63 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝑀 + 𝑗 ) ∈ ℕ0 )
65 2 eftval ⊢ ( ( 𝑀 + 𝑗 ) ∈ ℕ0 → ( 𝐺 ‘ ( 𝑀 + 𝑗 ) ) = ( ( ( abs ‘ 𝐴 ) ↑ ( 𝑀 + 𝑗 ) ) / ( ! ‘ ( 𝑀 + 𝑗 ) ) ) )
66 64 65 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐺 ‘ ( 𝑀 + 𝑗 ) ) = ( ( ( abs ‘ 𝐴 ) ↑ ( 𝑀 + 𝑗 ) ) / ( ! ‘ ( 𝑀 + 𝑗 ) ) ) )
67 11 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
68 reeftcl ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℝ ∧ ( 𝑀 + 𝑗 ) ∈ ℕ0 ) → ( ( ( abs ‘ 𝐴 ) ↑ ( 𝑀 + 𝑗 ) ) / ( ! ‘ ( 𝑀 + 𝑗 ) ) ) ∈ ℝ )
69 67 64 68 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ( abs ‘ 𝐴 ) ↑ ( 𝑀 + 𝑗 ) ) / ( ! ‘ ( 𝑀 + 𝑗 ) ) ) ∈ ℝ )
70 66 69 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐺 ‘ ( 𝑀 + 𝑗 ) ) ∈ ℝ )
71 oveq2 ⊢ ( 𝑛 = 𝑗 → ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑛 ) = ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) )
72 71 oveq2d ⊢ ( 𝑛 = 𝑗 → ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑛 ) ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) )
73 ovex ⊢ ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) ∈ V
74 72 3 73 fvmpt ⊢ ( 𝑗 ∈ ℕ0 → ( 𝐻 ‘ 𝑗 ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) )
75 74 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑗 ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) )
76 14 18 nndivred ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ∈ ℝ )
77 76 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ∈ ℝ )
78 4 peano2nnd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℕ )
79 78 nnrecred ⊢ ( 𝜑 → ( 1 / ( 𝑀 + 1 ) ) ∈ ℝ )
80 reexpcl ⊢ ( ( ( 1 / ( 𝑀 + 1 ) ) ∈ ℝ ∧ 𝑗 ∈ ℕ0 ) → ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ∈ ℝ )
81 79 80 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ∈ ℝ )
82 77 81 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) ∈ ℝ )
83 67 64 reexpcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) ↑ ( 𝑀 + 𝑗 ) ) ∈ ℝ )
84 14 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ∈ ℝ )
85 64 faccld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ! ‘ ( 𝑀 + 𝑗 ) ) ∈ ℕ )
86 85 nnred ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ! ‘ ( 𝑀 + 𝑗 ) ) ∈ ℝ )
87 86 82 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ! ‘ ( 𝑀 + 𝑗 ) ) · ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) ) ∈ ℝ )
88 7 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 )
89 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
90 23 89 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
91 uzaddcl ⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑗 ∈ ℕ0 ) → ( 𝑀 + 𝑗 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
92 90 91 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝑀 + 𝑗 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
93 5 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝐴 ) )
94 93 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 0 ≤ ( abs ‘ 𝐴 ) )
95 6 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( abs ‘ 𝐴 ) ≤ 1 )
96 67 88 92 94 95 leexp2rd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) ↑ ( 𝑀 + 𝑗 ) ) ≤ ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) )
97 18 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ! ‘ 𝑀 ) ∈ ℕ )
98 nnexpcl ⊢ ( ( ( 𝑀 + 1 ) ∈ ℕ ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) ↑ 𝑗 ) ∈ ℕ )
99 78 98 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) ↑ 𝑗 ) ∈ ℕ )
100 97 99 nnmulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ∈ ℕ )
101 100 nnred ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ∈ ℝ )
102 11 7 93 expge0d ⊢ ( 𝜑 → 0 ≤ ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) )
103 14 102 jca ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ∈ ℝ ∧ 0 ≤ ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ) )
104 103 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ∈ ℝ ∧ 0 ≤ ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ) )
105 faclbnd6 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑗 ∈ ℕ0 ) → ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ≤ ( ! ‘ ( 𝑀 + 𝑗 ) ) )
106 7 105 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ≤ ( ! ‘ ( 𝑀 + 𝑗 ) ) )
107 lemul1a ⊢ ( ( ( ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ∈ ℝ ∧ ( ! ‘ ( 𝑀 + 𝑗 ) ) ∈ ℝ ∧ ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ∈ ℝ ∧ 0 ≤ ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ) ) ∧ ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ≤ ( ! ‘ ( 𝑀 + 𝑗 ) ) ) → ( ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) · ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ) ≤ ( ( ! ‘ ( 𝑀 + 𝑗 ) ) · ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ) )
108 101 86 104 106 107 syl31anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) · ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ) ≤ ( ( ! ‘ ( 𝑀 + 𝑗 ) ) · ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ) )
109 86 84 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ! ‘ ( 𝑀 + 𝑗 ) ) · ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ) ∈ ℝ )
110 100 nnrpd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ∈ ℝ+ )
111 84 109 110 lemuldiv2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) · ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ) ≤ ( ( ! ‘ ( 𝑀 + 𝑗 ) ) · ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ) ↔ ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ≤ ( ( ( ! ‘ ( 𝑀 + 𝑗 ) ) · ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ) / ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ) ) )
112 108 111 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ≤ ( ( ( ! ‘ ( 𝑀 + 𝑗 ) ) · ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ) / ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ) )
113 85 nncnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ! ‘ ( 𝑀 + 𝑗 ) ) ∈ ℂ )
114 14 recnd ⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ∈ ℂ )
115 114 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ∈ ℂ )
116 100 nncnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ∈ ℂ )
117 100 nnne0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ≠ 0 )
118 113 115 116 117 divassd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ( ! ‘ ( 𝑀 + 𝑗 ) ) · ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ) / ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ) = ( ( ! ‘ ( 𝑀 + 𝑗 ) ) · ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ) ) )
119 78 nncnd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℂ )
120 119 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝑀 + 1 ) ∈ ℂ )
121 78 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝑀 + 1 ) ∈ ℕ )
122 121 nnne0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝑀 + 1 ) ≠ 0 )
123 nn0z ⊢ ( 𝑗 ∈ ℕ0 → 𝑗 ∈ ℤ )
124 123 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ℤ )
125 120 122 124 exprecd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) = ( 1 / ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) )
126 125 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( 1 / ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ) )
127 76 recnd ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ∈ ℂ )
128 127 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) ∈ ℂ )
129 99 nncnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) ↑ 𝑗 ) ∈ ℂ )
130 99 nnne0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑀 + 1 ) ↑ 𝑗 ) ≠ 0 )
131 128 129 130 divrecd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) / ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( 1 / ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ) )
132 18 nncnd ⊢ ( 𝜑 → ( ! ‘ 𝑀 ) ∈ ℂ )
133 132 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ! ‘ 𝑀 ) ∈ ℂ )
134 facne0 ⊢ ( 𝑀 ∈ ℕ0 → ( ! ‘ 𝑀 ) ≠ 0 )
135 7 134 syl ⊢ ( 𝜑 → ( ! ‘ 𝑀 ) ≠ 0 )
136 135 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ! ‘ 𝑀 ) ≠ 0 )
137 115 133 129 136 130 divdiv1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) / ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ) )
138 126 131 137 3eqtr2rd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) )
139 138 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ! ‘ ( 𝑀 + 𝑗 ) ) · ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ) ) = ( ( ! ‘ ( 𝑀 + 𝑗 ) ) · ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) ) )
140 118 139 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ( ! ‘ ( 𝑀 + 𝑗 ) ) · ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ) / ( ( ! ‘ 𝑀 ) · ( ( 𝑀 + 1 ) ↑ 𝑗 ) ) ) = ( ( ! ‘ ( 𝑀 + 𝑗 ) ) · ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) ) )
141 112 140 breqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) ≤ ( ( ! ‘ ( 𝑀 + 𝑗 ) ) · ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) ) )
142 83 84 87 96 141 letrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) ↑ ( 𝑀 + 𝑗 ) ) ≤ ( ( ! ‘ ( 𝑀 + 𝑗 ) ) · ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) ) )
143 85 nngt0d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 0 < ( ! ‘ ( 𝑀 + 𝑗 ) ) )
144 ledivmul ⊢ ( ( ( ( abs ‘ 𝐴 ) ↑ ( 𝑀 + 𝑗 ) ) ∈ ℝ ∧ ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) ∈ ℝ ∧ ( ( ! ‘ ( 𝑀 + 𝑗 ) ) ∈ ℝ ∧ 0 < ( ! ‘ ( 𝑀 + 𝑗 ) ) ) ) → ( ( ( ( abs ‘ 𝐴 ) ↑ ( 𝑀 + 𝑗 ) ) / ( ! ‘ ( 𝑀 + 𝑗 ) ) ) ≤ ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) ↔ ( ( abs ‘ 𝐴 ) ↑ ( 𝑀 + 𝑗 ) ) ≤ ( ( ! ‘ ( 𝑀 + 𝑗 ) ) · ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) ) ) )
145 83 82 86 143 144 syl112anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ( ( abs ‘ 𝐴 ) ↑ ( 𝑀 + 𝑗 ) ) / ( ! ‘ ( 𝑀 + 𝑗 ) ) ) ≤ ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) ↔ ( ( abs ‘ 𝐴 ) ↑ ( 𝑀 + 𝑗 ) ) ≤ ( ( ! ‘ ( 𝑀 + 𝑗 ) ) · ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) ) ) )
146 142 145 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ( abs ‘ 𝐴 ) ↑ ( 𝑀 + 𝑗 ) ) / ( ! ‘ ( 𝑀 + 𝑗 ) ) ) ≤ ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) )
147 66 146 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐺 ‘ ( 𝑀 + 𝑗 ) ) ≤ ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) )
148 0z ⊢ 0 ∈ ℤ
149 23 znegcld ⊢ ( 𝜑 → - 𝑀 ∈ ℤ )
150 60 seqshft ⊢ ( ( 0 ∈ ℤ ∧ - 𝑀 ∈ ℤ ) → seq 0 ( + , ( 𝐺 shift - 𝑀 ) ) = ( seq ( 0 − - 𝑀 ) ( + , 𝐺 ) shift - 𝑀 ) )
151 148 149 150 sylancr ⊢ ( 𝜑 → seq 0 ( + , ( 𝐺 shift - 𝑀 ) ) = ( seq ( 0 − - 𝑀 ) ( + , 𝐺 ) shift - 𝑀 ) )
152 0cn ⊢ 0 ∈ ℂ
153 subneg ⊢ ( ( 0 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 0 − - 𝑀 ) = ( 0 + 𝑀 ) )
154 152 153 mpan ⊢ ( 𝑀 ∈ ℂ → ( 0 − - 𝑀 ) = ( 0 + 𝑀 ) )
155 addlid ⊢ ( 𝑀 ∈ ℂ → ( 0 + 𝑀 ) = 𝑀 )
156 154 155 eqtrd ⊢ ( 𝑀 ∈ ℂ → ( 0 − - 𝑀 ) = 𝑀 )
157 56 156 syl ⊢ ( 𝜑 → ( 0 − - 𝑀 ) = 𝑀 )
158 157 seqeq1d ⊢ ( 𝜑 → seq ( 0 − - 𝑀 ) ( + , 𝐺 ) = seq 𝑀 ( + , 𝐺 ) )
159 158 47 eqbrtrd ⊢ ( 𝜑 → seq ( 0 − - 𝑀 ) ( + , 𝐺 ) ⇝ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐺 ‘ 𝑘 ) )
160 seqex ⊢ seq ( 0 − - 𝑀 ) ( + , 𝐺 ) ∈ V
161 climshft ⊢ ( ( - 𝑀 ∈ ℤ ∧ seq ( 0 − - 𝑀 ) ( + , 𝐺 ) ∈ V ) → ( ( seq ( 0 − - 𝑀 ) ( + , 𝐺 ) shift - 𝑀 ) ⇝ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐺 ‘ 𝑘 ) ↔ seq ( 0 − - 𝑀 ) ( + , 𝐺 ) ⇝ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐺 ‘ 𝑘 ) ) )
162 149 160 161 sylancl ⊢ ( 𝜑 → ( ( seq ( 0 − - 𝑀 ) ( + , 𝐺 ) shift - 𝑀 ) ⇝ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐺 ‘ 𝑘 ) ↔ seq ( 0 − - 𝑀 ) ( + , 𝐺 ) ⇝ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐺 ‘ 𝑘 ) ) )
163 159 162 mpbird ⊢ ( 𝜑 → ( seq ( 0 − - 𝑀 ) ( + , 𝐺 ) shift - 𝑀 ) ⇝ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐺 ‘ 𝑘 ) )
164 ovex ⊢ ( seq ( 0 − - 𝑀 ) ( + , 𝐺 ) shift - 𝑀 ) ∈ V
165 sumex ⊢ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐺 ‘ 𝑘 ) ∈ V
166 164 165 breldm ⊢ ( ( seq ( 0 − - 𝑀 ) ( + , 𝐺 ) shift - 𝑀 ) ⇝ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐺 ‘ 𝑘 ) → ( seq ( 0 − - 𝑀 ) ( + , 𝐺 ) shift - 𝑀 ) ∈ dom ⇝ )
167 163 166 syl ⊢ ( 𝜑 → ( seq ( 0 − - 𝑀 ) ( + , 𝐺 ) shift - 𝑀 ) ∈ dom ⇝ )
168 151 167 eqeltrd ⊢ ( 𝜑 → seq 0 ( + , ( 𝐺 shift - 𝑀 ) ) ∈ dom ⇝ )
169 4 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑀 )
170 1nn ⊢ 1 ∈ ℕ
171 nnleltp1 ⊢ ( ( 1 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 1 ≤ 𝑀 ↔ 1 < ( 𝑀 + 1 ) ) )
172 170 4 171 sylancr ⊢ ( 𝜑 → ( 1 ≤ 𝑀 ↔ 1 < ( 𝑀 + 1 ) ) )
173 169 172 mpbid ⊢ ( 𝜑 → 1 < ( 𝑀 + 1 ) )
174 16 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( 𝑀 + 1 ) )
175 17 174 absidd ⊢ ( 𝜑 → ( abs ‘ ( 𝑀 + 1 ) ) = ( 𝑀 + 1 ) )
176 173 175 breqtrrd ⊢ ( 𝜑 → 1 < ( abs ‘ ( 𝑀 + 1 ) ) )
177 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑛 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑛 ) )
178 ovex ⊢ ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ∈ V
179 71 177 178 fvmpt ⊢ ( 𝑗 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑛 ) ) ‘ 𝑗 ) = ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) )
180 179 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑛 ) ) ‘ 𝑗 ) = ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) )
181 119 176 180 georeclim ⊢ ( 𝜑 → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑛 ) ) ) ⇝ ( ( 𝑀 + 1 ) / ( ( 𝑀 + 1 ) − 1 ) ) )
182 81 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ∈ ℂ )
183 180 182 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑛 ) ) ‘ 𝑗 ) ∈ ℂ )
184 180 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑛 ) ) ‘ 𝑗 ) ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) )
185 75 184 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑗 ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑛 ) ) ‘ 𝑗 ) ) )
186 54 55 127 181 183 185 isermulc2 ⊢ ( 𝜑 → seq 0 ( + , 𝐻 ) ⇝ ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 𝑀 + 1 ) / ( ( 𝑀 + 1 ) − 1 ) ) ) )
187 ax-1cn ⊢ 1 ∈ ℂ
188 pncan ⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
189 56 187 188 sylancl ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
190 189 oveq2d ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) / ( ( 𝑀 + 1 ) − 1 ) ) = ( ( 𝑀 + 1 ) / 𝑀 ) )
191 190 oveq2d ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 𝑀 + 1 ) / ( ( 𝑀 + 1 ) − 1 ) ) ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 𝑀 + 1 ) / 𝑀 ) ) )
192 17 4 nndivred ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) / 𝑀 ) ∈ ℝ )
193 192 recnd ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) / 𝑀 ) ∈ ℂ )
194 114 193 132 135 div23d ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) · ( ( 𝑀 + 1 ) / 𝑀 ) ) / ( ! ‘ 𝑀 ) ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 𝑀 + 1 ) / 𝑀 ) ) )
195 191 194 eqtr4d ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 𝑀 + 1 ) / ( ( 𝑀 + 1 ) − 1 ) ) ) = ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) · ( ( 𝑀 + 1 ) / 𝑀 ) ) / ( ! ‘ 𝑀 ) ) )
196 114 193 132 135 divassd ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) · ( ( 𝑀 + 1 ) / 𝑀 ) ) / ( ! ‘ 𝑀 ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) · ( ( ( 𝑀 + 1 ) / 𝑀 ) / ( ! ‘ 𝑀 ) ) ) )
197 4 nnne0d ⊢ ( 𝜑 → 𝑀 ≠ 0 )
198 119 56 132 197 135 divdiv1d ⊢ ( 𝜑 → ( ( ( 𝑀 + 1 ) / 𝑀 ) / ( ! ‘ 𝑀 ) ) = ( ( 𝑀 + 1 ) / ( 𝑀 · ( ! ‘ 𝑀 ) ) ) )
199 56 132 mulcomd ⊢ ( 𝜑 → ( 𝑀 · ( ! ‘ 𝑀 ) ) = ( ( ! ‘ 𝑀 ) · 𝑀 ) )
200 199 oveq2d ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) / ( 𝑀 · ( ! ‘ 𝑀 ) ) ) = ( ( 𝑀 + 1 ) / ( ( ! ‘ 𝑀 ) · 𝑀 ) ) )
201 198 200 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑀 + 1 ) / 𝑀 ) / ( ! ‘ 𝑀 ) ) = ( ( 𝑀 + 1 ) / ( ( ! ‘ 𝑀 ) · 𝑀 ) ) )
202 201 oveq2d ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) · ( ( ( 𝑀 + 1 ) / 𝑀 ) / ( ! ‘ 𝑀 ) ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) · ( ( 𝑀 + 1 ) / ( ( ! ‘ 𝑀 ) · 𝑀 ) ) ) )
203 195 196 202 3eqtrd ⊢ ( 𝜑 → ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 𝑀 + 1 ) / ( ( 𝑀 + 1 ) − 1 ) ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) · ( ( 𝑀 + 1 ) / ( ( ! ‘ 𝑀 ) · 𝑀 ) ) ) )
204 186 203 breqtrd ⊢ ( 𝜑 → seq 0 ( + , 𝐻 ) ⇝ ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) · ( ( 𝑀 + 1 ) / ( ( ! ‘ 𝑀 ) · 𝑀 ) ) ) )
205 seqex ⊢ seq 0 ( + , 𝐻 ) ∈ V
206 ovex ⊢ ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) · ( ( 𝑀 + 1 ) / ( ( ! ‘ 𝑀 ) · 𝑀 ) ) ) ∈ V
207 205 206 breldm ⊢ ( seq 0 ( + , 𝐻 ) ⇝ ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) · ( ( 𝑀 + 1 ) / ( ( ! ‘ 𝑀 ) · 𝑀 ) ) ) → seq 0 ( + , 𝐻 ) ∈ dom ⇝ )
208 204 207 syl ⊢ ( 𝜑 → seq 0 ( + , 𝐻 ) ∈ dom ⇝ )
209 54 55 62 70 75 82 147 168 208 isumle ⊢ ( 𝜑 → Σ 𝑗 ∈ ℕ0 ( 𝐺 ‘ ( 𝑀 + 𝑗 ) ) ≤ Σ 𝑗 ∈ ℕ0 ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) )
210 eqid ⊢ ( ℤ≥ ‘ ( 0 + 𝑀 ) ) = ( ℤ≥ ‘ ( 0 + 𝑀 ) )
211 fveq2 ⊢ ( 𝑘 = ( 𝑀 + 𝑗 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑀 + 𝑗 ) ) )
212 56 addlidd ⊢ ( 𝜑 → ( 0 + 𝑀 ) = 𝑀 )
213 212 fveq2d ⊢ ( 𝜑 → ( ℤ≥ ‘ ( 0 + 𝑀 ) ) = ( ℤ≥ ‘ 𝑀 ) )
214 213 eleq2d ⊢ ( 𝜑 → ( 𝑘 ∈ ( ℤ≥ ‘ ( 0 + 𝑀 ) ) ↔ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
215 214 biimpa ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 0 + 𝑀 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
216 215 43 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 0 + 𝑀 ) ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
217 54 210 211 23 55 216 isumshft ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 0 + 𝑀 ) ) ( 𝐺 ‘ 𝑘 ) = Σ 𝑗 ∈ ℕ0 ( 𝐺 ‘ ( 𝑀 + 𝑗 ) ) )
218 213 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 0 + 𝑀 ) ) ( 𝐺 ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐺 ‘ 𝑘 ) )
219 217 218 eqtr3d ⊢ ( 𝜑 → Σ 𝑗 ∈ ℕ0 ( 𝐺 ‘ ( 𝑀 + 𝑗 ) ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐺 ‘ 𝑘 ) )
220 82 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) ∈ ℂ )
221 54 55 75 220 204 isumclim ⊢ ( 𝜑 → Σ 𝑗 ∈ ℕ0 ( ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) / ( ! ‘ 𝑀 ) ) · ( ( 1 / ( 𝑀 + 1 ) ) ↑ 𝑗 ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) · ( ( 𝑀 + 1 ) / ( ( ! ‘ 𝑀 ) · 𝑀 ) ) ) )
222 209 219 221 3brtr3d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐺 ‘ 𝑘 ) ≤ ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) · ( ( 𝑀 + 1 ) / ( ( ! ‘ 𝑀 ) · 𝑀 ) ) ) )
223 10 13 21 53 222 letrd ⊢ ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( ( abs ‘ 𝐴 ) ↑ 𝑀 ) · ( ( 𝑀 + 1 ) / ( ( ! ‘ 𝑀 ) · 𝑀 ) ) ) )