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	$⊢ F = (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})$
	eftl.2	$⊢ G = (n \in ℕ_{0} ⟼ \frac{{\|A\|}^{n}}{n!})$
	eftl.3	$⊢ H = (n \in ℕ_{0} ⟼ (\frac{{\|A\|}^{M}}{M!}) {(\frac{1}{M + 1})}^{n})$
	eftl.4	$⊢ φ \to M \in ℕ$
	eftl.5	$⊢ φ \to A \in ℂ$
	eftl.6	$⊢ φ \to \|A\| \leq 1$
Assertion	eftlub	$⊢ φ \to \|\sum_{k \in ℤ_{\geq M}} F (k)\| \leq {\|A\|}^{M} (\frac{M + 1}{M! \cdot M})$

Proof

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

Metamath Proof Explorer

Theorem eftlub

Proof