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

Theorem dchrisumlem2 26854
Description: Lemma for dchrisum 26856. 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 13613 . . . . . . . . 9 ((1..^(𝐼 + 1)) ∩ ((𝐼 + 1)..^(𝐽 + 1))) = βˆ…
21a1i 11 . . . . . . . 8 (πœ‘ β†’ ((1..^(𝐼 + 1)) ∩ ((𝐼 + 1)..^(𝐽 + 1))) = βˆ…)
3 dchrisumlem2.4 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐼 ∈ β„•)
43peano2nnd 12177 . . . . . . . . . . 11 (πœ‘ β†’ (𝐼 + 1) ∈ β„•)
5 nnuz 12813 . . . . . . . . . . 11 β„• = (β„€β‰₯β€˜1)
64, 5eleqtrdi 2848 . . . . . . . . . 10 (πœ‘ β†’ (𝐼 + 1) ∈ (β„€β‰₯β€˜1))
7 dchrisumlem2.5 . . . . . . . . . . 11 (πœ‘ β†’ 𝐽 ∈ (β„€β‰₯β€˜πΌ))
8 eluzp1p1 12798 . . . . . . . . . . 11 (𝐽 ∈ (β„€β‰₯β€˜πΌ) β†’ (𝐽 + 1) ∈ (β„€β‰₯β€˜(𝐼 + 1)))
97, 8syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝐽 + 1) ∈ (β„€β‰₯β€˜(𝐼 + 1)))
10 elfzuzb 13442 . . . . . . . . . 10 ((𝐼 + 1) ∈ (1...(𝐽 + 1)) ↔ ((𝐼 + 1) ∈ (β„€β‰₯β€˜1) ∧ (𝐽 + 1) ∈ (β„€β‰₯β€˜(𝐼 + 1))))
116, 9, 10sylanbrc 584 . . . . . . . . 9 (πœ‘ β†’ (𝐼 + 1) ∈ (1...(𝐽 + 1)))
12 fzosplit 13612 . . . . . . . . 9 ((𝐼 + 1) ∈ (1...(𝐽 + 1)) β†’ (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) βˆͺ ((𝐼 + 1)..^(𝐽 + 1))))
1311, 12syl 17 . . . . . . . 8 (πœ‘ β†’ (1..^(𝐽 + 1)) = ((1..^(𝐼 + 1)) βˆͺ ((𝐼 + 1)..^(𝐽 + 1))))
14 fzofi 13886 . . . . . . . . 9 (1..^(𝐽 + 1)) ∈ Fin
1514a1i 11 . . . . . . . 8 (πœ‘ β†’ (1..^(𝐽 + 1)) ∈ Fin)
16 elfzouz 13583 . . . . . . . . . 10 (𝑖 ∈ (1..^(𝐽 + 1)) β†’ 𝑖 ∈ (β„€β‰₯β€˜1))
1716, 5eleqtrrdi 2849 . . . . . . . . 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 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ 𝑋 ∈ 𝐷)
24 nnz 12527 . . . . . . . . . . . 12 (𝑖 ∈ β„• β†’ 𝑖 ∈ β„€)
2524adantl 483 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ 𝑖 ∈ β„€)
2618, 19, 20, 21, 23, 25dchrzrhcl 26609 . . . . . . . . . 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 26852 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝑖 ∈ ℝ+ β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ) ∧ (𝑖 ∈ (𝑀[,)+∞) β†’ 0 ≀ ⦋𝑖 / π‘›β¦Œπ΄)))
3736simpld 496 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑖 ∈ ℝ+ β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ))
38 nnrp 12933 . . . . . . . . . . . 12 (𝑖 ∈ β„• β†’ 𝑖 ∈ ℝ+)
3937, 38impel 507 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ)
4039recnd 11190 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ β„‚)
4126, 40mulcld 11182 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
4217, 41sylan2 594 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (1..^(𝐽 + 1))) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
432, 13, 15, 42fsumsplit 15633 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ (1..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)))
44 eluzelz 12780 . . . . . . . . 9 (𝐽 ∈ (β„€β‰₯β€˜πΌ) β†’ 𝐽 ∈ β„€)
45 fzval3 13648 . . . . . . . . 9 (𝐽 ∈ β„€ β†’ (1...𝐽) = (1..^(𝐽 + 1)))
467, 44, 453syl 18 . . . . . . . 8 (πœ‘ β†’ (1...𝐽) = (1..^(𝐽 + 1)))
4746sumeq1d 15593 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ (1...𝐽)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = Σ𝑖 ∈ (1..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
483nnzd 12533 . . . . . . . . . 10 (πœ‘ β†’ 𝐼 ∈ β„€)
49 fzval3 13648 . . . . . . . . . 10 (𝐼 ∈ β„€ β†’ (1...𝐼) = (1..^(𝐼 + 1)))
5048, 49syl 17 . . . . . . . . 9 (πœ‘ β†’ (1...𝐼) = (1..^(𝐼 + 1)))
5150sumeq1d 15593 . . . . . . . 8 (πœ‘ β†’ Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = Σ𝑖 ∈ (1..^(𝐼 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
5251oveq1d 7377 . . . . . . 7 (πœ‘ β†’ (Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) = (Σ𝑖 ∈ (1..^(𝐼 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)))
5343, 47, 523eqtr4d 2787 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ (1...𝐽)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = (Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)))
54 elfznn 13477 . . . . . . . 8 (𝑖 ∈ (1...𝐽) β†’ 𝑖 ∈ β„•)
55 simpr 486 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ 𝑖 ∈ β„•)
56 nfcv 2908 . . . . . . . . . 10 Ⅎ𝑛𝑖
57 nfcv 2908 . . . . . . . . . . 11 Ⅎ𝑛(π‘‹β€˜(πΏβ€˜π‘–))
58 nfcv 2908 . . . . . . . . . . 11 Ⅎ𝑛 Β·
59 nfcsb1v 3885 . . . . . . . . . . 11 Ⅎ𝑛⦋𝑖 / π‘›β¦Œπ΄
6057, 58, 59nfov 7392 . . . . . . . . . 10 Ⅎ𝑛((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)
61 2fveq3 6852 . . . . . . . . . . 11 (𝑛 = 𝑖 β†’ (π‘‹β€˜(πΏβ€˜π‘›)) = (π‘‹β€˜(πΏβ€˜π‘–)))
62 csbeq1a 3874 . . . . . . . . . . 11 (𝑛 = 𝑖 β†’ 𝐴 = ⦋𝑖 / π‘›β¦Œπ΄)
6361, 62oveq12d 7380 . . . . . . . . . 10 (𝑛 = 𝑖 β†’ ((π‘‹β€˜(πΏβ€˜π‘›)) Β· 𝐴) = ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
6456, 60, 63, 35fvmptf 6974 . . . . . . . . 9 ((𝑖 ∈ β„• ∧ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚) β†’ (πΉβ€˜π‘–) = ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
6555, 41, 64syl2anc 585 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (πΉβ€˜π‘–) = ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
6654, 65sylan2 594 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (1...𝐽)) β†’ (πΉβ€˜π‘–) = ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
673, 5eleqtrdi 2848 . . . . . . . 8 (πœ‘ β†’ 𝐼 ∈ (β„€β‰₯β€˜1))
68 uztrn 12788 . . . . . . . 8 ((𝐽 ∈ (β„€β‰₯β€˜πΌ) ∧ 𝐼 ∈ (β„€β‰₯β€˜1)) β†’ 𝐽 ∈ (β„€β‰₯β€˜1))
697, 67, 68syl2anc 585 . . . . . . 7 (πœ‘ β†’ 𝐽 ∈ (β„€β‰₯β€˜1))
7054, 41sylan2 594 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (1...𝐽)) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
7166, 69, 70fsumser 15622 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ (1...𝐽)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = (seq1( + , 𝐹)β€˜π½))
7253, 71eqtr3d 2779 . . . . 5 (πœ‘ β†’ (Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) = (seq1( + , 𝐹)β€˜π½))
73 elfznn 13477 . . . . . . 7 (𝑖 ∈ (1...𝐼) β†’ 𝑖 ∈ β„•)
7473, 65sylan2 594 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (1...𝐼)) β†’ (πΉβ€˜π‘–) = ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
7573, 41sylan2 594 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (1...𝐼)) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
7674, 67, 75fsumser 15622 . . . . 5 (πœ‘ β†’ Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = (seq1( + , 𝐹)β€˜πΌ))
7772, 76oveq12d 7380 . . . 4 (πœ‘ β†’ ((Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) βˆ’ Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) = ((seq1( + , 𝐹)β€˜π½) βˆ’ (seq1( + , 𝐹)β€˜πΌ)))
78 fzfid 13885 . . . . . 6 (πœ‘ β†’ (1...𝐼) ∈ Fin)
7978, 75fsumcl 15625 . . . . 5 (πœ‘ β†’ Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
80 fzofi 13886 . . . . . . 7 ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin
8180a1i 11 . . . . . 6 (πœ‘ β†’ ((𝐼 + 1)..^(𝐽 + 1)) ∈ Fin)
82 ssun2 4138 . . . . . . . . 9 ((𝐼 + 1)..^(𝐽 + 1)) βŠ† ((1..^(𝐼 + 1)) βˆͺ ((𝐼 + 1)..^(𝐽 + 1)))
8382, 13sseqtrrid 4002 . . . . . . . 8 (πœ‘ β†’ ((𝐼 + 1)..^(𝐽 + 1)) βŠ† (1..^(𝐽 + 1)))
8483sselda 3949 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ 𝑖 ∈ (1..^(𝐽 + 1)))
8584, 42syldan 592 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
8681, 85fsumcl 15625 . . . . 5 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
8779, 86pncan2d 11521 . . . 4 (πœ‘ β†’ ((Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) + Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) βˆ’ Σ𝑖 ∈ (1...𝐼)((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
8877, 87eqtr3d 2779 . . 3 (πœ‘ β†’ ((seq1( + , 𝐹)β€˜π½) βˆ’ (seq1( + , 𝐹)β€˜πΌ)) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
8988fveq2d 6851 . 2 (πœ‘ β†’ (absβ€˜((seq1( + , 𝐹)β€˜π½) βˆ’ (seq1( + , 𝐹)β€˜πΌ))) = (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)))
9086abscld 15328 . . 3 (πœ‘ β†’ (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) ∈ ℝ)
91 2re 12234 . . . . . 6 2 ∈ ℝ
9291a1i 11 . . . . 5 (πœ‘ β†’ 2 ∈ ℝ)
93 dchrisum.9 . . . . 5 (πœ‘ β†’ 𝑅 ∈ ℝ)
9492, 93remulcld 11192 . . . 4 (πœ‘ β†’ (2 Β· 𝑅) ∈ ℝ)
9539ralrimiva 3144 . . . . 5 (πœ‘ β†’ βˆ€π‘– ∈ β„• ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ)
96 csbeq1 3863 . . . . . . 7 (𝑖 = (𝐼 + 1) β†’ ⦋𝑖 / π‘›β¦Œπ΄ = ⦋(𝐼 + 1) / π‘›β¦Œπ΄)
9796eleq1d 2823 . . . . . 6 (𝑖 = (𝐼 + 1) β†’ (⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ ↔ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ∈ ℝ))
9897rspcv 3580 . . . . 5 ((𝐼 + 1) ∈ β„• β†’ (βˆ€π‘– ∈ β„• ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ β†’ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ∈ ℝ))
994, 95, 98sylc 65 . . . 4 (πœ‘ β†’ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ∈ ℝ)
10094, 99remulcld 11192 . . 3 (πœ‘ β†’ ((2 Β· 𝑅) Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄) ∈ ℝ)
101 dchrisumlem2.1 . . . . 5 (πœ‘ β†’ π‘ˆ ∈ ℝ+)
10232ralrimiva 3144 . . . . 5 (πœ‘ β†’ βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ)
103 nfcsb1v 3885 . . . . . . 7 β„²π‘›β¦‹π‘ˆ / π‘›β¦Œπ΄
104103nfel1 2924 . . . . . 6 β„²π‘›β¦‹π‘ˆ / π‘›β¦Œπ΄ ∈ ℝ
105 csbeq1a 3874 . . . . . . 7 (𝑛 = π‘ˆ β†’ 𝐴 = β¦‹π‘ˆ / π‘›β¦Œπ΄)
106105eleq1d 2823 . . . . . 6 (𝑛 = π‘ˆ β†’ (𝐴 ∈ ℝ ↔ β¦‹π‘ˆ / π‘›β¦Œπ΄ ∈ ℝ))
107104, 106rspc 3572 . . . . 5 (π‘ˆ ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ β†’ β¦‹π‘ˆ / π‘›β¦Œπ΄ ∈ ℝ))
108101, 102, 107sylc 65 . . . 4 (πœ‘ β†’ β¦‹π‘ˆ / π‘›β¦Œπ΄ ∈ ℝ)
10994, 108remulcld 11192 . . 3 (πœ‘ β†’ ((2 Β· 𝑅) Β· β¦‹π‘ˆ / π‘›β¦Œπ΄) ∈ ℝ)
11069, 5eleqtrrdi 2849 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐽 ∈ β„•)
111110peano2nnd 12177 . . . . . . . . . . 11 (πœ‘ β†’ (𝐽 + 1) ∈ β„•)
112111nnrpd 12962 . . . . . . . . . 10 (πœ‘ β†’ (𝐽 + 1) ∈ ℝ+)
11319, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35dchrisumlema 26852 . . . . . . . . . . 11 (πœ‘ β†’ (((𝐽 + 1) ∈ ℝ+ β†’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄ ∈ ℝ) ∧ ((𝐽 + 1) ∈ (𝑀[,)+∞) β†’ 0 ≀ ⦋(𝐽 + 1) / π‘›β¦Œπ΄)))
114113simpld 496 . . . . . . . . . 10 (πœ‘ β†’ ((𝐽 + 1) ∈ ℝ+ β†’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄ ∈ ℝ))
115112, 114mpd 15 . . . . . . . . 9 (πœ‘ β†’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄ ∈ ℝ)
116115recnd 11190 . . . . . . . 8 (πœ‘ β†’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄ ∈ β„‚)
117 fzofi 13886 . . . . . . . . . 10 (0..^(𝐽 + 1)) ∈ Fin
118117a1i 11 . . . . . . . . 9 (πœ‘ β†’ (0..^(𝐽 + 1)) ∈ Fin)
119 elfzoelz 13579 . . . . . . . . . 10 (𝑛 ∈ (0..^(𝐽 + 1)) β†’ 𝑛 ∈ β„€)
12022adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„€) β†’ 𝑋 ∈ 𝐷)
121 simpr 486 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„€) β†’ 𝑛 ∈ β„€)
12218, 19, 20, 21, 120, 121dchrzrhcl 26609 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„€) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
123119, 122sylan2 594 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (0..^(𝐽 + 1))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
124118, 123fsumcl 15625 . . . . . . . 8 (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
125116, 124mulcld 11182 . . . . . . 7 (πœ‘ β†’ (⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ∈ β„‚)
12699recnd 11190 . . . . . . . 8 (πœ‘ β†’ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ∈ β„‚)
127 fzofi 13886 . . . . . . . . . 10 (0..^(𝐼 + 1)) ∈ Fin
128127a1i 11 . . . . . . . . 9 (πœ‘ β†’ (0..^(𝐼 + 1)) ∈ Fin)
129 elfzoelz 13579 . . . . . . . . . 10 (𝑛 ∈ (0..^(𝐼 + 1)) β†’ 𝑛 ∈ β„€)
130129, 122sylan2 594 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (0..^(𝐼 + 1))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
131128, 130fsumcl 15625 . . . . . . . 8 (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
132126, 131mulcld 11182 . . . . . . 7 (πœ‘ β†’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ∈ β„‚)
133125, 132subcld 11519 . . . . . 6 (πœ‘ β†’ ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ∈ β„‚)
134133abscld 15328 . . . . 5 (πœ‘ β†’ (absβ€˜((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ∈ ℝ)
13584, 17syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ 𝑖 ∈ β„•)
136 peano2nn 12172 . . . . . . . . . . . . 13 (𝑖 ∈ β„• β†’ (𝑖 + 1) ∈ β„•)
137136nnrpd 12962 . . . . . . . . . . . 12 (𝑖 ∈ β„• β†’ (𝑖 + 1) ∈ ℝ+)
138 nfcsb1v 3885 . . . . . . . . . . . . . . 15 Ⅎ𝑛⦋(𝑖 + 1) / π‘›β¦Œπ΄
139138nfel1 2924 . . . . . . . . . . . . . 14 Ⅎ𝑛⦋(𝑖 + 1) / π‘›β¦Œπ΄ ∈ ℝ
140 csbeq1a 3874 . . . . . . . . . . . . . . 15 (𝑛 = (𝑖 + 1) β†’ 𝐴 = ⦋(𝑖 + 1) / π‘›β¦Œπ΄)
141140eleq1d 2823 . . . . . . . . . . . . . 14 (𝑛 = (𝑖 + 1) β†’ (𝐴 ∈ ℝ ↔ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ∈ ℝ))
142139, 141rspc 3572 . . . . . . . . . . . . 13 ((𝑖 + 1) ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ∈ ℝ))
143142impcom 409 . . . . . . . . . . . 12 ((βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ ∧ (𝑖 + 1) ∈ ℝ+) β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ∈ ℝ)
144102, 137, 143syl2an 597 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ∈ ℝ)
145144, 39resubcld 11590 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) ∈ ℝ)
146145recnd 11190 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
147 fzofi 13886 . . . . . . . . . . . 12 (0..^(𝑖 + 1)) ∈ Fin
148147a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (0..^(𝑖 + 1)) ∈ Fin)
149 elfzoelz 13579 . . . . . . . . . . . 12 (𝑛 ∈ (0..^(𝑖 + 1)) β†’ 𝑛 ∈ β„€)
150149, 122sylan2 594 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (0..^(𝑖 + 1))) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
151148, 150fsumcl 15625 . . . . . . . . . 10 (πœ‘ β†’ Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
152151adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
153146, 152mulcld 11182 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ∈ β„‚)
154135, 153syldan 592 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ∈ β„‚)
15581, 154fsumcl 15625 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ∈ β„‚)
156155abscld 15328 . . . . 5 (πœ‘ β†’ (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ∈ ℝ)
157134, 156readdcld 11191 . . . 4 (πœ‘ β†’ ((absβ€˜((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) + (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ∈ ℝ)
15826, 40mulcomd 11183 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = (⦋𝑖 / π‘›β¦Œπ΄ Β· (π‘‹β€˜(πΏβ€˜π‘–))))
159 nnnn0 12427 . . . . . . . . . . . . . . . 16 (𝑖 ∈ β„• β†’ 𝑖 ∈ β„•0)
160159adantl 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ 𝑖 ∈ β„•0)
161 nn0uz 12812 . . . . . . . . . . . . . . 15 β„•0 = (β„€β‰₯β€˜0)
162160, 161eleqtrdi 2848 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ 𝑖 ∈ (β„€β‰₯β€˜0))
163 elfzelz 13448 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0...𝑖) β†’ 𝑛 ∈ β„€)
164122adantlr 714 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑖 ∈ β„•) ∧ 𝑛 ∈ β„€) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
165163, 164sylan2 594 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑖 ∈ β„•) ∧ 𝑛 ∈ (0...𝑖)) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
166162, 165, 61fzosump1 15644 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) = (Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)) + (π‘‹β€˜(πΏβ€˜π‘–))))
167166oveq1d 7377 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›))) = ((Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)) + (π‘‹β€˜(πΏβ€˜π‘–))) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›))))
168 fzofi 13886 . . . . . . . . . . . . . . 15 (0..^𝑖) ∈ Fin
169168a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (0..^𝑖) ∈ Fin)
170 elfzoelz 13579 . . . . . . . . . . . . . . 15 (𝑛 ∈ (0..^𝑖) β†’ 𝑛 ∈ β„€)
171170, 164sylan2 594 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑖 ∈ β„•) ∧ 𝑛 ∈ (0..^𝑖)) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
172169, 171fsumcl 15625 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
173172, 26pncan2d 11521 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ((Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)) + (π‘‹β€˜(πΏβ€˜π‘–))) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›))) = (π‘‹β€˜(πΏβ€˜π‘–)))
174167, 173eqtr2d 2778 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (π‘‹β€˜(πΏβ€˜π‘–)) = (Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›))))
175174oveq2d 7378 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (⦋𝑖 / π‘›β¦Œπ΄ Β· (π‘‹β€˜(πΏβ€˜π‘–))) = (⦋𝑖 / π‘›β¦Œπ΄ Β· (Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)))))
176158, 175eqtrd 2777 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = (⦋𝑖 / π‘›β¦Œπ΄ Β· (Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)))))
177135, 176syldan 592 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = (⦋𝑖 / π‘›β¦Œπ΄ Β· (Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)))))
178177sumeq2dv 15595 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / π‘›β¦Œπ΄ Β· (Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)))))
179 csbeq1 3863 . . . . . . . . 9 (π‘˜ = 𝑖 β†’ β¦‹π‘˜ / π‘›β¦Œπ΄ = ⦋𝑖 / π‘›β¦Œπ΄)
180 oveq2 7370 . . . . . . . . . 10 (π‘˜ = 𝑖 β†’ (0..^π‘˜) = (0..^𝑖))
181180sumeq1d 15593 . . . . . . . . 9 (π‘˜ = 𝑖 β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)))
182179, 181jca 513 . . . . . . . 8 (π‘˜ = 𝑖 β†’ (β¦‹π‘˜ / π‘›β¦Œπ΄ = ⦋𝑖 / π‘›β¦Œπ΄ ∧ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›))))
183 csbeq1 3863 . . . . . . . . 9 (π‘˜ = (𝑖 + 1) β†’ β¦‹π‘˜ / π‘›β¦Œπ΄ = ⦋(𝑖 + 1) / π‘›β¦Œπ΄)
184 oveq2 7370 . . . . . . . . . 10 (π‘˜ = (𝑖 + 1) β†’ (0..^π‘˜) = (0..^(𝑖 + 1)))
185184sumeq1d 15593 . . . . . . . . 9 (π‘˜ = (𝑖 + 1) β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))
186183, 185jca 513 . . . . . . . 8 (π‘˜ = (𝑖 + 1) β†’ (β¦‹π‘˜ / π‘›β¦Œπ΄ = ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ∧ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))
187 csbeq1 3863 . . . . . . . . 9 (π‘˜ = (𝐼 + 1) β†’ β¦‹π‘˜ / π‘›β¦Œπ΄ = ⦋(𝐼 + 1) / π‘›β¦Œπ΄)
188 oveq2 7370 . . . . . . . . . 10 (π‘˜ = (𝐼 + 1) β†’ (0..^π‘˜) = (0..^(𝐼 + 1)))
189188sumeq1d 15593 . . . . . . . . 9 (π‘˜ = (𝐼 + 1) β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))
190187, 189jca 513 . . . . . . . 8 (π‘˜ = (𝐼 + 1) β†’ (β¦‹π‘˜ / π‘›β¦Œπ΄ = ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ∧ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))
191 csbeq1 3863 . . . . . . . . 9 (π‘˜ = (𝐽 + 1) β†’ β¦‹π‘˜ / π‘›β¦Œπ΄ = ⦋(𝐽 + 1) / π‘›β¦Œπ΄)
192 oveq2 7370 . . . . . . . . . 10 (π‘˜ = (𝐽 + 1) β†’ (0..^π‘˜) = (0..^(𝐽 + 1)))
193192sumeq1d 15593 . . . . . . . . 9 (π‘˜ = (𝐽 + 1) β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))
194191, 193jca 513 . . . . . . . 8 (π‘˜ = (𝐽 + 1) β†’ (β¦‹π‘˜ / π‘›β¦Œπ΄ = ⦋(𝐽 + 1) / π‘›β¦Œπ΄ ∧ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))
19540ralrimiva 3144 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘– ∈ β„• ⦋𝑖 / π‘›β¦Œπ΄ ∈ β„‚)
196 elfzuz 13444 . . . . . . . . . 10 (π‘˜ ∈ ((𝐼 + 1)...(𝐽 + 1)) β†’ π‘˜ ∈ (β„€β‰₯β€˜(𝐼 + 1)))
197 eluznn 12850 . . . . . . . . . 10 (((𝐼 + 1) ∈ β„• ∧ π‘˜ ∈ (β„€β‰₯β€˜(𝐼 + 1))) β†’ π‘˜ ∈ β„•)
1984, 196, 197syl2an 597 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ ((𝐼 + 1)...(𝐽 + 1))) β†’ π‘˜ ∈ β„•)
199 csbeq1 3863 . . . . . . . . . . 11 (𝑖 = π‘˜ β†’ ⦋𝑖 / π‘›β¦Œπ΄ = β¦‹π‘˜ / π‘›β¦Œπ΄)
200199eleq1d 2823 . . . . . . . . . 10 (𝑖 = π‘˜ β†’ (⦋𝑖 / π‘›β¦Œπ΄ ∈ β„‚ ↔ β¦‹π‘˜ / π‘›β¦Œπ΄ ∈ β„‚))
201200rspccva 3583 . . . . . . . . 9 ((βˆ€π‘– ∈ β„• ⦋𝑖 / π‘›β¦Œπ΄ ∈ β„‚ ∧ π‘˜ ∈ β„•) β†’ β¦‹π‘˜ / π‘›β¦Œπ΄ ∈ β„‚)
202195, 198, 201syl2an2r 684 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ ((𝐼 + 1)...(𝐽 + 1))) β†’ β¦‹π‘˜ / π‘›β¦Œπ΄ ∈ β„‚)
203 fzofi 13886 . . . . . . . . . . 11 (0..^π‘˜) ∈ Fin
204203a1i 11 . . . . . . . . . 10 (πœ‘ β†’ (0..^π‘˜) ∈ Fin)
205 elfzoelz 13579 . . . . . . . . . . 11 (𝑛 ∈ (0..^π‘˜) β†’ 𝑛 ∈ β„€)
206205, 122sylan2 594 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (0..^π‘˜)) β†’ (π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
207204, 206fsumcl 15625 . . . . . . . . 9 (πœ‘ β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
208207adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ ((𝐼 + 1)...(𝐽 + 1))) β†’ Σ𝑛 ∈ (0..^π‘˜)(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
209182, 186, 190, 194, 9, 202, 208fsumparts 15698 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / π‘›β¦Œπ΄ Β· (Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) βˆ’ Σ𝑛 ∈ (0..^𝑖)(π‘‹β€˜(πΏβ€˜π‘›)))) = (((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) βˆ’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
210178, 209eqtrd 2777 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) = (((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) βˆ’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
211210fveq2d 6851 . . . . 5 (πœ‘ β†’ (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) = (absβ€˜(((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) βˆ’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))))
212133, 155abs2dif2d 15350 . . . . 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 5132 . . . 4 (πœ‘ β†’ (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) ≀ ((absβ€˜((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) + (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))))
214115, 99readdcld 11191 . . . . . . 7 (πœ‘ β†’ (⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) ∈ ℝ)
215214, 93remulcld 11192 . . . . . 6 (πœ‘ β†’ ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅) ∈ ℝ)
216179, 183, 187, 191, 9, 202telfsumo 15694 . . . . . . . 8 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) = (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄))
217135, 39syldan 592 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ)
218135, 144syldan 592 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ∈ ℝ)
219217, 218resubcld 11590 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) ∈ ℝ)
22081, 219fsumrecl 15626 . . . . . . . 8 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) ∈ ℝ)
221216, 220eqeltrrd 2839 . . . . . . 7 (πœ‘ β†’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) ∈ ℝ)
222221, 93remulcld 11192 . . . . . 6 (πœ‘ β†’ ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) Β· 𝑅) ∈ ℝ)
223125abscld 15328 . . . . . . . 8 (πœ‘ β†’ (absβ€˜(⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ∈ ℝ)
224132abscld 15328 . . . . . . . 8 (πœ‘ β†’ (absβ€˜(⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ∈ ℝ)
225223, 224readdcld 11191 . . . . . . 7 (πœ‘ β†’ ((absβ€˜(⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) + (absβ€˜(⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ∈ ℝ)
226125, 132abs2dif2d 15350 . . . . . . 7 (πœ‘ β†’ (absβ€˜((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ≀ ((absβ€˜(⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) + (absβ€˜(⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))))
227115, 93remulcld 11192 . . . . . . . . 9 (πœ‘ β†’ (⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· 𝑅) ∈ ℝ)
22899, 93remulcld 11192 . . . . . . . . 9 (πœ‘ β†’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· 𝑅) ∈ ℝ)
229116, 124absmuld 15346 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜(⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = ((absβ€˜β¦‹(𝐽 + 1) / π‘›β¦Œπ΄) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
230 eluzelre 12781 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑖 ∈ ℝ)
231230adantl 483 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ ℝ)
232 eluzle 12783 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑀 ≀ 𝑖)
233232adantl 483 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑀 ≀ 𝑖)
23431nnred 12175 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝑀 ∈ ℝ)
235234adantr 482 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑀 ∈ ℝ)
236 elicopnf 13369 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℝ β†’ (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀 ≀ 𝑖)))
237235, 236syl 17 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝑖 ∈ (𝑀[,)+∞) ↔ (𝑖 ∈ ℝ ∧ 𝑀 ≀ 𝑖)))
238231, 233, 237mpbir2and 712 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ (𝑀[,)+∞))
239238ex 414 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑖 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑖 ∈ (𝑀[,)+∞)))
240239ssrdv 3955 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (β„€β‰₯β€˜π‘€) βŠ† (𝑀[,)+∞))
24131nnzd 12533 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑀 ∈ β„€)
24248peano2zd 12617 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐼 + 1) ∈ β„€)
243101rpred 12964 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ π‘ˆ ∈ ℝ)
2444nnred 12175 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐼 + 1) ∈ ℝ)
245 dchrisumlem2.2 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑀 ≀ π‘ˆ)
246 dchrisumlem2.3 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ π‘ˆ ≀ (𝐼 + 1))
247234, 243, 244, 245, 246letrd 11319 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑀 ≀ (𝐼 + 1))
248 eluz2 12776 . . . . . . . . . . . . . . . . 17 ((𝐼 + 1) ∈ (β„€β‰₯β€˜π‘€) ↔ (𝑀 ∈ β„€ ∧ (𝐼 + 1) ∈ β„€ ∧ 𝑀 ≀ (𝐼 + 1)))
249241, 242, 247, 248syl3anbrc 1344 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐼 + 1) ∈ (β„€β‰₯β€˜π‘€))
250 uztrn 12788 . . . . . . . . . . . . . . . 16 (((𝐽 + 1) ∈ (β„€β‰₯β€˜(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝐽 + 1) ∈ (β„€β‰₯β€˜π‘€))
2519, 249, 250syl2anc 585 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐽 + 1) ∈ (β„€β‰₯β€˜π‘€))
252240, 251sseldd 3950 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐽 + 1) ∈ (𝑀[,)+∞))
253113simprd 497 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝐽 + 1) ∈ (𝑀[,)+∞) β†’ 0 ≀ ⦋(𝐽 + 1) / π‘›β¦Œπ΄))
254252, 253mpd 15 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 ≀ ⦋(𝐽 + 1) / π‘›β¦Œπ΄)
255115, 254absidd 15314 . . . . . . . . . . . 12 (πœ‘ β†’ (absβ€˜β¦‹(𝐽 + 1) / π‘›β¦Œπ΄) = ⦋(𝐽 + 1) / π‘›β¦Œπ΄)
256255oveq1d 7377 . . . . . . . . . . 11 (πœ‘ β†’ ((absβ€˜β¦‹(𝐽 + 1) / π‘›β¦Œπ΄) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = (⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
257229, 256eqtrd 2777 . . . . . . . . . 10 (πœ‘ β†’ (absβ€˜(⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = (⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
258124abscld 15328 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ∈ ℝ)
259111nnnn0d 12480 . . . . . . . . . . . 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 26853 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝐽 + 1) ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
262259, 261mpdan 686 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
263258, 93, 115, 254, 262lemul2ad 12102 . . . . . . . . . 10 (πœ‘ β†’ (⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ (⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· 𝑅))
264257, 263eqbrtrd 5132 . . . . . . . . 9 (πœ‘ β†’ (absβ€˜(⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ (⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· 𝑅))
265126, 131absmuld 15346 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜(⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = ((absβ€˜β¦‹(𝐼 + 1) / π‘›β¦Œπ΄) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
266240, 249sseldd 3950 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐼 + 1) ∈ (𝑀[,)+∞))
26719, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35dchrisumlema 26852 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (((𝐼 + 1) ∈ ℝ+ β†’ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ∈ ℝ) ∧ ((𝐼 + 1) ∈ (𝑀[,)+∞) β†’ 0 ≀ ⦋(𝐼 + 1) / π‘›β¦Œπ΄)))
268267simprd 497 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝐼 + 1) ∈ (𝑀[,)+∞) β†’ 0 ≀ ⦋(𝐼 + 1) / π‘›β¦Œπ΄))
269266, 268mpd 15 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 ≀ ⦋(𝐼 + 1) / π‘›β¦Œπ΄)
27099, 269absidd 15314 . . . . . . . . . . . 12 (πœ‘ β†’ (absβ€˜β¦‹(𝐼 + 1) / π‘›β¦Œπ΄) = ⦋(𝐼 + 1) / π‘›β¦Œπ΄)
271270oveq1d 7377 . . . . . . . . . . 11 (πœ‘ β†’ ((absβ€˜β¦‹(𝐼 + 1) / π‘›β¦Œπ΄) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
272265, 271eqtrd 2777 . . . . . . . . . 10 (πœ‘ β†’ (absβ€˜(⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
273131abscld 15328 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ∈ ℝ)
2744nnnn0d 12480 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐼 + 1) ∈ β„•0)
27519, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35, 93, 260dchrisumlem1 26853 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝐼 + 1) ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
276274, 275mpdan 686 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
277273, 93, 99, 269, 276lemul2ad 12102 . . . . . . . . . 10 (πœ‘ β†’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· 𝑅))
278272, 277eqbrtrd 5132 . . . . . . . . 9 (πœ‘ β†’ (absβ€˜(⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· 𝑅))
279223, 224, 227, 228, 264, 278le2addd 11781 . . . . . . . 8 (πœ‘ β†’ ((absβ€˜(⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) + (absβ€˜(⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ≀ ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· 𝑅) + (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· 𝑅)))
28093recnd 11190 . . . . . . . . 9 (πœ‘ β†’ 𝑅 ∈ β„‚)
281116, 126, 280adddird 11187 . . . . . . . 8 (πœ‘ β†’ ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅) = ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· 𝑅) + (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· 𝑅)))
282279, 281breqtrrd 5138 . . . . . . 7 (πœ‘ β†’ ((absβ€˜(⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) + (absβ€˜(⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ≀ ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
283134, 225, 215, 226, 282letrd 11319 . . . . . 6 (πœ‘ β†’ (absβ€˜((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ≀ ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
284154abscld 15328 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (absβ€˜((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ∈ ℝ)
28581, 284fsumrecl 15626 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(absβ€˜((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ∈ ℝ)
28681, 154fsumabs 15693 . . . . . . 7 (πœ‘ β†’ (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(absβ€˜((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
28793adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ 𝑅 ∈ ℝ)
288219, 287remulcld 11192 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· 𝑅) ∈ ℝ)
289135, 146syldan 592 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
290151adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)) ∈ β„‚)
291289, 290absmuld 15346 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (absβ€˜((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = ((absβ€˜(⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄)) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
292 elfzouz 13583 . . . . . . . . . . . . . . 15 (𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1)) β†’ 𝑖 ∈ (β„€β‰₯β€˜(𝐼 + 1)))
293 uztrn 12788 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (β„€β‰₯β€˜(𝐼 + 1)) ∧ (𝐼 + 1) ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ (β„€β‰₯β€˜π‘€))
294292, 249, 293syl2anr 598 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ 𝑖 ∈ (β„€β‰₯β€˜π‘€))
295 eluznn 12850 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ β„• ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ β„•)
29631, 295sylan 581 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ β„•)
297296, 137syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝑖 + 1) ∈ ℝ+)
298296nnrpd 12962 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ∈ ℝ+)
299333expia 1122 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑛 ∈ ℝ+ ∧ π‘₯ ∈ ℝ+)) β†’ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴))
300299ralrimivva 3198 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ βˆ€π‘› ∈ ℝ+ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴))
301300adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ βˆ€π‘› ∈ ℝ+ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴))
302 nfcv 2908 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑛ℝ+
303 nfv 1918 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑛(𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯)
304 nfcv 2908 . . . . . . . . . . . . . . . . . . . 20 Ⅎ𝑛𝐡
305 nfcv 2908 . . . . . . . . . . . . . . . . . . . 20 Ⅎ𝑛 ≀
306304, 305, 59nfbr 5157 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑛 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄
307303, 306nfim 1900 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑛((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄)
308302, 307nfralw 3297 . . . . . . . . . . . . . . . . 17 β„²π‘›βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄)
309 breq2 5114 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑖 β†’ (𝑀 ≀ 𝑛 ↔ 𝑀 ≀ 𝑖))
310 breq1 5113 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑖 β†’ (𝑛 ≀ π‘₯ ↔ 𝑖 ≀ π‘₯))
311309, 310anbi12d 632 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑖 β†’ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) ↔ (𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯)))
31262breq2d 5122 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑖 β†’ (𝐡 ≀ 𝐴 ↔ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄))
313311, 312imbi12d 345 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑖 β†’ (((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴) ↔ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄)))
314313ralbidv 3175 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 β†’ (βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴) ↔ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄)))
315308, 314rspc 3572 . . . . . . . . . . . . . . . 16 (𝑖 ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴) β†’ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄)))
316298, 301, 315sylc 65 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄))
317231lep1d 12093 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ 𝑖 ≀ (𝑖 + 1))
318233, 317jca 513 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ (𝑀 ≀ 𝑖 ∧ 𝑖 ≀ (𝑖 + 1)))
319 breq2 5114 . . . . . . . . . . . . . . . . . 18 (π‘₯ = (𝑖 + 1) β†’ (𝑖 ≀ π‘₯ ↔ 𝑖 ≀ (𝑖 + 1)))
320319anbi2d 630 . . . . . . . . . . . . . . . . 17 (π‘₯ = (𝑖 + 1) β†’ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) ↔ (𝑀 ≀ 𝑖 ∧ 𝑖 ≀ (𝑖 + 1))))
321 eqvisset 3465 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = (𝑖 + 1) β†’ (𝑖 + 1) ∈ V)
322 eqtr3 2763 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) β†’ π‘₯ = 𝑛)
32330equcoms 2024 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑛 β†’ 𝐴 = 𝐡)
324322, 323syl 17 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ = (𝑖 + 1) ∧ 𝑛 = (𝑖 + 1)) β†’ 𝐴 = 𝐡)
325321, 324csbied 3898 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = (𝑖 + 1) β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ = 𝐡)
326325eqcomd 2743 . . . . . . . . . . . . . . . . . 18 (π‘₯ = (𝑖 + 1) β†’ 𝐡 = ⦋(𝑖 + 1) / π‘›β¦Œπ΄)
327326breq1d 5120 . . . . . . . . . . . . . . . . 17 (π‘₯ = (𝑖 + 1) β†’ (𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄ ↔ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ≀ ⦋𝑖 / π‘›β¦Œπ΄))
328320, 327imbi12d 345 . . . . . . . . . . . . . . . 16 (π‘₯ = (𝑖 + 1) β†’ (((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄) ↔ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ (𝑖 + 1)) β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ≀ ⦋𝑖 / π‘›β¦Œπ΄)))
329328rspcv 3580 . . . . . . . . . . . . . . 15 ((𝑖 + 1) ∈ ℝ+ β†’ (βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ π‘₯) β†’ 𝐡 ≀ ⦋𝑖 / π‘›β¦Œπ΄) β†’ ((𝑀 ≀ 𝑖 ∧ 𝑖 ≀ (𝑖 + 1)) β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ≀ ⦋𝑖 / π‘›β¦Œπ΄)))
330297, 316, 318, 329syl3c 66 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (β„€β‰₯β€˜π‘€)) β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ≀ ⦋𝑖 / π‘›β¦Œπ΄)
331294, 330syldan 592 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ≀ ⦋𝑖 / π‘›β¦Œπ΄)
332218, 217, 331abssuble0d 15324 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (absβ€˜(⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄)) = (⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄))
333332oveq1d 7377 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ((absβ€˜(⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄)) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = ((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
334291, 333eqtrd 2777 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (absβ€˜((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) = ((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))))
335290abscld 15328 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ∈ ℝ)
336217, 218subge0d 11752 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (0 ≀ (⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) ↔ ⦋(𝑖 + 1) / π‘›β¦Œπ΄ ≀ ⦋𝑖 / π‘›β¦Œπ΄))
337331, 336mpbird 257 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ 0 ≀ (⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄))
338135peano2nnd 12177 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (𝑖 + 1) ∈ β„•)
339338nnnn0d 12480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (𝑖 + 1) ∈ β„•0)
34019, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35, 93, 260dchrisumlem1 26853 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑖 + 1) ∈ β„•0) β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
341339, 340syldan 592 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (absβ€˜Ξ£π‘› ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
342335, 287, 219, 337, 341lemul2ad 12102 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ ((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· (absβ€˜Ξ£π‘› ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ ((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
343334, 342eqbrtrd 5132 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (absβ€˜((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ ((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
34481, 284, 288, 343fsumle 15691 . . . . . . . 8 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(absβ€˜((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
345219recnd 11190 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))) β†’ (⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) ∈ β„‚)
34681, 280, 345fsummulc1 15677 . . . . . . . . 9 (πœ‘ β†’ (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· 𝑅) = Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
347216oveq1d 7377 . . . . . . . . 9 (πœ‘ β†’ (Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· 𝑅) = ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
348346, 347eqtr3d 2779 . . . . . . . 8 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋𝑖 / π‘›β¦Œπ΄ βˆ’ ⦋(𝑖 + 1) / π‘›β¦Œπ΄) Β· 𝑅) = ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
349344, 348breqtrd 5136 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ ((𝐼 + 1)..^(𝐽 + 1))(absβ€˜((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
350156, 285, 222, 286, 349letrd 11319 . . . . . 6 (πœ‘ β†’ (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›)))) ≀ ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) Β· 𝑅))
351134, 156, 215, 222, 283, 350le2addd 11781 . . . . 5 (πœ‘ β†’ ((absβ€˜((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) + (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ≀ (((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅) + ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) Β· 𝑅)))
3521262timesd 12403 . . . . . . . 8 (πœ‘ β†’ (2 Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄) = (⦋(𝐼 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄))
353126, 116, 126ppncand 11559 . . . . . . . 8 (πœ‘ β†’ ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ + ⦋(𝐽 + 1) / π‘›β¦Œπ΄) + (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄)) = (⦋(𝐼 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄))
354126, 116addcomd 11364 . . . . . . . . 9 (πœ‘ β†’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ + ⦋(𝐽 + 1) / π‘›β¦Œπ΄) = (⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄))
355354oveq1d 7377 . . . . . . . 8 (πœ‘ β†’ ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ + ⦋(𝐽 + 1) / π‘›β¦Œπ΄) + (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄)) = ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) + (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄)))
356352, 353, 3553eqtr2d 2783 . . . . . . 7 (πœ‘ β†’ (2 Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄) = ((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) + (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄)))
357356oveq1d 7377 . . . . . 6 (πœ‘ β†’ ((2 Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅) = (((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) + (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄)) Β· 𝑅))
358 2cnd 12238 . . . . . . 7 (πœ‘ β†’ 2 ∈ β„‚)
359358, 126, 280mul32d 11372 . . . . . 6 (πœ‘ β†’ ((2 Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅) = ((2 Β· 𝑅) Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄))
360214recnd 11190 . . . . . . 7 (πœ‘ β†’ (⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) ∈ β„‚)
361221recnd 11190 . . . . . . 7 (πœ‘ β†’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) ∈ β„‚)
362360, 361, 280adddird 11187 . . . . . 6 (πœ‘ β†’ (((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) + (⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄)) Β· 𝑅) = (((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅) + ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) Β· 𝑅)))
363357, 359, 3623eqtr3d 2785 . . . . 5 (πœ‘ β†’ ((2 Β· 𝑅) Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄) = (((⦋(𝐽 + 1) / π‘›β¦Œπ΄ + ⦋(𝐼 + 1) / π‘›β¦Œπ΄) Β· 𝑅) + ((⦋(𝐼 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋(𝐽 + 1) / π‘›β¦Œπ΄) Β· 𝑅)))
364351, 363breqtrrd 5138 . . . 4 (πœ‘ β†’ ((absβ€˜((⦋(𝐽 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))) βˆ’ (⦋(𝐼 + 1) / π‘›β¦Œπ΄ Β· Σ𝑛 ∈ (0..^(𝐼 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) + (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((⦋(𝑖 + 1) / π‘›β¦Œπ΄ βˆ’ ⦋𝑖 / π‘›β¦Œπ΄) Β· Σ𝑛 ∈ (0..^(𝑖 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))) ≀ ((2 Β· 𝑅) Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄))
36590, 157, 100, 213, 364letrd 11319 . . 3 (πœ‘ β†’ (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) ≀ ((2 Β· 𝑅) Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄))
366 2nn0 12437 . . . . . 6 2 ∈ β„•0
367 nn0ge0 12445 . . . . . 6 (2 ∈ β„•0 β†’ 0 ≀ 2)
368366, 367mp1i 13 . . . . 5 (πœ‘ β†’ 0 ≀ 2)
369 0red 11165 . . . . . 6 (πœ‘ β†’ 0 ∈ ℝ)
370124absge0d 15336 . . . . . 6 (πœ‘ β†’ 0 ≀ (absβ€˜Ξ£π‘› ∈ (0..^(𝐽 + 1))(π‘‹β€˜(πΏβ€˜π‘›))))
371369, 258, 93, 370, 262letrd 11319 . . . . 5 (πœ‘ β†’ 0 ≀ 𝑅)
37292, 93, 368, 371mulge0d 11739 . . . 4 (πœ‘ β†’ 0 ≀ (2 Β· 𝑅))
3734nnrpd 12962 . . . . 5 (πœ‘ β†’ (𝐼 + 1) ∈ ℝ+)
374 nfv 1918 . . . . . . . . 9 Ⅎ𝑛(𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯)
375304, 305, 103nfbr 5157 . . . . . . . . 9 Ⅎ𝑛 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄
376374, 375nfim 1900 . . . . . . . 8 Ⅎ𝑛((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) β†’ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄)
377302, 376nfralw 3297 . . . . . . 7 β„²π‘›βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) β†’ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄)
378 breq2 5114 . . . . . . . . . 10 (𝑛 = π‘ˆ β†’ (𝑀 ≀ 𝑛 ↔ 𝑀 ≀ π‘ˆ))
379 breq1 5113 . . . . . . . . . 10 (𝑛 = π‘ˆ β†’ (𝑛 ≀ π‘₯ ↔ π‘ˆ ≀ π‘₯))
380378, 379anbi12d 632 . . . . . . . . 9 (𝑛 = π‘ˆ β†’ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) ↔ (𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯)))
381105breq2d 5122 . . . . . . . . 9 (𝑛 = π‘ˆ β†’ (𝐡 ≀ 𝐴 ↔ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄))
382380, 381imbi12d 345 . . . . . . . 8 (𝑛 = π‘ˆ β†’ (((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴) ↔ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) β†’ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄)))
383382ralbidv 3175 . . . . . . 7 (𝑛 = π‘ˆ β†’ (βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴) ↔ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) β†’ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄)))
384377, 383rspc 3572 . . . . . 6 (π‘ˆ ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯) β†’ 𝐡 ≀ 𝐴) β†’ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) β†’ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄)))
385101, 300, 384sylc 65 . . . . 5 (πœ‘ β†’ βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) β†’ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄))
386245, 246jca 513 . . . . 5 (πœ‘ β†’ (𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ (𝐼 + 1)))
387 breq2 5114 . . . . . . . 8 (π‘₯ = (𝐼 + 1) β†’ (π‘ˆ ≀ π‘₯ ↔ π‘ˆ ≀ (𝐼 + 1)))
388387anbi2d 630 . . . . . . 7 (π‘₯ = (𝐼 + 1) β†’ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) ↔ (𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ (𝐼 + 1))))
389 eqvisset 3465 . . . . . . . . . 10 (π‘₯ = (𝐼 + 1) β†’ (𝐼 + 1) ∈ V)
390 eqtr3 2763 . . . . . . . . . . 11 ((π‘₯ = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) β†’ π‘₯ = 𝑛)
391390, 323syl 17 . . . . . . . . . 10 ((π‘₯ = (𝐼 + 1) ∧ 𝑛 = (𝐼 + 1)) β†’ 𝐴 = 𝐡)
392389, 391csbied 3898 . . . . . . . . 9 (π‘₯ = (𝐼 + 1) β†’ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ = 𝐡)
393392eqcomd 2743 . . . . . . . 8 (π‘₯ = (𝐼 + 1) β†’ 𝐡 = ⦋(𝐼 + 1) / π‘›β¦Œπ΄)
394393breq1d 5120 . . . . . . 7 (π‘₯ = (𝐼 + 1) β†’ (𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄ ↔ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄))
395388, 394imbi12d 345 . . . . . 6 (π‘₯ = (𝐼 + 1) β†’ (((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) β†’ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄) ↔ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ (𝐼 + 1)) β†’ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄)))
396395rspcv 3580 . . . . 5 ((𝐼 + 1) ∈ ℝ+ β†’ (βˆ€π‘₯ ∈ ℝ+ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ π‘₯) β†’ 𝐡 ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄) β†’ ((𝑀 ≀ π‘ˆ ∧ π‘ˆ ≀ (𝐼 + 1)) β†’ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄)))
397373, 385, 386, 396syl3c 66 . . . 4 (πœ‘ β†’ ⦋(𝐼 + 1) / π‘›β¦Œπ΄ ≀ β¦‹π‘ˆ / π‘›β¦Œπ΄)
39899, 108, 94, 372, 397lemul2ad 12102 . . 3 (πœ‘ β†’ ((2 Β· 𝑅) Β· ⦋(𝐼 + 1) / π‘›β¦Œπ΄) ≀ ((2 Β· 𝑅) Β· β¦‹π‘ˆ / π‘›β¦Œπ΄))
39990, 100, 109, 365, 398letrd 11319 . 2 (πœ‘ β†’ (absβ€˜Ξ£π‘– ∈ ((𝐼 + 1)..^(𝐽 + 1))((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)) ≀ ((2 Β· 𝑅) Β· β¦‹π‘ˆ / π‘›β¦Œπ΄))
40089, 399eqbrtrd 5132 1 (πœ‘ β†’ (absβ€˜((seq1( + , 𝐹)β€˜π½) βˆ’ (seq1( + , 𝐹)β€˜πΌ))) ≀ ((2 Β· 𝑅) Β· β¦‹π‘ˆ / π‘›β¦Œπ΄))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  Vcvv 3448  β¦‹csb 3860   βˆͺ cun 3913   ∩ cin 3914  βˆ…c0 4287   class class class wbr 5110   ↦ cmpt 5193  β€˜cfv 6501  (class class class)co 7362  Fincfn 8890  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063  +∞cpnf 11193   ≀ cle 11197   βˆ’ cmin 11392  β„•cn 12160  2c2 12215  β„•0cn0 12420  β„€cz 12506  β„€β‰₯cuz 12770  β„+crp 12922  [,)cico 13273  ...cfz 13431  ..^cfzo 13574  seqcseq 13913  abscabs 15126   β‡π‘Ÿ crli 15374  Ξ£csu 15577  Basecbs 17090  0gc0g 17328  β„€RHomczrh 20916  β„€/nβ„€czn 20919  DChrcdchr 26596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136  ax-addf 11137  ax-mulf 11138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-tpos 8162  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-oadd 8421  df-er 8655  df-ec 8657  df-qs 8661  df-map 8774  df-pm 8775  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-inf 9386  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-xnn0 12493  df-z 12507  df-dec 12626  df-uz 12771  df-rp 12923  df-ico 13277  df-fz 13432  df-fzo 13575  df-fl 13704  df-mod 13782  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-clim 15377  df-rlim 15378  df-sum 15578  df-dvds 16144  df-gcd 16382  df-phi 16645  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-0g 17330  df-imas 17397  df-qus 17398  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-mhm 18608  df-grp 18758  df-minusg 18759  df-sbg 18760  df-mulg 18880  df-subg 18932  df-nsg 18933  df-eqg 18934  df-ghm 19013  df-cmn 19571  df-abl 19572  df-mgp 19904  df-ur 19921  df-ring 19973  df-cring 19974  df-oppr 20056  df-dvdsr 20077  df-unit 20078  df-invr 20108  df-rnghom 20155  df-subrg 20236  df-lmod 20340  df-lss 20409  df-lsp 20449  df-sra 20649  df-rgmod 20650  df-lidl 20651  df-rsp 20652  df-2idl 20718  df-cnfld 20813  df-zring 20886  df-zrh 20920  df-zn 20923  df-dchr 26597
This theorem is referenced by:  dchrisumlem3  26855
  Copyright terms: Public domain W3C validator