abelthlem8

	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$
Assertion	abelthlem8	$⊢ (φ \land R \in ℝ^{+}) \to \exists w \in ℝ^{+} \forall y \in S (\|1 - y\| < w \to \|F (1) - F (y)\| < 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		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
9		0zd	$⊢ (φ \land R \in ℝ^{+}) \to 0 \in ℤ$
10		id	$⊢ R \in ℝ^{+} \to R \in ℝ^{+}$
11	3 4	ge0p1rpd	$⊢ φ \to M + 1 \in ℝ^{+}$
12		rpdivcl	$⊢ (R \in ℝ^{+} \land M + 1 \in ℝ^{+}) \to \frac{R}{M + 1} \in ℝ^{+}$
13	10 11 12	syl2anr	$⊢ (φ \land R \in ℝ^{+}) \to \frac{R}{M + 1} \in ℝ^{+}$
14		eqidd	$⊢ ((φ \land R \in ℝ^{+}) \land k \in ℕ_{0}) \to seq 0 (+ A) (k) = seq 0 (+ A) (k)$
15	7	adantr	$⊢ (φ \land R \in ℝ^{+}) \to seq 0 (+ A) ⇝ 0$
16	8 9 13 14 15	climi0	$⊢ (φ \land R \in ℝ^{+}) \to \exists j \in ℕ_{0} \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1}$
17	13	adantr	$⊢ ((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \to \frac{R}{M + 1} \in ℝ^{+}$
18		fzfid	$⊢ φ \to (0 \dots j - 1) \in Fin$
19		0zd	$⊢ φ \to 0 \in ℤ$
20	1	ffvelrnda	$⊢ (φ \land w \in ℕ_{0}) \to A (w) \in ℂ$
21	8 19 20	serf	$⊢ φ \to seq 0 (+ A) : ℕ_{0} ⟶ ℂ$
22		elfznn0	$⊢ i \in (0 \dots j - 1) \to i \in ℕ_{0}$
23		ffvelrn	$⊢ (seq 0 (+ A) : ℕ_{0} ⟶ ℂ \land i \in ℕ_{0}) \to seq 0 (+ A) (i) \in ℂ$
24	21 22 23	syl2an	$⊢ (φ \land i \in (0 \dots j - 1)) \to seq 0 (+ A) (i) \in ℂ$
25	24	abscld	$⊢ (φ \land i \in (0 \dots j - 1)) \to \|seq 0 (+ A) (i)\| \in ℝ$
26	18 25	fsumrecl	$⊢ φ \to \sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| \in ℝ$
27	26	ad2antrr	$⊢ ((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \to \sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| \in ℝ$
28	24	absge0d	$⊢ (φ \land i \in (0 \dots j - 1)) \to 0 \leq \|seq 0 (+ A) (i)\|$
29	18 25 28	fsumge0	$⊢ φ \to 0 \leq \sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\|$
30	29	ad2antrr	$⊢ ((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \to 0 \leq \sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\|$
31	27 30	ge0p1rpd	$⊢ ((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \to \sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1 \in ℝ^{+}$
32	17 31	rpdivcld	$⊢ ((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \to \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1} \in ℝ^{+}$
33	1 2 3 4 5	abelthlem2	$⊢ φ \to (1 \in S \land S ∖ \{1\} \subseteq 0 ball (abs \circ -) 1)$
34	33	simpld	$⊢ φ \to 1 \in S$
35		oveq1	$⊢ x = 1 \to x^{n} = 1^{n}$
36		nn0z	$⊢ n \in ℕ_{0} \to n \in ℤ$
37		1exp	$⊢ n \in ℤ \to 1^{n} = 1$
38	36 37	syl	$⊢ n \in ℕ_{0} \to 1^{n} = 1$
39	35 38	sylan9eq	$⊢ (x = 1 \land n \in ℕ_{0}) \to x^{n} = 1$
40	39	oveq2d	$⊢ (x = 1 \land n \in ℕ_{0}) \to A (n) x^{n} = A (n) \cdot 1$
41	40	sumeq2dv	$⊢ x = 1 \to \sum_{n \in ℕ_{0}} A (n) x^{n} = \sum_{n \in ℕ_{0}} A (n) \cdot 1$
42		sumex	$⊢ \sum_{n \in ℕ_{0}} A (n) \cdot 1 \in V$
43	41 6 42	fvmpt	$⊢ 1 \in S \to F (1) = \sum_{n \in ℕ_{0}} A (n) \cdot 1$
44	34 43	syl	$⊢ φ \to F (1) = \sum_{n \in ℕ_{0}} A (n) \cdot 1$
45	1	ffvelrnda	$⊢ (φ \land n \in ℕ_{0}) \to A (n) \in ℂ$
46	45	mulid1d	$⊢ (φ \land n \in ℕ_{0}) \to A (n) \cdot 1 = A (n)$
47	46	eqcomd	$⊢ (φ \land n \in ℕ_{0}) \to A (n) = A (n) \cdot 1$
48	46 45	eqeltrd	$⊢ (φ \land n \in ℕ_{0}) \to A (n) \cdot 1 \in ℂ$
49	8 19 47 48 7	isumclim	$⊢ φ \to \sum_{n \in ℕ_{0}} A (n) \cdot 1 = 0$
50	44 49	eqtrd	$⊢ φ \to F (1) = 0$
51	50	adantr	$⊢ (φ \land y \in S) \to F (1) = 0$
52	51	oveq1d	$⊢ (φ \land y \in S) \to F (1) - F (y) = 0 - F (y)$
53		df-neg	$⊢ - F (y) = 0 - F (y)$
54	52 53	syl6eqr	$⊢ (φ \land y \in S) \to F (1) - F (y) = - F (y)$
55	54	fveq2d	$⊢ (φ \land y \in S) \to \|F (1) - F (y)\| = \|- F (y)\|$
56	1 2 3 4 5 6	abelthlem4	$⊢ φ \to F : S ⟶ ℂ$
57	56	ffvelrnda	$⊢ (φ \land y \in S) \to F (y) \in ℂ$
58	57	absnegd	$⊢ (φ \land y \in S) \to \|- F (y)\| = \|F (y)\|$
59	55 58	eqtrd	$⊢ (φ \land y \in S) \to \|F (1) - F (y)\| = \|F (y)\|$
60	59	adantlr	$⊢ ((φ \land R \in ℝ^{+}) \land y \in S) \to \|F (1) - F (y)\| = \|F (y)\|$
61	60	ad2ant2r	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land (y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1})) \to \|F (1) - F (y)\| = \|F (y)\|$
62		fveq2	$⊢ y = 1 \to F (y) = F (1)$
63	62 50	sylan9eqr	$⊢ (φ \land y = 1) \to F (y) = 0$
64	63	abs00bd	$⊢ (φ \land y = 1) \to \|F (y)\| = 0$
65	64	ad5ant15	$⊢ ((((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land (y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1})) \land y = 1) \to \|F (y)\| = 0$
66		simpllr	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land (y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1})) \to R \in ℝ^{+}$
67	66	rpgt0d	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land (y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1})) \to 0 < R$
68	67	adantr	$⊢ ((((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land (y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1})) \land y = 1) \to 0 < R$
69	65 68	eqbrtrd	$⊢ ((((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land (y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1})) \land y = 1) \to \|F (y)\| < R$
70	1	ad3antrrr	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land ((y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}) \land y \neq 1)) \to A : ℕ_{0} ⟶ ℂ$
71	2	ad3antrrr	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land ((y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}) \land y \neq 1)) \to seq 0 (+ A) \in dom ⇝$
72	3	ad3antrrr	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land ((y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}) \land y \neq 1)) \to M \in ℝ$
73	4	ad3antrrr	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land ((y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}) \land y \neq 1)) \to 0 \leq M$
74	7	ad3antrrr	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land ((y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}) \land y \neq 1)) \to seq 0 (+ A) ⇝ 0$
75		simprll	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land ((y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}) \land y \neq 1)) \to y \in S$
76		simprr	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land ((y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}) \land y \neq 1)) \to y \neq 1$
77		eldifsn	$⊢ y \in (S ∖ \{1\}) \leftrightarrow (y \in S \land y \neq 1)$
78	75 76 77	sylanbrc	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land ((y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}) \land y \neq 1)) \to y \in (S ∖ \{1\})$
79	13	ad2antrr	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land ((y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}) \land y \neq 1)) \to \frac{R}{M + 1} \in ℝ^{+}$
80		simplrl	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land ((y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}) \land y \neq 1)) \to j \in ℕ_{0}$
81		simplrr	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land ((y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}) \land y \neq 1)) \to \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1}$
82		2fveq3	$⊢ k = m \to \|seq 0 (+ A) (k)\| = \|seq 0 (+ A) (m)\|$
83	82	breq1d	$⊢ k = m \to (\|seq 0 (+ A) (k)\| < \frac{R}{M + 1} \leftrightarrow \|seq 0 (+ A) (m)\| < \frac{R}{M + 1})$
84	83	cbvralvw	$⊢ \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1} \leftrightarrow \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < \frac{R}{M + 1}$
85	81 84	sylib	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land ((y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}) \land y \neq 1)) \to \forall m \in ℤ_{\geq j} \|seq 0 (+ A) (m)\| < \frac{R}{M + 1}$
86		simprlr	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land ((y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}) \land y \neq 1)) \to \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}$
87		2fveq3	$⊢ i = n \to \|seq 0 (+ A) (i)\| = \|seq 0 (+ A) (n)\|$
88	87	cbvsumv	$⊢ \sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| = \sum_{n = 0}^{j - 1} \|seq 0 (+ A) (n)\|$
89	88	oveq1i	$⊢ \sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1 = \sum_{n = 0}^{j - 1} \|seq 0 (+ A) (n)\| + 1$
90	89	oveq2i	$⊢ \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1} = \frac{\frac{R}{M + 1}}{\sum_{n = 0}^{j - 1} \|seq 0 (+ A) (n)\| + 1}$
91	86 90	breqtrdi	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land ((y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}) \land y \neq 1)) \to \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{n = 0}^{j - 1} \|seq 0 (+ A) (n)\| + 1}$
92	70 71 72 73 5 6 74 78 79 80 85 91	abelthlem7	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land ((y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}) \land y \neq 1)) \to \|F (y)\| < (M + 1) (\frac{R}{M + 1})$
93		rpcn	$⊢ R \in ℝ^{+} \to R \in ℂ$
94	93	adantl	$⊢ (φ \land R \in ℝ^{+}) \to R \in ℂ$
95	11	adantr	$⊢ (φ \land R \in ℝ^{+}) \to M + 1 \in ℝ^{+}$
96	95	rpcnd	$⊢ (φ \land R \in ℝ^{+}) \to M + 1 \in ℂ$
97	95	rpne0d	$⊢ (φ \land R \in ℝ^{+}) \to M + 1 \neq 0$
98	94 96 97	divcan2d	$⊢ (φ \land R \in ℝ^{+}) \to (M + 1) (\frac{R}{M + 1}) = R$
99	98	ad2antrr	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land ((y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}) \land y \neq 1)) \to (M + 1) (\frac{R}{M + 1}) = R$
100	92 99	breqtrd	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land ((y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1}) \land y \neq 1)) \to \|F (y)\| < R$
101	100	anassrs	$⊢ ((((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land (y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1})) \land y \neq 1) \to \|F (y)\| < R$
102	69 101	pm2.61dane	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land (y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1})) \to \|F (y)\| < R$
103	61 102	eqbrtrd	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land (y \in S \land \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1})) \to \|F (1) - F (y)\| < R$
104	103	expr	$⊢ (((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \land y \in S) \to (\|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1} \to \|F (1) - F (y)\| < R)$
105	104	ralrimiva	$⊢ ((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \to \forall y \in S (\|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1} \to \|F (1) - F (y)\| < R)$
106		breq2	$⊢ w = \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1} \to (\|1 - y\| < w \leftrightarrow \|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1})$
107	106	rspceaimv	$⊢ (\frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1} \in ℝ^{+} \land \forall y \in S (\|1 - y\| < \frac{\frac{R}{M + 1}}{\sum_{i = 0}^{j - 1} \|seq 0 (+ A) (i)\| + 1} \to \|F (1) - F (y)\| < R)) \to \exists w \in ℝ^{+} \forall y \in S (\|1 - y\| < w \to \|F (1) - F (y)\| < R)$
108	32 105 107	syl2anc	$⊢ ((φ \land R \in ℝ^{+}) \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|seq 0 (+ A) (k)\| < \frac{R}{M + 1})) \to \exists w \in ℝ^{+} \forall y \in S (\|1 - y\| < w \to \|F (1) - F (y)\| < R)$
109	16 108	rexlimddv	$⊢ (φ \land R \in ℝ^{+}) \to \exists w \in ℝ^{+} \forall y \in S (\|1 - y\| < w \to \|F (1) - F (y)\| < R)$

Metamath Proof Explorer

Theorem abelthlem8

Proof