MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrisumlem3 Structured version   Visualization version   GIF version

Theorem dchrisumlem3 25753
Description: Lemma for dchrisum 25754. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.)
Hypotheses
Ref Expression
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
Ref Expression
dchrisumlem3 (𝜑 → ∃𝑡𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)))
Distinct variable groups:   𝑢,𝑛,𝑥,𝑐,𝑡   1 ,𝑐   𝑡,𝑛, 1 ,𝑥   𝑢,𝑐,𝐹,𝑛,𝑡,𝑥   𝐴,𝑐,𝑡,𝑥   𝑁,𝑐,𝑛,𝑡,𝑢,𝑥   𝜑,𝑐,𝑛,𝑡,𝑢,𝑥   𝑅,𝑐,𝑛,𝑢,𝑥   𝐵,𝑐,𝑛   𝑛,𝑍,𝑥   𝐷,𝑐,𝑛,𝑡,𝑥   𝐿,𝑐,𝑛,𝑡,𝑢,𝑥   𝑀,𝑐,𝑛,𝑢,𝑥   𝑋,𝑐,𝑛,𝑡,𝑢,𝑥
Allowed substitution hints:   𝐴(𝑢,𝑛)   𝐵(𝑥,𝑢,𝑡)   𝐷(𝑢)   𝑅(𝑡)   1 (𝑢)   𝐺(𝑥,𝑢,𝑡,𝑛,𝑐)   𝑀(𝑡)   𝑍(𝑢,𝑡,𝑐)

Proof of Theorem dchrisumlem3
Dummy variables 𝑘 𝑚 𝑖 𝑗 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 12134 . . . 4 ℕ = (ℤ‘1)
2 1zzd 11867 . . . . . 6 (𝜑 → 1 ∈ ℤ)
3 simpr 485 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℕ)
4 rpvmasum.g . . . . . . . . . 10 𝐺 = (DChr‘𝑁)
5 rpvmasum.z . . . . . . . . . 10 𝑍 = (ℤ/nℤ‘𝑁)
6 rpvmasum.d . . . . . . . . . 10 𝐷 = (Base‘𝐺)
7 rpvmasum.l . . . . . . . . . 10 𝐿 = (ℤRHom‘𝑍)
8 dchrisum.b . . . . . . . . . . 11 (𝜑𝑋𝐷)
98adantr 481 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → 𝑋𝐷)
103nnzd 11940 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℤ)
114, 5, 6, 7, 9, 10dchrzrhcl 25507 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → (𝑋‘(𝐿𝑖)) ∈ ℂ)
12 dchrisum.4 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)
1312ralrimiva 3151 . . . . . . . . . . 11 (𝜑 → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ)
14 nnrp 12254 . . . . . . . . . . 11 (𝑖 ∈ ℕ → 𝑖 ∈ ℝ+)
15 nfcsb1v 3839 . . . . . . . . . . . . . 14 𝑛𝑖 / 𝑛𝐴
1615nfel1 2965 . . . . . . . . . . . . 13 𝑛𝑖 / 𝑛𝐴 ∈ ℝ
17 csbeq1a 3830 . . . . . . . . . . . . . 14 (𝑛 = 𝑖𝐴 = 𝑖 / 𝑛𝐴)
1817eleq1d 2869 . . . . . . . . . . . . 13 (𝑛 = 𝑖 → (𝐴 ∈ ℝ ↔ 𝑖 / 𝑛𝐴 ∈ ℝ))
1916, 18rspc 3555 . . . . . . . . . . . 12 (𝑖 ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → 𝑖 / 𝑛𝐴 ∈ ℝ))
2019impcom 408 . . . . . . . . . . 11 ((∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ ∧ 𝑖 ∈ ℝ+) → 𝑖 / 𝑛𝐴 ∈ ℝ)
2113, 14, 20syl2an 595 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → 𝑖 / 𝑛𝐴 ∈ ℝ)
2221recnd 10522 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → 𝑖 / 𝑛𝐴 ∈ ℂ)
2311, 22mulcld 10514 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
24 nfcv 2951 . . . . . . . . 9 𝑛𝑖
25 nfcv 2951 . . . . . . . . . 10 𝑛(𝑋‘(𝐿𝑖))
26 nfcv 2951 . . . . . . . . . 10 𝑛 ·
2725, 26, 15nfov 7053 . . . . . . . . 9 𝑛((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)
28 2fveq3 6550 . . . . . . . . . 10 (𝑛 = 𝑖 → (𝑋‘(𝐿𝑛)) = (𝑋‘(𝐿𝑖)))
2928, 17oveq12d 7041 . . . . . . . . 9 (𝑛 = 𝑖 → ((𝑋‘(𝐿𝑛)) · 𝐴) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
30 dchrisum.7 . . . . . . . . 9 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿𝑛)) · 𝐴))
3124, 27, 29, 30fvmptf 6662 . . . . . . . 8 ((𝑖 ∈ ℕ ∧ ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
323, 23, 31syl2anc 584 . . . . . . 7 ((𝜑𝑖 ∈ ℕ) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
3332, 23eqeltrd 2885 . . . . . 6 ((𝜑𝑖 ∈ ℕ) → (𝐹𝑖) ∈ ℂ)
341, 2, 33serf 13252 . . . . 5 (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ)
3534ffvelrnda 6723 . . . 4 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℂ)
3612recnd 10522 . . . . . . . . 9 ((𝜑𝑛 ∈ ℝ+) → 𝐴 ∈ ℂ)
3736ralrimiva 3151 . . . . . . . 8 (𝜑 → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℂ)
3837adantr 481 . . . . . . 7 ((𝜑𝑒 ∈ ℝ+) → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℂ)
39 id 22 . . . . . . . 8 (𝑒 ∈ ℝ+𝑒 ∈ ℝ+)
40 2re 11565 . . . . . . . . . 10 2 ∈ ℝ
41 dchrisum.9 . . . . . . . . . 10 (𝜑𝑅 ∈ ℝ)
42 remulcl 10475 . . . . . . . . . 10 ((2 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (2 · 𝑅) ∈ ℝ)
4340, 41, 42sylancr 587 . . . . . . . . 9 (𝜑 → (2 · 𝑅) ∈ ℝ)
44 rpvmasum.a . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ)
45 lbfzo0 12931 . . . . . . . . . . . 12 (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
4644, 45sylibr 235 . . . . . . . . . . 11 (𝜑 → 0 ∈ (0..^𝑁))
47 dchrisum.10 . . . . . . . . . . 11 (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅)
48 oveq2 7031 . . . . . . . . . . . . . . . . 17 (𝑢 = 0 → (0..^𝑢) = (0..^0))
49 fzo0 12915 . . . . . . . . . . . . . . . . 17 (0..^0) = ∅
5048, 49syl6eq 2849 . . . . . . . . . . . . . . . 16 (𝑢 = 0 → (0..^𝑢) = ∅)
5150sumeq1d 14895 . . . . . . . . . . . . . . 15 (𝑢 = 0 → Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ ∅ (𝑋‘(𝐿𝑛)))
52 sum0 14915 . . . . . . . . . . . . . . 15 Σ𝑛 ∈ ∅ (𝑋‘(𝐿𝑛)) = 0
5351, 52syl6eq 2849 . . . . . . . . . . . . . 14 (𝑢 = 0 → Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛)) = 0)
5453abs00bd 14489 . . . . . . . . . . . . 13 (𝑢 = 0 → (abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) = 0)
5554breq1d 4978 . . . . . . . . . . . 12 (𝑢 = 0 → ((abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅 ↔ 0 ≤ 𝑅))
5655rspcv 3557 . . . . . . . . . . 11 (0 ∈ (0..^𝑁) → (∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅 → 0 ≤ 𝑅))
5746, 47, 56sylc 65 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝑅)
58 0le2 11593 . . . . . . . . . . 11 0 ≤ 2
59 mulge0 11012 . . . . . . . . . . 11 (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅)) → 0 ≤ (2 · 𝑅))
6040, 58, 59mpanl12 698 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 0 ≤ (2 · 𝑅))
6141, 57, 60syl2anc 584 . . . . . . . . 9 (𝜑 → 0 ≤ (2 · 𝑅))
6243, 61ge0p1rpd 12315 . . . . . . . 8 (𝜑 → ((2 · 𝑅) + 1) ∈ ℝ+)
63 rpdivcl 12268 . . . . . . . 8 ((𝑒 ∈ ℝ+ ∧ ((2 · 𝑅) + 1) ∈ ℝ+) → (𝑒 / ((2 · 𝑅) + 1)) ∈ ℝ+)
6439, 62, 63syl2anr 596 . . . . . . 7 ((𝜑𝑒 ∈ ℝ+) → (𝑒 / ((2 · 𝑅) + 1)) ∈ ℝ+)
65 dchrisum.6 . . . . . . . 8 (𝜑 → (𝑛 ∈ ℝ+𝐴) ⇝𝑟 0)
6665adantr 481 . . . . . . 7 ((𝜑𝑒 ∈ ℝ+) → (𝑛 ∈ ℝ+𝐴) ⇝𝑟 0)
6738, 64, 66rlimi 14708 . . . . . 6 ((𝜑𝑒 ∈ ℝ+) → ∃𝑚 ∈ ℝ ∀𝑛 ∈ ℝ+ (𝑚𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))))
68 simpr 485 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → 𝑚 ∈ ℝ)
69 dchrisum.3 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℕ)
7069nnred 11507 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℝ)
7170adantr 481 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → 𝑀 ∈ ℝ)
7268, 71ifcld 4432 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ)
73 0red 10497 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → 0 ∈ ℝ)
7469nngt0d 11540 . . . . . . . . . . . . 13 (𝜑 → 0 < 𝑀)
7574adantr 481 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → 0 < 𝑀)
76 max1 12432 . . . . . . . . . . . . 13 ((𝑀 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))
7770, 76sylan 580 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))
7873, 71, 72, 75, 77ltletrd 10653 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℝ) → 0 < if(𝑀𝑚, 𝑚, 𝑀))
7972, 78elrpd 12282 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ+)
8079adantlr 711 . . . . . . . . 9 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ+)
81 nfv 1896 . . . . . . . . . . 11 𝑛 𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀)
82 nfcv 2951 . . . . . . . . . . . . 13 𝑛abs
83 nfcsb1v 3839 . . . . . . . . . . . . . 14 𝑛if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴
84 nfcv 2951 . . . . . . . . . . . . . 14 𝑛
85 nfcv 2951 . . . . . . . . . . . . . 14 𝑛0
8683, 84, 85nfov 7053 . . . . . . . . . . . . 13 𝑛(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)
8782, 86nffv 6555 . . . . . . . . . . . 12 𝑛(abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0))
88 nfcv 2951 . . . . . . . . . . . 12 𝑛 <
89 nfcv 2951 . . . . . . . . . . . 12 𝑛(𝑒 / ((2 · 𝑅) + 1))
9087, 88, 89nfbr 5015 . . . . . . . . . . 11 𝑛(abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))
9181, 90nfim 1882 . . . . . . . . . 10 𝑛(𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀) → (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)))
92 breq2 4972 . . . . . . . . . . 11 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → (𝑚𝑛𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀)))
93 csbeq1a 3830 . . . . . . . . . . . . 13 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → 𝐴 = if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)
9493fvoveq1d 7045 . . . . . . . . . . . 12 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → (abs‘(𝐴 − 0)) = (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)))
9594breq1d 4978 . . . . . . . . . . 11 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → ((abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) ↔ (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))))
9692, 95imbi12d 346 . . . . . . . . . 10 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → ((𝑚𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) ↔ (𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀) → (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)))))
9791, 96rspc 3555 . . . . . . . . 9 (if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ+ → (∀𝑛 ∈ ℝ+ (𝑚𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) → (𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀) → (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)))))
9880, 97syl 17 . . . . . . . 8 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (∀𝑛 ∈ ℝ+ (𝑚𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) → (𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀) → (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)))))
9970ad2antrr 722 . . . . . . . . . 10 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑀 ∈ ℝ)
100 max2 12434 . . . . . . . . . 10 ((𝑀 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀))
10199, 100sylancom 588 . . . . . . . . 9 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀))
10213ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ)
10383nfel1 2965 . . . . . . . . . . . . . . . . . . 19 𝑛if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℝ
10493eleq1d 2869 . . . . . . . . . . . . . . . . . . 19 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → (𝐴 ∈ ℝ ↔ if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℝ))
105103, 104rspc 3555 . . . . . . . . . . . . . . . . . 18 (if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℝ))
10680, 102, 105sylc 65 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℝ)
107106recnd 10522 . . . . . . . . . . . . . . . 16 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℂ)
108107subid1d 10840 . . . . . . . . . . . . . . 15 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0) = if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)
109108fveq2d 6549 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) = (abs‘if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴))
11072adantlr 711 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ)
11199, 76sylancom 588 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))
112 elicopnf 12687 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ℝ → (if(𝑀𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) ↔ (if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ ∧ 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))))
11399, 112syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (if(𝑀𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) ↔ (if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ ∧ 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))))
114110, 111, 113mpbir2and 709 . . . . . . . . . . . . . . . 16 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞))
11544ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑁 ∈ ℕ)
116 rpvmasum.1 . . . . . . . . . . . . . . . . . 18 1 = (0g𝐺)
1178ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑋𝐷)
118 dchrisum.n1 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋1 )
119118ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑋1 )
120 dchrisum.2 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑥𝐴 = 𝐵)
12169ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑀 ∈ ℕ)
12212ad4ant14 748 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)
123 simpll 763 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝜑)
124 dchrisum.5 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+) ∧ (𝑀𝑛𝑛𝑥)) → 𝐵𝐴)
125123, 124syl3an1 1156 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+) ∧ (𝑀𝑛𝑛𝑥)) → 𝐵𝐴)
12665ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (𝑛 ∈ ℝ+𝐴) ⇝𝑟 0)
1275, 7, 115, 4, 6, 116, 117, 119, 120, 121, 122, 125, 126, 30dchrisumlema 25750 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ+if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℝ) ∧ (if(𝑀𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) → 0 ≤ if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)))
128127simprd 496 . . . . . . . . . . . . . . . 16 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (if(𝑀𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) → 0 ≤ if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴))
129114, 128mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 0 ≤ if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)
130106, 129absidd 14620 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (abs‘if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) = if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)
131109, 130eqtrd 2833 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) = if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)
132131breq1d 4978 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) ↔ if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 < (𝑒 / ((2 · 𝑅) + 1))))
133 rpre 12251 . . . . . . . . . . . . . 14 (𝑒 ∈ ℝ+𝑒 ∈ ℝ)
134133ad2antlr 723 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑒 ∈ ℝ)
13562ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2 · 𝑅) + 1) ∈ ℝ+)
136106, 134, 135ltmuldiv2d 12333 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 < (𝑒 / ((2 · 𝑅) + 1))))
137132, 136bitr4d 283 . . . . . . . . . . 11 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) ↔ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒))
13843ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (2 · 𝑅) ∈ ℝ)
139135rpred 12285 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2 · 𝑅) + 1) ∈ ℝ)
140138lep1d 11425 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (2 · 𝑅) ≤ ((2 · 𝑅) + 1))
141138, 139, 106, 129, 140lemul1ad 11433 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ≤ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴))
142138, 106remulcld 10524 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ)
143139, 106remulcld 10524 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ)
144 lelttr 10584 . . . . . . . . . . . . 13 ((((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ ∧ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) → ((((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ≤ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∧ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒))
145142, 143, 134, 144syl3anc 1364 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ≤ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∧ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒))
146141, 145mpand 691 . . . . . . . . . . 11 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒 → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒))
147137, 146sylbid 241 . . . . . . . . . 10 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒))
148 1red 10495 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℝ) → 1 ∈ ℝ)
14969adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℝ) → 𝑀 ∈ ℕ)
150149nnge1d 11539 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℝ) → 1 ≤ 𝑀)
151148, 71, 72, 150, 77letrd 10650 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℝ) → 1 ≤ if(𝑀𝑚, 𝑚, 𝑀))
152 flge1nn 13045 . . . . . . . . . . . . 13 ((if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ ∧ 1 ≤ if(𝑀𝑚, 𝑚, 𝑀)) → (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ)
15372, 151, 152syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ)
154153adantlr 711 . . . . . . . . . . 11 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ)
15544ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑁 ∈ ℕ)
1568ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑋𝐷)
157118ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑋1 )
15869ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑀 ∈ ℕ)
15912ad4ant14 748 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)
1601243adant1r 1170 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℝ) ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+) ∧ (𝑀𝑛𝑛𝑥)) → 𝐵𝐴)
1611603adant1r 1170 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+) ∧ (𝑀𝑛𝑛𝑥)) → 𝐵𝐴)
16265ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (𝑛 ∈ ℝ+𝐴) ⇝𝑟 0)
16341ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑅 ∈ ℝ)
16447ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅)
16579adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ+)
16677adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))
16772adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ)
168 fllep1 13025 . . . . . . . . . . . . . . . 16 (if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ → if(𝑀𝑚, 𝑚, 𝑀) ≤ ((⌊‘if(𝑀𝑚, 𝑚, 𝑀)) + 1))
169167, 168syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → if(𝑀𝑚, 𝑚, 𝑀) ≤ ((⌊‘if(𝑀𝑚, 𝑚, 𝑀)) + 1))
170153adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ)
171 simpr 485 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))
1725, 7, 155, 4, 6, 116, 156, 157, 120, 158, 159, 161, 162, 30, 163, 164, 165, 166, 169, 170, 171dchrisumlem2 25752 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴))
173172adantllr 715 . . . . . . . . . . . . 13 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴))
17434ad3antrrr 726 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → seq1( + , 𝐹):ℕ⟶ℂ)
175 eluznn 12171 . . . . . . . . . . . . . . . . . 18 (((⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑘 ∈ ℕ)
176154, 175sylan 580 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑘 ∈ ℕ)
177174, 176ffvelrnd 6724 . . . . . . . . . . . . . . . 16 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (seq1( + , 𝐹)‘𝑘) ∈ ℂ)
178154adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ)
179174, 178ffvelrnd 6724 . . . . . . . . . . . . . . . 16 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))) ∈ ℂ)
180177, 179subcld 10851 . . . . . . . . . . . . . . 15 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → ((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) ∈ ℂ)
181180abscld 14634 . . . . . . . . . . . . . 14 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ∈ ℝ)
182142adantr 481 . . . . . . . . . . . . . 14 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ)
183134adantr 481 . . . . . . . . . . . . . 14 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑒 ∈ ℝ)
184 lelttr 10584 . . . . . . . . . . . . . 14 (((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ∈ ℝ ∧ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) → (((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∧ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
185181, 182, 183, 184syl3anc 1364 . . . . . . . . . . . . 13 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∧ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
186173, 185mpand 691 . . . . . . . . . . . 12 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒 → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
187186ralrimdva 3158 . . . . . . . . . . 11 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒 → ∀𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
188 fveq2 6545 . . . . . . . . . . . . 13 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → (ℤ𝑗) = (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))
189 fveq2 6545 . . . . . . . . . . . . . . . 16 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → (seq1( + , 𝐹)‘𝑗) = (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))
190189oveq2d 7039 . . . . . . . . . . . . . . 15 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → ((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗)) = ((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))))
191190fveq2d 6549 . . . . . . . . . . . . . 14 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) = (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))))
192191breq1d 4978 . . . . . . . . . . . . 13 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → ((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒 ↔ (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
193188, 192raleqbidv 3363 . . . . . . . . . . . 12 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → (∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒 ↔ ∀𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
194193rspcev 3561 . . . . . . . . . . 11 (((⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ ∧ ∀𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)
195154, 187, 194syl6an 680 . . . . . . . . . 10 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒))
196147, 195syld 47 . . . . . . . . 9 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒))
197101, 196embantd 59 . . . . . . . 8 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀) → (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒))
19898, 197syld 47 . . . . . . 7 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (∀𝑛 ∈ ℝ+ (𝑚𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒))
199198rexlimdva 3249 . . . . . 6 ((𝜑𝑒 ∈ ℝ+) → (∃𝑚 ∈ ℝ ∀𝑛 ∈ ℝ+ (𝑚𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒))
20067, 199mpd 15 . . . . 5 ((𝜑𝑒 ∈ ℝ+) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)
201200ralrimiva 3151 . . . 4 (𝜑 → ∀𝑒 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)
202 seqex 13225 . . . . 5 seq1( + , 𝐹) ∈ V
203202a1i 11 . . . 4 (𝜑 → seq1( + , 𝐹) ∈ V)
2041, 35, 201, 203caucvg 14873 . . 3 (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
205202eldm 5662 . . 3 (seq1( + , 𝐹) ∈ dom ⇝ ↔ ∃𝑡seq1( + , 𝐹) ⇝ 𝑡)
206204, 205sylib 219 . 2 (𝜑 → ∃𝑡seq1( + , 𝐹) ⇝ 𝑡)
207 simpr 485 . . . . 5 ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → seq1( + , 𝐹) ⇝ 𝑡)
208 elrege0 12696 . . . . . . . 8 ((2 · 𝑅) ∈ (0[,)+∞) ↔ ((2 · 𝑅) ∈ ℝ ∧ 0 ≤ (2 · 𝑅)))
20943, 61, 208sylanbrc 583 . . . . . . 7 (𝜑 → (2 · 𝑅) ∈ (0[,)+∞))
210209adantr 481 . . . . . 6 ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → (2 · 𝑅) ∈ (0[,)+∞))
211 eqid 2797 . . . . . . . 8 (ℤ‘(⌊‘𝑚)) = (ℤ‘(⌊‘𝑚))
212 pnfxr 10548 . . . . . . . . . . . 12 +∞ ∈ ℝ*
213 icossre 12671 . . . . . . . . . . . 12 ((𝑀 ∈ ℝ ∧ +∞ ∈ ℝ*) → (𝑀[,)+∞) ⊆ ℝ)
21470, 212, 213sylancl 586 . . . . . . . . . . 11 (𝜑 → (𝑀[,)+∞) ⊆ ℝ)
215214sselda 3895 . . . . . . . . . 10 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ)
216215adantlr 711 . . . . . . . . 9 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ)
217216flcld 13022 . . . . . . . 8 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (⌊‘𝑚) ∈ ℤ)
218 simplr 765 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → seq1( + , 𝐹) ⇝ 𝑡)
21934ad2antrr 722 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → seq1( + , 𝐹):ℕ⟶ℂ)
220 1red 10495 . . . . . . . . . . . . 13 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 1 ∈ ℝ)
22170ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℝ)
22269ad2antrr 722 . . . . . . . . . . . . . 14 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℕ)
223222nnge1d 11539 . . . . . . . . . . . . 13 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 1 ≤ 𝑀)
224 elicopnf 12687 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℝ → (𝑚 ∈ (𝑀[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 𝑀𝑚)))
22570, 224syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑚 ∈ (𝑀[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 𝑀𝑚)))
226225simplbda 500 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 𝑀𝑚)
227226adantlr 711 . . . . . . . . . . . . 13 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀𝑚)
228220, 221, 216, 223, 227letrd 10650 . . . . . . . . . . . 12 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 1 ≤ 𝑚)
229 flge1nn 13045 . . . . . . . . . . . 12 ((𝑚 ∈ ℝ ∧ 1 ≤ 𝑚) → (⌊‘𝑚) ∈ ℕ)
230216, 228, 229syl2anc 584 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (⌊‘𝑚) ∈ ℕ)
231219, 230ffvelrnd 6724 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈ ℂ)
232 nnex 11498 . . . . . . . . . . . 12 ℕ ∈ V
233232mptex 6859 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ∈ V
234233a1i 11 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ∈ V)
235219adantr 481 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → seq1( + , 𝐹):ℕ⟶ℂ)
236 eluznn 12171 . . . . . . . . . . . 12 (((⌊‘𝑚) ∈ ℕ ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑖 ∈ ℕ)
237230, 236sylan 580 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑖 ∈ ℕ)
238235, 237ffvelrnd 6724 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (seq1( + , 𝐹)‘𝑖) ∈ ℂ)
239 fveq2 6545 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (seq1( + , 𝐹)‘𝑘) = (seq1( + , 𝐹)‘𝑖))
240239oveq2d 7039 . . . . . . . . . . . 12 (𝑘 = 𝑖 → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))
241 eqid 2797 . . . . . . . . . . . 12 (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) = (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))
242 ovex 7055 . . . . . . . . . . . 12 ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)) ∈ V
243240, 241, 242fvmpt3i 6647 . . . . . . . . . . 11 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))
244237, 243syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))
245211, 217, 218, 231, 234, 238, 244climsubc2 14833 . . . . . . . . 9 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ⇝ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡))
246232mptex 6859 . . . . . . . . . 10 (𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) ∈ V
247246a1i 11 . . . . . . . . 9 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) ∈ V)
248 fvex 6558 . . . . . . . . . . . . . 14 (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈ V
249248fvconst2 6840 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → ((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) = (seq1( + , 𝐹)‘(⌊‘𝑚)))
250237, 249syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) = (seq1( + , 𝐹)‘(⌊‘𝑚)))
251250oveq1d 7038 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) − (seq1( + , 𝐹)‘𝑖)) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))
252244, 251eqtr4d 2836 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) = (((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) − (seq1( + , 𝐹)‘𝑖)))
253231adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈ ℂ)
254250, 253eqeltrd 2885 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) ∈ ℂ)
255254, 238subcld 10851 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) − (seq1( + , 𝐹)‘𝑖)) ∈ ℂ)
256252, 255eqeltrd 2885 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) ∈ ℂ)
257240fveq2d 6549 . . . . . . . . . . . 12 (𝑘 = 𝑖 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))))
258 eqid 2797 . . . . . . . . . . . 12 (𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) = (𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))
259 fvex 6558 . . . . . . . . . . . 12 (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ∈ V
260257, 258, 259fvmpt3i 6647 . . . . . . . . . . 11 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))))
261237, 260syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))))
262244fveq2d 6549 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (abs‘((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))))
263261, 262eqtr4d 2836 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖)))
264211, 245, 247, 217, 256, 263climabs 14798 . . . . . . . 8 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) ⇝ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)))
26543ad2antrr 722 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (2 · 𝑅) ∈ ℝ)
266 0red 10497 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 0 ∈ ℝ)
26770adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℝ)
26874adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 0 < 𝑀)
269266, 267, 215, 268, 226ltletrd 10653 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 0 < 𝑚)
270215, 269elrpd 12282 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ+)
271 nfcsb1v 3839 . . . . . . . . . . . . . . . 16 𝑛𝑚 / 𝑛𝐴
272271nfel1 2965 . . . . . . . . . . . . . . 15 𝑛𝑚 / 𝑛𝐴 ∈ ℝ
273 csbeq1a 3830 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚𝐴 = 𝑚 / 𝑛𝐴)
274273eleq1d 2869 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → (𝐴 ∈ ℝ ↔ 𝑚 / 𝑛𝐴 ∈ ℝ))
275272, 274rspc 3555 . . . . . . . . . . . . . 14 (𝑚 ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → 𝑚 / 𝑛𝐴 ∈ ℝ))
27613, 275mpan9 507 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℝ+) → 𝑚 / 𝑛𝐴 ∈ ℝ)
277270, 276syldan 591 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 𝑚 / 𝑛𝐴 ∈ ℝ)
278277adantlr 711 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑚 / 𝑛𝐴 ∈ ℝ)
279265, 278remulcld 10524 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ∈ ℝ)
280279recnd 10522 . . . . . . . . 9 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ∈ ℂ)
281 1z 11866 . . . . . . . . 9 1 ∈ ℤ
2821eqimss2i 3953 . . . . . . . . . 10 (ℤ‘1) ⊆ ℕ
283282, 232climconst2 14743 . . . . . . . . 9 ((((2 · 𝑅) · 𝑚 / 𝑛𝐴) ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)}) ⇝ ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
284280, 281, 283sylancl 586 . . . . . . . 8 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)}) ⇝ ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
285253, 238subcld 10851 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)) ∈ ℂ)
286285abscld 14634 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) ∈ ℝ)
287261, 286eqeltrd 2885 . . . . . . . 8 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) ∈ ℝ)
288 ovex 7055 . . . . . . . . . . 11 ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ∈ V
289288fvconst2 6840 . . . . . . . . . 10 (𝑖 ∈ ℕ → ((ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)})‘𝑖) = ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
290237, 289syl 17 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)})‘𝑖) = ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
291279adantr 481 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ∈ ℝ)
292290, 291eqeltrd 2885 . . . . . . . 8 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)})‘𝑖) ∈ ℝ)
293 simplll 771 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝜑)
294293, 44syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑁 ∈ ℕ)
295293, 8syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑋𝐷)
296293, 118syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑋1 )
297222adantr 481 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑀 ∈ ℕ)
298293, 12sylan 580 . . . . . . . . . 10 (((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)
299293, 124syl3an1 1156 . . . . . . . . . 10 (((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+) ∧ (𝑀𝑛𝑛𝑥)) → 𝐵𝐴)
300293, 65syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (𝑛 ∈ ℝ+𝐴) ⇝𝑟 0)
301293, 41syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑅 ∈ ℝ)
302293, 47syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅)
303270adantlr 711 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ+)
304303adantr 481 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑚 ∈ ℝ+)
305227adantr 481 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑀𝑚)
306216adantr 481 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑚 ∈ ℝ)
307 reflcl 13020 . . . . . . . . . . . 12 (𝑚 ∈ ℝ → (⌊‘𝑚) ∈ ℝ)
308 peano2re 10666 . . . . . . . . . . . 12 ((⌊‘𝑚) ∈ ℝ → ((⌊‘𝑚) + 1) ∈ ℝ)
309306, 307, 3083syl 18 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((⌊‘𝑚) + 1) ∈ ℝ)
310 flltp1 13024 . . . . . . . . . . . 12 (𝑚 ∈ ℝ → 𝑚 < ((⌊‘𝑚) + 1))
311306, 310syl 17 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑚 < ((⌊‘𝑚) + 1))
312306, 309, 311ltled 10641 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑚 ≤ ((⌊‘𝑚) + 1))
313230adantr 481 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (⌊‘𝑚) ∈ ℕ)
314 simpr 485 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑖 ∈ (ℤ‘(⌊‘𝑚)))
3155, 7, 294, 4, 6, 116, 295, 296, 120, 297, 298, 299, 300, 30, 301, 302, 304, 305, 312, 313, 314dchrisumlem2 25752 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (abs‘((seq1( + , 𝐹)‘𝑖) − (seq1( + , 𝐹)‘(⌊‘𝑚)))) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
316253, 238abssubd 14651 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) = (abs‘((seq1( + , 𝐹)‘𝑖) − (seq1( + , 𝐹)‘(⌊‘𝑚)))))
317261, 316eqtrd 2833 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((seq1( + , 𝐹)‘𝑖) − (seq1( + , 𝐹)‘(⌊‘𝑚)))))
318315, 317, 2903brtr4d 5000 . . . . . . . 8 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) ≤ ((ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)})‘𝑖))
319211, 217, 264, 284, 287, 292, 318climle 14834 . . . . . . 7 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
320319ralrimiva 3151 . . . . . 6 ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → ∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
321 oveq1 7030 . . . . . . . . . 10 (𝑐 = (2 · 𝑅) → (𝑐 · 𝐵) = ((2 · 𝑅) · 𝐵))
322321breq2d 4980 . . . . . . . . 9 (𝑐 = (2 · 𝑅) → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵)))
323322ralbidv 3166 . . . . . . . 8 (𝑐 = (2 · 𝑅) → (∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵) ↔ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵)))
324 2fveq3 6550 . . . . . . . . . . 11 (𝑚 = 𝑥 → (seq1( + , 𝐹)‘(⌊‘𝑚)) = (seq1( + , 𝐹)‘(⌊‘𝑥)))
325324fvoveq1d 7045 . . . . . . . . . 10 (𝑚 = 𝑥 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)))
326 vex 3443 . . . . . . . . . . . . 13 𝑚 ∈ V
327326a1i 11 . . . . . . . . . . . 12 (𝑚 = 𝑥𝑚 ∈ V)
328 equequ2 2014 . . . . . . . . . . . . . 14 (𝑚 = 𝑥 → (𝑛 = 𝑚𝑛 = 𝑥))
329328biimpa 477 . . . . . . . . . . . . 13 ((𝑚 = 𝑥𝑛 = 𝑚) → 𝑛 = 𝑥)
330329, 120syl 17 . . . . . . . . . . . 12 ((𝑚 = 𝑥𝑛 = 𝑚) → 𝐴 = 𝐵)
331327, 330csbied 3850 . . . . . . . . . . 11 (𝑚 = 𝑥𝑚 / 𝑛𝐴 = 𝐵)
332331oveq2d 7039 . . . . . . . . . 10 (𝑚 = 𝑥 → ((2 · 𝑅) · 𝑚 / 𝑛𝐴) = ((2 · 𝑅) · 𝐵))
333325, 332breq12d 4981 . . . . . . . . 9 (𝑚 = 𝑥 → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵)))
334333cbvralv 3405 . . . . . . . 8 (∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ↔ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵))
335323, 334syl6bbr 290 . . . . . . 7 (𝑐 = (2 · 𝑅) → (∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵) ↔ ∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴)))
336335rspcev 3561 . . . . . 6 (((2 · 𝑅) ∈ (0[,)+∞) ∧ ∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴)) → ∃𝑐 ∈ (0[,)+∞)∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))
337210, 320, 336syl2anc 584 . . . . 5 ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → ∃𝑐 ∈ (0[,)+∞)∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))
338 r19.42v 3313 . . . . 5 (∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)) ↔ (seq1( + , 𝐹) ⇝ 𝑡 ∧ ∃𝑐 ∈ (0[,)+∞)∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)))
339207, 337, 338sylanbrc 583 . . . 4 ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → ∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)))
340339ex 413 . . 3 (𝜑 → (seq1( + , 𝐹) ⇝ 𝑡 → ∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))))
341340eximdv 1899 . 2 (𝜑 → (∃𝑡seq1( + , 𝐹) ⇝ 𝑡 → ∃𝑡𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))))
342206, 341mpd 15 1 (𝜑 → ∃𝑡𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1080   = wceq 1525  wex 1765  wcel 2083  wne 2986  wral 3107  wrex 3108  Vcvv 3440  csb 3817  wss 3865  c0 4217  ifcif 4387  {csn 4478   class class class wbr 4968  cmpt 5047   × cxp 5448  dom cdm 5450  wf 6228  cfv 6232  (class class class)co 7023  cc 10388  cr 10389  0cc0 10390  1c1 10391   + caddc 10393   · cmul 10395  +∞cpnf 10525  *cxr 10527   < clt 10528  cle 10529  cmin 10723   / cdiv 11151  cn 11492  2c2 11546  cz 11835  cuz 12097  +crp 12243  [,)cico 12594  ..^cfzo 12887  cfl 13014  seqcseq 13223  abscabs 14431  cli 14679  𝑟 crli 14680  Σcsu 14880  Basecbs 16316  0gc0g 16546  ℤRHomczrh 20333  ℤ/nczn 20336  DChrcdchr 25494
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-inf2 8957  ax-cnex 10446  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466  ax-pre-mulgt0 10467  ax-pre-sup 10468  ax-addf 10469  ax-mulf 10470
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-fal 1538  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-se 5410  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-isom 6241  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-of 7274  df-om 7444  df-1st 7552  df-2nd 7553  df-tpos 7750  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-oadd 7964  df-er 8146  df-ec 8148  df-qs 8152  df-map 8265  df-pm 8266  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-sup 8759  df-inf 8760  df-oi 8827  df-card 9221  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534  df-sub 10725  df-neg 10726  df-div 11152  df-nn 11493  df-2 11554  df-3 11555  df-4 11556  df-5 11557  df-6 11558  df-7 11559  df-8 11560  df-9 11561  df-n0 11752  df-xnn0 11822  df-z 11836  df-dec 11953  df-uz 12098  df-rp 12244  df-ico 12598  df-fz 12747  df-fzo 12888  df-fl 13016  df-mod 13092  df-seq 13224  df-exp 13284  df-hash 13545  df-cj 14296  df-re 14297  df-im 14298  df-sqrt 14432  df-abs 14433  df-limsup 14666  df-clim 14683  df-rlim 14684  df-sum 14881  df-dvds 15445  df-gcd 15681  df-phi 15936  df-struct 16318  df-ndx 16319  df-slot 16320  df-base 16322  df-sets 16323  df-ress 16324  df-plusg 16411  df-mulr 16412  df-starv 16413  df-sca 16414  df-vsca 16415  df-ip 16416  df-tset 16417  df-ple 16418  df-ds 16420  df-unif 16421  df-0g 16548  df-imas 16614  df-qus 16615  df-mgm 17685  df-sgrp 17727  df-mnd 17738  df-mhm 17778  df-grp 17868  df-minusg 17869  df-sbg 17870  df-mulg 17986  df-subg 18034  df-nsg 18035  df-eqg 18036  df-ghm 18101  df-cmn 18639  df-abl 18640  df-mgp 18934  df-ur 18946  df-ring 18993  df-cring 18994  df-oppr 19067  df-dvdsr 19085  df-unit 19086  df-invr 19116  df-rnghom 19161  df-subrg 19227  df-lmod 19330  df-lss 19398  df-lsp 19438  df-sra 19638  df-rgmod 19639  df-lidl 19640  df-rsp 19641  df-2idl 19698  df-cnfld 20232  df-zring 20304  df-zrh 20337  df-zn 20340  df-dchr 25495
This theorem is referenced by:  dchrisum  25754
  Copyright terms: Public domain W3C validator