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

Theorem dchrisumlem3 26082
 Description: Lemma for dchrisum 26083. 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 12271 . . . 4 ℕ = (ℤ‘1)
2 1zzd 12003 . . . . . 6 (𝜑 → 1 ∈ ℤ)
3 simpr 488 . . . . . . . 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 484 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → 𝑋𝐷)
103nnzd 12076 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → 𝑖 ∈ ℤ)
114, 5, 6, 7, 9, 10dchrzrhcl 25836 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → (𝑋‘(𝐿𝑖)) ∈ ℂ)
12 dchrisum.4 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)
1312ralrimiva 3149 . . . . . . . . . . 11 (𝜑 → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ)
14 nnrp 12390 . . . . . . . . . . 11 (𝑖 ∈ ℕ → 𝑖 ∈ ℝ+)
15 nfcsb1v 3852 . . . . . . . . . . . . . 14 𝑛𝑖 / 𝑛𝐴
1615nfel1 2971 . . . . . . . . . . . . 13 𝑛𝑖 / 𝑛𝐴 ∈ ℝ
17 csbeq1a 3842 . . . . . . . . . . . . . 14 (𝑛 = 𝑖𝐴 = 𝑖 / 𝑛𝐴)
1817eleq1d 2874 . . . . . . . . . . . . 13 (𝑛 = 𝑖 → (𝐴 ∈ ℝ ↔ 𝑖 / 𝑛𝐴 ∈ ℝ))
1916, 18rspc 3559 . . . . . . . . . . . 12 (𝑖 ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → 𝑖 / 𝑛𝐴 ∈ ℝ))
2019impcom 411 . . . . . . . . . . 11 ((∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ ∧ 𝑖 ∈ ℝ+) → 𝑖 / 𝑛𝐴 ∈ ℝ)
2113, 14, 20syl2an 598 . . . . . . . . . 10 ((𝜑𝑖 ∈ ℕ) → 𝑖 / 𝑛𝐴 ∈ ℝ)
2221recnd 10660 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → 𝑖 / 𝑛𝐴 ∈ ℂ)
2311, 22mulcld 10652 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ) → ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ)
24 nfcv 2955 . . . . . . . . 9 𝑛𝑖
25 nfcv 2955 . . . . . . . . . 10 𝑛(𝑋‘(𝐿𝑖))
26 nfcv 2955 . . . . . . . . . 10 𝑛 ·
2725, 26, 15nfov 7165 . . . . . . . . 9 𝑛((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴)
28 2fveq3 6650 . . . . . . . . . 10 (𝑛 = 𝑖 → (𝑋‘(𝐿𝑛)) = (𝑋‘(𝐿𝑖)))
2928, 17oveq12d 7153 . . . . . . . . 9 (𝑛 = 𝑖 → ((𝑋‘(𝐿𝑛)) · 𝐴) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
30 dchrisum.7 . . . . . . . . 9 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿𝑛)) · 𝐴))
3124, 27, 29, 30fvmptf 6766 . . . . . . . 8 ((𝑖 ∈ ℕ ∧ ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴) ∈ ℂ) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
323, 23, 31syl2anc 587 . . . . . . 7 ((𝜑𝑖 ∈ ℕ) → (𝐹𝑖) = ((𝑋‘(𝐿𝑖)) · 𝑖 / 𝑛𝐴))
3332, 23eqeltrd 2890 . . . . . 6 ((𝜑𝑖 ∈ ℕ) → (𝐹𝑖) ∈ ℂ)
341, 2, 33serf 13396 . . . . 5 (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ)
3534ffvelrnda 6828 . . . 4 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℂ)
3612recnd 10660 . . . . . . . . 9 ((𝜑𝑛 ∈ ℝ+) → 𝐴 ∈ ℂ)
3736ralrimiva 3149 . . . . . . . 8 (𝜑 → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℂ)
3837adantr 484 . . . . . . 7 ((𝜑𝑒 ∈ ℝ+) → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℂ)
39 id 22 . . . . . . . 8 (𝑒 ∈ ℝ+𝑒 ∈ ℝ+)
40 2re 11701 . . . . . . . . . 10 2 ∈ ℝ
41 dchrisum.9 . . . . . . . . . 10 (𝜑𝑅 ∈ ℝ)
42 remulcl 10613 . . . . . . . . . 10 ((2 ∈ ℝ ∧ 𝑅 ∈ ℝ) → (2 · 𝑅) ∈ ℝ)
4340, 41, 42sylancr 590 . . . . . . . . 9 (𝜑 → (2 · 𝑅) ∈ ℝ)
44 rpvmasum.a . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ)
45 lbfzo0 13074 . . . . . . . . . . . 12 (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ ℕ)
4644, 45sylibr 237 . . . . . . . . . . 11 (𝜑 → 0 ∈ (0..^𝑁))
47 dchrisum.10 . . . . . . . . . . 11 (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅)
48 oveq2 7143 . . . . . . . . . . . . . . . . 17 (𝑢 = 0 → (0..^𝑢) = (0..^0))
49 fzo0 13058 . . . . . . . . . . . . . . . . 17 (0..^0) = ∅
5048, 49eqtrdi 2849 . . . . . . . . . . . . . . . 16 (𝑢 = 0 → (0..^𝑢) = ∅)
5150sumeq1d 15052 . . . . . . . . . . . . . . 15 (𝑢 = 0 → Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛)) = Σ𝑛 ∈ ∅ (𝑋‘(𝐿𝑛)))
52 sum0 15072 . . . . . . . . . . . . . . 15 Σ𝑛 ∈ ∅ (𝑋‘(𝐿𝑛)) = 0
5351, 52eqtrdi 2849 . . . . . . . . . . . . . 14 (𝑢 = 0 → Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛)) = 0)
5453abs00bd 14645 . . . . . . . . . . . . 13 (𝑢 = 0 → (abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) = 0)
5554breq1d 5040 . . . . . . . . . . . 12 (𝑢 = 0 → ((abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅 ↔ 0 ≤ 𝑅))
5655rspcv 3566 . . . . . . . . . . 11 (0 ∈ (0..^𝑁) → (∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅 → 0 ≤ 𝑅))
5746, 47, 56sylc 65 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝑅)
58 0le2 11729 . . . . . . . . . . 11 0 ≤ 2
59 mulge0 11149 . . . . . . . . . . 11 (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅)) → 0 ≤ (2 · 𝑅))
6040, 58, 59mpanl12 701 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅) → 0 ≤ (2 · 𝑅))
6141, 57, 60syl2anc 587 . . . . . . . . 9 (𝜑 → 0 ≤ (2 · 𝑅))
6243, 61ge0p1rpd 12451 . . . . . . . 8 (𝜑 → ((2 · 𝑅) + 1) ∈ ℝ+)
63 rpdivcl 12404 . . . . . . . 8 ((𝑒 ∈ ℝ+ ∧ ((2 · 𝑅) + 1) ∈ ℝ+) → (𝑒 / ((2 · 𝑅) + 1)) ∈ ℝ+)
6439, 62, 63syl2anr 599 . . . . . . 7 ((𝜑𝑒 ∈ ℝ+) → (𝑒 / ((2 · 𝑅) + 1)) ∈ ℝ+)
65 dchrisum.6 . . . . . . . 8 (𝜑 → (𝑛 ∈ ℝ+𝐴) ⇝𝑟 0)
6665adantr 484 . . . . . . 7 ((𝜑𝑒 ∈ ℝ+) → (𝑛 ∈ ℝ+𝐴) ⇝𝑟 0)
6738, 64, 66rlimi 14864 . . . . . 6 ((𝜑𝑒 ∈ ℝ+) → ∃𝑚 ∈ ℝ ∀𝑛 ∈ ℝ+ (𝑚𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))))
68 simpr 488 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → 𝑚 ∈ ℝ)
69 dchrisum.3 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℕ)
7069nnred 11642 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℝ)
7170adantr 484 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → 𝑀 ∈ ℝ)
7268, 71ifcld 4470 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ)
73 0red 10635 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → 0 ∈ ℝ)
7469nngt0d 11676 . . . . . . . . . . . . 13 (𝜑 → 0 < 𝑀)
7574adantr 484 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → 0 < 𝑀)
76 max1 12568 . . . . . . . . . . . . 13 ((𝑀 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))
7770, 76sylan 583 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))
7873, 71, 72, 75, 77ltletrd 10791 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℝ) → 0 < if(𝑀𝑚, 𝑚, 𝑀))
7972, 78elrpd 12418 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ+)
8079adantlr 714 . . . . . . . . 9 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ+)
81 nfv 1915 . . . . . . . . . . 11 𝑛 𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀)
82 nfcv 2955 . . . . . . . . . . . . 13 𝑛abs
83 nfcsb1v 3852 . . . . . . . . . . . . . 14 𝑛if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴
84 nfcv 2955 . . . . . . . . . . . . . 14 𝑛
85 nfcv 2955 . . . . . . . . . . . . . 14 𝑛0
8683, 84, 85nfov 7165 . . . . . . . . . . . . 13 𝑛(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)
8782, 86nffv 6655 . . . . . . . . . . . 12 𝑛(abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0))
88 nfcv 2955 . . . . . . . . . . . 12 𝑛 <
89 nfcv 2955 . . . . . . . . . . . 12 𝑛(𝑒 / ((2 · 𝑅) + 1))
9087, 88, 89nfbr 5077 . . . . . . . . . . 11 𝑛(abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))
9181, 90nfim 1897 . . . . . . . . . 10 𝑛(𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀) → (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)))
92 breq2 5034 . . . . . . . . . . 11 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → (𝑚𝑛𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀)))
93 csbeq1a 3842 . . . . . . . . . . . . 13 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → 𝐴 = if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)
9493fvoveq1d 7157 . . . . . . . . . . . 12 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → (abs‘(𝐴 − 0)) = (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)))
9594breq1d 5040 . . . . . . . . . . 11 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → ((abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) ↔ (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))))
9692, 95imbi12d 348 . . . . . . . . . 10 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → ((𝑚𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) ↔ (𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀) → (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)))))
9791, 96rspc 3559 . . . . . . . . 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 725 . . . . . . . . . 10 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑀 ∈ ℝ)
100 max2 12570 . . . . . . . . . 10 ((𝑀 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀))
10199, 100sylancom 591 . . . . . . . . 9 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑚 ≤ if(𝑀𝑚, 𝑚, 𝑀))
10213ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ)
10383nfel1 2971 . . . . . . . . . . . . . . . . . . 19 𝑛if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℝ
10493eleq1d 2874 . . . . . . . . . . . . . . . . . . 19 (𝑛 = if(𝑀𝑚, 𝑚, 𝑀) → (𝐴 ∈ ℝ ↔ if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℝ))
105103, 104rspc 3559 . . . . . . . . . . . . . . . . . 18 (if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℝ))
10680, 102, 105sylc 65 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℝ)
107106recnd 10660 . . . . . . . . . . . . . . . 16 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℂ)
108107subid1d 10977 . . . . . . . . . . . . . . 15 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0) = if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)
109108fveq2d 6649 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) = (abs‘if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴))
11072adantlr 714 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ)
11199, 76sylancom 591 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))
112 elicopnf 12825 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ℝ → (if(𝑀𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) ↔ (if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ ∧ 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))))
11399, 112syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (if(𝑀𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) ↔ (if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ ∧ 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))))
114110, 111, 113mpbir2and 712 . . . . . . . . . . . . . . . 16 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → if(𝑀𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞))
11544ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑁 ∈ ℕ)
116 rpvmasum.1 . . . . . . . . . . . . . . . . . 18 1 = (0g𝐺)
1178ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑋𝐷)
118 dchrisum.n1 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋1 )
119118ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑋1 )
120 dchrisum.2 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑥𝐴 = 𝐵)
12169ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑀 ∈ ℕ)
12212ad4ant14 751 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)
123 simpll 766 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝜑)
124 dchrisum.5 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+) ∧ (𝑀𝑛𝑛𝑥)) → 𝐵𝐴)
125123, 124syl3an1 1160 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+) ∧ (𝑀𝑛𝑛𝑥)) → 𝐵𝐴)
12665ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (𝑛 ∈ ℝ+𝐴) ⇝𝑟 0)
1275, 7, 115, 4, 6, 116, 117, 119, 120, 121, 122, 125, 126, 30dchrisumlema 26079 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ+if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 ∈ ℝ) ∧ (if(𝑀𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) → 0 ≤ if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)))
128127simprd 499 . . . . . . . . . . . . . . . 16 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (if(𝑀𝑚, 𝑚, 𝑀) ∈ (𝑀[,)+∞) → 0 ≤ if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴))
129114, 128mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 0 ≤ if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)
130106, 129absidd 14776 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (abs‘if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) = if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)
131109, 130eqtrd 2833 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) = if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴)
132131breq1d 5040 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) ↔ if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 < (𝑒 / ((2 · 𝑅) + 1))))
133 rpre 12387 . . . . . . . . . . . . . 14 (𝑒 ∈ ℝ+𝑒 ∈ ℝ)
134133ad2antlr 726 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → 𝑒 ∈ ℝ)
13562ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2 · 𝑅) + 1) ∈ ℝ+)
136106, 134, 135ltmuldiv2d 12469 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 < (𝑒 / ((2 · 𝑅) + 1))))
137132, 136bitr4d 285 . . . . . . . . . . 11 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) ↔ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒))
13843ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (2 · 𝑅) ∈ ℝ)
139135rpred 12421 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2 · 𝑅) + 1) ∈ ℝ)
140138lep1d 11562 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (2 · 𝑅) ≤ ((2 · 𝑅) + 1))
141138, 139, 106, 129, 140lemul1ad 11570 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ≤ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴))
142138, 106remulcld 10662 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ)
143139, 106remulcld 10662 . . . . . . . . . . . . 13 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ)
144 lelttr 10722 . . . . . . . . . . . . 13 ((((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ ∧ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) → ((((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ≤ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∧ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒))
145142, 143, 134, 144syl3anc 1368 . . . . . . . . . . . 12 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ≤ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∧ (((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒))
146141, 145mpand 694 . . . . . . . . . . 11 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((((2 · 𝑅) + 1) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒 → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒))
147137, 146sylbid 243 . . . . . . . . . 10 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → ((abs‘(if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1)) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒))
148 1red 10633 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℝ) → 1 ∈ ℝ)
14969adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℝ) → 𝑀 ∈ ℕ)
150149nnge1d 11675 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℝ) → 1 ≤ 𝑀)
151148, 71, 72, 150, 77letrd 10788 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℝ) → 1 ≤ if(𝑀𝑚, 𝑚, 𝑀))
152 flge1nn 13188 . . . . . . . . . . . . 13 ((if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ ∧ 1 ≤ if(𝑀𝑚, 𝑚, 𝑀)) → (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ)
15372, 151, 152syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℝ) → (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ)
154153adantlr 714 . . . . . . . . . . 11 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ)
15544ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑁 ∈ ℕ)
1568ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑋𝐷)
157118ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑋1 )
15869ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑀 ∈ ℕ)
15912ad4ant14 751 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)
1601243adant1r 1174 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℝ) ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+) ∧ (𝑀𝑛𝑛𝑥)) → 𝐵𝐴)
1611603adant1r 1174 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+) ∧ (𝑀𝑛𝑛𝑥)) → 𝐵𝐴)
16265ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (𝑛 ∈ ℝ+𝐴) ⇝𝑟 0)
16341ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑅 ∈ ℝ)
16447ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅)
16579adantr 484 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ+)
16677adantr 484 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑀 ≤ if(𝑀𝑚, 𝑚, 𝑀))
16772adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ)
168 fllep1 13168 . . . . . . . . . . . . . . . 16 (if(𝑀𝑚, 𝑚, 𝑀) ∈ ℝ → if(𝑀𝑚, 𝑚, 𝑀) ≤ ((⌊‘if(𝑀𝑚, 𝑚, 𝑀)) + 1))
169167, 168syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → if(𝑀𝑚, 𝑚, 𝑀) ≤ ((⌊‘if(𝑀𝑚, 𝑚, 𝑀)) + 1))
170153adantr 484 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ)
171 simpr 488 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))
1725, 7, 155, 4, 6, 116, 156, 157, 120, 158, 159, 161, 162, 30, 163, 164, 165, 166, 169, 170, 171dchrisumlem2 26081 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴))
173172adantllr 718 . . . . . . . . . . . . 13 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴))
17434ad3antrrr 729 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → seq1( + , 𝐹):ℕ⟶ℂ)
175 eluznn 12308 . . . . . . . . . . . . . . . . . 18 (((⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑘 ∈ ℕ)
176154, 175sylan 583 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑘 ∈ ℕ)
177174, 176ffvelrnd 6829 . . . . . . . . . . . . . . . 16 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (seq1( + , 𝐹)‘𝑘) ∈ ℂ)
178154adantr 484 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ)
179174, 178ffvelrnd 6829 . . . . . . . . . . . . . . . 16 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))) ∈ ℂ)
180177, 179subcld 10988 . . . . . . . . . . . . . . 15 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → ((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) ∈ ℂ)
181180abscld 14790 . . . . . . . . . . . . . 14 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ∈ ℝ)
182142adantr 484 . . . . . . . . . . . . . 14 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ)
183134adantr 484 . . . . . . . . . . . . . 14 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → 𝑒 ∈ ℝ)
184 lelttr 10722 . . . . . . . . . . . . . 14 (((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ∈ ℝ ∧ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) → (((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∧ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
185181, 182, 183, 184syl3anc 1368 . . . . . . . . . . . . 13 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) ≤ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) ∧ ((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
186173, 185mpand 694 . . . . . . . . . . . 12 ((((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))) → (((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒 → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
187186ralrimdva 3154 . . . . . . . . . . 11 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑚 ∈ ℝ) → (((2 · 𝑅) · if(𝑀𝑚, 𝑚, 𝑀) / 𝑛𝐴) < 𝑒 → ∀𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
188 fveq2 6645 . . . . . . . . . . . . 13 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → (ℤ𝑗) = (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))
189 fveq2 6645 . . . . . . . . . . . . . . . 16 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → (seq1( + , 𝐹)‘𝑗) = (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))
190189oveq2d 7151 . . . . . . . . . . . . . . 15 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → ((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗)) = ((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))))
191190fveq2d 6649 . . . . . . . . . . . . . 14 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) = (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))))
192191breq1d 5040 . . . . . . . . . . . . 13 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → ((abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒 ↔ (abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
193188, 192raleqbidv 3354 . . . . . . . . . . . 12 (𝑗 = (⌊‘if(𝑀𝑚, 𝑚, 𝑀)) → (∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒 ↔ ∀𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒))
194193rspcev 3571 . . . . . . . . . . 11 (((⌊‘if(𝑀𝑚, 𝑚, 𝑀)) ∈ ℕ ∧ ∀𝑘 ∈ (ℤ‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀)))(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘(⌊‘if(𝑀𝑚, 𝑚, 𝑀))))) < 𝑒) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)
195154, 187, 194syl6an 683 . . . . . . . . . 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 3243 . . . . . 6 ((𝜑𝑒 ∈ ℝ+) → (∃𝑚 ∈ ℝ ∀𝑛 ∈ ℝ+ (𝑚𝑛 → (abs‘(𝐴 − 0)) < (𝑒 / ((2 · 𝑅) + 1))) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒))
20067, 199mpd 15 . . . . 5 ((𝜑𝑒 ∈ ℝ+) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)
201200ralrimiva 3149 . . . 4 (𝜑 → ∀𝑒 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)(abs‘((seq1( + , 𝐹)‘𝑘) − (seq1( + , 𝐹)‘𝑗))) < 𝑒)
202 seqex 13368 . . . . 5 seq1( + , 𝐹) ∈ V
203202a1i 11 . . . 4 (𝜑 → seq1( + , 𝐹) ∈ V)
2041, 35, 201, 203caucvg 15029 . . 3 (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
205202eldm 5733 . . 3 (seq1( + , 𝐹) ∈ dom ⇝ ↔ ∃𝑡seq1( + , 𝐹) ⇝ 𝑡)
206204, 205sylib 221 . 2 (𝜑 → ∃𝑡seq1( + , 𝐹) ⇝ 𝑡)
207 simpr 488 . . . . 5 ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → seq1( + , 𝐹) ⇝ 𝑡)
208 elrege0 12834 . . . . . . . 8 ((2 · 𝑅) ∈ (0[,)+∞) ↔ ((2 · 𝑅) ∈ ℝ ∧ 0 ≤ (2 · 𝑅)))
20943, 61, 208sylanbrc 586 . . . . . . 7 (𝜑 → (2 · 𝑅) ∈ (0[,)+∞))
210209adantr 484 . . . . . 6 ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → (2 · 𝑅) ∈ (0[,)+∞))
211 eqid 2798 . . . . . . . 8 (ℤ‘(⌊‘𝑚)) = (ℤ‘(⌊‘𝑚))
212 pnfxr 10686 . . . . . . . . . . . 12 +∞ ∈ ℝ*
213 icossre 12808 . . . . . . . . . . . 12 ((𝑀 ∈ ℝ ∧ +∞ ∈ ℝ*) → (𝑀[,)+∞) ⊆ ℝ)
21470, 212, 213sylancl 589 . . . . . . . . . . 11 (𝜑 → (𝑀[,)+∞) ⊆ ℝ)
215214sselda 3915 . . . . . . . . . 10 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ)
216215adantlr 714 . . . . . . . . 9 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ)
217216flcld 13165 . . . . . . . 8 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (⌊‘𝑚) ∈ ℤ)
218 simplr 768 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → seq1( + , 𝐹) ⇝ 𝑡)
21934ad2antrr 725 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → seq1( + , 𝐹):ℕ⟶ℂ)
220 1red 10633 . . . . . . . . . . . . 13 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 1 ∈ ℝ)
22170ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℝ)
22269ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℕ)
223222nnge1d 11675 . . . . . . . . . . . . 13 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 1 ≤ 𝑀)
224 elicopnf 12825 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℝ → (𝑚 ∈ (𝑀[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 𝑀𝑚)))
22570, 224syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑚 ∈ (𝑀[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 𝑀𝑚)))
226225simplbda 503 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 𝑀𝑚)
227226adantlr 714 . . . . . . . . . . . . 13 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑀𝑚)
228220, 221, 216, 223, 227letrd 10788 . . . . . . . . . . . 12 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 1 ≤ 𝑚)
229 flge1nn 13188 . . . . . . . . . . . 12 ((𝑚 ∈ ℝ ∧ 1 ≤ 𝑚) → (⌊‘𝑚) ∈ ℕ)
230216, 228, 229syl2anc 587 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (⌊‘𝑚) ∈ ℕ)
231219, 230ffvelrnd 6829 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈ ℂ)
232 nnex 11633 . . . . . . . . . . . 12 ℕ ∈ V
233232mptex 6963 . . . . . . . . . . 11 (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ∈ V
234233a1i 11 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ∈ V)
235219adantr 484 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → seq1( + , 𝐹):ℕ⟶ℂ)
236 eluznn 12308 . . . . . . . . . . . 12 (((⌊‘𝑚) ∈ ℕ ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑖 ∈ ℕ)
237230, 236sylan 583 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑖 ∈ ℕ)
238235, 237ffvelrnd 6829 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (seq1( + , 𝐹)‘𝑖) ∈ ℂ)
239 fveq2 6645 . . . . . . . . . . . . 13 (𝑘 = 𝑖 → (seq1( + , 𝐹)‘𝑘) = (seq1( + , 𝐹)‘𝑖))
240239oveq2d 7151 . . . . . . . . . . . 12 (𝑘 = 𝑖 → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))
241 eqid 2798 . . . . . . . . . . . 12 (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) = (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))
242 ovex 7168 . . . . . . . . . . . 12 ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)) ∈ V
243240, 241, 242fvmpt3i 6750 . . . . . . . . . . 11 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))
244237, 243syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))
245211, 217, 218, 231, 234, 238, 244climsubc2 14989 . . . . . . . . 9 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ⇝ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡))
246232mptex 6963 . . . . . . . . . 10 (𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) ∈ V
247246a1i 11 . . . . . . . . 9 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) ∈ V)
248 fvex 6658 . . . . . . . . . . . . . 14 (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈ V
249248fvconst2 6943 . . . . . . . . . . . . 13 (𝑖 ∈ ℕ → ((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) = (seq1( + , 𝐹)‘(⌊‘𝑚)))
250237, 249syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) = (seq1( + , 𝐹)‘(⌊‘𝑚)))
251250oveq1d 7150 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) − (seq1( + , 𝐹)‘𝑖)) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)))
252244, 251eqtr4d 2836 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) = (((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) − (seq1( + , 𝐹)‘𝑖)))
253231adantr 484 . . . . . . . . . . . 12 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈ ℂ)
254250, 253eqeltrd 2890 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) ∈ ℂ)
255254, 238subcld 10988 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (((ℕ × {(seq1( + , 𝐹)‘(⌊‘𝑚))})‘𝑖) − (seq1( + , 𝐹)‘𝑖)) ∈ ℂ)
256252, 255eqeltrd 2890 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))‘𝑖) ∈ ℂ)
257240fveq2d 6649 . . . . . . . . . . . 12 (𝑘 = 𝑖 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))))
258 eqid 2798 . . . . . . . . . . . 12 (𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) = (𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))
259 fvex 6658 . . . . . . . . . . . 12 (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))) ∈ V
260257, 258, 259fvmpt3i 6750 . . . . . . . . . . 11 (𝑖 ∈ ℕ → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))))
261237, 260syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))))
262244fveq2d 6649 . . . . . . . . . 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 14954 . . . . . . . 8 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘)))) ⇝ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)))
26543ad2antrr 725 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (2 · 𝑅) ∈ ℝ)
266 0red 10635 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 0 ∈ ℝ)
26770adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 𝑀 ∈ ℝ)
26874adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 0 < 𝑀)
269266, 267, 215, 268, 226ltletrd 10791 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 0 < 𝑚)
270215, 269elrpd 12418 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ+)
271 nfcsb1v 3852 . . . . . . . . . . . . . . . 16 𝑛𝑚 / 𝑛𝐴
272271nfel1 2971 . . . . . . . . . . . . . . 15 𝑛𝑚 / 𝑛𝐴 ∈ ℝ
273 csbeq1a 3842 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚𝐴 = 𝑚 / 𝑛𝐴)
274273eleq1d 2874 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → (𝐴 ∈ ℝ ↔ 𝑚 / 𝑛𝐴 ∈ ℝ))
275272, 274rspc 3559 . . . . . . . . . . . . . 14 (𝑚 ∈ ℝ+ → (∀𝑛 ∈ ℝ+ 𝐴 ∈ ℝ → 𝑚 / 𝑛𝐴 ∈ ℝ))
27613, 275mpan9 510 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℝ+) → 𝑚 / 𝑛𝐴 ∈ ℝ)
277270, 276syldan 594 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (𝑀[,)+∞)) → 𝑚 / 𝑛𝐴 ∈ ℝ)
278277adantlr 714 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑚 / 𝑛𝐴 ∈ ℝ)
279265, 278remulcld 10662 . . . . . . . . . 10 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ∈ ℝ)
280279recnd 10660 . . . . . . . . 9 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ∈ ℂ)
281 1z 12002 . . . . . . . . 9 1 ∈ ℤ
2821eqimss2i 3974 . . . . . . . . . 10 (ℤ‘1) ⊆ ℕ
283282, 232climconst2 14899 . . . . . . . . 9 ((((2 · 𝑅) · 𝑚 / 𝑛𝐴) ∈ ℂ ∧ 1 ∈ ℤ) → (ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)}) ⇝ ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
284280, 281, 283sylancl 589 . . . . . . . 8 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)}) ⇝ ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
285253, 238subcld 10988 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖)) ∈ ℂ)
286285abscld 14790 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) ∈ ℝ)
287261, 286eqeltrd 2890 . . . . . . . 8 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) ∈ ℝ)
288 ovex 7168 . . . . . . . . . . 11 ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ∈ V
289288fvconst2 6943 . . . . . . . . . 10 (𝑖 ∈ ℕ → ((ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)})‘𝑖) = ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
290237, 289syl 17 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)})‘𝑖) = ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
291279adantr 484 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ∈ ℝ)
292290, 291eqeltrd 2890 . . . . . . . 8 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)})‘𝑖) ∈ ℝ)
293 simplll 774 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝜑)
294293, 44syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑁 ∈ ℕ)
295293, 8syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑋𝐷)
296293, 118syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑋1 )
297222adantr 484 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑀 ∈ ℕ)
298293, 12sylan 583 . . . . . . . . . 10 (((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)
299293, 124syl3an1 1160 . . . . . . . . . 10 (((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) ∧ (𝑛 ∈ ℝ+𝑥 ∈ ℝ+) ∧ (𝑀𝑛𝑛𝑥)) → 𝐵𝐴)
300293, 65syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (𝑛 ∈ ℝ+𝐴) ⇝𝑟 0)
301293, 41syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑅 ∈ ℝ)
302293, 47syl 17 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿𝑛))) ≤ 𝑅)
303270adantlr 714 . . . . . . . . . . 11 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → 𝑚 ∈ ℝ+)
304303adantr 484 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑚 ∈ ℝ+)
305227adantr 484 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑀𝑚)
306216adantr 484 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑚 ∈ ℝ)
307 reflcl 13163 . . . . . . . . . . . 12 (𝑚 ∈ ℝ → (⌊‘𝑚) ∈ ℝ)
308 peano2re 10804 . . . . . . . . . . . 12 ((⌊‘𝑚) ∈ ℝ → ((⌊‘𝑚) + 1) ∈ ℝ)
309306, 307, 3083syl 18 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((⌊‘𝑚) + 1) ∈ ℝ)
310 flltp1 13167 . . . . . . . . . . . 12 (𝑚 ∈ ℝ → 𝑚 < ((⌊‘𝑚) + 1))
311306, 310syl 17 . . . . . . . . . . 11 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑚 < ((⌊‘𝑚) + 1))
312306, 309, 311ltled 10779 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑚 ≤ ((⌊‘𝑚) + 1))
313230adantr 484 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (⌊‘𝑚) ∈ ℕ)
314 simpr 488 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → 𝑖 ∈ (ℤ‘(⌊‘𝑚)))
3155, 7, 294, 4, 6, 116, 295, 296, 120, 297, 298, 299, 300, 30, 301, 302, 304, 305, 312, 313, 314dchrisumlem2 26081 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (abs‘((seq1( + , 𝐹)‘𝑖) − (seq1( + , 𝐹)‘(⌊‘𝑚)))) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
316253, 238abssubd 14807 . . . . . . . . . 10 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑖))) = (abs‘((seq1( + , 𝐹)‘𝑖) − (seq1( + , 𝐹)‘(⌊‘𝑚)))))
317261, 316eqtrd 2833 . . . . . . . . 9 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) = (abs‘((seq1( + , 𝐹)‘𝑖) − (seq1( + , 𝐹)‘(⌊‘𝑚)))))
318315, 317, 2903brtr4d 5062 . . . . . . . 8 ((((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (ℤ‘(⌊‘𝑚))) → ((𝑘 ∈ ℕ ↦ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − (seq1( + , 𝐹)‘𝑘))))‘𝑖) ≤ ((ℕ × {((2 · 𝑅) · 𝑚 / 𝑛𝐴)})‘𝑖))
319211, 217, 264, 284, 287, 292, 318climle 14990 . . . . . . 7 (((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) ∧ 𝑚 ∈ (𝑀[,)+∞)) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
320319ralrimiva 3149 . . . . . 6 ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → ∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴))
321 oveq1 7142 . . . . . . . . . 10 (𝑐 = (2 · 𝑅) → (𝑐 · 𝐵) = ((2 · 𝑅) · 𝐵))
322321breq2d 5042 . . . . . . . . 9 (𝑐 = (2 · 𝑅) → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵)))
323322ralbidv 3162 . . . . . . . 8 (𝑐 = (2 · 𝑅) → (∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵) ↔ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵)))
324 2fveq3 6650 . . . . . . . . . . 11 (𝑚 = 𝑥 → (seq1( + , 𝐹)‘(⌊‘𝑚)) = (seq1( + , 𝐹)‘(⌊‘𝑥)))
325324fvoveq1d 7157 . . . . . . . . . 10 (𝑚 = 𝑥 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)))
326 vex 3444 . . . . . . . . . . . . 13 𝑚 ∈ V
327326a1i 11 . . . . . . . . . . . 12 (𝑚 = 𝑥𝑚 ∈ V)
328 equequ2 2033 . . . . . . . . . . . . . 14 (𝑚 = 𝑥 → (𝑛 = 𝑚𝑛 = 𝑥))
329328biimpa 480 . . . . . . . . . . . . 13 ((𝑚 = 𝑥𝑛 = 𝑚) → 𝑛 = 𝑥)
330329, 120syl 17 . . . . . . . . . . . 12 ((𝑚 = 𝑥𝑛 = 𝑚) → 𝐴 = 𝐵)
331327, 330csbied 3864 . . . . . . . . . . 11 (𝑚 = 𝑥𝑚 / 𝑛𝐴 = 𝐵)
332331oveq2d 7151 . . . . . . . . . 10 (𝑚 = 𝑥 → ((2 · 𝑅) · 𝑚 / 𝑛𝐴) = ((2 · 𝑅) · 𝐵))
333325, 332breq12d 5043 . . . . . . . . 9 (𝑚 = 𝑥 → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵)))
334333cbvralvw 3396 . . . . . . . 8 (∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴) ↔ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ ((2 · 𝑅) · 𝐵))
335323, 334bitr4di 292 . . . . . . 7 (𝑐 = (2 · 𝑅) → (∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵) ↔ ∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴)))
336335rspcev 3571 . . . . . 6 (((2 · 𝑅) ∈ (0[,)+∞) ∧ ∀𝑚 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑡)) ≤ ((2 · 𝑅) · 𝑚 / 𝑛𝐴)) → ∃𝑐 ∈ (0[,)+∞)∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))
337210, 320, 336syl2anc 587 . . . . 5 ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → ∃𝑐 ∈ (0[,)+∞)∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))
338 r19.42v 3303 . . . . 5 (∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)) ↔ (seq1( + , 𝐹) ⇝ 𝑡 ∧ ∃𝑐 ∈ (0[,)+∞)∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)))
339207, 337, 338sylanbrc 586 . . . 4 ((𝜑 ∧ seq1( + , 𝐹) ⇝ 𝑡) → ∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)))
340339ex 416 . . 3 (𝜑 → (seq1( + , 𝐹) ⇝ 𝑡 → ∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵))))
341340eximdv 1918 . 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 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  Vcvv 3441  ⦋csb 3828   ⊆ wss 3881  ∅c0 4243  ifcif 4425  {csn 4525   class class class wbr 5030   ↦ cmpt 5110   × cxp 5517  dom cdm 5519  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135  ℂcc 10526  ℝcr 10527  0cc0 10528  1c1 10529   + caddc 10531   · cmul 10533  +∞cpnf 10663  ℝ*cxr 10665   < clt 10666   ≤ cle 10667   − cmin 10861   / cdiv 11288  ℕcn 11627  2c2 11682  ℤcz 11971  ℤ≥cuz 12233  ℝ+crp 12379  [,)cico 12730  ..^cfzo 13030  ⌊cfl 13157  seqcseq 13366  abscabs 14587   ⇝ cli 14835   ⇝𝑟 crli 14836  Σcsu 15036  Basecbs 16477  0gc0g 16707  ℤRHomczrh 20197  ℤ/nℤczn 20200  DChrcdchr 25823 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443  ax-inf2 9090  ax-cnex 10584  ax-resscn 10585  ax-1cn 10586  ax-icn 10587  ax-addcl 10588  ax-addrcl 10589  ax-mulcl 10590  ax-mulrcl 10591  ax-mulcom 10592  ax-addass 10593  ax-mulass 10594  ax-distr 10595  ax-i2m1 10596  ax-1ne0 10597  ax-1rid 10598  ax-rnegex 10599  ax-rrecex 10600  ax-cnre 10601  ax-pre-lttri 10602  ax-pre-lttrn 10603  ax-pre-ltadd 10604  ax-pre-mulgt0 10605  ax-pre-sup 10606  ax-addf 10607  ax-mulf 10608 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-of 7390  df-om 7563  df-1st 7673  df-2nd 7674  df-tpos 7877  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-1o 8087  df-oadd 8091  df-er 8274  df-ec 8276  df-qs 8280  df-map 8393  df-pm 8394  df-en 8495  df-dom 8496  df-sdom 8497  df-fin 8498  df-sup 8892  df-inf 8893  df-oi 8960  df-card 9354  df-pnf 10668  df-mnf 10669  df-xr 10670  df-ltxr 10671  df-le 10672  df-sub 10863  df-neg 10864  df-div 11289  df-nn 11628  df-2 11690  df-3 11691  df-4 11692  df-5 11693  df-6 11694  df-7 11695  df-8 11696  df-9 11697  df-n0 11888  df-xnn0 11958  df-z 11972  df-dec 12089  df-uz 12234  df-rp 12380  df-ico 12734  df-fz 12888  df-fzo 13031  df-fl 13159  df-mod 13235  df-seq 13367  df-exp 13428  df-hash 13689  df-cj 14452  df-re 14453  df-im 14454  df-sqrt 14588  df-abs 14589  df-limsup 14822  df-clim 14839  df-rlim 14840  df-sum 15037  df-dvds 15602  df-gcd 15836  df-phi 16095  df-struct 16479  df-ndx 16480  df-slot 16481  df-base 16483  df-sets 16484  df-ress 16485  df-plusg 16572  df-mulr 16573  df-starv 16574  df-sca 16575  df-vsca 16576  df-ip 16577  df-tset 16578  df-ple 16579  df-ds 16581  df-unif 16582  df-0g 16709  df-imas 16775  df-qus 16776  df-mgm 17846  df-sgrp 17895  df-mnd 17906  df-mhm 17950  df-grp 18100  df-minusg 18101  df-sbg 18102  df-mulg 18220  df-subg 18271  df-nsg 18272  df-eqg 18273  df-ghm 18351  df-cmn 18903  df-abl 18904  df-mgp 19236  df-ur 19248  df-ring 19295  df-cring 19296  df-oppr 19372  df-dvdsr 19390  df-unit 19391  df-invr 19421  df-rnghom 19466  df-subrg 19529  df-lmod 19632  df-lss 19700  df-lsp 19740  df-sra 19940  df-rgmod 19941  df-lidl 19942  df-rsp 19943  df-2idl 20001  df-cnfld 20095  df-zring 20167  df-zrh 20201  df-zn 20204  df-dchr 25824 This theorem is referenced by:  dchrisum  26083
 Copyright terms: Public domain W3C validator