This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) 𝐵 ) ) < 𝐸 )