mertenslem1

	Ref	Expression
Hypotheses	mertens.1	$⊢ (φ \land j \in ℕ_{0}) \to F (j) = A$
	mertens.2	$⊢ (φ \land j \in ℕ_{0}) \to K (j) = \|A\|$
	mertens.3	$⊢ (φ \land j \in ℕ_{0}) \to A \in ℂ$
	mertens.4	$⊢ (φ \land k \in ℕ_{0}) \to G (k) = B$
	mertens.5	$⊢ (φ \land k \in ℕ_{0}) \to B \in ℂ$
	mertens.6	$⊢ (φ \land k \in ℕ_{0}) \to H (k) = \sum_{j = 0}^{k} A G (k - j)$
	mertens.7	$⊢ φ \to seq 0 (+ K) \in dom ⇝$
	mertens.8	$⊢ φ \to seq 0 (+ G) \in dom ⇝$
	mertens.9	$⊢ φ \to E \in ℝ^{+}$
	mertens.10	$⊢ T = \{z \| \exists n \in (0 \dots s - 1) z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|\}$
	mertens.11	$⊢ ψ \leftrightarrow (s \in ℕ \land \forall n \in ℤ_{\geq s} \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
	mertens.12	$⊢ φ \to (ψ \land (t \in ℕ_{0} \land \forall m \in ℤ_{\geq t} K (m) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}))$
	mertens.13	$⊢ φ \to (0 \leq sup (T ℝ <) \land (T \subseteq ℝ \land T \neq \emptyset \land \exists z \in ℝ \forall w \in T w \leq z))$
Assertion	mertenslem1	$⊢ φ \to \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E$

Proof

Step	Hyp	Ref	Expression
1		mertens.1	$⊢ (φ \land j \in ℕ_{0}) \to F (j) = A$
2		mertens.2	$⊢ (φ \land j \in ℕ_{0}) \to K (j) = \|A\|$
3		mertens.3	$⊢ (φ \land j \in ℕ_{0}) \to A \in ℂ$
4		mertens.4	$⊢ (φ \land k \in ℕ_{0}) \to G (k) = B$
5		mertens.5	$⊢ (φ \land k \in ℕ_{0}) \to B \in ℂ$
6		mertens.6	$⊢ (φ \land k \in ℕ_{0}) \to H (k) = \sum_{j = 0}^{k} A G (k - j)$
7		mertens.7	$⊢ φ \to seq 0 (+ K) \in dom ⇝$
8		mertens.8	$⊢ φ \to seq 0 (+ G) \in dom ⇝$
9		mertens.9	$⊢ φ \to E \in ℝ^{+}$
10		mertens.10	$⊢ T = \{z \| \exists n \in (0 \dots s - 1) z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|\}$
11		mertens.11	$⊢ ψ \leftrightarrow (s \in ℕ \land \forall n \in ℤ_{\geq s} \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
12		mertens.12	$⊢ φ \to (ψ \land (t \in ℕ_{0} \land \forall m \in ℤ_{\geq t} K (m) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}))$
13		mertens.13	$⊢ φ \to (0 \leq sup (T ℝ <) \land (T \subseteq ℝ \land T \neq \emptyset \land \exists z \in ℝ \forall w \in T w \leq z))$
14	12	simpld	$⊢ φ \to ψ$
15	14 11	sylib	$⊢ φ \to (s \in ℕ \land \forall n \in ℤ_{\geq s} \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
16	15	simpld	$⊢ φ \to s \in ℕ$
17	16	nnnn0d	$⊢ φ \to s \in ℕ_{0}$
18	12	simprd	$⊢ φ \to (t \in ℕ_{0} \land \forall m \in ℤ_{\geq t} K (m) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})$
19	18	simpld	$⊢ φ \to t \in ℕ_{0}$
20	17 19	nn0addcld	$⊢ φ \to s + t \in ℕ_{0}$
21		fzfid	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (0 \dots m) \in Fin$
22		simpl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to φ$
23		elfznn0	$⊢ j \in (0 \dots m) \to j \in ℕ_{0}$
24	22 23 3	syl2an	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \to A \in ℂ$
25		eqid	$⊢ ℤ_{\geq (m - j + 1)} = ℤ_{\geq (m - j + 1)}$
26		fznn0sub	$⊢ j \in (0 \dots m) \to m - j \in ℕ_{0}$
27	26	adantl	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \to m - j \in ℕ_{0}$
28		peano2nn0	$⊢ m - j \in ℕ_{0} \to m - j + 1 \in ℕ_{0}$
29	27 28	syl	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \to m - j + 1 \in ℕ_{0}$
30	29	nn0zd	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \to m - j + 1 \in ℤ$
31		simplll	$⊢ (((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \land k \in ℤ_{\geq (m - j + 1)}) \to φ$
32		eluznn0	$⊢ (m - j + 1 \in ℕ_{0} \land k \in ℤ_{\geq (m - j + 1)}) \to k \in ℕ_{0}$
33	29 32	sylan	$⊢ (((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \land k \in ℤ_{\geq (m - j + 1)}) \to k \in ℕ_{0}$
34	31 33 4	syl2anc	$⊢ (((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \land k \in ℤ_{\geq (m - j + 1)}) \to G (k) = B$
35	31 33 5	syl2anc	$⊢ (((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \land k \in ℤ_{\geq (m - j + 1)}) \to B \in ℂ$
36	8	ad2antrr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \to seq 0 (+ G) \in dom ⇝$
37		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
38		simpll	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \to φ$
39	4 5	eqeltrd	$⊢ (φ \land k \in ℕ_{0}) \to G (k) \in ℂ$
40	38 39	sylan	$⊢ (((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \land k \in ℕ_{0}) \to G (k) \in ℂ$
41	37 29 40	iserex	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \to (seq 0 (+ G) \in dom ⇝ \leftrightarrow seq (m - j + 1) (+ G) \in dom ⇝)$
42	36 41	mpbid	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \to seq (m - j + 1) (+ G) \in dom ⇝$
43	25 30 34 35 42	isumcl	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \to \sum_{k \in ℤ_{\geq (m - j + 1)}} B \in ℂ$
44	24 43	mulcld	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \to A \sum_{k \in ℤ_{\geq (m - j + 1)}} B \in ℂ$
45	21 44	fsumcl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B \in ℂ$
46	45	abscld	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in ℝ$
47	44	abscld	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \to \|A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in ℝ$
48	21 47	fsumrecl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m} \|A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in ℝ$
49	9	rpred	$⊢ φ \to E \in ℝ$
50	49	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to E \in ℝ$
51	21 44	fsumabs	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \leq \sum_{j = 0}^{m} \|A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\|$
52		fzfid	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (0 \dots m - s) \in Fin$
53	17	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to s \in ℕ_{0}$
54	53	nn0ge0d	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to 0 \leq s$
55		eluzelz	$⊢ m \in ℤ_{\geq (s + t)} \to m \in ℤ$
56	55	adantl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to m \in ℤ$
57	56	zred	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to m \in ℝ$
58	53	nn0red	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to s \in ℝ$
59	57 58	subge02d	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (0 \leq s \leftrightarrow m - s \leq m)$
60	54 59	mpbid	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to m - s \leq m$
61	53 37	eleqtrdi	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to s \in ℤ_{\geq 0}$
62	16	nnzd	$⊢ φ \to s \in ℤ$
63		uzid	$⊢ s \in ℤ \to s \in ℤ_{\geq s}$
64	62 63	syl	$⊢ φ \to s \in ℤ_{\geq s}$
65		uzaddcl	$⊢ (s \in ℤ_{\geq s} \land t \in ℕ_{0}) \to s + t \in ℤ_{\geq s}$
66	64 19 65	syl2anc	$⊢ φ \to s + t \in ℤ_{\geq s}$
67		eqid	$⊢ ℤ_{\geq s} = ℤ_{\geq s}$
68	67	uztrn2	$⊢ (s + t \in ℤ_{\geq s} \land m \in ℤ_{\geq (s + t)}) \to m \in ℤ_{\geq s}$
69	66 68	sylan	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to m \in ℤ_{\geq s}$
70		elfzuzb	$⊢ s \in (0 \dots m) \leftrightarrow (s \in ℤ_{\geq 0} \land m \in ℤ_{\geq s})$
71	61 69 70	sylanbrc	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to s \in (0 \dots m)$
72		fznn0sub2	$⊢ s \in (0 \dots m) \to m - s \in (0 \dots m)$
73	71 72	syl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to m - s \in (0 \dots m)$
74		elfzelz	$⊢ m - s \in (0 \dots m) \to m - s \in ℤ$
75	73 74	syl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to m - s \in ℤ$
76		eluz	$⊢ (m - s \in ℤ \land m \in ℤ) \to (m \in ℤ_{\geq (m - s)} \leftrightarrow m - s \leq m)$
77	75 56 76	syl2anc	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (m \in ℤ_{\geq (m - s)} \leftrightarrow m - s \leq m)$
78	60 77	mpbird	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to m \in ℤ_{\geq (m - s)}$
79		fzss2	$⊢ m \in ℤ_{\geq (m - s)} \to (0 \dots m - s) \subseteq (0 \dots m)$
80	78 79	syl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (0 \dots m - s) \subseteq (0 \dots m)$
81	80	sselda	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to j \in (0 \dots m)$
82	3	abscld	$⊢ (φ \land j \in ℕ_{0}) \to \|A\| \in ℝ$
83	22 23 82	syl2an	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \to \|A\| \in ℝ$
84	43	abscld	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \to \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in ℝ$
85	83 84	remulcld	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \to \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in ℝ$
86	81 85	syldan	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in ℝ$
87	52 86	fsumrecl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m - s} \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in ℝ$
88		fzfid	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (m - s + 1 \dots m) \in Fin$
89		elfznn0	$⊢ m - s \in (0 \dots m) \to m - s \in ℕ_{0}$
90	73 89	syl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to m - s \in ℕ_{0}$
91		peano2nn0	$⊢ m - s \in ℕ_{0} \to m - s + 1 \in ℕ_{0}$
92	90 91	syl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to m - s + 1 \in ℕ_{0}$
93	92 37	eleqtrdi	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to m - s + 1 \in ℤ_{\geq 0}$
94		fzss1	$⊢ m - s + 1 \in ℤ_{\geq 0} \to (m - s + 1 \dots m) \subseteq (0 \dots m)$
95	93 94	syl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (m - s + 1 \dots m) \subseteq (0 \dots m)$
96	95	sselda	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to j \in (0 \dots m)$
97	96 85	syldan	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in ℝ$
98	88 97	fsumrecl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = m - s + 1}^{m} \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in ℝ$
99	9	rphalfcld	$⊢ φ \to \frac{E}{2} \in ℝ^{+}$
100	99	rpred	$⊢ φ \to \frac{E}{2} \in ℝ$
101	100	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \frac{E}{2} \in ℝ$
102		elfznn0	$⊢ j \in (0 \dots m - s) \to j \in ℕ_{0}$
103	22 102 82	syl2an	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to \|A\| \in ℝ$
104	52 103	fsumrecl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m - s} \|A\| \in ℝ$
105	104 101	remulcld	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m - s} \|A\| (\frac{E}{2}) \in ℝ$
106		0zd	$⊢ φ \to 0 \in ℤ$
107		eqidd	$⊢ (φ \land j \in ℕ_{0}) \to K (j) = K (j)$
108	2 82	eqeltrd	$⊢ (φ \land j \in ℕ_{0}) \to K (j) \in ℝ$
109	37 106 107 108 7	isumrecl	$⊢ φ \to \sum_{j \in ℕ_{0}} K (j) \in ℝ$
110	3	absge0d	$⊢ (φ \land j \in ℕ_{0}) \to 0 \leq \|A\|$
111	110 2	breqtrrd	$⊢ (φ \land j \in ℕ_{0}) \to 0 \leq K (j)$
112	37 106 107 108 7 111	isumge0	$⊢ φ \to 0 \leq \sum_{j \in ℕ_{0}} K (j)$
113	109 112	ge0p1rpd	$⊢ φ \to \sum_{j \in ℕ_{0}} K (j) + 1 \in ℝ^{+}$
114	113	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j \in ℕ_{0}} K (j) + 1 \in ℝ^{+}$
115	105 114	rerpdivcld	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \frac{\sum_{j = 0}^{m - s} \|A\| (\frac{E}{2})}{\sum_{j \in ℕ_{0}} K (j) + 1} \in ℝ$
116	99 113	rpdivcld	$⊢ φ \to \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1} \in ℝ^{+}$
117	116	rpred	$⊢ φ \to \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1} \in ℝ$
118	117	ad2antrr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1} \in ℝ$
119	103 118	remulcld	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to \|A\| (\frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1}) \in ℝ$
120	81 30	syldan	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to m - j + 1 \in ℤ$
121		simplll	$⊢ (((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \land k \in ℤ_{\geq (m - j + 1)}) \to φ$
122	81 29	syldan	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to m - j + 1 \in ℕ_{0}$
123	122 32	sylan	$⊢ (((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \land k \in ℤ_{\geq (m - j + 1)}) \to k \in ℕ_{0}$
124	121 123 4	syl2anc	$⊢ (((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \land k \in ℤ_{\geq (m - j + 1)}) \to G (k) = B$
125	121 123 5	syl2anc	$⊢ (((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \land k \in ℤ_{\geq (m - j + 1)}) \to B \in ℂ$
126	81 42	syldan	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to seq (m - j + 1) (+ G) \in dom ⇝$
127	25 120 124 125 126	isumcl	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to \sum_{k \in ℤ_{\geq (m - j + 1)}} B \in ℂ$
128	127	abscld	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in ℝ$
129	82 110	jca	$⊢ (φ \land j \in ℕ_{0}) \to (\|A\| \in ℝ \land 0 \leq \|A\|)$
130	22 102 129	syl2an	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to (\|A\| \in ℝ \land 0 \leq \|A\|)$
131	124	sumeq2dv	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to \sum_{k \in ℤ_{\geq (m - j + 1)}} G (k) = \sum_{k \in ℤ_{\geq (m - j + 1)}} B$
132	131	fveq2d	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to \|\sum_{k \in ℤ_{\geq (m - j + 1)}} G (k)\| = \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\|$
133		fvoveq1	$⊢ n = m - j \to ℤ_{\geq (n + 1)} = ℤ_{\geq (m - j + 1)}$
134	133	sumeq1d	$⊢ n = m - j \to \sum_{k \in ℤ_{\geq (n + 1)}} G (k) = \sum_{k \in ℤ_{\geq (m - j + 1)}} G (k)$
135	134	fveq2d	$⊢ n = m - j \to \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| = \|\sum_{k \in ℤ_{\geq (m - j + 1)}} G (k)\|$
136	135	breq1d	$⊢ n = m - j \to (\|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1} \leftrightarrow \|\sum_{k \in ℤ_{\geq (m - j + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
137	15	simprd	$⊢ φ \to \forall n \in ℤ_{\geq s} \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1}$
138	137	ad2antrr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to \forall n \in ℤ_{\geq s} \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1}$
139		elfzelz	$⊢ j \in (0 \dots m - s) \to j \in ℤ$
140	139	adantl	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to j \in ℤ$
141	140	zred	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to j \in ℝ$
142	55	ad2antlr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to m \in ℤ$
143	142	zred	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to m \in ℝ$
144	62	ad2antrr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to s \in ℤ$
145	144	zred	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to s \in ℝ$
146		elfzle2	$⊢ j \in (0 \dots m - s) \to j \leq m - s$
147	146	adantl	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to j \leq m - s$
148	141 143 145 147	lesubd	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to s \leq m - j$
149	142 140	zsubcld	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to m - j \in ℤ$
150		eluz	$⊢ (s \in ℤ \land m - j \in ℤ) \to (m - j \in ℤ_{\geq s} \leftrightarrow s \leq m - j)$
151	144 149 150	syl2anc	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to (m - j \in ℤ_{\geq s} \leftrightarrow s \leq m - j)$
152	148 151	mpbird	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to m - j \in ℤ_{\geq s}$
153	136 138 152	rspcdva	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to \|\sum_{k \in ℤ_{\geq (m - j + 1)}} G (k)\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1}$
154	132 153	eqbrtrrd	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1}$
155	128 118 154	ltled	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \leq \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1}$
156		lemul2a	$⊢ ((\|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in ℝ \land \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1} \in ℝ \land (\|A\| \in ℝ \land 0 \leq \|A\|)) \land \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \leq \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1}) \to \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \leq \|A\| (\frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
157	128 118 130 155 156	syl31anc	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \leq \|A\| (\frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
158	52 86 119 157	fsumle	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m - s} \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \leq \sum_{j = 0}^{m - s} \|A\| (\frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
159	104	recnd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m - s} \|A\| \in ℂ$
160	99	rpcnd	$⊢ φ \to \frac{E}{2} \in ℂ$
161	160	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \frac{E}{2} \in ℂ$
162		peano2re	$⊢ \sum_{j \in ℕ_{0}} K (j) \in ℝ \to \sum_{j \in ℕ_{0}} K (j) + 1 \in ℝ$
163	109 162	syl	$⊢ φ \to \sum_{j \in ℕ_{0}} K (j) + 1 \in ℝ$
164	163	recnd	$⊢ φ \to \sum_{j \in ℕ_{0}} K (j) + 1 \in ℂ$
165	164	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j \in ℕ_{0}} K (j) + 1 \in ℂ$
166	113	rpne0d	$⊢ φ \to \sum_{j \in ℕ_{0}} K (j) + 1 \neq 0$
167	166	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j \in ℕ_{0}} K (j) + 1 \neq 0$
168	159 161 165 167	divassd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \frac{\sum_{j = 0}^{m - s} \|A\| (\frac{E}{2})}{\sum_{j \in ℕ_{0}} K (j) + 1} = \sum_{j = 0}^{m - s} \|A\| (\frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
169		fveq2	$⊢ n = j \to K (n) = K (j)$
170	169	cbvsumv	$⊢ \sum_{n \in ℕ_{0}} K (n) = \sum_{j \in ℕ_{0}} K (j)$
171	170	oveq1i	$⊢ \sum_{n \in ℕ_{0}} K (n) + 1 = \sum_{j \in ℕ_{0}} K (j) + 1$
172	171	oveq2i	$⊢ \frac{\frac{E}{2}}{\sum_{n \in ℕ_{0}} K (n) + 1} = \frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1}$
173	172 116	eqeltrid	$⊢ φ \to \frac{\frac{E}{2}}{\sum_{n \in ℕ_{0}} K (n) + 1} \in ℝ^{+}$
174	173	rpcnd	$⊢ φ \to \frac{\frac{E}{2}}{\sum_{n \in ℕ_{0}} K (n) + 1} \in ℂ$
175	174	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \frac{\frac{E}{2}}{\sum_{n \in ℕ_{0}} K (n) + 1} \in ℂ$
176	82	recnd	$⊢ (φ \land j \in ℕ_{0}) \to \|A\| \in ℂ$
177	22 102 176	syl2an	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m - s)) \to \|A\| \in ℂ$
178	52 175 177	fsummulc1	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m - s} \|A\| (\frac{\frac{E}{2}}{\sum_{n \in ℕ_{0}} K (n) + 1}) = \sum_{j = 0}^{m - s} \|A\| (\frac{\frac{E}{2}}{\sum_{n \in ℕ_{0}} K (n) + 1})$
179	172	oveq2i	$⊢ \sum_{j = 0}^{m - s} \|A\| (\frac{\frac{E}{2}}{\sum_{n \in ℕ_{0}} K (n) + 1}) = \sum_{j = 0}^{m - s} \|A\| (\frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
180	172	oveq2i	$⊢ \|A\| (\frac{\frac{E}{2}}{\sum_{n \in ℕ_{0}} K (n) + 1}) = \|A\| (\frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
181	180	a1i	$⊢ j \in (0 \dots m - s) \to \|A\| (\frac{\frac{E}{2}}{\sum_{n \in ℕ_{0}} K (n) + 1}) = \|A\| (\frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
182	181	sumeq2i	$⊢ \sum_{j = 0}^{m - s} \|A\| (\frac{\frac{E}{2}}{\sum_{n \in ℕ_{0}} K (n) + 1}) = \sum_{j = 0}^{m - s} \|A\| (\frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
183	178 179 182	3eqtr3g	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m - s} \|A\| (\frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1}) = \sum_{j = 0}^{m - s} \|A\| (\frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
184	168 183	eqtrd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \frac{\sum_{j = 0}^{m - s} \|A\| (\frac{E}{2})}{\sum_{j \in ℕ_{0}} K (j) + 1} = \sum_{j = 0}^{m - s} \|A\| (\frac{\frac{E}{2}}{\sum_{j \in ℕ_{0}} K (j) + 1})$
185	158 184	breqtrrd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m - s} \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \leq \frac{\sum_{j = 0}^{m - s} \|A\| (\frac{E}{2})}{\sum_{j \in ℕ_{0}} K (j) + 1}$
186	109	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j \in ℕ_{0}} K (j) \in ℝ$
187	163	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j \in ℕ_{0}} K (j) + 1 \in ℝ$
188		0zd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to 0 \in ℤ$
189		fz0ssnn0	$⊢ (0 \dots m - s) \subseteq ℕ_{0}$
190	189	a1i	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (0 \dots m - s) \subseteq ℕ_{0}$
191	2	adantlr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in ℕ_{0}) \to K (j) = \|A\|$
192	82	adantlr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in ℕ_{0}) \to \|A\| \in ℝ$
193	110	adantlr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in ℕ_{0}) \to 0 \leq \|A\|$
194	7	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to seq 0 (+ K) \in dom ⇝$
195	37 188 52 190 191 192 193 194	isumless	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m - s} \|A\| \leq \sum_{j \in ℕ_{0}} \|A\|$
196	2	sumeq2dv	$⊢ φ \to \sum_{j \in ℕ_{0}} K (j) = \sum_{j \in ℕ_{0}} \|A\|$
197	196	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j \in ℕ_{0}} K (j) = \sum_{j \in ℕ_{0}} \|A\|$
198	195 197	breqtrrd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m - s} \|A\| \leq \sum_{j \in ℕ_{0}} K (j)$
199	109	ltp1d	$⊢ φ \to \sum_{j \in ℕ_{0}} K (j) < \sum_{j \in ℕ_{0}} K (j) + 1$
200	199	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j \in ℕ_{0}} K (j) < \sum_{j \in ℕ_{0}} K (j) + 1$
201	104 186 187 198 200	lelttrd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m - s} \|A\| < \sum_{j \in ℕ_{0}} K (j) + 1$
202	99	rpregt0d	$⊢ φ \to (\frac{E}{2} \in ℝ \land 0 < \frac{E}{2})$
203	202	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (\frac{E}{2} \in ℝ \land 0 < \frac{E}{2})$
204		ltmul1	$⊢ (\sum_{j = 0}^{m - s} \|A\| \in ℝ \land \sum_{j \in ℕ_{0}} K (j) + 1 \in ℝ \land (\frac{E}{2} \in ℝ \land 0 < \frac{E}{2})) \to (\sum_{j = 0}^{m - s} \|A\| < \sum_{j \in ℕ_{0}} K (j) + 1 \leftrightarrow \sum_{j = 0}^{m - s} \|A\| (\frac{E}{2}) < (\sum_{j \in ℕ_{0}} K (j) + 1) (\frac{E}{2}))$
205	104 187 203 204	syl3anc	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (\sum_{j = 0}^{m - s} \|A\| < \sum_{j \in ℕ_{0}} K (j) + 1 \leftrightarrow \sum_{j = 0}^{m - s} \|A\| (\frac{E}{2}) < (\sum_{j \in ℕ_{0}} K (j) + 1) (\frac{E}{2}))$
206	201 205	mpbid	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m - s} \|A\| (\frac{E}{2}) < (\sum_{j \in ℕ_{0}} K (j) + 1) (\frac{E}{2})$
207	113	rpregt0d	$⊢ φ \to (\sum_{j \in ℕ_{0}} K (j) + 1 \in ℝ \land 0 < \sum_{j \in ℕ_{0}} K (j) + 1)$
208	207	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (\sum_{j \in ℕ_{0}} K (j) + 1 \in ℝ \land 0 < \sum_{j \in ℕ_{0}} K (j) + 1)$
209		ltdivmul	$⊢ (\sum_{j = 0}^{m - s} \|A\| (\frac{E}{2}) \in ℝ \land \frac{E}{2} \in ℝ \land (\sum_{j \in ℕ_{0}} K (j) + 1 \in ℝ \land 0 < \sum_{j \in ℕ_{0}} K (j) + 1)) \to (\frac{\sum_{j = 0}^{m - s} \|A\| (\frac{E}{2})}{\sum_{j \in ℕ_{0}} K (j) + 1} < \frac{E}{2} \leftrightarrow \sum_{j = 0}^{m - s} \|A\| (\frac{E}{2}) < (\sum_{j \in ℕ_{0}} K (j) + 1) (\frac{E}{2}))$
210	105 101 208 209	syl3anc	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (\frac{\sum_{j = 0}^{m - s} \|A\| (\frac{E}{2})}{\sum_{j \in ℕ_{0}} K (j) + 1} < \frac{E}{2} \leftrightarrow \sum_{j = 0}^{m - s} \|A\| (\frac{E}{2}) < (\sum_{j \in ℕ_{0}} K (j) + 1) (\frac{E}{2}))$
211	206 210	mpbird	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \frac{\sum_{j = 0}^{m - s} \|A\| (\frac{E}{2})}{\sum_{j \in ℕ_{0}} K (j) + 1} < \frac{E}{2}$
212	87 115 101 185 211	lelttrd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m - s} \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < \frac{E}{2}$
213	13	simprd	$⊢ φ \to (T \subseteq ℝ \land T \neq \emptyset \land \exists z \in ℝ \forall w \in T w \leq z)$
214		suprcl	$⊢ (T \subseteq ℝ \land T \neq \emptyset \land \exists z \in ℝ \forall w \in T w \leq z) \to sup (T ℝ <) \in ℝ$
215	213 214	syl	$⊢ φ \to sup (T ℝ <) \in ℝ$
216	100 215	remulcld	$⊢ φ \to (\frac{E}{2}) sup (T ℝ <) \in ℝ$
217	13	simpld	$⊢ φ \to 0 \leq sup (T ℝ <)$
218	215 217	ge0p1rpd	$⊢ φ \to sup (T ℝ <) + 1 \in ℝ^{+}$
219	216 218	rerpdivcld	$⊢ φ \to \frac{(\frac{E}{2}) sup (T ℝ <)}{sup (T ℝ <) + 1} \in ℝ$
220	219	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \frac{(\frac{E}{2}) sup (T ℝ <)}{sup (T ℝ <) + 1} \in ℝ$
221	16	nnrpd	$⊢ φ \to s \in ℝ^{+}$
222	99 221	rpdivcld	$⊢ φ \to \frac{\frac{E}{2}}{s} \in ℝ^{+}$
223	222 218	rpdivcld	$⊢ φ \to \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1} \in ℝ^{+}$
224	223	rpred	$⊢ φ \to \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1} \in ℝ$
225	224 215	remulcld	$⊢ φ \to (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <) \in ℝ$
226	225	ad2antrr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <) \in ℝ$
227		simpll	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to φ$
228	96 23	syl	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to j \in ℕ_{0}$
229	227 228 82	syl2anc	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to \|A\| \in ℝ$
230	224	ad2antrr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1} \in ℝ$
231	227 228 2	syl2anc	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to K (j) = \|A\|$
232		fveq2	$⊢ m = j \to K (m) = K (j)$
233	232	breq1d	$⊢ m = j \to (K (m) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1} \leftrightarrow K (j) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})$
234	18	simprd	$⊢ φ \to \forall m \in ℤ_{\geq t} K (m) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}$
235	234	ad2antrr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to \forall m \in ℤ_{\geq t} K (m) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}$
236		elfzuz	$⊢ j \in (m - s + 1 \dots m) \to j \in ℤ_{\geq (m - s + 1)}$
237		eluzle	$⊢ m \in ℤ_{\geq (s + t)} \to s + t \leq m$
238	237	adantl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to s + t \leq m$
239	19	nn0zd	$⊢ φ \to t \in ℤ$
240	239	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to t \in ℤ$
241	240	zred	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to t \in ℝ$
242	58 241 57	leaddsub2d	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (s + t \leq m \leftrightarrow t \leq m - s)$
243	238 242	mpbid	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to t \leq m - s$
244		eluz	$⊢ (t \in ℤ \land m - s \in ℤ) \to (m - s \in ℤ_{\geq t} \leftrightarrow t \leq m - s)$
245	240 75 244	syl2anc	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (m - s \in ℤ_{\geq t} \leftrightarrow t \leq m - s)$
246	243 245	mpbird	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to m - s \in ℤ_{\geq t}$
247		peano2uz	$⊢ m - s \in ℤ_{\geq t} \to m - s + 1 \in ℤ_{\geq t}$
248	246 247	syl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to m - s + 1 \in ℤ_{\geq t}$
249		uztrn	$⊢ (j \in ℤ_{\geq (m - s + 1)} \land m - s + 1 \in ℤ_{\geq t}) \to j \in ℤ_{\geq t}$
250	236 248 249	syl2anr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to j \in ℤ_{\geq t}$
251	233 235 250	rspcdva	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to K (j) < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}$
252	231 251	eqbrtrrd	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to \|A\| < \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}$
253	229 230 252	ltled	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to \|A\| \leq \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}$
254	213	ad2antrr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to (T \subseteq ℝ \land T \neq \emptyset \land \exists z \in ℝ \forall w \in T w \leq z)$
255	57	adantr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to m \in ℝ$
256		peano2zm	$⊢ s \in ℤ \to s - 1 \in ℤ$
257	62 256	syl	$⊢ φ \to s - 1 \in ℤ$
258	257	zred	$⊢ φ \to s - 1 \in ℝ$
259	258	ad2antrr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to s - 1 \in ℝ$
260	228	nn0red	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to j \in ℝ$
261	56	zcnd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to m \in ℂ$
262	58	recnd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to s \in ℂ$
263		1cnd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to 1 \in ℂ$
264	261 262 263	subsubd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to m - (s - 1) = m - s + 1$
265	264	adantr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to m - (s - 1) = m - s + 1$
266		elfzle1	$⊢ j \in (m - s + 1 \dots m) \to m - s + 1 \leq j$
267	266	adantl	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to m - s + 1 \leq j$
268	265 267	eqbrtrd	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to m - (s - 1) \leq j$
269	255 259 260 268	subled	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to m - j \leq s - 1$
270	96 26	syl	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to m - j \in ℕ_{0}$
271	270 37	eleqtrdi	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to m - j \in ℤ_{\geq 0}$
272	257	ad2antrr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to s - 1 \in ℤ$
273		elfz5	$⊢ (m - j \in ℤ_{\geq 0} \land s - 1 \in ℤ) \to (m - j \in (0 \dots s - 1) \leftrightarrow m - j \leq s - 1)$
274	271 272 273	syl2anc	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to (m - j \in (0 \dots s - 1) \leftrightarrow m - j \leq s - 1)$
275	269 274	mpbird	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to m - j \in (0 \dots s - 1)$
276		simplll	$⊢ (((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \land k \in ℤ_{\geq (m - j + 1)}) \to φ$
277	96 29	syldan	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to m - j + 1 \in ℕ_{0}$
278	277 32	sylan	$⊢ (((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \land k \in ℤ_{\geq (m - j + 1)}) \to k \in ℕ_{0}$
279	276 278 4	syl2anc	$⊢ (((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \land k \in ℤ_{\geq (m - j + 1)}) \to G (k) = B$
280	279	sumeq2dv	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to \sum_{k \in ℤ_{\geq (m - j + 1)}} G (k) = \sum_{k \in ℤ_{\geq (m - j + 1)}} B$
281	280	eqcomd	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to \sum_{k \in ℤ_{\geq (m - j + 1)}} B = \sum_{k \in ℤ_{\geq (m - j + 1)}} G (k)$
282	281	fveq2d	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| = \|\sum_{k \in ℤ_{\geq (m - j + 1)}} G (k)\|$
283	135	rspceeqv	$⊢ (m - j \in (0 \dots s - 1) \land \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| = \|\sum_{k \in ℤ_{\geq (m - j + 1)}} G (k)\|) \to \exists n \in (0 \dots s - 1) \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|$
284	275 282 283	syl2anc	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to \exists n \in (0 \dots s - 1) \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|$
285		fvex	$⊢ \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in V$
286		eqeq1	$⊢ z = \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \to (z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| \leftrightarrow \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|)$
287	286	rexbidv	$⊢ z = \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \to (\exists n \in (0 \dots s - 1) z = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\| \leftrightarrow \exists n \in (0 \dots s - 1) \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|)$
288	285 287 10	elab2	$⊢ \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in T \leftrightarrow \exists n \in (0 \dots s - 1) \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| = \|\sum_{k \in ℤ_{\geq (n + 1)}} G (k)\|$
289	284 288	sylibr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in T$
290		suprub	$⊢ ((T \subseteq ℝ \land T \neq \emptyset \land \exists z \in ℝ \forall w \in T w \leq z) \land \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in T) \to \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \leq sup (T ℝ <)$
291	254 289 290	syl2anc	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \leq sup (T ℝ <)$
292	227 228 129	syl2anc	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to (\|A\| \in ℝ \land 0 \leq \|A\|)$
293	96 84	syldan	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in ℝ$
294	43	absge0d	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \to 0 \leq \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\|$
295	96 294	syldan	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to 0 \leq \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\|$
296	293 295	jca	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to (\|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in ℝ \land 0 \leq \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\|)$
297	215	ad2antrr	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to sup (T ℝ <) \in ℝ$
298		lemul12a	$⊢ (((\|A\| \in ℝ \land 0 \leq \|A\|) \land \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1} \in ℝ) \land ((\|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in ℝ \land 0 \leq \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\|) \land sup (T ℝ <) \in ℝ)) \to ((\|A\| \leq \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1} \land \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \leq sup (T ℝ <)) \to \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \leq (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <))$
299	292 230 296 297 298	syl22anc	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to ((\|A\| \leq \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1} \land \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \leq sup (T ℝ <)) \to \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \leq (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <))$
300	253 291 299	mp2and	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (m - s + 1 \dots m)) \to \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \leq (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <)$
301	88 97 226 300	fsumle	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = m - s + 1}^{m} \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \leq \sum_{j = m - s + 1}^{m} (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <)$
302	225	recnd	$⊢ φ \to (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <) \in ℂ$
303	302	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <) \in ℂ$
304		fsumconst	$⊢ ((m - s + 1 \dots m) \in Fin \land (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <) \in ℂ) \to \sum_{j = m - s + 1}^{m} (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <) = \|(m - s + 1 \dots m)\| (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <)$
305	88 303 304	syl2anc	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = m - s + 1}^{m} (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <) = \|(m - s + 1 \dots m)\| (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <)$
306		1zzd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to 1 \in ℤ$
307	62	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to s \in ℤ$
308		fzen	$⊢ (1 \in ℤ \land s \in ℤ \land m - s \in ℤ) \to (1 \dots s) \approx (1 + m - s \dots s + m - s)$
309	306 307 75 308	syl3anc	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (1 \dots s) \approx (1 + m - s \dots s + m - s)$
310		ax-1cn	$⊢ 1 \in ℂ$
311	75	zcnd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to m - s \in ℂ$
312		addcom	$⊢ (1 \in ℂ \land m - s \in ℂ) \to 1 + m - s = m - s + 1$
313	310 311 312	sylancr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to 1 + m - s = m - s + 1$
314	262 261	pncan3d	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to s + m - s = m$
315	313 314	oveq12d	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (1 + m - s \dots s + m - s) = (m - s + 1 \dots m)$
316	309 315	breqtrd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (1 \dots s) \approx (m - s + 1 \dots m)$
317		fzfid	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (1 \dots s) \in Fin$
318		hashen	$⊢ ((1 \dots s) \in Fin \land (m - s + 1 \dots m) \in Fin) \to (\|(1 \dots s)\| = \|(m - s + 1 \dots m)\| \leftrightarrow (1 \dots s) \approx (m - s + 1 \dots m))$
319	317 88 318	syl2anc	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (\|(1 \dots s)\| = \|(m - s + 1 \dots m)\| \leftrightarrow (1 \dots s) \approx (m - s + 1 \dots m))$
320	316 319	mpbird	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \|(1 \dots s)\| = \|(m - s + 1 \dots m)\|$
321		hashfz1	$⊢ s \in ℕ_{0} \to \|(1 \dots s)\| = s$
322	53 321	syl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \|(1 \dots s)\| = s$
323	320 322	eqtr3d	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \|(m - s + 1 \dots m)\| = s$
324	323	oveq1d	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \|(m - s + 1 \dots m)\| (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <) = s (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <)$
325	215	recnd	$⊢ φ \to sup (T ℝ <) \in ℂ$
326	218	rpcnne0d	$⊢ φ \to (sup (T ℝ <) + 1 \in ℂ \land sup (T ℝ <) + 1 \neq 0)$
327		div23	$⊢ (\frac{E}{2} \in ℂ \land sup (T ℝ <) \in ℂ \land (sup (T ℝ <) + 1 \in ℂ \land sup (T ℝ <) + 1 \neq 0)) \to \frac{(\frac{E}{2}) sup (T ℝ <)}{sup (T ℝ <) + 1} = (\frac{\frac{E}{2}}{sup (T ℝ <) + 1}) sup (T ℝ <)$
328	160 325 326 327	syl3anc	$⊢ φ \to \frac{(\frac{E}{2}) sup (T ℝ <)}{sup (T ℝ <) + 1} = (\frac{\frac{E}{2}}{sup (T ℝ <) + 1}) sup (T ℝ <)$
329	62	zcnd	$⊢ φ \to s \in ℂ$
330	222	rpcnd	$⊢ φ \to \frac{\frac{E}{2}}{s} \in ℂ$
331		divass	$⊢ (s \in ℂ \land \frac{\frac{E}{2}}{s} \in ℂ \land (sup (T ℝ <) + 1 \in ℂ \land sup (T ℝ <) + 1 \neq 0)) \to \frac{s (\frac{\frac{E}{2}}{s})}{sup (T ℝ <) + 1} = s (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})$
332	329 330 326 331	syl3anc	$⊢ φ \to \frac{s (\frac{\frac{E}{2}}{s})}{sup (T ℝ <) + 1} = s (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1})$
333	16	nnne0d	$⊢ φ \to s \neq 0$
334	160 329 333	divcan2d	$⊢ φ \to s (\frac{\frac{E}{2}}{s}) = \frac{E}{2}$
335	334	oveq1d	$⊢ φ \to \frac{s (\frac{\frac{E}{2}}{s})}{sup (T ℝ <) + 1} = \frac{\frac{E}{2}}{sup (T ℝ <) + 1}$
336	332 335	eqtr3d	$⊢ φ \to s (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) = \frac{\frac{E}{2}}{sup (T ℝ <) + 1}$
337	336	oveq1d	$⊢ φ \to s (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <) = (\frac{\frac{E}{2}}{sup (T ℝ <) + 1}) sup (T ℝ <)$
338	223	rpcnd	$⊢ φ \to \frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1} \in ℂ$
339	329 338 325	mulassd	$⊢ φ \to s (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <) = s (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <)$
340	328 337 339	3eqtr2rd	$⊢ φ \to s (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <) = \frac{(\frac{E}{2}) sup (T ℝ <)}{sup (T ℝ <) + 1}$
341	340	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to s (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <) = \frac{(\frac{E}{2}) sup (T ℝ <)}{sup (T ℝ <) + 1}$
342	305 324 341	3eqtrd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = m - s + 1}^{m} (\frac{\frac{\frac{E}{2}}{s}}{sup (T ℝ <) + 1}) sup (T ℝ <) = \frac{(\frac{E}{2}) sup (T ℝ <)}{sup (T ℝ <) + 1}$
343	301 342	breqtrd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = m - s + 1}^{m} \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \leq \frac{(\frac{E}{2}) sup (T ℝ <)}{sup (T ℝ <) + 1}$
344		peano2re	$⊢ sup (T ℝ <) \in ℝ \to sup (T ℝ <) + 1 \in ℝ$
345	215 344	syl	$⊢ φ \to sup (T ℝ <) + 1 \in ℝ$
346	215	ltp1d	$⊢ φ \to sup (T ℝ <) < sup (T ℝ <) + 1$
347	215 345 99 346	ltmul2dd	$⊢ φ \to (\frac{E}{2}) sup (T ℝ <) < (\frac{E}{2}) (sup (T ℝ <) + 1)$
348	216 100 218	ltdivmul2d	$⊢ φ \to (\frac{(\frac{E}{2}) sup (T ℝ <)}{sup (T ℝ <) + 1} < \frac{E}{2} \leftrightarrow (\frac{E}{2}) sup (T ℝ <) < (\frac{E}{2}) (sup (T ℝ <) + 1))$
349	347 348	mpbird	$⊢ φ \to \frac{(\frac{E}{2}) sup (T ℝ <)}{sup (T ℝ <) + 1} < \frac{E}{2}$
350	349	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \frac{(\frac{E}{2}) sup (T ℝ <)}{sup (T ℝ <) + 1} < \frac{E}{2}$
351	98 220 101 343 350	lelttrd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = m - s + 1}^{m} \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < \frac{E}{2}$
352	87 98 101 101 212 351	lt2addd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m - s} \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| + \sum_{j = m - s + 1}^{m} \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < (\frac{E}{2}) + (\frac{E}{2})$
353	24 43	absmuld	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \to \|A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| = \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\|$
354	353	sumeq2dv	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m} \|A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| = \sum_{j = 0}^{m} \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\|$
355	75	zred	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to m - s \in ℝ$
356	355	ltp1d	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to m - s < m - s + 1$
357		fzdisj	$⊢ m - s < m - s + 1 \to (0 \dots m - s) \cap (m - s + 1 \dots m) = \emptyset$
358	356 357	syl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (0 \dots m - s) \cap (m - s + 1 \dots m) = \emptyset$
359		fzsplit	$⊢ m - s \in (0 \dots m) \to (0 \dots m) = (0 \dots m - s) \cup (m - s + 1 \dots m)$
360	73 359	syl	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (0 \dots m) = (0 \dots m - s) \cup (m - s + 1 \dots m)$
361	85	recnd	$⊢ ((φ \land m \in ℤ_{\geq (s + t)}) \land j \in (0 \dots m)) \to \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| \in ℂ$
362	358 360 21 361	fsumsplit	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m} \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| = \sum_{j = 0}^{m - s} \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| + \sum_{j = m - s + 1}^{m} \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\|$
363	354 362	eqtr2d	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m - s} \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| + \sum_{j = m - s + 1}^{m} \|A\| \|\sum_{k \in ℤ_{\geq (m - j + 1)}} B\| = \sum_{j = 0}^{m} \|A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\|$
364	9	rpcnd	$⊢ φ \to E \in ℂ$
365	364	adantr	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to E \in ℂ$
366	365	2halvesd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to (\frac{E}{2}) + (\frac{E}{2}) = E$
367	352 363 366	3brtr3d	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \sum_{j = 0}^{m} \|A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E$
368	46 48 50 51 367	lelttrd	$⊢ (φ \land m \in ℤ_{\geq (s + t)}) \to \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E$
369	368	ralrimiva	$⊢ φ \to \forall m \in ℤ_{\geq (s + t)} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E$
370		fveq2	$⊢ y = s + t \to ℤ_{\geq y} = ℤ_{\geq (s + t)}$
371	370	raleqdv	$⊢ y = s + t \to (\forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E \leftrightarrow \forall m \in ℤ_{\geq (s + t)} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E)$
372	371	rspcev	$⊢ (s + t \in ℕ_{0} \land \forall m \in ℤ_{\geq (s + t)} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E) \to \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E$
373	20 369 372	syl2anc	$⊢ φ \to \exists y \in ℕ_{0} \forall m \in ℤ_{\geq y} \|\sum_{j = 0}^{m} A \sum_{k \in ℤ_{\geq (m - j + 1)}} B\| < E$

Metamath Proof Explorer

Theorem mertenslem1

Proof