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

Theorem dchrisumlem2 27410
Description: Lemma for dchrisum 27412. 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..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
dchrisumlem2.1 (πœ‘ β†’ π‘ˆ ∈ ℝ+)
dchrisumlem2.2 (πœ‘ β†’ 𝑀 ≀ π‘ˆ)
dchrisumlem2.3 (πœ‘ β†’ π‘ˆ ≀ (𝐼 + 1))
dchrisumlem2.4 (πœ‘ β†’ 𝐼 ∈ β„•)
dchrisumlem2.5 (πœ‘ β†’ 𝐽 ∈ (β„€β‰₯β€˜πΌ))
Assertion
Ref Expression
dchrisumlem2 (πœ‘ β†’ (absβ€˜((seq1( + , 𝐹)β€˜π½) βˆ’ (seq1( + , 𝐹)β€˜πΌ))) ≀ ((2 Β· 𝑅) Β· β¦‹π‘ˆ / π‘›β¦Œπ΄))
Distinct variable groups:   𝑒,𝑛,π‘₯   1 ,𝑛,π‘₯   𝑛,𝐹,𝑒,π‘₯   𝑛,𝐼,𝑒,π‘₯   𝑛,𝐽,𝑒,π‘₯   π‘₯,𝐴   𝑛,𝑁,𝑒,π‘₯   πœ‘,𝑛,𝑒,π‘₯   𝑅,𝑛,𝑒,π‘₯   π‘ˆ,𝑛,𝑒,π‘₯   𝐡,𝑛   𝑛,𝑍,π‘₯   𝐷,𝑛,π‘₯   𝑛,𝐿,𝑒,π‘₯   𝑛,𝑀,𝑒,π‘₯   𝑛,𝑋,𝑒,π‘₯
Allowed substitution hints:   𝐴(𝑒,𝑛)   𝐡(π‘₯,𝑒)   𝐷(𝑒)   1 (𝑒)   𝐺(π‘₯,𝑒,𝑛)   𝑍(𝑒)

Proof of Theorem dchrisumlem2
Dummy variables π‘˜ 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzodisj 13690 . . . . . . . . 9 ((1..^(𝐼 + 1)) ∩ ((𝐼 + 1)..^(𝐽 + 1))) = βˆ…
21a1i 11 . . . . . . . 8 (πœ‘ β†’ ((1..^(𝐼 + 1)) ∩ ((𝐼 + 1)..^(𝐽 + 1))) = βˆ…)
3 dchrisumlem2.4 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐼 ∈ β„•)
43peano2nnd 12251 . . . . . . . . . . 11 (πœ‘ β†’ (𝐼 + 1) ∈ β„•)
5 nnuz 12887 . . . . . . . . . . 11 β„• = (β„€β‰₯β€˜1)
64, 5eleqtrdi 2838 . . . . . . . . . 10 (πœ‘ β†’ (𝐼 + 1) ∈ (β„€β‰₯β€˜1))
7 dchrisumlem2.5 . . . . . . . . . . 11 (πœ‘ β†’ 𝐽 ∈ (β„€β‰₯β€˜πΌ))
8 eluzp1p1 12872 . . . . . . . . . . 11 (𝐽 ∈ (β„€β‰₯β€˜πΌ) β†’ (𝐽 + 1) ∈ (β„€β‰₯β€˜(𝐼 + 1)))
97, 8syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝐽 + 1) ∈ (β„€β‰₯β€˜(𝐼 + 1)))
10 elfzuzb 13519 . . . . . . . . . 10 ((𝐼 + 1) ∈ (1...(𝐽 + 1)) ↔ ((𝐼 + 1) ∈ (β„€β‰₯β€˜1) ∧ (𝐽 + 1) ∈ (β„€β‰₯β€˜(𝐼 + 1))))
116, 9, 10sylanbrc 582 . . . . . . . . 9 (πœ‘ β†’ (𝐼 + 1) ∈ (1...(𝐽 + 1)))
12 fzosplit 13689 . . . . . . . . 9 ((𝐼 + 1) ∈ (1...(𝐽 + 1)) β†’ (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) βˆͺ ((𝐼 + 1)..^(𝐽 + 1))))
1311, 12syl 17 . . . . . . . 8 (πœ‘ β†’ (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) βˆͺ ((𝐼 + 1)..^(𝐽 + 1))))
14 fzofi 13963 . . . . . . . . 9 (1..^(𝐽 + 1)) ∈ Fin
1514a1i 11 . . . . . . . 8 (πœ‘ β†’ (1..^(𝐽 + 1)) ∈ Fin)
16 elfzouz 13660 . . . . . . . . . 10 (𝑖 ∈ (1..^(𝐽 + 1)) β†’ 𝑖 ∈ (β„€β‰₯β€˜1))
1716, 5eleqtrrdi 2839 . . . . . . . . 9 (𝑖 ∈ (1..^(𝐽 + 1)) β†’ 𝑖 ∈ β„•)
18 rpvmasum.g . . . . . . . . . . 11 𝐺 = (DChrβ€˜π‘)
19 rpvmasum.z . . . . . . . . . . 11 𝑍 = (β„€/nβ„€β€˜π‘)
20 rpvmasum.d . . . . . . . . . . 11 𝐷 = (Baseβ€˜πΊ)
21 rpvmasum.l . . . . . . . . . . 11 𝐿 = (β„€RHomβ€˜π‘)
22 dchrisum.b . . . . . . . . . . . 12 (πœ‘ β†’ 𝑋 ∈ 𝐷)
2322adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ 𝑋 ∈ 𝐷)
24 nnz 12601 . . . . . . . . . . . 12 (𝑖 ∈ β„• β†’ 𝑖 ∈ β„€)
2524adantl 481 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ 𝑖 ∈ β„€)
2618, 19, 20, 21, 23, 25dchrzrhcl 27165 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (π‘‹β€˜(πΏβ€˜π‘–)) ∈ β„‚)
27 rpvmasum.a . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑁 ∈ β„•)
28 rpvmasum.1 . . . . . . . . . . . . . 14 1 = (0gβ€˜πΊ)
29 dchrisum.n1 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑋 β‰  1 )
30 dchrisum.2 . . . . . . . . . . . . . 14 (𝑛 = π‘₯ β†’ 𝐴 = 𝐡)
31 dchrisum.3 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑀 ∈ β„•)
32 dchrisum.4 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ ℝ+) β†’ 𝐴 ∈ ℝ)
33 dchrisum.5 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑛 ∈ ℝ+ ∧ π‘₯ ∈ ℝ+) ∧ (𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯)) β†’ 𝐡 ≀ 𝐴)
34 dchrisum.6 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑛 ∈ ℝ+ ↦ 𝐴) β‡π‘Ÿ 0)
35 dchrisum.7 . . . . . . . . . . . . . 14 𝐹 = (𝑛 ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘›)) Β· 𝐴))
3619, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35dchrisumlema 27408 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝑖 ∈ ℝ+ β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ) ∧ (𝑖 ∈ (𝑀[,)+∞) β†’ 0 ≀ ⦋𝑖 / π‘›β¦Œπ΄)))
3736simpld 494 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑖 ∈ ℝ+ β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ))
38 nnrp 13009 . . . . . . . . . . . 12 (𝑖 ∈ β„• β†’ 𝑖 ∈ ℝ+)
3937, 38impel 505 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ)
4039recnd 11264 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ β„‚)
4126, 40mulcld 11256 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
4217, 41sylan2 592 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (1..^(𝐽 + 1))) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
432, 13, 15, 42fsumsplit 15711 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ (1..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)))
44 eluzelz 12854 . . . . . . . . 9 (𝐽 ∈ (β„€β‰₯β€˜πΌ) β†’ 𝐽 ∈ β„€)
45 fzval3 13725 . . . . . . . . 9 (𝐽 ∈ β„€ β†’ (1...𝐽) = (1..^(𝐽 + 1)))
467, 44, 453syl 18 . . . . . . . 8 (πœ‘ β†’ (1...𝐽) = (1..^(𝐽 + 1)))
4746sumeq1d 15671 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ (1...𝐽)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = Σ𝑖 ∈ (1..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
483nnzd 12607 . . . . . . . . . 10 (πœ‘ β†’ 𝐼 ∈ β„€)
49 fzval3 13725 . . . . . . . . . 10 (𝐼 ∈ β„€ β†’ (1...𝐼) = (1..^(𝐼 + 1)))
5048, 49syl 17 . . . . . . . . 9 (πœ‘ β†’ (1...𝐼) = (1..^(𝐼 + 1)))
5150sumeq1d 15671 . . . . . . . 8 (πœ‘ β†’ Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = Σ𝑖 ∈ (1..^(𝐼 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
5251oveq1d 7429 . . . . . . 7 (πœ‘ β†’ (Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)))
5343, 47, 523eqtr4d 2777 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ (1...𝐽)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = (Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)))
54 elfznn 13554 . . . . . . . 8 (𝑖 ∈ (1...𝐽) β†’ 𝑖 ∈ β„•)
55 simpr 484 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ 𝑖 ∈ β„•)
56 nfcv 2898 . . . . . . . . . 10 Ⅎ𝑛𝑖
57 nfcv 2898 . . . . . . . . . . 11 Ⅎ𝑛(π‘‹β€˜(πΏβ€˜π‘–))
58 nfcv 2898 . . . . . . . . . . 11 Ⅎ𝑛 Β·
59 nfcsb1v 3914 . . . . . . . . . . 11 Ⅎ𝑛⦋𝑖 / π‘›β¦Œπ΄
6057, 58, 59nfov 7444 . . . . . . . . . 10 Ⅎ𝑛((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)
61 2fveq3 6896 . . . . . . . . . . 11 (𝑛 = 𝑖 β†’ (π‘‹β€˜(πΏβ€˜π‘›)) = (π‘‹β€˜(πΏβ€˜π‘–)))
62 csbeq1a 3903 . . . . . . . . . . 11 (𝑛 = 𝑖 β†’ 𝐴 = ⦋𝑖 / π‘›β¦Œπ΄)
6361, 62oveq12d 7432 . . . . . . . . . 10 (𝑛 = 𝑖 β†’ ((π‘‹β€˜(πΏβ€˜π‘›)) Β· 𝐴) = ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
6456, 60, 63, 35fvmptf 7020 . . . . . . . . 9 ((𝑖 ∈ β„• ∧ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚) β†’ (πΉβ€˜π‘–) = ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
6555, 41, 64syl2anc 583 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (πΉβ€˜π‘–) = ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
6654, 65sylan2 592 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (1...𝐽)) β†’ (πΉβ€˜π‘–) = ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
673, 5eleqtrdi 2838 . . . . . . . 8 (πœ‘ β†’ 𝐼 ∈ (β„€β‰₯β€˜1))
68 uztrn 12862 . . . . . . . 8 ((𝐽 ∈ (β„€β‰₯β€˜πΌ) ∧ 𝐼 ∈ (β„€β‰₯β€˜1)) β†’ 𝐽 ∈ (β„€β‰₯β€˜1))
697, 67, 68syl2anc 583 . . . . . . 7 (πœ‘ β†’ 𝐽 ∈ (β„€β‰₯β€˜1))
7054, 41sylan2 592 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (1...𝐽)) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
7166, 69, 70fsumser 15700 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ (1...𝐽)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = (seq1( + , 𝐹)β€˜π½))
7253, 71eqtr3d 2769 . . . . 5 (πœ‘ β†’ (Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) = (seq1( + , 𝐹)β€˜π½))
73 elfznn 13554 . . . . . . 7 (𝑖 ∈ (1...𝐼) β†’ 𝑖 ∈ β„•)
7473, 65sylan2 592 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (1...𝐼)) β†’ (πΉβ€˜π‘–) = ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
7573, 41sylan2 592 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (1...𝐼)) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
7674, 67, 75fsumser 15700 . . . . 5 (πœ‘ β†’ Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = (seq1( + , 𝐹)β€˜πΌ))
7772, 76oveq12d 7432 . . . 4 (πœ‘ β†’ ((Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) βˆ’ Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) = ((seq1( + , 𝐹)β€˜π½) βˆ’ (seq1( + , 𝐹)β€˜πΌ)))
78 fzfid 13962 . . . . . 6 (πœ‘ β†’ (1...𝐼) ∈ Fin)
7978, 75fsumcl 15703 . . . . 5 (πœ‘ β†’ Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
80 fzofi 13963 . . . . . . 7 ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin
8180a1i 11 . . . . . 6 (πœ‘ β†’ ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin)
82 ssun2 4169 . . . . . . . . 9 ((𝐼 + 1)..^(𝐽 + 1)) βŠ† ((1..^(𝐼 + 1)) βˆͺ ((𝐼 + 1)..^(𝐽 + 1)))
8382, 13sseqtrrid 4031 . . . . . . . 8 (πœ‘ β†’ ((𝐼 + 1)..^(𝐽 + 1)) βŠ† (1..^(𝐽 + 1)))
8483sselda 3978 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ 𝑖 ∈ (1..^(𝐽 + 1)))
8584, 42syldan 590 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
8681, 85fsumcl 15703 . . . . 5 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
8779, 86pncan2d 11595 . . . 4 (πœ‘ β†’ ((Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) βˆ’ Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
8877, 87eqtr3d 2769 . . 3 (πœ‘ β†’ ((seq1( + , 𝐹)β€˜π½) βˆ’ (seq1( + , 𝐹)β€˜πΌ)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
8988fveq2d 6895 . 2 (πœ‘ β†’ (absβ€˜((seq1( + , 𝐹)β€˜π½) βˆ’ (seq1( + , 𝐹)β€˜πΌ))) = (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)))
9086abscld 15407 . . 3 (πœ‘ β†’ (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) ∈ ℝ)
91 2re 12308 . . . . . 6 2 ∈ ℝ
9291a1i 11 . . . . 5 (πœ‘ β†’ 2 ∈ ℝ)
93 dchrisum.9 . . . . 5 (πœ‘ β†’ 𝑅 ∈ ℝ)
9492, 93remulcld 11266 . . . 4 (πœ‘ β†’ (2 Β· 𝑅) ∈ ℝ)
9539ralrimiva 3141 . . . . 5 (πœ‘ β†’ βˆ€π‘– ∈ β„• ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ)
96 csbeq1 3892 . . . . . . 7 (𝑖 = (𝐼 + 1) β†’ ⦋𝑖 / π‘›β¦Œπ΄ = ⦋(𝐼 + 1) / π‘›β¦Œπ΄)
9796eleq1d 2813 . . . . . 6 (𝑖 = (𝐼 + 1) β†’ (⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ ↔ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ∈ ℝ))
9897rspcv 3603 . . . . 5 ((𝐼 + 1) ∈ β„• β†’ (βˆ€π‘– ∈ β„• ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ β†’ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ∈ ℝ))
994, 95, 98sylc 65 . . . 4 (πœ‘ β†’ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ∈ ℝ)
10094, 99remulcld 11266 . . 3 (πœ‘ β†’ ((2 Β· 𝑅) Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄) ∈ ℝ)
101 dchrisumlem2.1 . . . . 5 (πœ‘ β†’ π‘ˆ ∈ ℝ+)
10232ralrimiva 3141 . . . . 5 (πœ‘ β†’ βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ)
103 nfcsb1v 3914 . . . . . . 7 β„²π‘›β¦‹π‘ˆ / π‘›β¦Œπ΄
104103nfel1 2914 . . . . . 6 β„²π‘›β¦‹π‘ˆ / π‘›β¦Œπ΄ ∈ ℝ
105 csbeq1a 3903 . . . . . . 7 (𝑛 = π‘ˆ β†’ 𝐴 = β¦‹π‘ˆ / π‘›β¦Œπ΄)
106105eleq1d 2813 . . . . . 6 (𝑛 = π‘ˆ β†’ (𝐴 ∈ ℝ ↔ β¦‹π‘ˆ / π‘›β¦Œπ΄ ∈ ℝ))
107104, 106rspc 3595 . . . . 5 (π‘ˆ ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ β†’ β¦‹π‘ˆ / π‘›β¦Œπ΄ ∈ ℝ))
108101, 102, 107sylc 65 . . . 4 (πœ‘ β†’ β¦‹π‘ˆ / π‘›β¦Œπ΄ ∈ ℝ)
10994, 108remulcld 11266 . . 3 (πœ‘ β†’ ((2 Β· 𝑅) Β· β¦‹π‘ˆ / π‘›β¦Œπ΄) ∈ ℝ)
11069, 5eleqtrrdi 2839 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐽 ∈ β„•)
111110peano2nnd 12251 . . . . . . . . . . 11 (πœ‘ β†’ (𝐽 + 1) ∈ β„•)
112111nnrpd 13038 . . . . . . . . . 10 (πœ‘ β†’ (𝐽 + 1) ∈ ℝ+)
11319, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35dchrisumlema 27408 . . . . . . . . . . 11 (πœ‘ β†’ (((𝐽 + 1) ∈ ℝ+ β†’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄ ∈ ℝ) ∧ ((𝐽 + 1) ∈ (𝑀[,)+∞) β†’ 0 ≀ ⦋(𝐽 + 1) / π‘›β¦Œπ΄)))
114113simpld 494 . . . . . . . . . 10 (πœ‘ β†’ ((𝐽 + 1) ∈ ℝ+ β†’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄ ∈ ℝ))
115112, 114mpd 15 . . . . . . . . 9 (πœ‘ β†’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄ ∈ ℝ)
116115recnd 11264 . . . . . . . 8 (πœ‘ β†’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄ ∈ β„‚)
117 fzofi 13963 . . . . . . . . . 10 (0..^(𝐽 + 1)) ∈ Fin
118117a1i 11 . . . . . . . . 9 (πœ‘ β†’ (0..^(𝐽 + 1)) ∈ Fin)
119 elfzoelz 13656 . . . . . . . . . 10 (𝑛 ∈ (0..^(𝐽 + 1)) β†’ 𝑛 ∈ β„€)
12022adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„€) β†’ 𝑋 ∈ 𝐷)
121 simpr 484 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„€) β†’ 𝑛 ∈ β„€)
12218, 19, 20, 21, 120, 121dchrzrhcl 27165 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„€) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
123119, 122sylan2 592 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (0..^(𝐽 + 1))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
124118, 123fsumcl 15703 . . . . . . . 8 (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
125116, 124mulcld 11256 . . . . . . 7 (πœ‘ β†’ (⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ∈ β„‚)
12699recnd 11264 . . . . . . . 8 (πœ‘ β†’ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ∈ β„‚)
127 fzofi 13963 . . . . . . . . . 10 (0..^(𝐼 + 1)) ∈ Fin
128127a1i 11 . . . . . . . . 9 (πœ‘ β†’ (0..^(𝐼 + 1)) ∈ Fin)
129 elfzoelz 13656 . . . . . . . . . 10 (𝑛 ∈ (0..^(𝐼 + 1)) β†’ 𝑛 ∈ β„€)
130129, 122sylan2 592 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (0..^(𝐼 + 1))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
131128, 130fsumcl 15703 . . . . . . . 8 (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
132126, 131mulcld 11256 . . . . . . 7 (πœ‘ β†’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ∈ β„‚)
133125, 132subcld 11593 . . . . . 6 (πœ‘ β†’ ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ∈ β„‚)
134133abscld 15407 . . . . 5 (πœ‘ β†’ (absβ€˜((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ∈ ℝ)
13584, 17syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ 𝑖 ∈ β„•)
136 peano2nn 12246 . . . . . . . . . . . . 13 (𝑖 ∈ β„• β†’ (𝑖 + 1) ∈ β„•)
137136nnrpd 13038 . . . . . . . . . . . 12 (𝑖 ∈ β„• β†’ (𝑖 + 1) ∈ ℝ+)
138 nfcsb1v 3914 . . . . . . . . . . . . . . 15 Ⅎ𝑛⦋(𝑖 + 1) / π‘›β¦Œπ΄
139138nfel1 2914 . . . . . . . . . . . . . 14 Ⅎ𝑛⦋(𝑖 + 1) / π‘›β¦Œπ΄ ∈ ℝ
140 csbeq1a 3903 . . . . . . . . . . . . . . 15 (𝑛 = (𝑖 + 1) β†’ 𝐴 = ⦋(𝑖 + 1) / π‘›β¦Œπ΄)
141140eleq1d 2813 . . . . . . . . . . . . . 14 (𝑛 = (𝑖 + 1) β†’ (𝐴 ∈ ℝ ↔ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ∈ ℝ))
142139, 141rspc 3595 . . . . . . . . . . . . 13 ((𝑖 + 1) ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ∈ ℝ))
143142impcom 407 . . . . . . . . . . . 12 ((βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ ∧ (𝑖 + 1) ∈ ℝ+) β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ∈ ℝ)
144102, 137, 143syl2an 595 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ∈ ℝ)
145144, 39resubcld 11664 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) ∈ ℝ)
146145recnd 11264 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
147 fzofi 13963 . . . . . . . . . . . 12 (0..^(𝑖 + 1)) ∈ Fin
148147a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (0..^(𝑖 + 1)) ∈ Fin)
149 elfzoelz 13656 . . . . . . . . . . . 12 (𝑛 ∈ (0..^(𝑖 + 1)) β†’ 𝑛 ∈ β„€)
150149, 122sylan2 592 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (0..^(𝑖 + 1))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
151148, 150fsumcl 15703 . . . . . . . . . 10 (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
152151adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
153146, 152mulcld 11256 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ∈ β„‚)
154135, 153syldan 590 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ∈ β„‚)
15581, 154fsumcl 15703 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ∈ β„‚)
156155abscld 15407 . . . . 5 (πœ‘ β†’ (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ∈ ℝ)
157134, 156readdcld 11265 . . . 4 (πœ‘ β†’ ((absβ€˜((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) + (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ∈ ℝ)
15826, 40mulcomd 11257 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = (⦋𝑖 / π‘›β¦Œπ΄ Β· (π‘‹β€˜(πΏβ€˜π‘–))))
159 nnnn0 12501 . . . . . . . . . . . . . . . 16 (𝑖 ∈ β„• β†’ 𝑖 ∈ β„•0)
160159adantl 481 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ 𝑖 ∈ β„•0)
161 nn0uz 12886 . . . . . . . . . . . . . . 15 β„•0 = (β„€β‰₯β€˜0)
162160, 161eleqtrdi 2838 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ 𝑖 ∈ (β„€β‰₯β€˜0))
163 elfzelz 13525 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0...𝑖) β†’ 𝑛 ∈ β„€)
164122adantlr 714 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑖 ∈ β„•) ∧ 𝑛 ∈ β„€) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
165163, 164sylan2 592 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑖 ∈ β„•) ∧ 𝑛 ∈ (0...𝑖)) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
166162, 165, 61fzosump1 15722 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) = (Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)) + (π‘‹β€˜(πΏβ€˜π‘–))))
167166oveq1d 7429 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›))) = ((Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)) + (π‘‹β€˜(πΏβ€˜π‘–))) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›))))
168 fzofi 13963 . . . . . . . . . . . . . . 15 (0..^𝑖) ∈ Fin
169168a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (0..^𝑖) ∈ Fin)
170 elfzoelz 13656 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0..^𝑖) β†’ 𝑛 ∈ β„€)
171170, 164sylan2 592 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑖 ∈ β„•) ∧ 𝑛 ∈ (0..^𝑖)) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
172169, 171fsumcl 15703 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
173172, 26pncan2d 11595 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ((Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)) + (π‘‹β€˜(πΏβ€˜π‘–))) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›))) = (π‘‹β€˜(πΏβ€˜π‘–)))
174167, 173eqtr2d 2768 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (π‘‹β€˜(πΏβ€˜π‘–)) = (Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›))))
175174oveq2d 7430 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (⦋𝑖 / π‘›β¦Œπ΄ Β· (π‘‹β€˜(πΏβ€˜π‘–))) = (⦋𝑖 / π‘›β¦Œπ΄ Β· (Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)))))
176158, 175eqtrd 2767 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = (⦋𝑖 / π‘›β¦Œπ΄ Β· (Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)))))
177135, 176syldan 590 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = (⦋𝑖 / π‘›β¦Œπ΄ Β· (Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)))))
178177sumeq2dv 15673 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / π‘›β¦Œπ΄ Β· (Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)))))
179 csbeq1 3892 . . . . . . . . 9 (π‘˜ = 𝑖 β†’ β¦‹π‘˜ / π‘›β¦Œπ΄ = ⦋𝑖 / π‘›β¦Œπ΄)
180 oveq2 7422 . . . . . . . . . 10 (π‘˜ = 𝑖 β†’ (0..^π‘˜) = (0..^𝑖))
181180sumeq1d 15671 . . . . . . . . 9 (π‘˜ = 𝑖 β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)))
182179, 181jca 511 . . . . . . . 8 (π‘˜ = 𝑖 β†’ (β¦‹π‘˜ / π‘›β¦Œπ΄ = ⦋𝑖 / π‘›β¦Œπ΄ ∧ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›))))
183 csbeq1 3892 . . . . . . . . 9 (π‘˜ = (𝑖 + 1) β†’ β¦‹π‘˜ / π‘›β¦Œπ΄ = ⦋(𝑖 + 1) / π‘›β¦Œπ΄)
184 oveq2 7422 . . . . . . . . . 10 (π‘˜ = (𝑖 + 1) β†’ (0..^π‘˜) = (0..^(𝑖 + 1)))
185184sumeq1d 15671 . . . . . . . . 9 (π‘˜ = (𝑖 + 1) β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))
186183, 185jca 511 . . . . . . . 8 (π‘˜ = (𝑖 + 1) β†’ (β¦‹π‘˜ / π‘›β¦Œπ΄ = ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ∧ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))
187 csbeq1 3892 . . . . . . . . 9 (π‘˜ = (𝐼 + 1) β†’ β¦‹π‘˜ / π‘›β¦Œπ΄ = ⦋(𝐼 + 1) / π‘›β¦Œπ΄)
188 oveq2 7422 . . . . . . . . . 10 (π‘˜ = (𝐼 + 1) β†’ (0..^π‘˜) = (0..^(𝐼 + 1)))
189188sumeq1d 15671 . . . . . . . . 9 (π‘˜ = (𝐼 + 1) β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))
190187, 189jca 511 . . . . . . . 8 (π‘˜ = (𝐼 + 1) β†’ (β¦‹π‘˜ / π‘›β¦Œπ΄ = ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ∧ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))
191 csbeq1 3892 . . . . . . . . 9 (π‘˜ = (𝐽 + 1) β†’ β¦‹π‘˜ / π‘›β¦Œπ΄ = ⦋(𝐽 + 1) / π‘›β¦Œπ΄)
192 oveq2 7422 . . . . . . . . . 10 (π‘˜ = (𝐽 + 1) β†’ (0..^π‘˜) = (0..^(𝐽 + 1)))
193192sumeq1d 15671 . . . . . . . . 9 (π‘˜ = (𝐽 + 1) β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))
194191, 193jca 511 . . . . . . . 8 (π‘˜ = (𝐽 + 1) β†’ (β¦‹π‘˜ / π‘›β¦Œπ΄ = ⦋(𝐽 + 1) / π‘›β¦Œπ΄ ∧ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))
19540ralrimiva 3141 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘– ∈ β„• ⦋𝑖 / π‘›β¦Œπ΄ ∈ β„‚)
196 elfzuz 13521 . . . . . . . . . 10 (π‘˜ ∈ ((𝐼 + 1)...(𝐽 + 1)) β†’ π‘˜ ∈ (β„€β‰₯β€˜(𝐼 + 1)))
197 eluznn 12924 . . . . . . . . . 10 (((𝐼 + 1) ∈ β„• ∧ π‘˜ ∈ (β„€β‰₯β€˜(𝐼 + 1))) β†’ π‘˜ ∈ β„•)
1984, 196, 197syl2an 595 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ ((𝐼 + 1)...(𝐽 + 1))) β†’ π‘˜ ∈ β„•)
199 csbeq1 3892 . . . . . . . . . . 11 (𝑖 = π‘˜ β†’ ⦋𝑖 / π‘›β¦Œπ΄ = β¦‹π‘˜ / π‘›β¦Œπ΄)
200199eleq1d 2813 . . . . . . . . . 10 (𝑖 = π‘˜ β†’ (⦋𝑖 / π‘›β¦Œπ΄ ∈ β„‚ ↔ β¦‹π‘˜ / π‘›β¦Œπ΄ ∈ β„‚))
201200rspccva 3606 . . . . . . . . 9 ((βˆ€π‘– ∈ β„• ⦋𝑖 / π‘›β¦Œπ΄ ∈ β„‚ ∧ π‘˜ ∈ β„•) β†’ β¦‹π‘˜ / π‘›β¦Œπ΄ ∈ β„‚)
202195, 198, 201syl2an2r 684 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ ((𝐼 + 1)...(𝐽 + 1))) β†’ β¦‹π‘˜ / π‘›β¦Œπ΄ ∈ β„‚)
203 fzofi 13963 . . . . . . . . . . 11 (0..^π‘˜) ∈ Fin
204203a1i 11 . . . . . . . . . 10 (πœ‘ β†’ (0..^π‘˜) ∈ Fin)
205 elfzoelz 13656 . . . . . . . . . . 11 (𝑛 ∈ (0..^π‘˜) β†’ 𝑛 ∈ β„€)
206205, 122sylan2 592 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (0..^π‘˜)) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
207204, 206fsumcl 15703 . . . . . . . . 9 (πœ‘ β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
208207adantr 480 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ ((𝐼 + 1)...(𝐽 + 1))) β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
209182, 186, 190, 194, 9, 202, 208fsumparts 15776 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / π‘›β¦Œπ΄ Β· (Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)))) = (((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) βˆ’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
210178, 209eqtrd 2767 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = (((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) βˆ’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
211210fveq2d 6895 . . . . 5 (πœ‘ β†’ (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) = (absβ€˜(((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) βˆ’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))))
212133, 155abs2dif2d 15429 . . . . 5 (πœ‘ β†’ (absβ€˜(((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) βˆ’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ≀ ((absβ€˜((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) + (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))))
213211, 212eqbrtrd 5164 . . . 4 (πœ‘ β†’ (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) ≀ ((absβ€˜((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) + (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))))
214115, 99readdcld 11265 . . . . . . 7 (πœ‘ β†’ (⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) ∈ ℝ)
215214, 93remulcld 11266 . . . . . 6 (πœ‘ β†’ ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅) ∈ ℝ)
216179, 183, 187, 191, 9, 202telfsumo 15772 . . . . . . . 8 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) = (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄))
217135, 39syldan 590 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ)
218135, 144syldan 590 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ∈ ℝ)
219217, 218resubcld 11664 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) ∈ ℝ)
22081, 219fsumrecl 15704 . . . . . . . 8 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) ∈ ℝ)
221216, 220eqeltrrd 2829 . . . . . . 7 (πœ‘ β†’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) ∈ ℝ)
222221, 93remulcld 11266 . . . . . 6 (πœ‘ β†’ ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) Β· 𝑅) ∈ ℝ)
223125abscld 15407 . . . . . . . 8 (πœ‘ β†’ (absβ€˜(⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ∈ ℝ)
224132abscld 15407 . . . . . . . 8 (πœ‘ β†’ (absβ€˜(⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ∈ ℝ)
225223, 224readdcld 11265 . . . . . . 7 (πœ‘ β†’ ((absβ€˜(⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) + (absβ€˜(⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ∈ ℝ)
226125, 132abs2dif2d 15429 . . . . . . 7 (πœ‘ β†’ (absβ€˜((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ≀ ((absβ€˜(⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) + (absβ€˜(⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))))
227115, 93remulcld 11266 . . . . . . . . 9 (πœ‘ β†’ (⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· 𝑅) ∈ ℝ)
22899, 93remulcld 11266 . . . . . . . . 9 (πœ‘ β†’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· 𝑅) ∈ ℝ)
229116, 124absmuld 15425 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜(⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = ((absβ€˜β¦‹(𝐽 + 1) / π‘›β¦Œπ΄) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
230 eluzelre 12855 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑖 ∈ ℝ)
231230adantl 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ ℝ)
232 eluzle 12857 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑀 ≀ 𝑖)
233232adantl 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑀 ≀ 𝑖)
23431nnred 12249 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝑀 ∈ ℝ)
235234adantr 480 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑀 ∈ ℝ)
236 elicopnf 13446 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℝ β†’ (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀 ≀ 𝑖)))
237235, 236syl 17 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀 ≀ 𝑖)))
238231, 233, 237mpbir2and 712 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ (𝑀[,)+∞))
239238ex 412 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑖 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑖 ∈ (𝑀[,)+∞)))
240239ssrdv 3984 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (β„€β‰₯β€˜π‘€) βŠ† (𝑀[,)+∞))
24131nnzd 12607 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑀 ∈ β„€)
24248peano2zd 12691 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐼 + 1) ∈ β„€)
243101rpred 13040 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ π‘ˆ ∈ ℝ)
2444nnred 12249 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐼 + 1) ∈ ℝ)
245 dchrisumlem2.2 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑀 ≀ π‘ˆ)
246 dchrisumlem2.3 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ π‘ˆ ≀ (𝐼 + 1))
247234, 243, 244, 245, 246letrd 11393 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑀 ≀ (𝐼 + 1))
248 eluz2 12850 . . . . . . . . . . . . . . . . 17 ((𝐼 + 1) ∈ (β„€β‰₯β€˜π‘€) ↔ (𝑀 ∈ β„€ ∧ (𝐼 + 1) ∈ β„€ ∧ 𝑀 ≀ (𝐼 + 1)))
249241, 242, 247, 248syl3anbrc 1341 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐼 + 1) ∈ (β„€β‰₯β€˜π‘€))
250 uztrn 12862 . . . . . . . . . . . . . . . 16 (((𝐽 + 1) ∈ (β„€β‰₯β€˜(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐽 + 1) ∈ (β„€β‰₯β€˜π‘€))
2519, 249, 250syl2anc 583 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐽 + 1) ∈ (β„€β‰₯β€˜π‘€))
252240, 251sseldd 3979 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐽 + 1) ∈ (𝑀[,)+∞))
253113simprd 495 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝐽 + 1) ∈ (𝑀[,)+∞) β†’ 0 ≀ ⦋(𝐽 + 1) / π‘›β¦Œπ΄))
254252, 253mpd 15 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 ≀ ⦋(𝐽 + 1) / π‘›β¦Œπ΄)
255115, 254absidd 15393 . . . . . . . . . . . 12 (πœ‘ β†’ (absβ€˜β¦‹(𝐽 + 1) / π‘›β¦Œπ΄) = ⦋(𝐽 + 1) / π‘›β¦Œπ΄)
256255oveq1d 7429 . . . . . . . . . . 11 (πœ‘ β†’ ((absβ€˜β¦‹(𝐽 + 1) / π‘›β¦Œπ΄) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = (⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
257229, 256eqtrd 2767 . . . . . . . . . 10 (πœ‘ β†’ (absβ€˜(⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = (⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
258124abscld 15407 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ∈ ℝ)
259111nnnn0d 12554 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐽 + 1) ∈ β„•0)
260 dchrisum.10 . . . . . . . . . . . . 13 (πœ‘ β†’ βˆ€π‘’ ∈ (0..^𝑁)(absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
26119, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35, 93, 260dchrisumlem1 27409 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝐽 + 1) ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
262259, 261mpdan 686 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
263258, 93, 115, 254, 262lemul2ad 12176 . . . . . . . . . 10 (πœ‘ β†’ (⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ (⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· 𝑅))
264257, 263eqbrtrd 5164 . . . . . . . . 9 (πœ‘ β†’ (absβ€˜(⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ (⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· 𝑅))
265126, 131absmuld 15425 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜(⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = ((absβ€˜β¦‹(𝐼 + 1) / π‘›β¦Œπ΄) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
266240, 249sseldd 3979 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐼 + 1) ∈ (𝑀[,)+∞))
26719, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35dchrisumlema 27408 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (((𝐼 + 1) ∈ ℝ+ β†’ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ∈ ℝ) ∧ ((𝐼 + 1) ∈ (𝑀[,)+∞) β†’ 0 ≀ ⦋(𝐼 + 1) / π‘›β¦Œπ΄)))
268267simprd 495 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝐼 + 1) ∈ (𝑀[,)+∞) β†’ 0 ≀ ⦋(𝐼 + 1) / π‘›β¦Œπ΄))
269266, 268mpd 15 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 ≀ ⦋(𝐼 + 1) / π‘›β¦Œπ΄)
27099, 269absidd 15393 . . . . . . . . . . . 12 (πœ‘ β†’ (absβ€˜β¦‹(𝐼 + 1) / π‘›β¦Œπ΄) = ⦋(𝐼 + 1) / π‘›β¦Œπ΄)
271270oveq1d 7429 . . . . . . . . . . 11 (πœ‘ β†’ ((absβ€˜β¦‹(𝐼 + 1) / π‘›β¦Œπ΄) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
272265, 271eqtrd 2767 . . . . . . . . . 10 (πœ‘ β†’ (absβ€˜(⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
273131abscld 15407 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ∈ ℝ)
2744nnnn0d 12554 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐼 + 1) ∈ β„•0)
27519, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35, 93, 260dchrisumlem1 27409 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝐼 + 1) ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
276274, 275mpdan 686 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
277273, 93, 99, 269, 276lemul2ad 12176 . . . . . . . . . 10 (πœ‘ β†’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· 𝑅))
278272, 277eqbrtrd 5164 . . . . . . . . 9 (πœ‘ β†’ (absβ€˜(⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· 𝑅))
279223, 224, 227, 228, 264, 278le2addd 11855 . . . . . . . 8 (πœ‘ β†’ ((absβ€˜(⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) + (absβ€˜(⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ≀ ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· 𝑅) + (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· 𝑅)))
28093recnd 11264 . . . . . . . . 9 (πœ‘ β†’ 𝑅 ∈ β„‚)
281116, 126, 280adddird 11261 . . . . . . . 8 (πœ‘ β†’ ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅) = ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· 𝑅) + (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· 𝑅)))
282279, 281breqtrrd 5170 . . . . . . 7 (πœ‘ β†’ ((absβ€˜(⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) + (absβ€˜(⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ≀ ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
283134, 225, 215, 226, 282letrd 11393 . . . . . 6 (πœ‘ β†’ (absβ€˜((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ≀ ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
284154abscld 15407 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (absβ€˜((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ∈ ℝ)
28581, 284fsumrecl 15704 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(absβ€˜((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ∈ ℝ)
28681, 154fsumabs 15771 . . . . . . 7 (πœ‘ β†’ (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(absβ€˜((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
28793adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ 𝑅 ∈ ℝ)
288219, 287remulcld 11266 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· 𝑅) ∈ ℝ)
289135, 146syldan 590 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
290151adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
291289, 290absmuld 15425 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (absβ€˜((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = ((absβ€˜(⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄)) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
292 elfzouz 13660 . . . . . . . . . . . . . . 15 (𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1)) β†’ 𝑖 ∈ (β„€β‰₯β€˜(𝐼 + 1)))
293 uztrn 12862 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (β„€β‰₯β€˜(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ (β„€β‰₯β€˜π‘€))
294292, 249, 293syl2anr 596 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ 𝑖 ∈ (β„€β‰₯β€˜π‘€))
295 eluznn 12924 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ β„• ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ β„•)
29631, 295sylan 579 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ β„•)
297296, 137syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝑖 + 1) ∈ ℝ+)
298296nnrpd 13038 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ ℝ+)
299333expia 1119 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑛 ∈ ℝ+ ∧ π‘₯ ∈ ℝ+)) β†’ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴))
300299ralrimivva 3195 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ βˆ€π‘› ∈ ℝ+ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴))
301300adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ βˆ€π‘› ∈ ℝ+ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴))
302 nfcv 2898 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑛ℝ+
303 nfv 1910 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑛(𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯)
304 nfcv 2898 . . . . . . . . . . . . . . . . . . . 20 Ⅎ𝑛𝐡
305 nfcv 2898 . . . . . . . . . . . . . . . . . . . 20 Ⅎ𝑛 ≀
306304, 305, 59nfbr 5189 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑛 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄
307303, 306nfim 1892 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑛((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄)
308302, 307nfralw 3303 . . . . . . . . . . . . . . . . 17 β„²π‘›βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄)
309 breq2 5146 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑖 β†’ (𝑀 ≀ 𝑛 ↔ 𝑀 ≀ 𝑖))
310 breq1 5145 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑖 β†’ (𝑛 ≀ π‘₯ ↔ 𝑖 ≀ π‘₯))
311309, 310anbi12d 630 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑖 β†’ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) ↔ (𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯)))
31262breq2d 5154 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑖 β†’ (𝐡 ≀ 𝐴 ↔ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄))
313311, 312imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑖 β†’ (((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴) ↔ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄)))
314313ralbidv 3172 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 β†’ (βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴) ↔ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄)))
315308, 314rspc 3595 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴) β†’ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄)))
316298, 301, 315sylc 65 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄))
317231lep1d 12167 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ≀ (𝑖 + 1))
318233, 317jca 511 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝑀 ≀ 𝑖 ∧ 𝑖 ≀ (𝑖 + 1)))
319 breq2 5146 . . . . . . . . . . . . . . . . . 18 (π‘₯ = (𝑖 + 1) β†’ (𝑖 ≀ π‘₯ ↔ 𝑖 ≀ (𝑖 + 1)))
320319anbi2d 628 . . . . . . . . . . . . . . . . 17 (π‘₯ = (𝑖 + 1) β†’ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) ↔ (𝑀 ≀ 𝑖 ∧ 𝑖 ≀ (𝑖 + 1))))
321 eqvisset 3487 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = (𝑖 + 1) β†’ (𝑖 + 1) ∈ V)
322 eqtr3 2753 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) β†’ π‘₯ = 𝑛)
32330equcoms 2016 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑛 β†’ 𝐴 = 𝐡)
324322, 323syl 17 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) β†’ 𝐴 = 𝐡)
325321, 324csbied 3927 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = (𝑖 + 1) β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ = 𝐡)
326325eqcomd 2733 . . . . . . . . . . . . . . . . . 18 (π‘₯ = (𝑖 + 1) β†’ 𝐡 = ⦋(𝑖 + 1) / π‘›β¦Œπ΄)
327326breq1d 5152 . . . . . . . . . . . . . . . . 17 (π‘₯ = (𝑖 + 1) β†’ (𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄ ↔ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ≀ ⦋𝑖 / π‘›β¦Œπ΄))
328320, 327imbi12d 344 . . . . . . . . . . . . . . . 16 (π‘₯ = (𝑖 + 1) β†’ (((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄) ↔ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ (𝑖 + 1)) β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ≀ ⦋𝑖 / π‘›β¦Œπ΄)))
329328rspcv 3603 . . . . . . . . . . . . . . 15 ((𝑖 + 1) ∈ ℝ+ β†’ (βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄) β†’ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ (𝑖 + 1)) β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ≀ ⦋𝑖 / π‘›β¦Œπ΄)))
330297, 316, 318, 329syl3c 66 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ≀ ⦋𝑖 / π‘›β¦Œπ΄)
331294, 330syldan 590 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ≀ ⦋𝑖 / π‘›β¦Œπ΄)
332218, 217, 331abssuble0d 15403 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (absβ€˜(⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄)) = (⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄))
333332oveq1d 7429 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ((absβ€˜(⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄)) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = ((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
334291, 333eqtrd 2767 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (absβ€˜((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = ((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
335290abscld 15407 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ∈ ℝ)
336217, 218subge0d 11826 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (0 ≀ (⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) ↔ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ≀ ⦋𝑖 / π‘›β¦Œπ΄))
337331, 336mpbird 257 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ 0 ≀ (⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄))
338135peano2nnd 12251 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (𝑖 + 1) ∈ β„•)
339338nnnn0d 12554 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (𝑖 + 1) ∈ β„•0)
34019, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35, 93, 260dchrisumlem1 27409 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑖 + 1) ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
341339, 340syldan 590 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
342335, 287, 219, 337, 341lemul2ad 12176 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ ((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
343334, 342eqbrtrd 5164 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (absβ€˜((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ ((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
34481, 284, 288, 343fsumle 15769 . . . . . . . 8 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(absβ€˜((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
345219recnd 11264 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) ∈ β„‚)
34681, 280, 345fsummulc1 15755 . . . . . . . . 9 (πœ‘ β†’ (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· 𝑅) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
347216oveq1d 7429 . . . . . . . . 9 (πœ‘ β†’ (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· 𝑅) = ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
348346, 347eqtr3d 2769 . . . . . . . 8 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· 𝑅) = ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
349344, 348breqtrd 5168 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(absβ€˜((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
350156, 285, 222, 286, 349letrd 11393 . . . . . 6 (πœ‘ β†’ (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
351134, 156, 215, 222, 283, 350le2addd 11855 . . . . 5 (πœ‘ β†’ ((absβ€˜((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) + (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ≀ (((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅) + ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) Β· 𝑅)))
3521262timesd 12477 . . . . . . . 8 (πœ‘ β†’ (2 Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄) = (⦋(𝐼 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄))
353126, 116, 126ppncand 11633 . . . . . . . 8 (πœ‘ β†’ ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ + ⦋(𝐽 + 1) / π‘›β¦Œπ΄) + (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄)) = (⦋(𝐼 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄))
354126, 116addcomd 11438 . . . . . . . . 9 (πœ‘ β†’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ + ⦋(𝐽 + 1) / π‘›β¦Œπ΄) = (⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄))
355354oveq1d 7429 . . . . . . . 8 (πœ‘ β†’ ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ + ⦋(𝐽 + 1) / π‘›β¦Œπ΄) + (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄)) = ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) + (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄)))
356352, 353, 3553eqtr2d 2773 . . . . . . 7 (πœ‘ β†’ (2 Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄) = ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) + (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄)))
357356oveq1d 7429 . . . . . 6 (πœ‘ β†’ ((2 Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅) = (((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) + (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄)) Β· 𝑅))
358 2cnd 12312 . . . . . . 7 (πœ‘ β†’ 2 ∈ β„‚)
359358, 126, 280mul32d 11446 . . . . . 6 (πœ‘ β†’ ((2 Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅) = ((2 Β· 𝑅) Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄))
360214recnd 11264 . . . . . . 7 (πœ‘ β†’ (⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) ∈ β„‚)
361221recnd 11264 . . . . . . 7 (πœ‘ β†’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) ∈ β„‚)
362360, 361, 280adddird 11261 . . . . . 6 (πœ‘ β†’ (((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) + (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄)) Β· 𝑅) = (((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅) + ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) Β· 𝑅)))
363357, 359, 3623eqtr3d 2775 . . . . 5 (πœ‘ β†’ ((2 Β· 𝑅) Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄) = (((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅) + ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) Β· 𝑅)))
364351, 363breqtrrd 5170 . . . 4 (πœ‘ β†’ ((absβ€˜((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) + (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ≀ ((2 Β· 𝑅) Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄))
36590, 157, 100, 213, 364letrd 11393 . . 3 (πœ‘ β†’ (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) ≀ ((2 Β· 𝑅) Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄))
366 2nn0 12511 . . . . . 6 2 ∈ β„•0
367 nn0ge0 12519 . . . . . 6 (2 ∈ β„•0 β†’ 0 ≀ 2)
368366, 367mp1i 13 . . . . 5 (πœ‘ β†’ 0 ≀ 2)
369 0red 11239 . . . . . 6 (πœ‘ β†’ 0 ∈ ℝ)
370124absge0d 15415 . . . . . 6 (πœ‘ β†’ 0 ≀ (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))
371369, 258, 93, 370, 262letrd 11393 . . . . 5 (πœ‘ β†’ 0 ≀ 𝑅)
37292, 93, 368, 371mulge0d 11813 . . . 4 (πœ‘ β†’ 0 ≀ (2 Β· 𝑅))
3734nnrpd 13038 . . . . 5 (πœ‘ β†’ (𝐼 + 1) ∈ ℝ+)
374 nfv 1910 . . . . . . . . 9 Ⅎ𝑛(𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯)
375304, 305, 103nfbr 5189 . . . . . . . . 9 Ⅎ𝑛 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄
376374, 375nfim 1892 . . . . . . . 8 Ⅎ𝑛((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) β†’ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄)
377302, 376nfralw 3303 . . . . . . 7 β„²π‘›βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) β†’ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄)
378 breq2 5146 . . . . . . . . . 10 (𝑛 = π‘ˆ β†’ (𝑀 ≀ 𝑛 ↔ 𝑀 ≀ π‘ˆ))
379 breq1 5145 . . . . . . . . . 10 (𝑛 = π‘ˆ β†’ (𝑛 ≀ π‘₯ ↔ π‘ˆ ≀ π‘₯))
380378, 379anbi12d 630 . . . . . . . . 9 (𝑛 = π‘ˆ β†’ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) ↔ (𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯)))
381105breq2d 5154 . . . . . . . . 9 (𝑛 = π‘ˆ β†’ (𝐡 ≀ 𝐴 ↔ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄))
382380, 381imbi12d 344 . . . . . . . 8 (𝑛 = π‘ˆ β†’ (((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴) ↔ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) β†’ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄)))
383382ralbidv 3172 . . . . . . 7 (𝑛 = π‘ˆ β†’ (βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴) ↔ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) β†’ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄)))
384377, 383rspc 3595 . . . . . 6 (π‘ˆ ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴) β†’ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) β†’ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄)))
385101, 300, 384sylc 65 . . . . 5 (πœ‘ β†’ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) β†’ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄))
386245, 246jca 511 . . . . 5 (πœ‘ β†’ (𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ (𝐼 + 1)))
387 breq2 5146 . . . . . . . 8 (π‘₯ = (𝐼 + 1) β†’ (π‘ˆ ≀ π‘₯ ↔ π‘ˆ ≀ (𝐼 + 1)))
388387anbi2d 628 . . . . . . 7 (π‘₯ = (𝐼 + 1) β†’ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) ↔ (𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ (𝐼 + 1))))
389 eqvisset 3487 . . . . . . . . . 10 (π‘₯ = (𝐼 + 1) β†’ (𝐼 + 1) ∈ V)
390 eqtr3 2753 . . . . . . . . . . 11 ((π‘₯ = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) β†’ π‘₯ = 𝑛)
391390, 323syl 17 . . . . . . . . . 10 ((π‘₯ = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) β†’ 𝐴 = 𝐡)
392389, 391csbied 3927 . . . . . . . . 9 (π‘₯ = (𝐼 + 1) β†’ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ = 𝐡)
393392eqcomd 2733 . . . . . . . 8 (π‘₯ = (𝐼 + 1) β†’ 𝐡 = ⦋(𝐼 + 1) / π‘›β¦Œπ΄)
394393breq1d 5152 . . . . . . 7 (π‘₯ = (𝐼 + 1) β†’ (𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄ ↔ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄))
395388, 394imbi12d 344 . . . . . 6 (π‘₯ = (𝐼 + 1) β†’ (((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) β†’ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄) ↔ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ (𝐼 + 1)) β†’ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄)))
396395rspcv 3603 . . . . 5 ((𝐼 + 1) ∈ ℝ+ β†’ (βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) β†’ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄) β†’ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ (𝐼 + 1)) β†’ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄)))
397373, 385, 386, 396syl3c 66 . . . 4 (πœ‘ β†’ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄)
39899, 108, 94, 372, 397lemul2ad 12176 . . 3 (πœ‘ β†’ ((2 Β· 𝑅) Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄) ≀ ((2 Β· 𝑅) Β· β¦‹π‘ˆ / π‘›β¦Œπ΄))
39990, 100, 109, 365, 398letrd 11393 . 2 (πœ‘ β†’ (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) ≀ ((2 Β· 𝑅) Β· β¦‹π‘ˆ / π‘›β¦Œπ΄))
40089, 399eqbrtrd 5164 1 (πœ‘ β†’ (absβ€˜((seq1( + , 𝐹)β€˜π½) βˆ’ (seq1( + , 𝐹)β€˜πΌ))) ≀ ((2 Β· 𝑅) Β· β¦‹π‘ˆ / π‘›β¦Œπ΄))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099   β‰  wne 2935  βˆ€wral 3056  Vcvv 3469  β¦‹csb 3889   βˆͺ cun 3942   ∩ cin 3943  βˆ…c0 4318   class class class wbr 5142   ↦ cmpt 5225  β€˜cfv 6542  (class class class)co 7414  Fincfn 8955  β„‚cc 11128  β„cr 11129  0cc0 11130  1c1 11131   + caddc 11133   Β· cmul 11135  +∞cpnf 11267   ≀ cle 11271   βˆ’ cmin 11466  β„•cn 12234  2c2 12289  β„•0cn0 12494  β„€cz 12580  β„€β‰₯cuz 12844  β„+crp 12998  [,)cico 13350  ...cfz 13508  ..^cfzo 13651  seqcseq 13990  abscabs 15205   β‡π‘Ÿ crli 15453  Ξ£csu 15656  Basecbs 17171  0gc0g 17412  β„€RHomczrh 21412  β„€/nβ„€czn 21415  DChrcdchr 27152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208  ax-addf 11209  ax-mulf 11210
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7865  df-1st 7987  df-2nd 7988  df-tpos 8225  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-oadd 8484  df-er 8718  df-ec 8720  df-qs 8724  df-map 8838  df-pm 8839  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-sup 9457  df-inf 9458  df-oi 9525  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-5 12300  df-6 12301  df-7 12302  df-8 12303  df-9 12304  df-n0 12495  df-xnn0 12567  df-z 12581  df-dec 12700  df-uz 12845  df-rp 12999  df-ico 13354  df-fz 13509  df-fzo 13652  df-fl 13781  df-mod 13859  df-seq 13991  df-exp 14051  df-hash 14314  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-clim 15456  df-rlim 15457  df-sum 15657  df-dvds 16223  df-gcd 16461  df-phi 16726  df-struct 17107  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-plusg 17237  df-mulr 17238  df-starv 17239  df-sca 17240  df-vsca 17241  df-ip 17242  df-tset 17243  df-ple 17244  df-ds 17246  df-unif 17247  df-0g 17414  df-imas 17481  df-qus 17482  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-mhm 18731  df-grp 18884  df-minusg 18885  df-sbg 18886  df-mulg 19015  df-subg 19069  df-nsg 19070  df-eqg 19071  df-ghm 19159  df-cmn 19728  df-abl 19729  df-mgp 20066  df-rng 20084  df-ur 20113  df-ring 20166  df-cring 20167  df-oppr 20262  df-dvdsr 20285  df-unit 20286  df-invr 20316  df-rhm 20400  df-subrng 20472  df-subrg 20497  df-lmod 20734  df-lss 20805  df-lsp 20845  df-sra 21047  df-rgmod 21048  df-lidl 21093  df-rsp 21094  df-2idl 21133  df-cnfld 21267  df-zring 21360  df-zrh 21416  df-zn 21419  df-dchr 27153
This theorem is referenced by:  dchrisumlem3  27411
  Copyright terms: Public domain W3C validator