Theorem mertenslem1

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