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

Theorem dchrisumlem3 26839
Description: Lemma for dchrisum 26840. 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 12806 . . . 4 ℕ = (ℤ‘1)
2 1zzd 12534 . . . . . 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 12526 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℤ)
114, 5, 6, 7, 9, 10dchrzrhcl 26593 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → (𝑋‘(𝐿𝑖)) ∈ ℂ)
12 dchrisum.4 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)
1312ralrimiva 3143 . . . . . . . . . . 11 (𝜑 → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ)
14 nnrp 12926 . . . . . . . . . . 11 (𝑖 ∈ ℕ → 𝑖 ∈ ℝ+)
15 nfcsb1v 3880 . . . . . . . . . . . . . 14 𝑛𝑖 / 𝑛𝐴
1615nfel1 2923 . . . . . . . . . . . . 13 𝑛𝑖 / 𝑛𝐴 ∈ ℝ
17 csbeq1a 3869 . . . . . . . . . . . . . 14 (𝑛 = 𝑖𝐴 = 𝑖 / 𝑛𝐴)
1817eleq1d 2822 . . . . . . . . . . . . 13 (𝑛 = 𝑖 → (𝐴 ∈ ℝ ↔ 𝑖 / 𝑛𝐴 ∈ ℝ))
1916, 18rspc 3569 . . . . . . . . . . . 12 (𝑖 ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → 𝑖 / 𝑛𝐴 ∈ ℝ))
2019impcom 408 . . . . . . . . . . 11 ((∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ ∧ 𝑖 ∈ ℝ+) → 𝑖 / 𝑛𝐴 ∈ ℝ)
2113, 14, 20syl2an 596 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → 𝑖 / 𝑛𝐴 ∈ ℝ)
2221recnd 11183 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → 𝑖 / 𝑛𝐴 ∈ ℂ)
2311, 22mulcld 11175 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
24 nfcv 2907 . . . . . . . . 9 𝑛𝑖
25 nfcv 2907 . . . . . . . . . 10 𝑛(𝑋‘(𝐿𝑖))
26 nfcv 2907 . . . . . . . . . 10 𝑛 ·
2725, 26, 15nfov 7387 . . . . . . . . 9 𝑛((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)
28 2fveq3 6847 . . . . . . . . . 10 (𝑛 = 𝑖 → (𝑋‘(𝐿𝑛)) = (𝑋‘(𝐿𝑖)))
2928, 17oveq12d 7375 . . . . . . . . 9 (𝑛 = 𝑖 → ((𝑋‘(𝐿𝑛)) · 𝐴) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
30 dchrisum.7 . . . . . . . . 9 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿𝑛)) · 𝐴))
3124, 27, 29, 30fvmptf 6969 . . . . . . . 8 ((𝑖 ∈ ℕ ∧ ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
323, 23, 31syl2anc 584 . . . . . . 7 ((𝜑𝑖 ∈ ℕ) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
3332, 23eqeltrd 2838 . . . . . 6 ((𝜑𝑖 ∈ ℕ) → (𝐹𝑖) ∈ ℂ)
341, 2, 33serf 13936 . . . . 5 (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ)
3534ffvelcdmda 7035 . . . 4 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℂ)
3612recnd 11183 . . . . . . . . 9 ((𝜑𝑛 ∈ ℝ+) → 𝐴 ∈ ℂ)
3736ralrimiva 3143 . . . . . . . 8 (𝜑 → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℂ)
3837adantr 481 . . . . . . 7 ((𝜑𝑒 ∈ ℝ+) → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℂ)
39 id 22 . . . . . . . 8 (𝑒 ∈ ℝ+𝑒 ∈ ℝ+)
40 2re 12227 . . . . . . . . . 10 2 ∈ ℝ
41 dchrisum.9 . . . . . . . . . 10 (𝜑𝑅 ∈ ℝ)
42 remulcl 11136 . . . . . . . . . 10 ((2 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (2 · 𝑅) ∈ ℝ)
4340, 41, 42sylancr 587 . . . . . . . . 9 (𝜑 → (2 · 𝑅) ∈ ℝ)
44 rpvmasum.a . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ)
45 lbfzo0 13612 . . . . . . . . . . . 12 (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
4644, 45sylibr 233 . . . . . . . . . . 11 (𝜑 → 0 ∈ (0..^𝑁))
47 dchrisum.10 . . . . . . . . . . 11 (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅)
48 oveq2 7365 . . . . . . . . . . . . . . . . 17 (𝑢 = 0 → (0..^𝑢) = (0..^0))
49 fzo0 13596 . . . . . . . . . . . . . . . . 17 (0..^0) = ∅
5048, 49eqtrdi 2792 . . . . . . . . . . . . . . . 16 (𝑢 = 0 → (0..^𝑢) = ∅)
5150sumeq1d 15586 . . . . . . . . . . . . . . 15 (𝑢 = 0 → Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ ∅ (𝑋‘(𝐿𝑛)))
52 sum0 15606 . . . . . . . . . . . . . . 15 Σ𝑛 ∈ ∅ (𝑋‘(𝐿𝑛)) = 0
5351, 52eqtrdi 2792 . . . . . . . . . . . . . 14 (𝑢 = 0 → Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛)) = 0)
5453abs00bd 15176 . . . . . . . . . . . . 13 (𝑢 = 0 → (abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) = 0)
5554breq1d 5115 . . . . . . . . . . . 12 (𝑢 = 0 → ((abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅 ↔ 0 ≤ 𝑅))
5655rspcv 3577 . . . . . . . . . . 11 (0 ∈ (0..^𝑁) → (∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅 → 0 ≤ 𝑅))
5746, 47, 56sylc 65 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝑅)
58 0le2 12255 . . . . . . . . . . 11 0 ≤ 2
59 mulge0 11673 . . . . . . . . . . 11 (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅)) → 0 ≤ (2 · 𝑅))
6040, 58, 59mpanl12 700 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 0 ≤ (2 · 𝑅))
6141, 57, 60syl2anc 584 . . . . . . . . 9 (𝜑 → 0 ≤ (2 · 𝑅))
6243, 61ge0p1rpd 12987 . . . . . . . 8 (𝜑 → ((2 · 𝑅) + 1) ∈ ℝ+)
63 rpdivcl 12940 . . . . . . . 8 ((𝑒 ∈ ℝ+ ∧ ((2 · 𝑅) + 1) ∈ ℝ+) → (𝑒 / ((2 · 𝑅) + 1)) ∈ ℝ+)
6439, 62, 63syl2anr 597 . . . . . . 7 ((𝜑𝑒 ∈ ℝ+) → (𝑒 / ((2 · 𝑅) + 1)) ∈ ℝ+)
65 dchrisum.6 . . . . . . . 8 (𝜑 → (𝑛 ∈ ℝ+𝐴) ⇝𝑟 0)
6665adantr 481 . . . . . . 7 ((𝜑𝑒 ∈ ℝ+) → (𝑛 ∈ ℝ+𝐴) ⇝𝑟 0)
6738, 64, 66rlimi 15395 . . . . . 6 ((𝜑𝑒 ∈ ℝ+) → ∃𝑚 ∈ ℝ ∀𝑛 ∈ ℝ+ (𝑚𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))))
68 simpr 485 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → 𝑚 ∈ ℝ)
69 dchrisum.3 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℕ)
7069nnred 12168 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℝ)
7170adantr 481 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → 𝑀 ∈ ℝ)
7268, 71ifcld 4532 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ)
73 0red 11158 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → 0 ∈ ℝ)
7469nngt0d 12202 . . . . . . . . . . . . 13 (𝜑 → 0 < 𝑀)
7574adantr 481 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → 0 < 𝑀)
76 max1 13104 . . . . . . . . . . . . 13 ((𝑀 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))
7770, 76sylan 580 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))
7873, 71, 72, 75, 77ltletrd 11315 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℝ) → 0 < if(𝑀𝑚, 𝑚, 𝑀))
7972, 78elrpd 12954 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ+)
8079adantlr 713 . . . . . . . . 9 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ+)
81 nfv 1917 . . . . . . . . . . 11 𝑛 𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀)
82 nfcv 2907 . . . . . . . . . . . . 13 𝑛abs
83 nfcsb1v 3880 . . . . . . . . . . . . . 14 𝑛if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴
84 nfcv 2907 . . . . . . . . . . . . . 14 𝑛
85 nfcv 2907 . . . . . . . . . . . . . 14 𝑛0
8683, 84, 85nfov 7387 . . . . . . . . . . . . 13 𝑛(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)
8782, 86nffv 6852 . . . . . . . . . . . 12 𝑛(abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0))
88 nfcv 2907 . . . . . . . . . . . 12 𝑛 <
89 nfcv 2907 . . . . . . . . . . . 12 𝑛(𝑒 / ((2 · 𝑅) + 1))
9087, 88, 89nfbr 5152 . . . . . . . . . . 11 𝑛(abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))
9181, 90nfim 1899 . . . . . . . . . 10 𝑛(𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀) → (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)))
92 breq2 5109 . . . . . . . . . . 11 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → (𝑚𝑛𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀)))
93 csbeq1a 3869 . . . . . . . . . . . . 13 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → 𝐴 = if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)
9493fvoveq1d 7379 . . . . . . . . . . . 12 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → (abs‘(𝐴 − 0)) = (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)))
9594breq1d 5115 . . . . . . . . . . 11 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → ((abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) ↔ (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))))
9692, 95imbi12d 344 . . . . . . . . . 10 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → ((𝑚𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) ↔ (𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀) → (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)))))
9791, 96rspc 3569 . . . . . . . . 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 724 . . . . . . . . . 10 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑀 ∈ ℝ)
100 max2 13106 . . . . . . . . . 10 ((𝑀 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀))
10199, 100sylancom 588 . . . . . . . . 9 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀))
10213ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ)
10383nfel1 2923 . . . . . . . . . . . . . . . . . . 19 𝑛if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℝ
10493eleq1d 2822 . . . . . . . . . . . . . . . . . . 19 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → (𝐴 ∈ ℝ ↔ if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℝ))
105103, 104rspc 3569 . . . . . . . . . . . . . . . . . 18 (if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℝ))
10680, 102, 105sylc 65 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℝ)
107106recnd 11183 . . . . . . . . . . . . . . . 16 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℂ)
108107subid1d 11501 . . . . . . . . . . . . . . 15 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0) = if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)
109108fveq2d 6846 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) = (abs‘if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴))
11072adantlr 713 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ)
11199, 76sylancom 588 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))
112 elicopnf 13362 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ℝ → (if(𝑀𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) ↔ (if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ ∧ 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))))
11399, 112syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (if(𝑀𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) ↔ (if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ ∧ 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))))
114110, 111, 113mpbir2and 711 . . . . . . . . . . . . . . . 16 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞))
11544ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑁 ∈ ℕ)
116 rpvmasum.1 . . . . . . . . . . . . . . . . . 18 1 = (0g𝐺)
1178ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑋𝐷)
118 dchrisum.n1 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋1 )
119118ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑋1 )
120 dchrisum.2 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑥𝐴 = 𝐵)
12169ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑀 ∈ ℕ)
12212ad4ant14 750 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)
123 simpll 765 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝜑)
124 dchrisum.5 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+) ∧ (𝑀𝑛𝑛𝑥)) → 𝐵𝐴)
125123, 124syl3an1 1163 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+) ∧ (𝑀𝑛𝑛𝑥)) → 𝐵𝐴)
12665ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (𝑛 ∈ ℝ+𝐴) ⇝𝑟 0)
1275, 7, 115, 4, 6, 116, 117, 119, 120, 121, 122, 125, 126, 30dchrisumlema 26836 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ+if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℝ) ∧ (if(𝑀𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) → 0 ≤ if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)))
128127simprd 496 . . . . . . . . . . . . . . . 16 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (if(𝑀𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) → 0 ≤ if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴))
129114, 128mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 0 ≤ if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)
130106, 129absidd 15307 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (abs‘if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) = if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)
131109, 130eqtrd 2776 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) = if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)
132131breq1d 5115 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) ↔ if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 < (𝑒 / ((2 · 𝑅) + 1))))
133 rpre 12923 . . . . . . . . . . . . . 14 (𝑒 ∈ ℝ+𝑒 ∈ ℝ)
134133ad2antlr 725 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑒 ∈ ℝ)
13562ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2 · 𝑅) + 1) ∈ ℝ+)
136106, 134, 135ltmuldiv2d 13005 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 < (𝑒 / ((2 · 𝑅) + 1))))
137132, 136bitr4d 281 . . . . . . . . . . 11 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) ↔ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒))
13843ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (2 · 𝑅) ∈ ℝ)
139135rpred 12957 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2 · 𝑅) + 1) ∈ ℝ)
140138lep1d 12086 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (2 · 𝑅) ≤ ((2 · 𝑅) + 1))
141138, 139, 106, 129, 140lemul1ad 12094 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ≤ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴))
142138, 106remulcld 11185 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ)
143139, 106remulcld 11185 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ)
144 lelttr 11245 . . . . . . . . . . . . 13 ((((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ ∧ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) → ((((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ≤ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∧ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒))
145142, 143, 134, 144syl3anc 1371 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ≤ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∧ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒))
146141, 145mpand 693 . . . . . . . . . . 11 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒 → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒))
147137, 146sylbid 239 . . . . . . . . . 10 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒))
148 1red 11156 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℝ) → 1 ∈ ℝ)
14969adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℝ) → 𝑀 ∈ ℕ)
150149nnge1d 12201 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℝ) → 1 ≤ 𝑀)
151148, 71, 72, 150, 77letrd 11312 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℝ) → 1 ≤ if(𝑀𝑚, 𝑚, 𝑀))
152 flge1nn 13726 . . . . . . . . . . . . 13 ((if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ ∧ 1 ≤ if(𝑀𝑚, 𝑚, 𝑀)) → (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ)
15372, 151, 152syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ)
154153adantlr 713 . . . . . . . . . . 11 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ)
15544ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑁 ∈ ℕ)
1568ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑋𝐷)
157118ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑋1 )
15869ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑀 ∈ ℕ)
15912ad4ant14 750 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)
1601243adant1r 1177 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℝ) ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+) ∧ (𝑀𝑛𝑛𝑥)) → 𝐵𝐴)
1611603adant1r 1177 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+) ∧ (𝑀𝑛𝑛𝑥)) → 𝐵𝐴)
16265ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (𝑛 ∈ ℝ+𝐴) ⇝𝑟 0)
16341ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑅 ∈ ℝ)
16447ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅)
16579adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ+)
16677adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))
16772adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ)
168 fllep1 13706 . . . . . . . . . . . . . . . 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 26838 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴))
173172adantllr 717 . . . . . . . . . . . . 13 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴))
17434ad3antrrr 728 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → seq1( + , 𝐹):ℕ⟶ℂ)
175 eluznn 12843 . . . . . . . . . . . . . . . . . 18 (((⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑘 ∈ ℕ)
176154, 175sylan 580 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑘 ∈ ℕ)
177174, 176ffvelcdmd 7036 . . . . . . . . . . . . . . . 16 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (seq1( + , 𝐹)‘𝑘) ∈ ℂ)
178154adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ)
179174, 178ffvelcdmd 7036 . . . . . . . . . . . . . . . 16 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))) ∈ ℂ)
180177, 179subcld 11512 . . . . . . . . . . . . . . 15 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → ((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) ∈ ℂ)
181180abscld 15321 . . . . . . . . . . . . . 14 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ∈ ℝ)
182142adantr 481 . . . . . . . . . . . . . 14 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ)
183134adantr 481 . . . . . . . . . . . . . 14 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑒 ∈ ℝ)
184 lelttr 11245 . . . . . . . . . . . . . 14 (((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ∈ ℝ ∧ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) → (((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∧ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
185181, 182, 183, 184syl3anc 1371 . . . . . . . . . . . . 13 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∧ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
186173, 185mpand 693 . . . . . . . . . . . 12 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒 → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
187186ralrimdva 3151 . . . . . . . . . . 11 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒 → ∀𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
188 fveq2 6842 . . . . . . . . . . . . 13 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → (ℤ𝑗) = (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))
189 fveq2 6842 . . . . . . . . . . . . . . . 16 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → (seq1( + , 𝐹)‘𝑗) = (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))
190189oveq2d 7373 . . . . . . . . . . . . . . 15 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → ((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗)) = ((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))))
191190fveq2d 6846 . . . . . . . . . . . . . 14 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) = (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))))
192191breq1d 5115 . . . . . . . . . . . . 13 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → ((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒 ↔ (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
193188, 192raleqbidv 3319 . . . . . . . . . . . 12 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → (∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒 ↔ ∀𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
194193rspcev 3581 . . . . . . . . . . 11 (((⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ ∧ ∀𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)
195154, 187, 194syl6an 682 . . . . . . . . . 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 3152 . . . . . 6 ((𝜑𝑒 ∈ ℝ+) → (∃𝑚 ∈ ℝ ∀𝑛 ∈ ℝ+ (𝑚𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒))
20067, 199mpd 15 . . . . 5 ((𝜑𝑒 ∈ ℝ+) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)
201200ralrimiva 3143 . . . 4 (𝜑 → ∀𝑒 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)
202 seqex 13908 . . . . 5 seq1( + , 𝐹) ∈ V
203202a1i 11 . . . 4 (𝜑 → seq1( + , 𝐹) ∈ V)
2041, 35, 201, 203caucvg 15563 . . 3 (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
205202eldm 5856 . . 3 (seq1( + , 𝐹) ∈ dom ⇝ ↔ ∃𝑡seq1( + , 𝐹) ⇝ 𝑡)
206204, 205sylib 217 . 2 (𝜑 → ∃𝑡seq1( + , 𝐹) ⇝ 𝑡)
207 simpr 485 . . . . 5 ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → seq1( + , 𝐹) ⇝ 𝑡)
208 elrege0 13371 . . . . . . . 8 ((2 · 𝑅) ∈ (0[,)+∞) ↔ ((2 · 𝑅) ∈ ℝ ∧ 0 ≤ (2 · 𝑅)))
20943, 61, 208sylanbrc 583 . . . . . . 7 (𝜑 → (2 · 𝑅) ∈ (0[,)+∞))
210209adantr 481 . . . . . 6 ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → (2 · 𝑅) ∈ (0[,)+∞))
211 eqid 2736 . . . . . . . 8 (ℤ‘(⌊‘𝑚)) = (ℤ‘(⌊‘𝑚))
212 pnfxr 11209 . . . . . . . . . . . 12 +∞ ∈ ℝ*
213 icossre 13345 . . . . . . . . . . . 12 ((𝑀 ∈ ℝ ∧ +∞ ∈ ℝ*) → (𝑀[,)+∞) ⊆ ℝ)
21470, 212, 213sylancl 586 . . . . . . . . . . 11 (𝜑 → (𝑀[,)+∞) ⊆ ℝ)
215214sselda 3944 . . . . . . . . . 10 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ)
216215adantlr 713 . . . . . . . . 9 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ)
217216flcld 13703 . . . . . . . 8 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (⌊‘𝑚) ∈ ℤ)
218 simplr 767 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → seq1( + , 𝐹) ⇝ 𝑡)
21934ad2antrr 724 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → seq1( + , 𝐹):ℕ⟶ℂ)
220 1red 11156 . . . . . . . . . . . . 13 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 1 ∈ ℝ)
22170ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℝ)
22269ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℕ)
223222nnge1d 12201 . . . . . . . . . . . . 13 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 1 ≤ 𝑀)
224 elicopnf 13362 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℝ → (𝑚 ∈ (𝑀[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 𝑀𝑚)))
22570, 224syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑚 ∈ (𝑀[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 𝑀𝑚)))
226225simplbda 500 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 𝑀𝑚)
227226adantlr 713 . . . . . . . . . . . . 13 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀𝑚)
228220, 221, 216, 223, 227letrd 11312 . . . . . . . . . . . 12 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 1 ≤ 𝑚)
229 flge1nn 13726 . . . . . . . . . . . 12 ((𝑚 ∈ ℝ ∧ 1 ≤ 𝑚) → (⌊‘𝑚) ∈ ℕ)
230216, 228, 229syl2anc 584 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (⌊‘𝑚) ∈ ℕ)
231219, 230ffvelcdmd 7036 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈ ℂ)
232 nnex 12159 . . . . . . . . . . . 12 ℕ ∈ V
233232mptex 7173 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ∈ V
234233a1i 11 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ∈ V)
235219adantr 481 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → seq1( + , 𝐹):ℕ⟶ℂ)
236 eluznn 12843 . . . . . . . . . . . 12 (((⌊‘𝑚) ∈ ℕ ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑖 ∈ ℕ)
237230, 236sylan 580 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑖 ∈ ℕ)
238235, 237ffvelcdmd 7036 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (seq1( + , 𝐹)‘𝑖) ∈ ℂ)
239 fveq2 6842 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (seq1( + , 𝐹)‘𝑘) = (seq1( + , 𝐹)‘𝑖))
240239oveq2d 7373 . . . . . . . . . . . 12 (𝑘 = 𝑖 → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))
241 eqid 2736 . . . . . . . . . . . 12 (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) = (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))
242 ovex 7390 . . . . . . . . . . . 12 ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)) ∈ V
243240, 241, 242fvmpt3i 6953 . . . . . . . . . . 11 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))
244237, 243syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))
245211, 217, 218, 231, 234, 238, 244climsubc2 15521 . . . . . . . . 9 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ⇝ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡))
246232mptex 7173 . . . . . . . . . 10 (𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) ∈ V
247246a1i 11 . . . . . . . . 9 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) ∈ V)
248 fvex 6855 . . . . . . . . . . . . . 14 (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈ V
249248fvconst2 7153 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → ((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) = (seq1( + , 𝐹)‘(⌊‘𝑚)))
250237, 249syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) = (seq1( + , 𝐹)‘(⌊‘𝑚)))
251250oveq1d 7372 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) − (seq1( + , 𝐹)‘𝑖)) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))
252244, 251eqtr4d 2779 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) = (((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) − (seq1( + , 𝐹)‘𝑖)))
253231adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈ ℂ)
254250, 253eqeltrd 2838 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) ∈ ℂ)
255254, 238subcld 11512 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) − (seq1( + , 𝐹)‘𝑖)) ∈ ℂ)
256252, 255eqeltrd 2838 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) ∈ ℂ)
257240fveq2d 6846 . . . . . . . . . . . 12 (𝑘 = 𝑖 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))))
258 eqid 2736 . . . . . . . . . . . 12 (𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) = (𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))
259 fvex 6855 . . . . . . . . . . . 12 (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ∈ V
260257, 258, 259fvmpt3i 6953 . . . . . . . . . . 11 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))))
261237, 260syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))))
262244fveq2d 6846 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (abs‘((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))))
263261, 262eqtr4d 2779 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖)))
264211, 245, 247, 217, 256, 263climabs 15486 . . . . . . . 8 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) ⇝ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)))
26543ad2antrr 724 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (2 · 𝑅) ∈ ℝ)
266 0red 11158 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 0 ∈ ℝ)
26770adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℝ)
26874adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 0 < 𝑀)
269266, 267, 215, 268, 226ltletrd 11315 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 0 < 𝑚)
270215, 269elrpd 12954 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ+)
271 nfcsb1v 3880 . . . . . . . . . . . . . . . 16 𝑛𝑚 / 𝑛𝐴
272271nfel1 2923 . . . . . . . . . . . . . . 15 𝑛𝑚 / 𝑛𝐴 ∈ ℝ
273 csbeq1a 3869 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚𝐴 = 𝑚 / 𝑛𝐴)
274273eleq1d 2822 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → (𝐴 ∈ ℝ ↔ 𝑚 / 𝑛𝐴 ∈ ℝ))
275272, 274rspc 3569 . . . . . . . . . . . . . 14 (𝑚 ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → 𝑚 / 𝑛𝐴 ∈ ℝ))
27613, 275mpan9 507 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℝ+) → 𝑚 / 𝑛𝐴 ∈ ℝ)
277270, 276syldan 591 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 𝑚 / 𝑛𝐴 ∈ ℝ)
278277adantlr 713 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑚 / 𝑛𝐴 ∈ ℝ)
279265, 278remulcld 11185 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ∈ ℝ)
280279recnd 11183 . . . . . . . . 9 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ∈ ℂ)
281 1z 12533 . . . . . . . . 9 1 ∈ ℤ
2821eqimss2i 4003 . . . . . . . . . 10 (ℤ‘1) ⊆ ℕ
283282, 232climconst2 15430 . . . . . . . . 9 ((((2 · 𝑅) · 𝑚 / 𝑛𝐴) ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)}) ⇝ ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
284280, 281, 283sylancl 586 . . . . . . . 8 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)}) ⇝ ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
285253, 238subcld 11512 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)) ∈ ℂ)
286285abscld 15321 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) ∈ ℝ)
287261, 286eqeltrd 2838 . . . . . . . 8 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) ∈ ℝ)
288 ovex 7390 . . . . . . . . . . 11 ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ∈ V
289288fvconst2 7153 . . . . . . . . . 10 (𝑖 ∈ ℕ → ((ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)})‘𝑖) = ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
290237, 289syl 17 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)})‘𝑖) = ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
291279adantr 481 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ∈ ℝ)
292290, 291eqeltrd 2838 . . . . . . . 8 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)})‘𝑖) ∈ ℝ)
293 simplll 773 . . . . . . . . . . 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 1163 . . . . . . . . . 10 (((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+) ∧ (𝑀𝑛𝑛𝑥)) → 𝐵𝐴)
300293, 65syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (𝑛 ∈ ℝ+𝐴) ⇝𝑟 0)
301293, 41syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑅 ∈ ℝ)
302293, 47syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅)
303270adantlr 713 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ+)
304303adantr 481 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑚 ∈ ℝ+)
305227adantr 481 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑀𝑚)
306216adantr 481 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑚 ∈ ℝ)
307 reflcl 13701 . . . . . . . . . . . 12 (𝑚 ∈ ℝ → (⌊‘𝑚) ∈ ℝ)
308 peano2re 11328 . . . . . . . . . . . 12 ((⌊‘𝑚) ∈ ℝ → ((⌊‘𝑚) + 1) ∈ ℝ)
309306, 307, 3083syl 18 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((⌊‘𝑚) + 1) ∈ ℝ)
310 flltp1 13705 . . . . . . . . . . . 12 (𝑚 ∈ ℝ → 𝑚 < ((⌊‘𝑚) + 1))
311306, 310syl 17 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑚 < ((⌊‘𝑚) + 1))
312306, 309, 311ltled 11303 . . . . . . . . . 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 26838 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (abs‘((seq1( + , 𝐹)‘𝑖) − (seq1( + , 𝐹)‘(⌊‘𝑚)))) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
316253, 238abssubd 15338 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) = (abs‘((seq1( + , 𝐹)‘𝑖) − (seq1( + , 𝐹)‘(⌊‘𝑚)))))
317261, 316eqtrd 2776 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((seq1( + , 𝐹)‘𝑖) − (seq1( + , 𝐹)‘(⌊‘𝑚)))))
318315, 317, 2903brtr4d 5137 . . . . . . . 8 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) ≤ ((ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)})‘𝑖))
319211, 217, 264, 284, 287, 292, 318climle 15522 . . . . . . 7 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
320319ralrimiva 3143 . . . . . 6 ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → ∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
321 oveq1 7364 . . . . . . . . . 10 (𝑐 = (2 · 𝑅) → (𝑐 · 𝐵) = ((2 · 𝑅) · 𝐵))
322321breq2d 5117 . . . . . . . . 9 (𝑐 = (2 · 𝑅) → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵)))
323322ralbidv 3174 . . . . . . . 8 (𝑐 = (2 · 𝑅) → (∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵) ↔ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵)))
324 2fveq3 6847 . . . . . . . . . . 11 (𝑚 = 𝑥 → (seq1( + , 𝐹)‘(⌊‘𝑚)) = (seq1( + , 𝐹)‘(⌊‘𝑥)))
325324fvoveq1d 7379 . . . . . . . . . 10 (𝑚 = 𝑥 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)))
326 vex 3449 . . . . . . . . . . . . 13 𝑚 ∈ V
327326a1i 11 . . . . . . . . . . . 12 (𝑚 = 𝑥𝑚 ∈ V)
328 equequ2 2029 . . . . . . . . . . . . . 14 (𝑚 = 𝑥 → (𝑛 = 𝑚𝑛 = 𝑥))
329328biimpa 477 . . . . . . . . . . . . 13 ((𝑚 = 𝑥𝑛 = 𝑚) → 𝑛 = 𝑥)
330329, 120syl 17 . . . . . . . . . . . 12 ((𝑚 = 𝑥𝑛 = 𝑚) → 𝐴 = 𝐵)
331327, 330csbied 3893 . . . . . . . . . . 11 (𝑚 = 𝑥𝑚 / 𝑛𝐴 = 𝐵)
332331oveq2d 7373 . . . . . . . . . 10 (𝑚 = 𝑥 → ((2 · 𝑅) · 𝑚 / 𝑛𝐴) = ((2 · 𝑅) · 𝐵))
333325, 332breq12d 5118 . . . . . . . . 9 (𝑚 = 𝑥 → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵)))
334333cbvralvw 3225 . . . . . . . 8 (∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ↔ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵))
335323, 334bitr4di 288 . . . . . . 7 (𝑐 = (2 · 𝑅) → (∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵) ↔ ∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴)))
336335rspcev 3581 . . . . . 6 (((2 · 𝑅) ∈ (0[,)+∞) ∧ ∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴)) → ∃𝑐 ∈ (0[,)+∞)∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))
337210, 320, 336syl2anc 584 . . . . 5 ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → ∃𝑐 ∈ (0[,)+∞)∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))
338 r19.42v 3187 . . . . 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 1920 . 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 205  wa 396  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wne 2943  wral 3064  wrex 3073  Vcvv 3445  csb 3855  wss 3910  c0 4282  ifcif 4486  {csn 4586   class class class wbr 5105  cmpt 5188   × cxp 5631  dom cdm 5633  wf 6492  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  +∞cpnf 11186  *cxr 11188   < clt 11189  cle 11190  cmin 11385   / cdiv 11812  cn 12153  2c2 12208  cz 12499  cuz 12763  +crp 12915  [,)cico 13266  ..^cfzo 13567  cfl 13695  seqcseq 13906  abscabs 15119  cli 15366  𝑟 crli 15367  Σcsu 15570  Basecbs 17083  0gc0g 17321  ℤRHomczrh 20900  ℤ/nczn 20903  DChrcdchr 26580
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-tpos 8157  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-er 8648  df-ec 8650  df-qs 8654  df-map 8767  df-pm 8768  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-xnn0 12486  df-z 12500  df-dec 12619  df-uz 12764  df-rp 12916  df-ico 13270  df-fz 13425  df-fzo 13568  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-limsup 15353  df-clim 15370  df-rlim 15371  df-sum 15571  df-dvds 16137  df-gcd 16375  df-phi 16638  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-0g 17323  df-imas 17390  df-qus 17391  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-mhm 18601  df-grp 18751  df-minusg 18752  df-sbg 18753  df-mulg 18873  df-subg 18925  df-nsg 18926  df-eqg 18927  df-ghm 19006  df-cmn 19564  df-abl 19565  df-mgp 19897  df-ur 19914  df-ring 19966  df-cring 19967  df-oppr 20049  df-dvdsr 20070  df-unit 20071  df-invr 20101  df-rnghom 20146  df-subrg 20220  df-lmod 20324  df-lss 20393  df-lsp 20433  df-sra 20633  df-rgmod 20634  df-lidl 20635  df-rsp 20636  df-2idl 20702  df-cnfld 20797  df-zring 20870  df-zrh 20904  df-zn 20907  df-dchr 26581
This theorem is referenced by:  dchrisum  26840
  Copyright terms: Public domain W3C validator