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 ) / ( ( ! ‘ 𝑀 ) · 𝑀 ) ) ) )