Theorem mertenslem2

Description: Lemma for mertens . (Contributed by Mario Carneiro, 28-Apr-2014)

	Ref	Expression
Hypotheses	mertens.1	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑗 ) = 𝐴 )
	mertens.2	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐾 ‘ 𝑗 ) = ( abs ‘ 𝐴 ) )
	mertens.3	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
	mertens.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
	mertens.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
	mertens.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( 𝐴 · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) )
	mertens.7	⊢ ( 𝜑 → seq 0 ( + , 𝐾 ) ∈ dom ⇝ )
	mertens.8	⊢ ( 𝜑 → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
	mertens.9	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
	mertens.10	⊢ 𝑇 = { 𝑧 ∣ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) }
	mertens.11	⊢ ( 𝜓 ↔ ( 𝑠 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
Assertion	mertenslem2	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		mertens.1	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑗 ) = 𝐴 )
2		mertens.2	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐾 ‘ 𝑗 ) = ( abs ‘ 𝐴 ) )
3		mertens.3	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
4		mertens.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
5		mertens.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
6		mertens.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( 𝐴 · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) )
7		mertens.7	⊢ ( 𝜑 → seq 0 ( + , 𝐾 ) ∈ dom ⇝ )
8		mertens.8	⊢ ( 𝜑 → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
9		mertens.9	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
10		mertens.10	⊢ 𝑇 = { 𝑧 ∣ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) }
11		mertens.11	⊢ ( 𝜓 ↔ ( 𝑠 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
12		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
13		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
14	9	rphalfcld	⊢ ( 𝜑 → ( 𝐸 / 2 ) ∈ ℝ+ )
15		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
16		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
17		eqidd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐾 ‘ 𝑗 ) = ( 𝐾 ‘ 𝑗 ) )
18	3	abscld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
19	2 18	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐾 ‘ 𝑗 ) ∈ ℝ )
20	15 16 17 19 7	isumrecl	⊢ ( 𝜑 → Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) ∈ ℝ )
21	3	absge0d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 0 ≤ ( abs ‘ 𝐴 ) )
22	21 2	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 0 ≤ ( 𝐾 ‘ 𝑗 ) )
23	15 16 17 19 7 22	isumge0	⊢ ( 𝜑 → 0 ≤ Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) )
24	20 23	ge0p1rpd	⊢ ( 𝜑 → ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ∈ ℝ+ )
25	14 24	rpdivcld	⊢ ( 𝜑 → ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ∈ ℝ+ )
26		eqidd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) = ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) )
27	15 16 4 5 8	isumclim2	⊢ ( 𝜑 → seq 0 ( + , 𝐺 ) ⇝ Σ 𝑘 ∈ ℕ0 𝐵 )
28	12 13 25 26 27	climi2	⊢ ( 𝜑 → ∃ 𝑠 ∈ ℕ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) )
29		eluznn	⊢ ( ( 𝑠 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ) → 𝑚 ∈ ℕ )
30	4 5	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
31	15 16 30	serf	⊢ ( 𝜑 → seq 0 ( + , 𝐺 ) : ℕ0 ⟶ ℂ )
32		nnnn0	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℕ0 )
33		ffvelcdm	⊢ ( ( seq 0 ( + , 𝐺 ) : ℕ0 ⟶ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) ∈ ℂ )
34	31 32 33	syl2an	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) ∈ ℂ )
35	15 16 4 5 8	isumcl	⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ0 𝐵 ∈ ℂ )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ℕ0 𝐵 ∈ ℂ )
37	34 36	abssubd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) = ( abs ‘ ( Σ 𝑘 ∈ ℕ0 𝐵 − ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) ) ) )
38		eqid	⊢ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) = ( ℤ≥ ‘ ( 𝑚 + 1 ) )
39	32	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ0 )
40		peano2nn0	⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 + 1 ) ∈ ℕ0 )
41	39 40	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℕ0 )
42	41	nn0zd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℤ )
43		simpll	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) → 𝜑 )
44		eluznn0	⊢ ( ( ( 𝑚 + 1 ) ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
45	41 44	sylan	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
46	43 45 4	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
47	43 45 5	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) → 𝐵 ∈ ℂ )
48	8	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
49	30	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
50	15 41 49	iserex	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( seq 0 ( + , 𝐺 ) ∈ dom ⇝ ↔ seq ( 𝑚 + 1 ) ( + , 𝐺 ) ∈ dom ⇝ ) )
51	48 50	mpbid	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → seq ( 𝑚 + 1 ) ( + , 𝐺 ) ∈ dom ⇝ )
52	38 42 46 47 51	isumcl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 ∈ ℂ )
53	34 52	pncan2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 ) − ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 )
54	4	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
55	5	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
56	15 38 41 54 55 48	isumsplit	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ℕ0 𝐵 = ( Σ 𝑘 ∈ ( 0 ... ( ( 𝑚 + 1 ) − 1 ) ) 𝐵 + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 ) )
57		nncn	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
58	57	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℂ )
59		ax-1cn	⊢ 1 ∈ ℂ
60		pncan	⊢ ( ( 𝑚 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑚 + 1 ) − 1 ) = 𝑚 )
61	58 59 60	sylancl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 + 1 ) − 1 ) = 𝑚 )
62	61	oveq2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 0 ... ( ( 𝑚 + 1 ) − 1 ) ) = ( 0 ... 𝑚 ) )
63	62	sumeq1d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( 0 ... ( ( 𝑚 + 1 ) − 1 ) ) 𝐵 = Σ 𝑘 ∈ ( 0 ... 𝑚 ) 𝐵 )
64		simpl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝜑 )
65		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑚 ) → 𝑘 ∈ ℕ0 )
66	64 65 4	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑚 ) ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
67	39 15	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ( ℤ≥ ‘ 0 ) )
68	64 65 5	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... 𝑚 ) ) → 𝐵 ∈ ℂ )
69	66 67 68	fsumser	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( 0 ... 𝑚 ) 𝐵 = ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) )
70	63 69	eqtrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( 0 ... ( ( 𝑚 + 1 ) − 1 ) ) 𝐵 = ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) )
71	70	oveq1d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( Σ 𝑘 ∈ ( 0 ... ( ( 𝑚 + 1 ) − 1 ) ) 𝐵 + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 ) = ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 ) )
72	56 71	eqtrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ℕ0 𝐵 = ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 ) )
73	72	oveq1d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( Σ 𝑘 ∈ ℕ0 𝐵 − ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) ) = ( ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 ) − ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) ) )
74	46	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) 𝐵 )
75	53 73 74	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( Σ 𝑘 ∈ ℕ0 𝐵 − ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) )
76	75	fveq2d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( abs ‘ ( Σ 𝑘 ∈ ℕ0 𝐵 − ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) ) ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) )
77	37 76	eqtrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) )
78	77	breq1d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ↔ ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
79	29 78	sylan2	⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ) ) → ( ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ↔ ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
80	79	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ) → ( ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ↔ ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
81	80	ralbidva	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
82		fvoveq1	⊢ ( 𝑚 = 𝑛 → ( ℤ≥ ‘ ( 𝑚 + 1 ) ) = ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
83	82	sumeq1d	⊢ ( 𝑚 = 𝑛 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) )
84	83	fveq2d	⊢ ( 𝑚 = 𝑛 → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) )
85	84	breq1d	⊢ ( 𝑚 = 𝑛 → ( ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ↔ ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
86	85	cbvralvw	⊢ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ↔ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) )
87	81 86	bitrdi	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ↔ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
88		0zd	⊢ ( ( 𝜑 ∧ 𝜓 ) → 0 ∈ ℤ )
89	14	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐸 / 2 ) ∈ ℝ+ )
90	11	simplbi	⊢ ( 𝜓 → 𝑠 ∈ ℕ )
91	90	adantl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑠 ∈ ℕ )
92	91	nnrpd	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑠 ∈ ℝ+ )
93	89 92	rpdivcld	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐸 / 2 ) / 𝑠 ) ∈ ℝ+ )
94		eqid	⊢ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) = ( ℤ≥ ‘ ( 𝑛 + 1 ) )
95		elfznn0	⊢ ( 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) → 𝑛 ∈ ℕ0 )
96	95	adantl	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → 𝑛 ∈ ℕ0 )
97		peano2nn0	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℕ0 )
98	96 97	syl	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( 𝑛 + 1 ) ∈ ℕ0 )
99	98	nn0zd	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( 𝑛 + 1 ) ∈ ℤ )
100		eqidd	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
101		simplll	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → 𝜑 )
102		eluznn0	⊢ ( ( ( 𝑛 + 1 ) ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
103	98 102	sylan	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
104	101 103 30	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
105	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
106	30	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
107	15 98 106	iserex	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( seq 0 ( + , 𝐺 ) ∈ dom ⇝ ↔ seq ( 𝑛 + 1 ) ( + , 𝐺 ) ∈ dom ⇝ ) )
108	105 107	mpbid	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → seq ( 𝑛 + 1 ) ( + , 𝐺 ) ∈ dom ⇝ )
109	94 99 100 104 108	isumcl	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
110	109	abscld	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
111		eleq1a	⊢ ( ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ → ( 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) → 𝑧 ∈ ℝ ) )
112	110 111	syl	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ) → ( 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) → 𝑧 ∈ ℝ ) )
113	112	rexlimdva	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) → 𝑧 ∈ ℝ ) )
114	113	abssdv	⊢ ( ( 𝜑 ∧ 𝜓 ) → { 𝑧 ∣ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) } ⊆ ℝ )
115	10 114	eqsstrid	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑇 ⊆ ℝ )
116		fzfid	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 0 ... ( 𝑠 − 1 ) ) ∈ Fin )
117		abrexfi	⊢ ( ( 0 ... ( 𝑠 − 1 ) ) ∈ Fin → { 𝑧 ∣ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) } ∈ Fin )
118	116 117	syl	⊢ ( ( 𝜑 ∧ 𝜓 ) → { 𝑧 ∣ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) } ∈ Fin )
119	10 118	eqeltrid	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑇 ∈ Fin )
120		nnm1nn0	⊢ ( 𝑠 ∈ ℕ → ( 𝑠 − 1 ) ∈ ℕ0 )
121	91 120	syl	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑠 − 1 ) ∈ ℕ0 )
122	121 15	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑠 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
123		eluzfz1	⊢ ( ( 𝑠 − 1 ) ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... ( 𝑠 − 1 ) ) )
124	122 123	syl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 0 ∈ ( 0 ... ( 𝑠 − 1 ) ) )
125		nnnn0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
126	125 4	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
127	126	sumeq2dv	⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ 𝐵 )
128	127	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ 𝐵 )
129	128	fveq2d	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ Σ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) ) = ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) )
130	129	eqcomd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) = ( abs ‘ Σ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) ) )
131		fv0p1e1	⊢ ( 𝑛 = 0 → ( ℤ≥ ‘ ( 𝑛 + 1 ) ) = ( ℤ≥ ‘ 1 ) )
132	131 12	eqtr4di	⊢ ( 𝑛 = 0 → ( ℤ≥ ‘ ( 𝑛 + 1 ) ) = ℕ )
133	132	sumeq1d	⊢ ( 𝑛 = 0 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) )
134	133	fveq2d	⊢ ( 𝑛 = 0 → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) = ( abs ‘ Σ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) ) )
135	134	rspceeqv	⊢ ( ( 0 ∈ ( 0 ... ( 𝑠 − 1 ) ) ∧ ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) = ( abs ‘ Σ 𝑘 ∈ ℕ ( 𝐺 ‘ 𝑘 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) )
136	124 130 135	syl2anc	⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) )
137		fvex	⊢ ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) ∈ V
138		eqeq1	⊢ ( 𝑧 = ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) → ( 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ↔ ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ) )
139	138	rexbidv	⊢ ( 𝑧 = ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) → ( ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ↔ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ) )
140	137 139 10	elab2	⊢ ( ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) ∈ 𝑇 ↔ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) )
141	136 140	sylibr	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) ∈ 𝑇 )
142	141	ne0d	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑇 ≠ ∅ )
143		ltso	⊢ < Or ℝ
144		fisupcl	⊢ ( ( < Or ℝ ∧ ( 𝑇 ∈ Fin ∧ 𝑇 ≠ ∅ ∧ 𝑇 ⊆ ℝ ) ) → sup ( 𝑇 , ℝ , < ) ∈ 𝑇 )
145	143 144	mpan	⊢ ( ( 𝑇 ∈ Fin ∧ 𝑇 ≠ ∅ ∧ 𝑇 ⊆ ℝ ) → sup ( 𝑇 , ℝ , < ) ∈ 𝑇 )
146	119 142 115 145	syl3anc	⊢ ( ( 𝜑 ∧ 𝜓 ) → sup ( 𝑇 , ℝ , < ) ∈ 𝑇 )
147	115 146	sseldd	⊢ ( ( 𝜑 ∧ 𝜓 ) → sup ( 𝑇 , ℝ , < ) ∈ ℝ )
148		0red	⊢ ( ( 𝜑 ∧ 𝜓 ) → 0 ∈ ℝ )
149	125 5	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐵 ∈ ℂ )
150		1nn0	⊢ 1 ∈ ℕ0
151	150	a1i	⊢ ( 𝜑 → 1 ∈ ℕ0 )
152	15 151 30	iserex	⊢ ( 𝜑 → ( seq 0 ( + , 𝐺 ) ∈ dom ⇝ ↔ seq 1 ( + , 𝐺 ) ∈ dom ⇝ ) )
153	8 152	mpbid	⊢ ( 𝜑 → seq 1 ( + , 𝐺 ) ∈ dom ⇝ )
154	12 13 126 149 153	isumcl	⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ 𝐵 ∈ ℂ )
155	154	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑘 ∈ ℕ 𝐵 ∈ ℂ )
156	155	abscld	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) ∈ ℝ )
157	155	absge0d	⊢ ( ( 𝜑 ∧ 𝜓 ) → 0 ≤ ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) )
158		fimaxre2	⊢ ( ( 𝑇 ⊆ ℝ ∧ 𝑇 ∈ Fin ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑤 ≤ 𝑧 )
159	115 119 158	syl2anc	⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑤 ≤ 𝑧 )
160	115 142 159 141	suprubd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( abs ‘ Σ 𝑘 ∈ ℕ 𝐵 ) ≤ sup ( 𝑇 , ℝ , < ) )
161	148 156 147 157 160	letrd	⊢ ( ( 𝜑 ∧ 𝜓 ) → 0 ≤ sup ( 𝑇 , ℝ , < ) )
162	147 161	ge0p1rpd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( sup ( 𝑇 , ℝ , < ) + 1 ) ∈ ℝ+ )
163	93 162	rpdivcld	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ∈ ℝ+ )
164		fveq2	⊢ ( 𝑛 = 𝑚 → ( 𝐾 ‘ 𝑛 ) = ( 𝐾 ‘ 𝑚 ) )
165		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) )
166		fvex	⊢ ( 𝐾 ‘ 𝑚 ) ∈ V
167	164 165 166	fvmpt	⊢ ( 𝑚 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ‘ 𝑚 ) = ( 𝐾 ‘ 𝑚 ) )
168	167	adantl	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ‘ 𝑚 ) = ( 𝐾 ‘ 𝑚 ) )
169		nn0ex	⊢ ℕ0 ∈ V
170	169	mptex	⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ∈ V
171	170	a1i	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ∈ V )
172		elnn0uz	⊢ ( 𝑗 ∈ ℕ0 ↔ 𝑗 ∈ ( ℤ≥ ‘ 0 ) )
173		fveq2	⊢ ( 𝑛 = 𝑗 → ( 𝐾 ‘ 𝑛 ) = ( 𝐾 ‘ 𝑗 ) )
174		fvex	⊢ ( 𝐾 ‘ 𝑗 ) ∈ V
175	173 165 174	fvmpt	⊢ ( 𝑗 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ‘ 𝑗 ) = ( 𝐾 ‘ 𝑗 ) )
176	175	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ‘ 𝑗 ) = ( 𝐾 ‘ 𝑗 ) )
177	172 176	sylan2br	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 0 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ‘ 𝑗 ) = ( 𝐾 ‘ 𝑗 ) )
178	16 177	seqfeq	⊢ ( 𝜑 → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ) = seq 0 ( + , 𝐾 ) )
179	178 7	eqeltrd	⊢ ( 𝜑 → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ) ∈ dom ⇝ )
180	176 2	eqtrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ‘ 𝑗 ) = ( abs ‘ 𝐴 ) )
181	180 18	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ‘ 𝑗 ) ∈ ℝ )
182	181	recnd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ‘ 𝑗 ) ∈ ℂ )
183	15 16 171 179 182	serf0	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ⇝ 0 )
184	183	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝐾 ‘ 𝑛 ) ) ⇝ 0 )
185	15 88 163 168 184	climi0	⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑡 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) )
186		simplll	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑡 ∈ ℕ0 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ) → 𝜑 )
187		eluznn0	⊢ ( ( 𝑡 ∈ ℕ0 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ) → 𝑚 ∈ ℕ0 )
188	187	adantll	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑡 ∈ ℕ0 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ) → 𝑚 ∈ ℕ0 )
189	19 22	absidd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( abs ‘ ( 𝐾 ‘ 𝑗 ) ) = ( 𝐾 ‘ 𝑗 ) )
190	189	ralrimiva	⊢ ( 𝜑 → ∀ 𝑗 ∈ ℕ0 ( abs ‘ ( 𝐾 ‘ 𝑗 ) ) = ( 𝐾 ‘ 𝑗 ) )
191		fveq2	⊢ ( 𝑗 = 𝑚 → ( 𝐾 ‘ 𝑗 ) = ( 𝐾 ‘ 𝑚 ) )
192	191	fveq2d	⊢ ( 𝑗 = 𝑚 → ( abs ‘ ( 𝐾 ‘ 𝑗 ) ) = ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) )
193	192 191	eqeq12d	⊢ ( 𝑗 = 𝑚 → ( ( abs ‘ ( 𝐾 ‘ 𝑗 ) ) = ( 𝐾 ‘ 𝑗 ) ↔ ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) = ( 𝐾 ‘ 𝑚 ) ) )
194	193	rspccva	⊢ ( ( ∀ 𝑗 ∈ ℕ0 ( abs ‘ ( 𝐾 ‘ 𝑗 ) ) = ( 𝐾 ‘ 𝑗 ) ∧ 𝑚 ∈ ℕ0 ) → ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) = ( 𝐾 ‘ 𝑚 ) )
195	190 194	sylan	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) = ( 𝐾 ‘ 𝑚 ) )
196	186 188 195	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑡 ∈ ℕ0 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ) → ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) = ( 𝐾 ‘ 𝑚 ) )
197	196	breq1d	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑡 ∈ ℕ0 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ) → ( ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ↔ ( 𝐾 ‘ 𝑚 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) )
198	197	ralbidva	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑡 ∈ ℕ0 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑚 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) )
199	164	breq1d	⊢ ( 𝑛 = 𝑚 → ( ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ↔ ( 𝐾 ‘ 𝑚 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) )
200	199	cbvralvw	⊢ ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑚 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) )
201	198 200	bitr4di	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑡 ∈ ℕ0 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ↔ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) )
202	1	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) ∧ 𝑗 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑗 ) = 𝐴 )
203	2	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) ∧ 𝑗 ∈ ℕ0 ) → ( 𝐾 ‘ 𝑗 ) = ( abs ‘ 𝐴 ) )
204	3	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) ∧ 𝑗 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
205	4	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
206	5	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
207	6	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( 𝐴 · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) )
208	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) → seq 0 ( + , 𝐾 ) ∈ dom ⇝ )
209	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
210	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) → 𝐸 ∈ ℝ+ )
211	200	anbi2i	⊢ ( ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ↔ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑚 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) )
212	211	anbi2i	⊢ ( ( 𝜓 ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) ↔ ( 𝜓 ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑚 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) )
213	212	biimpi	⊢ ( ( 𝜓 ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) → ( 𝜓 ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑚 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) )
214	213	adantll	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) → ( 𝜓 ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑚 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) )
215	115 142 159	3jca	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑤 ≤ 𝑧 ) )
216	161 215	jca	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 0 ≤ sup ( 𝑇 , ℝ , < ) ∧ ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑤 ≤ 𝑧 ) ) )
217	216	adantr	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) → ( 0 ≤ sup ( 𝑇 , ℝ , < ) ∧ ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑇 𝑤 ≤ 𝑧 ) ) )
218	202 203 204 205 206 207 208 209 210 10 11 214 217	mertenslem1	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑡 ∈ ℕ0 ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 )
219	218	expr	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑡 ∈ ℕ0 ) → ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑡 ) ( 𝐾 ‘ 𝑛 ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 ) )
220	201 219	sylbid	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑡 ∈ ℕ0 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 ) )
221	220	rexlimdva	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ∃ 𝑡 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑡 ) ( abs ‘ ( 𝐾 ‘ 𝑚 ) ) < ( ( ( 𝐸 / 2 ) / 𝑠 ) / ( sup ( 𝑇 , ℝ , < ) + 1 ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 ) )
222	185 221	mpd	⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 )
223	222	ex	⊢ ( 𝜑 → ( 𝜓 → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 ) )
224	11 223	biimtrrid	⊢ ( 𝜑 → ( ( 𝑠 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 ) )
225	224	expdimp	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ ) → ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 ) )
226	87 225	sylbid	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℕ ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 ) )
227	226	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ℕ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ ( ( seq 0 ( + , 𝐺 ) ‘ 𝑚 ) − Σ 𝑘 ∈ ℕ0 𝐵 ) ) < ( ( 𝐸 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 ) )
228	28 227	mpd	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝐸 )