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

Metamath Proof Explorer

Theorem dchrisumlem3

Description: Lemma for dchrisum . Lemma 9.4.1 of Shapiro, p. 377. (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
rpvmasum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
rpvmasum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
rpvmasum.1 ⊢ 1 = ( 0g ‘ 𝐺 )
dchrisum.b ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
dchrisum.n1 ⊢ ( 𝜑 → 𝑋 ≠ 1 )
dchrisum.2 ⊢ ( 𝑛 = 𝑥 → 𝐴 = 𝐵 )
dchrisum.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
dchrisum.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
dchrisum.5 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
dchrisum.6 ⊢ ( 𝜑 → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
dchrisum.7 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · 𝐴 ) )
dchrisum.9 ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
dchrisum.10 ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( 0 ..^ 𝑁 ) ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
Assertion dchrisumlem3 ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2 rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3 rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 rpvmasum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
5 rpvmasum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
6 rpvmasum.1 ⊢ 1 = ( 0g ‘ 𝐺 )
7 dchrisum.b ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8 dchrisum.n1 ⊢ ( 𝜑 → 𝑋 ≠ 1 )
9 dchrisum.2 ⊢ ( 𝑛 = 𝑥 → 𝐴 = 𝐵 )
10 dchrisum.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
11 dchrisum.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
12 dchrisum.5 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
13 dchrisum.6 ⊢ ( 𝜑 → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
14 dchrisum.7 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · 𝐴 ) )
15 dchrisum.9 ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
16 dchrisum.10 ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( 0 ..^ 𝑁 ) ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
17 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
18 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
19 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ℕ )
20 7 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑋 ∈ 𝐷 )
21 19 nnzd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → 𝑖 ∈ ℤ )
22 4 1 5 2 20 21 dchrzrhcl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) ∈ ℂ )
23 11 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ )
24 nnrp ⊢ ( 𝑖 ∈ ℕ → 𝑖 ∈ ℝ+ )
25 nfcsb1v ⊢ Ⅎ 𝑛 ⦋ 𝑖 / 𝑛 ⦌ 𝐴
26 25 nfel1 ⊢ Ⅎ 𝑛 ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ
27 csbeq1a ⊢ ( 𝑛 = 𝑖 → 𝐴 = ⦋ 𝑖 / 𝑛 ⦌ 𝐴 )
28 27 eleq1d ⊢ ( 𝑛 = 𝑖 → ( 𝐴 ∈ ℝ ↔ ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
29 26 28 rspc ⊢ ( 𝑖 ∈ ℝ+ → ( ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
30 29 impcom ⊢ ( ( ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ ∧ 𝑖 ∈ ℝ+ ) → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ )
31 23 24 30 syl2an ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℝ )
32 31 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ∈ ℂ )
33 22 32 mulcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ∈ ℂ )
34 nfcv ⊢ Ⅎ 𝑛 𝑖
35 nfcv ⊢ Ⅎ 𝑛 ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) )
36 nfcv ⊢ Ⅎ 𝑛 ·
37 35 36 25 nfov ⊢ Ⅎ 𝑛 ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 )
38 2fveq3 ⊢ ( 𝑛 = 𝑖 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) )
39 38 27 oveq12d ⊢ ( 𝑛 = 𝑖 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · 𝐴 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
40 34 37 39 14 fvmptf ⊢ ( ( 𝑖 ∈ ℕ ∧ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) ∈ ℂ ) → ( 𝐹 ‘ 𝑖 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
41 19 33 40 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝐹 ‘ 𝑖 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑖 ) ) · ⦋ 𝑖 / 𝑛 ⦌ 𝐴 ) )
42 41 33 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ ) → ( 𝐹 ‘ 𝑖 ) ∈ ℂ )
43 17 18 42 serf ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℂ )
44 43 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ∈ ℂ )
45 11 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
46 45 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℂ )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℂ )
48 id ⊢ ( 𝑒 ∈ ℝ+ → 𝑒 ∈ ℝ+ )
49 2re ⊢ 2 ∈ ℝ
50 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( 2 · 𝑅 ) ∈ ℝ )
51 49 15 50 sylancr ⊢ ( 𝜑 → ( 2 · 𝑅 ) ∈ ℝ )
52 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑁 ∈ ℕ )
53 3 52 sylibr ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ 𝑁 ) )
54 oveq2 ⊢ ( 𝑢 = 0 → ( 0 ..^ 𝑢 ) = ( 0 ..^ 0 ) )
55 fzo0 ⊢ ( 0 ..^ 0 ) = ∅
56 54 55 eqtrdi ⊢ ( 𝑢 = 0 → ( 0 ..^ 𝑢 ) = ∅ )
57 56 sumeq1d ⊢ ( 𝑢 = 0 → Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = Σ 𝑛 ∈ ∅ ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) )
58 sum0 ⊢ Σ 𝑛 ∈ ∅ ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0
59 57 58 eqtrdi ⊢ ( 𝑢 = 0 → Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 )
60 59 abs00bd ⊢ ( 𝑢 = 0 → ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) = 0 )
61 60 breq1d ⊢ ( 𝑢 = 0 → ( ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 ↔ 0 ≤ 𝑅 ) )
62 61 rspcv ⊢ ( 0 ∈ ( 0 ..^ 𝑁 ) → ( ∀ 𝑢 ∈ ( 0 ..^ 𝑁 ) ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 → 0 ≤ 𝑅 ) )
63 53 16 62 sylc ⊢ ( 𝜑 → 0 ≤ 𝑅 )
64 0le2 ⊢ 0 ≤ 2
65 mulge0 ⊢ ( ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) ∧ ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ) → 0 ≤ ( 2 · 𝑅 ) )
66 49 64 65 mpanl12 ⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) → 0 ≤ ( 2 · 𝑅 ) )
67 15 63 66 syl2anc ⊢ ( 𝜑 → 0 ≤ ( 2 · 𝑅 ) )
68 51 67 ge0p1rpd ⊢ ( 𝜑 → ( ( 2 · 𝑅 ) + 1 ) ∈ ℝ+ )
69 rpdivcl ⊢ ( ( 𝑒 ∈ ℝ+ ∧ ( ( 2 · 𝑅 ) + 1 ) ∈ ℝ+ ) → ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ∈ ℝ+ )
70 48 68 69 syl2anr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ∈ ℝ+ )
71 13 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
72 47 70 71 rlimi ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑚 ∈ ℝ ∀ 𝑛 ∈ ℝ+ ( 𝑚 ≤ 𝑛 → ( abs ‘ ( 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) )
73 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 𝑚 ∈ ℝ )
74 10 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 𝑀 ∈ ℝ )
76 73 75 ifcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ )
77 0red ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 0 ∈ ℝ )
78 10 nngt0d ⊢ ( 𝜑 → 0 < 𝑀 )
79 78 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 0 < 𝑀 )
80 max1 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) )
81 74 80 sylan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) )
82 77 75 76 79 81 ltletrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 0 < if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) )
83 76 82 elrpd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ+ )
84 83 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ+ )
85 nfv ⊢ Ⅎ 𝑛 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 )
86 nfcv ⊢ Ⅎ 𝑛 abs
87 nfcsb1v ⊢ Ⅎ 𝑛 ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴
88 nfcv ⊢ Ⅎ 𝑛 −
89 nfcv ⊢ Ⅎ 𝑛 0
90 87 88 89 nfov ⊢ Ⅎ 𝑛 ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 )
91 86 90 nffv ⊢ Ⅎ 𝑛 ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) )
92 nfcv ⊢ Ⅎ 𝑛 <
93 nfcv ⊢ Ⅎ 𝑛 ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) )
94 91 92 93 nfbr ⊢ Ⅎ 𝑛 ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) )
95 85 94 nfim ⊢ Ⅎ 𝑛 ( 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) )
96 breq2 ⊢ ( 𝑛 = if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( 𝑚 ≤ 𝑛 ↔ 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) )
97 csbeq1a ⊢ ( 𝑛 = if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → 𝐴 = ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 )
98 97 fvoveq1d ⊢ ( 𝑛 = if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( abs ‘ ( 𝐴 − 0 ) ) = ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) )
99 98 breq1d ⊢ ( 𝑛 = if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( ( abs ‘ ( 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ↔ ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) )
100 96 99 imbi12d ⊢ ( 𝑛 = if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( ( 𝑚 ≤ 𝑛 → ( abs ‘ ( 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) ↔ ( 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) ) )
101 95 100 rspc ⊢ ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ+ → ( ∀ 𝑛 ∈ ℝ+ ( 𝑚 ≤ 𝑛 → ( abs ‘ ( 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) → ( 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) ) )
102 84 101 syl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ∀ 𝑛 ∈ ℝ+ ( 𝑚 ≤ 𝑛 → ( abs ‘ ( 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) → ( 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) ) )
103 74 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝑀 ∈ ℝ )
104 max2 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) )
105 103 104 sylancom ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) )
106 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ )
107 87 nfel1 ⊢ Ⅎ 𝑛 ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ∈ ℝ
108 97 eleq1d ⊢ ( 𝑛 = if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( 𝐴 ∈ ℝ ↔ ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
109 107 108 rspc ⊢ ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ+ → ( ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
110 84 106 109 sylc ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ∈ ℝ )
111 110 recnd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ∈ ℂ )
112 111 subid1d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) = ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 )
113 112 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) = ( abs ‘ ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) )
114 76 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ )
115 103 80 sylancom ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) )
116 elicopnf ⊢ ( 𝑀 ∈ ℝ → ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ( 𝑀 [,) +∞ ) ↔ ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ ∧ 𝑀 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) )
117 103 116 syl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ( 𝑀 [,) +∞ ) ↔ ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ ∧ 𝑀 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) )
118 114 115 117 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ( 𝑀 [,) +∞ ) )
119 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝑁 ∈ ℕ )
120 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝑋 ∈ 𝐷 )
121 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝑋 ≠ 1 )
122 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝑀 ∈ ℕ )
123 11 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
124 simpll ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝜑 )
125 124 12 syl3an1 ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
126 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
127 1 2 119 4 5 6 120 121 9 122 123 125 126 14 dchrisumlema ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ+ → ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ∈ ℝ ) ∧ ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ( 𝑀 [,) +∞ ) → 0 ≤ ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ) )
128 127 simprd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ( 𝑀 [,) +∞ ) → 0 ≤ ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) )
129 118 128 mpd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 0 ≤ ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 )
130 110 129 absidd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( abs ‘ ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) = ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 )
131 113 130 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) = ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 )
132 131 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ↔ ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) )
133 rpre ⊢ ( 𝑒 ∈ ℝ+ → 𝑒 ∈ ℝ )
134 133 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → 𝑒 ∈ ℝ )
135 68 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( 2 · 𝑅 ) + 1 ) ∈ ℝ+ )
136 110 134 135 ltmuldiv2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ↔ ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) )
137 132 136 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ↔ ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) )
138 51 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( 2 · 𝑅 ) ∈ ℝ )
139 135 rpred ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( 2 · 𝑅 ) + 1 ) ∈ ℝ )
140 138 lep1d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( 2 · 𝑅 ) ≤ ( ( 2 · 𝑅 ) + 1 ) )
141 138 139 110 129 140 lemul1ad ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ≤ ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) )
142 138 110 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
143 139 110 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
144 lelttr ⊢ ( ( ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∈ ℝ ∧ ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∈ ℝ ∧ 𝑒 ∈ ℝ ) → ( ( ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ≤ ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∧ ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) → ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) )
145 142 143 134 144 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ≤ ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∧ ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) → ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) )
146 141 145 mpand ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( ( ( 2 · 𝑅 ) + 1 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 → ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) )
147 137 146 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) → ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) )
148 1red ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 1 ∈ ℝ )
149 10 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 𝑀 ∈ ℕ )
150 149 nnge1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 1 ≤ 𝑀 )
151 148 75 76 150 81 letrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → 1 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) )
152 flge1nn ⊢ ( ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ ∧ 1 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) → ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ∈ ℕ )
153 76 151 152 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) → ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ∈ ℕ )
154 153 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ∈ ℕ )
155 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑁 ∈ ℕ )
156 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑋 ∈ 𝐷 )
157 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑋 ≠ 1 )
158 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑀 ∈ ℕ )
159 11 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
160 12 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
161 160 3adant1r ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
162 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
163 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑅 ∈ ℝ )
164 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ∀ 𝑢 ∈ ( 0 ..^ 𝑁 ) ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
165 83 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ+ )
166 81 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑀 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) )
167 76 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ )
168 fllep1 ⊢ ( if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ∈ ℝ → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ≤ ( ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) + 1 ) )
169 167 168 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ≤ ( ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) + 1 ) )
170 153 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ∈ ℕ )
171 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) )
172 1 2 155 4 5 6 156 157 9 158 159 161 162 14 163 164 165 166 169 170 171 dchrisumlem2 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) )
173 172 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) )
174 43 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℂ )
175 eluznn ⊢ ( ( ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑘 ∈ ℕ )
176 154 175 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑘 ∈ ℕ )
177 174 176 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ∈ ℂ )
178 154 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ∈ ℕ )
179 174 178 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ∈ ℂ )
180 177 179 subcld ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ∈ ℂ )
181 180 abscld ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) ∈ ℝ )
182 142 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
183 134 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → 𝑒 ∈ ℝ )
184 lelttr ⊢ ( ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) ∈ ℝ ∧ ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∈ ℝ ∧ 𝑒 ∈ ℝ ) → ( ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∧ ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) < 𝑒 ) )
185 181 182 183 184 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) ∧ ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) < 𝑒 ) )
186 173 185 mpand ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) → ( ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) < 𝑒 ) )
187 186 ralrimdva ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 → ∀ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) < 𝑒 ) )
188 fveq2 ⊢ ( 𝑗 = ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) )
189 fveq2 ⊢ ( 𝑗 = ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) )
190 189 oveq2d ⊢ ( 𝑗 = ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) → ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) = ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) )
191 190 fveq2d ⊢ ( 𝑗 = ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) )
192 191 breq1d ⊢ ( 𝑗 = ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 ↔ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) < 𝑒 ) )
193 188 192 raleqbidv ⊢ ( 𝑗 = ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) < 𝑒 ) )
194 193 rspcev ⊢ ( ( ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ∈ ℕ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) ) ) ) ) < 𝑒 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 )
195 154 187 194 syl6an ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( ( 2 · 𝑅 ) · ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 ) < 𝑒 → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 ) )
196 147 195 syld ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 ) )
197 105 196 embantd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ( 𝑚 ≤ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) → ( abs ‘ ( ⦋ if ( 𝑀 ≤ 𝑚 , 𝑚 , 𝑀 ) / 𝑛 ⦌ 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 ) )
198 102 197 syld ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑚 ∈ ℝ ) → ( ∀ 𝑛 ∈ ℝ+ ( 𝑚 ≤ 𝑛 → ( abs ‘ ( 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 ) )
199 198 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( ∃ 𝑚 ∈ ℝ ∀ 𝑛 ∈ ℝ+ ( 𝑚 ≤ 𝑛 → ( abs ‘ ( 𝐴 − 0 ) ) < ( 𝑒 / ( ( 2 · 𝑅 ) + 1 ) ) ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 ) )
200 72 199 mpd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 )
201 200 ralrimiva ⊢ ( 𝜑 → ∀ 𝑒 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑒 )
202 seqex ⊢ seq 1 ( + , 𝐹 ) ∈ V
203 202 a1i ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ∈ V )
204 17 44 201 203 caucvg ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
205 202 eldm ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ↔ ∃ 𝑡 seq 1 ( + , 𝐹 ) ⇝ 𝑡 )
206 204 205 sylib ⊢ ( 𝜑 → ∃ 𝑡 seq 1 ( + , 𝐹 ) ⇝ 𝑡 )
207 simpr ⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) → seq 1 ( + , 𝐹 ) ⇝ 𝑡 )
208 elrege0 ⊢ ( ( 2 · 𝑅 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 2 · 𝑅 ) ∈ ℝ ∧ 0 ≤ ( 2 · 𝑅 ) ) )
209 51 67 208 sylanbrc ⊢ ( 𝜑 → ( 2 · 𝑅 ) ∈ ( 0 [,) +∞ ) )
210 209 adantr ⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) → ( 2 · 𝑅 ) ∈ ( 0 [,) +∞ ) )
211 eqid ⊢ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) = ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) )
212 pnfxr ⊢ +∞ ∈ ℝ*
213 icossre ⊢ ( ( 𝑀 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 𝑀 [,) +∞ ) ⊆ ℝ )
214 74 212 213 sylancl ⊢ ( 𝜑 → ( 𝑀 [,) +∞ ) ⊆ ℝ )
215 214 sselda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑚 ∈ ℝ )
216 215 adantlr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑚 ∈ ℝ )
217 216 flcld ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( ⌊ ‘ 𝑚 ) ∈ ℤ )
218 simplr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → seq 1 ( + , 𝐹 ) ⇝ 𝑡 )
219 43 ad2antrr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℂ )
220 1red ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 1 ∈ ℝ )
221 74 ad2antrr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑀 ∈ ℝ )
222 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑀 ∈ ℕ )
223 222 nnge1d ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 1 ≤ 𝑀 )
224 elicopnf ⊢ ( 𝑀 ∈ ℝ → ( 𝑚 ∈ ( 𝑀 [,) +∞ ) ↔ ( 𝑚 ∈ ℝ ∧ 𝑀 ≤ 𝑚 ) ) )
225 74 224 syl ⊢ ( 𝜑 → ( 𝑚 ∈ ( 𝑀 [,) +∞ ) ↔ ( 𝑚 ∈ ℝ ∧ 𝑀 ≤ 𝑚 ) ) )
226 225 simplbda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑀 ≤ 𝑚 )
227 226 adantlr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑀 ≤ 𝑚 )
228 220 221 216 223 227 letrd ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 1 ≤ 𝑚 )
229 flge1nn ⊢ ( ( 𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ) → ( ⌊ ‘ 𝑚 ) ∈ ℕ )
230 216 228 229 syl2anc ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( ⌊ ‘ 𝑚 ) ∈ ℕ )
231 219 230 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ∈ ℂ )
232 nnex ⊢ ℕ ∈ V
233 232 mptex ⊢ ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ∈ V
234 233 a1i ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ∈ V )
235 219 adantr ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℂ )
236 eluznn ⊢ ( ( ( ⌊ ‘ 𝑚 ) ∈ ℕ ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑖 ∈ ℕ )
237 230 236 sylan ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑖 ∈ ℕ )
238 235 237 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ∈ ℂ )
239 fveq2 ⊢ ( 𝑘 = 𝑖 → ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) = ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) )
240 239 oveq2d ⊢ ( 𝑘 = 𝑖 → ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) = ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) )
241 eqid ⊢ ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) )
242 ovex ⊢ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ∈ V
243 240 241 242 fvmpt3i ⊢ ( 𝑖 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ‘ 𝑖 ) = ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) )
244 237 243 syl ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ‘ 𝑖 ) = ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) )
245 211 217 218 231 234 238 244 climsubc2 ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ⇝ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) )
246 232 mptex ⊢ ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ∈ V
247 246 a1i ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ∈ V )
248 fvex ⊢ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ∈ V
249 248 fvconst2 ⊢ ( 𝑖 ∈ ℕ → ( ( ℕ × { ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) } ) ‘ 𝑖 ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) )
250 237 249 syl ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( ℕ × { ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) } ) ‘ 𝑖 ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) )
251 250 oveq1d ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( ( ℕ × { ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) } ) ‘ 𝑖 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) = ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) )
252 244 251 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ‘ 𝑖 ) = ( ( ( ℕ × { ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) } ) ‘ 𝑖 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) )
253 231 adantr ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ∈ ℂ )
254 250 253 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( ℕ × { ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) } ) ‘ 𝑖 ) ∈ ℂ )
255 254 238 subcld ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( ( ℕ × { ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) } ) ‘ 𝑖 ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) ∈ ℂ )
256 252 255 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ‘ 𝑖 ) ∈ ℂ )
257 240 fveq2d ⊢ ( 𝑘 = 𝑖 → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) ) )
258 eqid ⊢ ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) = ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) )
259 fvex ⊢ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ∈ V
260 257 258 259 fvmpt3i ⊢ ( 𝑖 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) ) )
261 237 260 syl ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) ) )
262 244 fveq2d ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( abs ‘ ( ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ‘ 𝑖 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) ) )
263 261 262 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( abs ‘ ( ( 𝑘 ∈ ℕ ↦ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ‘ 𝑖 ) ) )
264 211 245 247 217 256 263 climabs ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ⇝ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) ) )
265 51 ad2antrr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( 2 · 𝑅 ) ∈ ℝ )
266 0red ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 0 ∈ ℝ )
267 74 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑀 ∈ ℝ )
268 78 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 0 < 𝑀 )
269 266 267 215 268 226 ltletrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 0 < 𝑚 )
270 215 269 elrpd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑚 ∈ ℝ+ )
271 nfcsb1v ⊢ Ⅎ 𝑛 ⦋ 𝑚 / 𝑛 ⦌ 𝐴
272 271 nfel1 ⊢ Ⅎ 𝑛 ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ ℝ
273 csbeq1a ⊢ ( 𝑛 = 𝑚 → 𝐴 = ⦋ 𝑚 / 𝑛 ⦌ 𝐴 )
274 273 eleq1d ⊢ ( 𝑛 = 𝑚 → ( 𝐴 ∈ ℝ ↔ ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
275 272 274 rspc ⊢ ( 𝑚 ∈ ℝ+ → ( ∀ 𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ ℝ ) )
276 23 275 mpan9 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ ℝ )
277 270 276 syldan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ ℝ )
278 277 adantlr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ∈ ℝ )
279 265 278 remulcld ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
280 279 recnd ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℂ )
281 1z ⊢ 1 ∈ ℤ
282 17 eqimss2i ⊢ ( ℤ≥ ‘ 1 ) ⊆ ℕ
283 282 232 climconst2 ⊢ ( ( ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℂ ∧ 1 ∈ ℤ ) → ( ℕ × { ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } ) ⇝ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
284 280 281 283 sylancl ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( ℕ × { ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } ) ⇝ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
285 253 238 subcld ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) ∈ ℂ )
286 285 abscld ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) ) ∈ ℝ )
287 261 286 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ∈ ℝ )
288 ovex ⊢ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ V
289 288 fvconst2 ⊢ ( 𝑖 ∈ ℕ → ( ( ℕ × { ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } ) ‘ 𝑖 ) = ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
290 237 289 syl ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( ℕ × { ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } ) ‘ 𝑖 ) = ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
291 279 adantr ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ∈ ℝ )
292 290 291 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( ℕ × { ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } ) ‘ 𝑖 ) ∈ ℝ )
293 simplll ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝜑 )
294 293 3 syl ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑁 ∈ ℕ )
295 293 7 syl ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑋 ∈ 𝐷 )
296 293 8 syl ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑋 ≠ 1 )
297 222 adantr ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑀 ∈ ℕ )
298 293 11 sylan ⊢ ( ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
299 293 12 syl3an1 ⊢ ( ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐵 ≤ 𝐴 )
300 293 13 syl ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( 𝑛 ∈ ℝ+ ↦ 𝐴 ) ⇝𝑟 0 )
301 293 15 syl ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑅 ∈ ℝ )
302 293 16 syl ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ∀ 𝑢 ∈ ( 0 ..^ 𝑁 ) ( abs ‘ Σ 𝑛 ∈ ( 0 ..^ 𝑢 ) ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ≤ 𝑅 )
303 270 adantlr ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → 𝑚 ∈ ℝ+ )
304 303 adantr ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑚 ∈ ℝ+ )
305 227 adantr ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑀 ≤ 𝑚 )
306 216 adantr ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑚 ∈ ℝ )
307 reflcl ⊢ ( 𝑚 ∈ ℝ → ( ⌊ ‘ 𝑚 ) ∈ ℝ )
308 peano2re ⊢ ( ( ⌊ ‘ 𝑚 ) ∈ ℝ → ( ( ⌊ ‘ 𝑚 ) + 1 ) ∈ ℝ )
309 306 307 308 3syl ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( ⌊ ‘ 𝑚 ) + 1 ) ∈ ℝ )
310 flltp1 ⊢ ( 𝑚 ∈ ℝ → 𝑚 < ( ( ⌊ ‘ 𝑚 ) + 1 ) )
311 306 310 syl ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑚 < ( ( ⌊ ‘ 𝑚 ) + 1 ) )
312 306 309 311 ltled ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑚 ≤ ( ( ⌊ ‘ 𝑚 ) + 1 ) )
313 230 adantr ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ⌊ ‘ 𝑚 ) ∈ ℕ )
314 simpr ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) )
315 1 2 294 4 5 6 295 296 9 297 298 299 300 14 301 302 304 305 312 313 314 dchrisumlem2 ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
316 253 238 abssubd ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ) )
317 261 316 eqtrd ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ 𝑖 ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) ) ) )
318 315 317 290 3brtr4d ⊢ ( ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) ∧ 𝑖 ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑘 ∈ ℕ ↦ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ≤ ( ( ℕ × { ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) } ) ‘ 𝑖 ) )
319 211 217 264 284 287 292 318 climle ⊢ ( ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) ∧ 𝑚 ∈ ( 𝑀 [,) +∞ ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
320 319 ralrimiva ⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) → ∀ 𝑚 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) )
321 oveq1 ⊢ ( 𝑐 = ( 2 · 𝑅 ) → ( 𝑐 · 𝐵 ) = ( ( 2 · 𝑅 ) · 𝐵 ) )
322 321 breq2d ⊢ ( 𝑐 = ( 2 · 𝑅 ) → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ↔ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · 𝐵 ) ) )
323 322 ralbidv ⊢ ( 𝑐 = ( 2 · 𝑅 ) → ( ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ↔ ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · 𝐵 ) ) )
324 2fveq3 ⊢ ( 𝑚 = 𝑥 → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) )
325 324 fvoveq1d ⊢ ( 𝑚 = 𝑥 → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) )
326 vex ⊢ 𝑚 ∈ V
327 326 a1i ⊢ ( 𝑚 = 𝑥 → 𝑚 ∈ V )
328 equequ2 ⊢ ( 𝑚 = 𝑥 → ( 𝑛 = 𝑚 ↔ 𝑛 = 𝑥 ) )
329 328 biimpa ⊢ ( ( 𝑚 = 𝑥 ∧ 𝑛 = 𝑚 ) → 𝑛 = 𝑥 )
330 329 9 syl ⊢ ( ( 𝑚 = 𝑥 ∧ 𝑛 = 𝑚 ) → 𝐴 = 𝐵 )
331 327 330 csbied ⊢ ( 𝑚 = 𝑥 → ⦋ 𝑚 / 𝑛 ⦌ 𝐴 = 𝐵 )
332 331 oveq2d ⊢ ( 𝑚 = 𝑥 → ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) = ( ( 2 · 𝑅 ) · 𝐵 ) )
333 325 332 breq12d ⊢ ( 𝑚 = 𝑥 → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ↔ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · 𝐵 ) ) )
334 333 cbvralvw ⊢ ( ∀ 𝑚 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ↔ ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · 𝐵 ) )
335 323 334 bitr4di ⊢ ( 𝑐 = ( 2 · 𝑅 ) → ( ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ↔ ∀ 𝑚 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) )
336 335 rspcev ⊢ ( ( ( 2 · 𝑅 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑚 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑚 ) ) − 𝑡 ) ) ≤ ( ( 2 · 𝑅 ) · ⦋ 𝑚 / 𝑛 ⦌ 𝐴 ) ) → ∃ 𝑐 ∈ ( 0 [,) +∞ ) ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) )
337 210 320 336 syl2anc ⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) → ∃ 𝑐 ∈ ( 0 [,) +∞ ) ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) )
338 r19.42v ⊢ ( ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ) ↔ ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∃ 𝑐 ∈ ( 0 [,) +∞ ) ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ) )
339 207 337 338 sylanbrc ⊢ ( ( 𝜑 ∧ seq 1 ( + , 𝐹 ) ⇝ 𝑡 ) → ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ) )
340 339 ex ⊢ ( 𝜑 → ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 → ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ) ) )
341 340 eximdv ⊢ ( 𝜑 → ( ∃ 𝑡 seq 1 ( + , 𝐹 ) ⇝ 𝑡 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ) ) )
342 206 341 mpd ⊢ ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , 𝐹 ) ⇝ 𝑡 ∧ ∀ 𝑥 ∈ ( 𝑀 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑡 ) ) ≤ ( 𝑐 · 𝐵 ) ) )