abelthlem7

	Ref	Expression
Hypotheses	abelth.1	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
	abelth.2	$⊢ φ \to seq 0 (+ A) \in dom ⇝$
	abelth.3	$⊢ φ \to M \in ℝ$
	abelth.4	$⊢ φ \to 0 \leq M$
	abelth.5	$⊢ S = \{z \in ℂ \| \|1 - z\| \leq M (1 - \|z\|)\}$
	abelth.6	$⊢ F = (x \in S ⟼ \sum_{n \in ℕ_{0}} A (n) x^{n})$
	abelth.7	$⊢ φ \to seq 0 (+ A) ⇝ 0$
	abelthlem6.1	$⊢ φ \to X \in (S ∖ \{1\})$
	abelthlem7.2	$⊢ φ \to R \in ℝ^{+}$
	abelthlem7.3	$⊢ φ \to N \in ℕ_{0}$
	abelthlem7.4	$⊢ φ \to \forall k \in ℤ_{\geq N} \|seq 0 (+ A) (k)\| < R$
	abelthlem7.5	$⊢ φ \to \|1 - X\| < \frac{R}{\sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1}$
Assertion	abelthlem7	$⊢ φ \to \|F (X)\| < (M + 1) R$

Proof

Step	Hyp	Ref	Expression
1		abelth.1	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
2		abelth.2	$⊢ φ \to seq 0 (+ A) \in dom ⇝$
3		abelth.3	$⊢ φ \to M \in ℝ$
4		abelth.4	$⊢ φ \to 0 \leq M$
5		abelth.5	$⊢ S = \{z \in ℂ \| \|1 - z\| \leq M (1 - \|z\|)\}$
6		abelth.6	$⊢ F = (x \in S ⟼ \sum_{n \in ℕ_{0}} A (n) x^{n})$
7		abelth.7	$⊢ φ \to seq 0 (+ A) ⇝ 0$
8		abelthlem6.1	$⊢ φ \to X \in (S ∖ \{1\})$
9		abelthlem7.2	$⊢ φ \to R \in ℝ^{+}$
10		abelthlem7.3	$⊢ φ \to N \in ℕ_{0}$
11		abelthlem7.4	$⊢ φ \to \forall k \in ℤ_{\geq N} \|seq 0 (+ A) (k)\| < R$
12		abelthlem7.5	$⊢ φ \to \|1 - X\| < \frac{R}{\sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1}$
13	1 2 3 4 5 6	abelthlem4	$⊢ φ \to F : S ⟶ ℂ$
14	8	eldifad	$⊢ φ \to X \in S$
15	13 14	ffvelcdmd	$⊢ φ \to F (X) \in ℂ$
16	15	abscld	$⊢ φ \to \|F (X)\| \in ℝ$
17		ax-1cn	$⊢ 1 \in ℂ$
18	1 2 3 4 5 6 7 8	abelthlem7a	$⊢ φ \to (X \in ℂ \land \|1 - X\| \leq M (1 - \|X\|))$
19	18	simpld	$⊢ φ \to X \in ℂ$
20		subcl	$⊢ (1 \in ℂ \land X \in ℂ) \to 1 - X \in ℂ$
21	17 19 20	sylancr	$⊢ φ \to 1 - X \in ℂ$
22		fzfid	$⊢ φ \to (0 \dots N - 1) \in Fin$
23		elfznn0	$⊢ n \in (0 \dots N - 1) \to n \in ℕ_{0}$
24		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
25		0zd	$⊢ φ \to 0 \in ℤ$
26	1	ffvelcdmda	$⊢ (φ \land n \in ℕ_{0}) \to A (n) \in ℂ$
27	24 25 26	serf	$⊢ φ \to seq 0 (+ A) : ℕ_{0} ⟶ ℂ$
28	27	ffvelcdmda	$⊢ (φ \land n \in ℕ_{0}) \to seq 0 (+ A) (n) \in ℂ$
29		expcl	$⊢ (X \in ℂ \land n \in ℕ_{0}) \to X^{n} \in ℂ$
30	19 29	sylan	$⊢ (φ \land n \in ℕ_{0}) \to X^{n} \in ℂ$
31	28 30	mulcld	$⊢ (φ \land n \in ℕ_{0}) \to seq 0 (+ A) (n) X^{n} \in ℂ$
32	23 31	sylan2	$⊢ (φ \land n \in (0 \dots N - 1)) \to seq 0 (+ A) (n) X^{n} \in ℂ$
33	22 32	fsumcl	$⊢ φ \to \sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n} \in ℂ$
34	21 33	mulcld	$⊢ φ \to (1 - X) \sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n} \in ℂ$
35	34	abscld	$⊢ φ \to \|(1 - X) \sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n}\| \in ℝ$
36		eqid	$⊢ ℤ_{\geq N} = ℤ_{\geq N}$
37	10	nn0zd	$⊢ φ \to N \in ℤ$
38		eluznn0	$⊢ (N \in ℕ_{0} \land n \in ℤ_{\geq N}) \to n \in ℕ_{0}$
39	10 38	sylan	$⊢ (φ \land n \in ℤ_{\geq N}) \to n \in ℕ_{0}$
40		fveq2	$⊢ k = n \to seq 0 (+ A) (k) = seq 0 (+ A) (n)$
41		oveq2	$⊢ k = n \to X^{k} = X^{n}$
42	40 41	oveq12d	$⊢ k = n \to seq 0 (+ A) (k) X^{k} = seq 0 (+ A) (n) X^{n}$
43		eqid	$⊢ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) = (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})$
44		ovex	$⊢ seq 0 (+ A) (n) X^{n} \in V$
45	42 43 44	fvmpt	$⊢ n \in ℕ_{0} \to (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (n) = seq 0 (+ A) (n) X^{n}$
46	39 45	syl	$⊢ (φ \land n \in ℤ_{\geq N}) \to (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (n) = seq 0 (+ A) (n) X^{n}$
47	39 31	syldan	$⊢ (φ \land n \in ℤ_{\geq N}) \to seq 0 (+ A) (n) X^{n} \in ℂ$
48	1 2 3 4 5	abelthlem2	$⊢ φ \to (1 \in S \land S ∖ \{1\} \subseteq 0 ball (abs \circ -) 1)$
49	48	simprd	$⊢ φ \to S ∖ \{1\} \subseteq 0 ball (abs \circ -) 1$
50	49 8	sseldd	$⊢ φ \to X \in (0 ball (abs \circ -) 1)$
51	1 2 3 4 5 6 7	abelthlem5	$⊢ (φ \land X \in (0 ball (abs \circ -) 1)) \to seq 0 (+ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})) \in dom ⇝$
52	50 51	mpdan	$⊢ φ \to seq 0 (+ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})) \in dom ⇝$
53	45	adantl	$⊢ (φ \land n \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (n) = seq 0 (+ A) (n) X^{n}$
54	53 31	eqeltrd	$⊢ (φ \land n \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (n) \in ℂ$
55	24 10 54	iserex	$⊢ φ \to (seq 0 (+ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})) \in dom ⇝ \leftrightarrow seq N (+ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})) \in dom ⇝)$
56	52 55	mpbid	$⊢ φ \to seq N (+ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})) \in dom ⇝$
57	36 37 46 47 56	isumcl	$⊢ φ \to \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n} \in ℂ$
58	21 57	mulcld	$⊢ φ \to (1 - X) \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n} \in ℂ$
59	58	abscld	$⊢ φ \to \|(1 - X) \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}\| \in ℝ$
60	35 59	readdcld	$⊢ φ \to \|(1 - X) \sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n}\| + \|(1 - X) \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}\| \in ℝ$
61		peano2re	$⊢ M \in ℝ \to M + 1 \in ℝ$
62	3 61	syl	$⊢ φ \to M + 1 \in ℝ$
63	9	rpred	$⊢ φ \to R \in ℝ$
64	62 63	remulcld	$⊢ φ \to (M + 1) R \in ℝ$
65	1 2 3 4 5 6 7 8	abelthlem6	$⊢ φ \to F (X) = (1 - X) \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n}$
66	24 36 10 53 31 52	isumsplit	$⊢ φ \to \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} = \sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n} + \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}$
67	66	oveq2d	$⊢ φ \to (1 - X) \sum_{n \in ℕ_{0}} seq 0 (+ A) (n) X^{n} = (1 - X) (\sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n} + \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n})$
68	21 33 57	adddid	$⊢ φ \to (1 - X) (\sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n} + \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}) = (1 - X) \sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n} + (1 - X) \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}$
69	65 67 68	3eqtrd	$⊢ φ \to F (X) = (1 - X) \sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n} + (1 - X) \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}$
70	69	fveq2d	$⊢ φ \to \|F (X)\| = \|(1 - X) \sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n} + (1 - X) \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}\|$
71	34 58	abstrid	$⊢ φ \to \|(1 - X) \sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n} + (1 - X) \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}\| \leq \|(1 - X) \sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n}\| + \|(1 - X) \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}\|$
72	70 71	eqbrtrd	$⊢ φ \to \|F (X)\| \leq \|(1 - X) \sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n}\| + \|(1 - X) \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}\|$
73	3 63	remulcld	$⊢ φ \to M R \in ℝ$
74	21	abscld	$⊢ φ \to \|1 - X\| \in ℝ$
75	28	abscld	$⊢ (φ \land n \in ℕ_{0}) \to \|seq 0 (+ A) (n)\| \in ℝ$
76	23 75	sylan2	$⊢ (φ \land n \in (0 \dots N - 1)) \to \|seq 0 (+ A) (n)\| \in ℝ$
77	22 76	fsumrecl	$⊢ φ \to \sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| \in ℝ$
78		peano2re	$⊢ \sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| \in ℝ \to \sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1 \in ℝ$
79	77 78	syl	$⊢ φ \to \sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1 \in ℝ$
80	74 79	remulcld	$⊢ φ \to \|1 - X\| (\sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1) \in ℝ$
81	21 33	absmuld	$⊢ φ \to \|(1 - X) \sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n}\| = \|1 - X\| \|\sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n}\|$
82	33	abscld	$⊢ φ \to \|\sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n}\| \in ℝ$
83	21	absge0d	$⊢ φ \to 0 \leq \|1 - X\|$
84	31	abscld	$⊢ (φ \land n \in ℕ_{0}) \to \|seq 0 (+ A) (n) X^{n}\| \in ℝ$
85	23 84	sylan2	$⊢ (φ \land n \in (0 \dots N - 1)) \to \|seq 0 (+ A) (n) X^{n}\| \in ℝ$
86	22 85	fsumrecl	$⊢ φ \to \sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n) X^{n}\| \in ℝ$
87	22 32	fsumabs	$⊢ φ \to \|\sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n}\| \leq \sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n) X^{n}\|$
88	19	abscld	$⊢ φ \to \|X\| \in ℝ$
89		reexpcl	$⊢ (\|X\| \in ℝ \land n \in ℕ_{0}) \to {\|X\|}^{n} \in ℝ$
90	88 89	sylan	$⊢ (φ \land n \in ℕ_{0}) \to {\|X\|}^{n} \in ℝ$
91		1red	$⊢ (φ \land n \in ℕ_{0}) \to 1 \in ℝ$
92	28	absge0d	$⊢ (φ \land n \in ℕ_{0}) \to 0 \leq \|seq 0 (+ A) (n)\|$
93	88	adantr	$⊢ (φ \land n \in ℕ_{0}) \to \|X\| \in ℝ$
94	19	absge0d	$⊢ φ \to 0 \leq \|X\|$
95	94	adantr	$⊢ (φ \land n \in ℕ_{0}) \to 0 \leq \|X\|$
96		0cn	$⊢ 0 \in ℂ$
97		eqid	$⊢ abs \circ - = abs \circ -$
98	97	cnmetdval	$⊢ (X \in ℂ \land 0 \in ℂ) \to X (abs \circ -) 0 = \|X - 0\|$
99	19 96 98	sylancl	$⊢ φ \to X (abs \circ -) 0 = \|X - 0\|$
100	19	subid1d	$⊢ φ \to X - 0 = X$
101	100	fveq2d	$⊢ φ \to \|X - 0\| = \|X\|$
102	99 101	eqtrd	$⊢ φ \to X (abs \circ -) 0 = \|X\|$
103		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
104		1xr	$⊢ 1 \in ℝ^{*}$
105		elbl3	$⊢ ((abs \circ - \in ∞Met (ℂ) \land 1 \in ℝ^{*}) \land (0 \in ℂ \land X \in ℂ)) \to (X \in (0 ball (abs \circ -) 1) \leftrightarrow X (abs \circ -) 0 < 1)$
106	103 104 105	mpanl12	$⊢ (0 \in ℂ \land X \in ℂ) \to (X \in (0 ball (abs \circ -) 1) \leftrightarrow X (abs \circ -) 0 < 1)$
107	96 19 106	sylancr	$⊢ φ \to (X \in (0 ball (abs \circ -) 1) \leftrightarrow X (abs \circ -) 0 < 1)$
108	50 107	mpbid	$⊢ φ \to X (abs \circ -) 0 < 1$
109	102 108	eqbrtrrd	$⊢ φ \to \|X\| < 1$
110		1re	$⊢ 1 \in ℝ$
111		ltle	$⊢ (\|X\| \in ℝ \land 1 \in ℝ) \to (\|X\| < 1 \to \|X\| \leq 1)$
112	88 110 111	sylancl	$⊢ φ \to (\|X\| < 1 \to \|X\| \leq 1)$
113	109 112	mpd	$⊢ φ \to \|X\| \leq 1$
114	113	adantr	$⊢ (φ \land n \in ℕ_{0}) \to \|X\| \leq 1$
115		simpr	$⊢ (φ \land n \in ℕ_{0}) \to n \in ℕ_{0}$
116		exple1	$⊢ ((\|X\| \in ℝ \land 0 \leq \|X\| \land \|X\| \leq 1) \land n \in ℕ_{0}) \to {\|X\|}^{n} \leq 1$
117	93 95 114 115 116	syl31anc	$⊢ (φ \land n \in ℕ_{0}) \to {\|X\|}^{n} \leq 1$
118	90 91 75 92 117	lemul2ad	$⊢ (φ \land n \in ℕ_{0}) \to \|seq 0 (+ A) (n)\| {\|X\|}^{n} \leq \|seq 0 (+ A) (n)\| \cdot 1$
119	28 30	absmuld	$⊢ (φ \land n \in ℕ_{0}) \to \|seq 0 (+ A) (n) X^{n}\| = \|seq 0 (+ A) (n)\| \|X^{n}\|$
120		absexp	$⊢ (X \in ℂ \land n \in ℕ_{0}) \to \|X^{n}\| = {\|X\|}^{n}$
121	19 120	sylan	$⊢ (φ \land n \in ℕ_{0}) \to \|X^{n}\| = {\|X\|}^{n}$
122	121	oveq2d	$⊢ (φ \land n \in ℕ_{0}) \to \|seq 0 (+ A) (n)\| \|X^{n}\| = \|seq 0 (+ A) (n)\| {\|X\|}^{n}$
123	119 122	eqtr2d	$⊢ (φ \land n \in ℕ_{0}) \to \|seq 0 (+ A) (n)\| {\|X\|}^{n} = \|seq 0 (+ A) (n) X^{n}\|$
124	75	recnd	$⊢ (φ \land n \in ℕ_{0}) \to \|seq 0 (+ A) (n)\| \in ℂ$
125	124	mulridd	$⊢ (φ \land n \in ℕ_{0}) \to \|seq 0 (+ A) (n)\| \cdot 1 = \|seq 0 (+ A) (n)\|$
126	118 123 125	3brtr3d	$⊢ (φ \land n \in ℕ_{0}) \to \|seq 0 (+ A) (n) X^{n}\| \leq \|seq 0 (+ A) (n)\|$
127	23 126	sylan2	$⊢ (φ \land n \in (0 \dots N - 1)) \to \|seq 0 (+ A) (n) X^{n}\| \leq \|seq 0 (+ A) (n)\|$
128	22 85 76 127	fsumle	$⊢ φ \to \sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n) X^{n}\| \leq \sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\|$
129	82 86 77 87 128	letrd	$⊢ φ \to \|\sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n}\| \leq \sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\|$
130	77	ltp1d	$⊢ φ \to \sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| < \sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1$
131	82 77 79 129 130	lelttrd	$⊢ φ \to \|\sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n}\| < \sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1$
132	82 79 131	ltled	$⊢ φ \to \|\sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n}\| \leq \sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1$
133	82 79 74 83 132	lemul2ad	$⊢ φ \to \|1 - X\| \|\sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n}\| \leq \|1 - X\| (\sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1)$
134	81 133	eqbrtrd	$⊢ φ \to \|(1 - X) \sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n}\| \leq \|1 - X\| (\sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1)$
135		0red	$⊢ φ \to 0 \in ℝ$
136	23 92	sylan2	$⊢ (φ \land n \in (0 \dots N - 1)) \to 0 \leq \|seq 0 (+ A) (n)\|$
137	22 76 136	fsumge0	$⊢ φ \to 0 \leq \sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\|$
138	135 77 79 137 130	lelttrd	$⊢ φ \to 0 < \sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1$
139		ltmuldiv	$⊢ (\|1 - X\| \in ℝ \land R \in ℝ \land (\sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1 \in ℝ \land 0 < \sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1)) \to (\|1 - X\| (\sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1) < R \leftrightarrow \|1 - X\| < \frac{R}{\sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1})$
140	74 63 79 138 139	syl112anc	$⊢ φ \to (\|1 - X\| (\sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1) < R \leftrightarrow \|1 - X\| < \frac{R}{\sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1})$
141	12 140	mpbird	$⊢ φ \to \|1 - X\| (\sum_{n = 0}^{N - 1} \|seq 0 (+ A) (n)\| + 1) < R$
142	35 80 63 134 141	lelttrd	$⊢ φ \to \|(1 - X) \sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n}\| < R$
143	21 57	absmuld	$⊢ φ \to \|(1 - X) \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}\| = \|1 - X\| \|\sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}\|$
144	57	abscld	$⊢ φ \to \|\sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}\| \in ℝ$
145	42	fveq2d	$⊢ k = n \to \|seq 0 (+ A) (k) X^{k}\| = \|seq 0 (+ A) (n) X^{n}\|$
146		eqid	$⊢ (k \in ℕ_{0} ⟼ \|seq 0 (+ A) (k) X^{k}\|) = (k \in ℕ_{0} ⟼ \|seq 0 (+ A) (k) X^{k}\|)$
147		fvex	$⊢ \|seq 0 (+ A) (n) X^{n}\| \in V$
148	145 146 147	fvmpt	$⊢ n \in ℕ_{0} \to (k \in ℕ_{0} ⟼ \|seq 0 (+ A) (k) X^{k}\|) (n) = \|seq 0 (+ A) (n) X^{n}\|$
149	39 148	syl	$⊢ (φ \land n \in ℤ_{\geq N}) \to (k \in ℕ_{0} ⟼ \|seq 0 (+ A) (k) X^{k}\|) (n) = \|seq 0 (+ A) (n) X^{n}\|$
150	47	abscld	$⊢ (φ \land n \in ℤ_{\geq N}) \to \|seq 0 (+ A) (n) X^{n}\| \in ℝ$
151		uzid	$⊢ N \in ℤ \to N \in ℤ_{\geq N}$
152	37 151	syl	$⊢ φ \to N \in ℤ_{\geq N}$
153		oveq2	$⊢ k = n \to {\|X\|}^{k} = {\|X\|}^{n}$
154		eqid	$⊢ (k \in ℕ_{0} ⟼ {\|X\|}^{k}) = (k \in ℕ_{0} ⟼ {\|X\|}^{k})$
155		ovex	$⊢ {\|X\|}^{n} \in V$
156	153 154 155	fvmpt	$⊢ n \in ℕ_{0} \to (k \in ℕ_{0} ⟼ {\|X\|}^{k}) (n) = {\|X\|}^{n}$
157	39 156	syl	$⊢ (φ \land n \in ℤ_{\geq N}) \to (k \in ℕ_{0} ⟼ {\|X\|}^{k}) (n) = {\|X\|}^{n}$
158	39 90	syldan	$⊢ (φ \land n \in ℤ_{\geq N}) \to {\|X\|}^{n} \in ℝ$
159	157 158	eqeltrd	$⊢ (φ \land n \in ℤ_{\geq N}) \to (k \in ℕ_{0} ⟼ {\|X\|}^{k}) (n) \in ℝ$
160	150	recnd	$⊢ (φ \land n \in ℤ_{\geq N}) \to \|seq 0 (+ A) (n) X^{n}\| \in ℂ$
161	149 160	eqeltrd	$⊢ (φ \land n \in ℤ_{\geq N}) \to (k \in ℕ_{0} ⟼ \|seq 0 (+ A) (k) X^{k}\|) (n) \in ℂ$
162	88	recnd	$⊢ φ \to \|X\| \in ℂ$
163		absidm	$⊢ X \in ℂ \to \|\|X\|\| = \|X\|$
164	19 163	syl	$⊢ φ \to \|\|X\|\| = \|X\|$
165	164 109	eqbrtrd	$⊢ φ \to \|\|X\|\| < 1$
166	162 165 10 157	geolim2	$⊢ φ \to seq N (+ (k \in ℕ_{0} ⟼ {\|X\|}^{k})) ⇝ (\frac{{\|X\|}^{N}}{1 - \|X\|})$
167		seqex	$⊢ seq N (+ (k \in ℕ_{0} ⟼ {\|X\|}^{k})) \in V$
168		ovex	$⊢ \frac{{\|X\|}^{N}}{1 - \|X\|} \in V$
169	167 168	breldm	$⊢ seq N (+ (k \in ℕ_{0} ⟼ {\|X\|}^{k})) ⇝ (\frac{{\|X\|}^{N}}{1 - \|X\|}) \to seq N (+ (k \in ℕ_{0} ⟼ {\|X\|}^{k})) \in dom ⇝$
170	166 169	syl	$⊢ φ \to seq N (+ (k \in ℕ_{0} ⟼ {\|X\|}^{k})) \in dom ⇝$
171	119 122	eqtrd	$⊢ (φ \land n \in ℕ_{0}) \to \|seq 0 (+ A) (n) X^{n}\| = \|seq 0 (+ A) (n)\| {\|X\|}^{n}$
172	39 171	syldan	$⊢ (φ \land n \in ℤ_{\geq N}) \to \|seq 0 (+ A) (n) X^{n}\| = \|seq 0 (+ A) (n)\| {\|X\|}^{n}$
173	39 75	syldan	$⊢ (φ \land n \in ℤ_{\geq N}) \to \|seq 0 (+ A) (n)\| \in ℝ$
174	63	adantr	$⊢ (φ \land n \in ℤ_{\geq N}) \to R \in ℝ$
175	88	adantr	$⊢ (φ \land n \in ℤ_{\geq N}) \to \|X\| \in ℝ$
176	94	adantr	$⊢ (φ \land n \in ℤ_{\geq N}) \to 0 \leq \|X\|$
177	175 39 176	expge0d	$⊢ (φ \land n \in ℤ_{\geq N}) \to 0 \leq {\|X\|}^{n}$
178	40	fveq2d	$⊢ k = n \to \|seq 0 (+ A) (k)\| = \|seq 0 (+ A) (n)\|$
179	178	breq1d	$⊢ k = n \to (\|seq 0 (+ A) (k)\| < R \leftrightarrow \|seq 0 (+ A) (n)\| < R)$
180	179	rspccva	$⊢ (\forall k \in ℤ_{\geq N} \|seq 0 (+ A) (k)\| < R \land n \in ℤ_{\geq N}) \to \|seq 0 (+ A) (n)\| < R$
181	11 180	sylan	$⊢ (φ \land n \in ℤ_{\geq N}) \to \|seq 0 (+ A) (n)\| < R$
182	173 174 181	ltled	$⊢ (φ \land n \in ℤ_{\geq N}) \to \|seq 0 (+ A) (n)\| \leq R$
183	173 174 158 177 182	lemul1ad	$⊢ (φ \land n \in ℤ_{\geq N}) \to \|seq 0 (+ A) (n)\| {\|X\|}^{n} \leq R {\|X\|}^{n}$
184	172 183	eqbrtrd	$⊢ (φ \land n \in ℤ_{\geq N}) \to \|seq 0 (+ A) (n) X^{n}\| \leq R {\|X\|}^{n}$
185	149	fveq2d	$⊢ (φ \land n \in ℤ_{\geq N}) \to \|(k \in ℕ_{0} ⟼ \|seq 0 (+ A) (k) X^{k}\|) (n)\| = \|\|seq 0 (+ A) (n) X^{n}\|\|$
186		absidm	$⊢ seq 0 (+ A) (n) X^{n} \in ℂ \to \|\|seq 0 (+ A) (n) X^{n}\|\| = \|seq 0 (+ A) (n) X^{n}\|$
187	47 186	syl	$⊢ (φ \land n \in ℤ_{\geq N}) \to \|\|seq 0 (+ A) (n) X^{n}\|\| = \|seq 0 (+ A) (n) X^{n}\|$
188	185 187	eqtrd	$⊢ (φ \land n \in ℤ_{\geq N}) \to \|(k \in ℕ_{0} ⟼ \|seq 0 (+ A) (k) X^{k}\|) (n)\| = \|seq 0 (+ A) (n) X^{n}\|$
189	157	oveq2d	$⊢ (φ \land n \in ℤ_{\geq N}) \to R (k \in ℕ_{0} ⟼ {\|X\|}^{k}) (n) = R {\|X\|}^{n}$
190	184 188 189	3brtr4d	$⊢ (φ \land n \in ℤ_{\geq N}) \to \|(k \in ℕ_{0} ⟼ \|seq 0 (+ A) (k) X^{k}\|) (n)\| \leq R (k \in ℕ_{0} ⟼ {\|X\|}^{k}) (n)$
191	36 152 159 161 170 63 190	cvgcmpce	$⊢ φ \to seq N (+ (k \in ℕ_{0} ⟼ \|seq 0 (+ A) (k) X^{k}\|)) \in dom ⇝$
192	36 37 149 150 191	isumrecl	$⊢ φ \to \sum_{n \in ℤ_{\geq N}} \|seq 0 (+ A) (n) X^{n}\| \in ℝ$
193		eldifsni	$⊢ X \in (S ∖ \{1\}) \to X \neq 1$
194	8 193	syl	$⊢ φ \to X \neq 1$
195	194	necomd	$⊢ φ \to 1 \neq X$
196		subeq0	$⊢ (1 \in ℂ \land X \in ℂ) \to (1 - X = 0 \leftrightarrow 1 = X)$
197	196	necon3bid	$⊢ (1 \in ℂ \land X \in ℂ) \to (1 - X \neq 0 \leftrightarrow 1 \neq X)$
198	17 19 197	sylancr	$⊢ φ \to (1 - X \neq 0 \leftrightarrow 1 \neq X)$
199	195 198	mpbird	$⊢ φ \to 1 - X \neq 0$
200	21 199	absrpcld	$⊢ φ \to \|1 - X\| \in ℝ^{+}$
201	73 200	rerpdivcld	$⊢ φ \to \frac{M R}{\|1 - X\|} \in ℝ$
202	36 37 46 47 56	isumclim2	$⊢ φ \to seq N (+ (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k})) ⇝ \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}$
203	36 37 149 160 191	isumclim2	$⊢ φ \to seq N (+ (k \in ℕ_{0} ⟼ \|seq 0 (+ A) (k) X^{k}\|)) ⇝ \sum_{n \in ℤ_{\geq N}} \|seq 0 (+ A) (n) X^{n}\|$
204	39 54	syldan	$⊢ (φ \land n \in ℤ_{\geq N}) \to (k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (n) \in ℂ$
205	46	fveq2d	$⊢ (φ \land n \in ℤ_{\geq N}) \to \|(k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (n)\| = \|seq 0 (+ A) (n) X^{n}\|$
206	149 205	eqtr4d	$⊢ (φ \land n \in ℤ_{\geq N}) \to (k \in ℕ_{0} ⟼ \|seq 0 (+ A) (k) X^{k}\|) (n) = \|(k \in ℕ_{0} ⟼ seq 0 (+ A) (k) X^{k}) (n)\|$
207	36 202 203 37 204 206	iserabs	$⊢ φ \to \|\sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}\| \leq \sum_{n \in ℤ_{\geq N}} \|seq 0 (+ A) (n) X^{n}\|$
208	88 10	reexpcld	$⊢ φ \to {\|X\|}^{N} \in ℝ$
209		difrp	$⊢ (\|X\| \in ℝ \land 1 \in ℝ) \to (\|X\| < 1 \leftrightarrow 1 - \|X\| \in ℝ^{+})$
210	88 110 209	sylancl	$⊢ φ \to (\|X\| < 1 \leftrightarrow 1 - \|X\| \in ℝ^{+})$
211	109 210	mpbid	$⊢ φ \to 1 - \|X\| \in ℝ^{+}$
212	208 211	rerpdivcld	$⊢ φ \to \frac{{\|X\|}^{N}}{1 - \|X\|} \in ℝ$
213	63 212	remulcld	$⊢ φ \to R (\frac{{\|X\|}^{N}}{1 - \|X\|}) \in ℝ$
214	153	oveq2d	$⊢ k = n \to R {\|X\|}^{k} = R {\|X\|}^{n}$
215		eqid	$⊢ (k \in ℕ_{0} ⟼ R {\|X\|}^{k}) = (k \in ℕ_{0} ⟼ R {\|X\|}^{k})$
216		ovex	$⊢ R {\|X\|}^{n} \in V$
217	214 215 216	fvmpt	$⊢ n \in ℕ_{0} \to (k \in ℕ_{0} ⟼ R {\|X\|}^{k}) (n) = R {\|X\|}^{n}$
218	39 217	syl	$⊢ (φ \land n \in ℤ_{\geq N}) \to (k \in ℕ_{0} ⟼ R {\|X\|}^{k}) (n) = R {\|X\|}^{n}$
219	174 158	remulcld	$⊢ (φ \land n \in ℤ_{\geq N}) \to R {\|X\|}^{n} \in ℝ$
220	9	rpcnd	$⊢ φ \to R \in ℂ$
221	159	recnd	$⊢ (φ \land n \in ℤ_{\geq N}) \to (k \in ℕ_{0} ⟼ {\|X\|}^{k}) (n) \in ℂ$
222	218 189	eqtr4d	$⊢ (φ \land n \in ℤ_{\geq N}) \to (k \in ℕ_{0} ⟼ R {\|X\|}^{k}) (n) = R (k \in ℕ_{0} ⟼ {\|X\|}^{k}) (n)$
223	36 37 220 166 221 222	isermulc2	$⊢ φ \to seq N (+ (k \in ℕ_{0} ⟼ R {\|X\|}^{k})) ⇝ R (\frac{{\|X\|}^{N}}{1 - \|X\|})$
224		seqex	$⊢ seq N (+ (k \in ℕ_{0} ⟼ R {\|X\|}^{k})) \in V$
225		ovex	$⊢ R (\frac{{\|X\|}^{N}}{1 - \|X\|}) \in V$
226	224 225	breldm	$⊢ seq N (+ (k \in ℕ_{0} ⟼ R {\|X\|}^{k})) ⇝ R (\frac{{\|X\|}^{N}}{1 - \|X\|}) \to seq N (+ (k \in ℕ_{0} ⟼ R {\|X\|}^{k})) \in dom ⇝$
227	223 226	syl	$⊢ φ \to seq N (+ (k \in ℕ_{0} ⟼ R {\|X\|}^{k})) \in dom ⇝$
228	36 37 149 150 218 219 184 191 227	isumle	$⊢ φ \to \sum_{n \in ℤ_{\geq N}} \|seq 0 (+ A) (n) X^{n}\| \leq \sum_{n \in ℤ_{\geq N}} R {\|X\|}^{n}$
229	219	recnd	$⊢ (φ \land n \in ℤ_{\geq N}) \to R {\|X\|}^{n} \in ℂ$
230	36 37 218 229 223	isumclim	$⊢ φ \to \sum_{n \in ℤ_{\geq N}} R {\|X\|}^{n} = R (\frac{{\|X\|}^{N}}{1 - \|X\|})$
231	228 230	breqtrd	$⊢ φ \to \sum_{n \in ℤ_{\geq N}} \|seq 0 (+ A) (n) X^{n}\| \leq R (\frac{{\|X\|}^{N}}{1 - \|X\|})$
232	9 211	rpdivcld	$⊢ φ \to \frac{R}{1 - \|X\|} \in ℝ^{+}$
233	232	rpred	$⊢ φ \to \frac{R}{1 - \|X\|} \in ℝ$
234	208	recnd	$⊢ φ \to {\|X\|}^{N} \in ℂ$
235	211	rpcnd	$⊢ φ \to 1 - \|X\| \in ℂ$
236	211	rpne0d	$⊢ φ \to 1 - \|X\| \neq 0$
237	220 234 235 236	div12d	$⊢ φ \to R (\frac{{\|X\|}^{N}}{1 - \|X\|}) = {\|X\|}^{N} (\frac{R}{1 - \|X\|})$
238		1red	$⊢ φ \to 1 \in ℝ$
239	232	rpge0d	$⊢ φ \to 0 \leq \frac{R}{1 - \|X\|}$
240		exple1	$⊢ ((\|X\| \in ℝ \land 0 \leq \|X\| \land \|X\| \leq 1) \land N \in ℕ_{0}) \to {\|X\|}^{N} \leq 1$
241	88 94 113 10 240	syl31anc	$⊢ φ \to {\|X\|}^{N} \leq 1$
242	208 238 233 239 241	lemul1ad	$⊢ φ \to {\|X\|}^{N} (\frac{R}{1 - \|X\|}) \leq 1 (\frac{R}{1 - \|X\|})$
243	232	rpcnd	$⊢ φ \to \frac{R}{1 - \|X\|} \in ℂ$
244	243	mullidd	$⊢ φ \to 1 (\frac{R}{1 - \|X\|}) = \frac{R}{1 - \|X\|}$
245	242 244	breqtrd	$⊢ φ \to {\|X\|}^{N} (\frac{R}{1 - \|X\|}) \leq \frac{R}{1 - \|X\|}$
246	237 245	eqbrtrd	$⊢ φ \to R (\frac{{\|X\|}^{N}}{1 - \|X\|}) \leq \frac{R}{1 - \|X\|}$
247	18	simprd	$⊢ φ \to \|1 - X\| \leq M (1 - \|X\|)$
248		resubcl	$⊢ (1 \in ℝ \land \|X\| \in ℝ) \to 1 - \|X\| \in ℝ$
249	110 88 248	sylancr	$⊢ φ \to 1 - \|X\| \in ℝ$
250	3 249	remulcld	$⊢ φ \to M (1 - \|X\|) \in ℝ$
251	74 250 9	lemul2d	$⊢ φ \to (\|1 - X\| \leq M (1 - \|X\|) \leftrightarrow R \|1 - X\| \leq R M (1 - \|X\|))$
252	247 251	mpbid	$⊢ φ \to R \|1 - X\| \leq R M (1 - \|X\|)$
253	3	recnd	$⊢ φ \to M \in ℂ$
254	220 253 235	mul12d	$⊢ φ \to R M (1 - \|X\|) = M R (1 - \|X\|)$
255	220 235	mulcomd	$⊢ φ \to R (1 - \|X\|) = (1 - \|X\|) R$
256	255	oveq2d	$⊢ φ \to M R (1 - \|X\|) = M (1 - \|X\|) R$
257	253 235 220	mul12d	$⊢ φ \to M (1 - \|X\|) R = (1 - \|X\|) M R$
258	254 256 257	3eqtrd	$⊢ φ \to R M (1 - \|X\|) = (1 - \|X\|) M R$
259	252 258	breqtrd	$⊢ φ \to R \|1 - X\| \leq (1 - \|X\|) M R$
260	249 73	remulcld	$⊢ φ \to (1 - \|X\|) M R \in ℝ$
261	63 260 200	lemuldivd	$⊢ φ \to (R \|1 - X\| \leq (1 - \|X\|) M R \leftrightarrow R \leq \frac{(1 - \|X\|) M R}{\|1 - X\|})$
262	259 261	mpbid	$⊢ φ \to R \leq \frac{(1 - \|X\|) M R}{\|1 - X\|}$
263	73	recnd	$⊢ φ \to M R \in ℂ$
264	74	recnd	$⊢ φ \to \|1 - X\| \in ℂ$
265	200	rpne0d	$⊢ φ \to \|1 - X\| \neq 0$
266	235 263 264 265	divassd	$⊢ φ \to \frac{(1 - \|X\|) M R}{\|1 - X\|} = (1 - \|X\|) (\frac{M R}{\|1 - X\|})$
267	262 266	breqtrd	$⊢ φ \to R \leq (1 - \|X\|) (\frac{M R}{\|1 - X\|})$
268		posdif	$⊢ (\|X\| \in ℝ \land 1 \in ℝ) \to (\|X\| < 1 \leftrightarrow 0 < 1 - \|X\|)$
269	88 110 268	sylancl	$⊢ φ \to (\|X\| < 1 \leftrightarrow 0 < 1 - \|X\|)$
270	109 269	mpbid	$⊢ φ \to 0 < 1 - \|X\|$
271		ledivmul	$⊢ (R \in ℝ \land \frac{M R}{\|1 - X\|} \in ℝ \land (1 - \|X\| \in ℝ \land 0 < 1 - \|X\|)) \to (\frac{R}{1 - \|X\|} \leq \frac{M R}{\|1 - X\|} \leftrightarrow R \leq (1 - \|X\|) (\frac{M R}{\|1 - X\|}))$
272	63 201 249 270 271	syl112anc	$⊢ φ \to (\frac{R}{1 - \|X\|} \leq \frac{M R}{\|1 - X\|} \leftrightarrow R \leq (1 - \|X\|) (\frac{M R}{\|1 - X\|}))$
273	267 272	mpbird	$⊢ φ \to \frac{R}{1 - \|X\|} \leq \frac{M R}{\|1 - X\|}$
274	213 233 201 246 273	letrd	$⊢ φ \to R (\frac{{\|X\|}^{N}}{1 - \|X\|}) \leq \frac{M R}{\|1 - X\|}$
275	192 213 201 231 274	letrd	$⊢ φ \to \sum_{n \in ℤ_{\geq N}} \|seq 0 (+ A) (n) X^{n}\| \leq \frac{M R}{\|1 - X\|}$
276	144 192 201 207 275	letrd	$⊢ φ \to \|\sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}\| \leq \frac{M R}{\|1 - X\|}$
277	144 73 200	lemuldiv2d	$⊢ φ \to (\|1 - X\| \|\sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}\| \leq M R \leftrightarrow \|\sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}\| \leq \frac{M R}{\|1 - X\|})$
278	276 277	mpbird	$⊢ φ \to \|1 - X\| \|\sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}\| \leq M R$
279	143 278	eqbrtrd	$⊢ φ \to \|(1 - X) \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}\| \leq M R$
280	35 59 63 73 142 279	ltleaddd	$⊢ φ \to \|(1 - X) \sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n}\| + \|(1 - X) \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}\| < R + M R$
281		1cnd	$⊢ φ \to 1 \in ℂ$
282	253 281 220	adddird	$⊢ φ \to (M + 1) R = M R + 1 R$
283	220	mullidd	$⊢ φ \to 1 R = R$
284	283	oveq2d	$⊢ φ \to M R + 1 R = M R + R$
285	263 220	addcomd	$⊢ φ \to M R + R = R + M R$
286	282 284 285	3eqtrd	$⊢ φ \to (M + 1) R = R + M R$
287	280 286	breqtrrd	$⊢ φ \to \|(1 - X) \sum_{n = 0}^{N - 1} seq 0 (+ A) (n) X^{n}\| + \|(1 - X) \sum_{n \in ℤ_{\geq N}} seq 0 (+ A) (n) X^{n}\| < (M + 1) R$
288	16 60 64 72 287	lelttrd	$⊢ φ \to \|F (X)\| < (M + 1) R$

Metamath Proof Explorer

Theorem abelthlem7

Proof