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

Theorem dchrisumlem3 26855
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..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
Assertion
Ref Expression
dchrisumlem3 (πœ‘ β†’ βˆƒπ‘‘βˆƒπ‘ ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑑 ∧ βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡)))
Distinct variable groups:   𝑒,𝑛,π‘₯,𝑐,𝑑   1 ,𝑐   𝑑,𝑛, 1 ,π‘₯   𝑒,𝑐,𝐹,𝑛,𝑑,π‘₯   𝐴,𝑐,𝑑,π‘₯   𝑁,𝑐,𝑛,𝑑,𝑒,π‘₯   πœ‘,𝑐,𝑛,𝑑,𝑒,π‘₯   𝑅,𝑐,𝑛,𝑒,π‘₯   𝐡,𝑐,𝑛   𝑛,𝑍,π‘₯   𝐷,𝑐,𝑛,𝑑,π‘₯   𝐿,𝑐,𝑛,𝑑,𝑒,π‘₯   𝑀,𝑐,𝑛,𝑒,π‘₯   𝑋,𝑐,𝑛,𝑑,𝑒,π‘₯
Allowed substitution hints:   𝐴(𝑒,𝑛)   𝐡(π‘₯,𝑒,𝑑)   𝐷(𝑒)   𝑅(𝑑)   1 (𝑒)   𝐺(π‘₯,𝑒,𝑑,𝑛,𝑐)   𝑀(𝑑)   𝑍(𝑒,𝑑,𝑐)

Proof of Theorem dchrisumlem3
Dummy variables π‘˜ π‘š 𝑖 𝑗 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 12813 . . . 4 β„• = (β„€β‰₯β€˜1)
2 1zzd 12541 . . . . . 6 (πœ‘ β†’ 1 ∈ β„€)
3 simpr 486 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ 𝑖 ∈ β„•)
4 rpvmasum.g . . . . . . . . . 10 𝐺 = (DChrβ€˜π‘)
5 rpvmasum.z . . . . . . . . . 10 𝑍 = (β„€/nβ„€β€˜π‘)
6 rpvmasum.d . . . . . . . . . 10 𝐷 = (Baseβ€˜πΊ)
7 rpvmasum.l . . . . . . . . . 10 𝐿 = (β„€RHomβ€˜π‘)
8 dchrisum.b . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 ∈ 𝐷)
98adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ 𝑋 ∈ 𝐷)
103nnzd 12533 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ 𝑖 ∈ β„€)
114, 5, 6, 7, 9, 10dchrzrhcl 26609 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (π‘‹β€˜(πΏβ€˜π‘–)) ∈ β„‚)
12 dchrisum.4 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ ℝ+) β†’ 𝐴 ∈ ℝ)
1312ralrimiva 3144 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ)
14 nnrp 12933 . . . . . . . . . . 11 (𝑖 ∈ β„• β†’ 𝑖 ∈ ℝ+)
15 nfcsb1v 3885 . . . . . . . . . . . . . 14 Ⅎ𝑛⦋𝑖 / π‘›β¦Œπ΄
1615nfel1 2924 . . . . . . . . . . . . 13 Ⅎ𝑛⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ
17 csbeq1a 3874 . . . . . . . . . . . . . 14 (𝑛 = 𝑖 β†’ 𝐴 = ⦋𝑖 / π‘›β¦Œπ΄)
1817eleq1d 2823 . . . . . . . . . . . . 13 (𝑛 = 𝑖 β†’ (𝐴 ∈ ℝ ↔ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ))
1916, 18rspc 3572 . . . . . . . . . . . 12 (𝑖 ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ))
2019impcom 409 . . . . . . . . . . 11 ((βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ ∧ 𝑖 ∈ ℝ+) β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ)
2113, 14, 20syl2an 597 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ)
2221recnd 11190 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ β„‚)
2311, 22mulcld 11182 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
24 nfcv 2908 . . . . . . . . 9 Ⅎ𝑛𝑖
25 nfcv 2908 . . . . . . . . . 10 Ⅎ𝑛(π‘‹β€˜(πΏβ€˜π‘–))
26 nfcv 2908 . . . . . . . . . 10 Ⅎ𝑛 Β·
2725, 26, 15nfov 7392 . . . . . . . . 9 Ⅎ𝑛((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)
28 2fveq3 6852 . . . . . . . . . 10 (𝑛 = 𝑖 β†’ (π‘‹β€˜(πΏβ€˜π‘›)) = (π‘‹β€˜(πΏβ€˜π‘–)))
2928, 17oveq12d 7380 . . . . . . . . 9 (𝑛 = 𝑖 β†’ ((π‘‹β€˜(πΏβ€˜π‘›)) Β· 𝐴) = ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
30 dchrisum.7 . . . . . . . . 9 𝐹 = (𝑛 ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘›)) Β· 𝐴))
3124, 27, 29, 30fvmptf 6974 . . . . . . . 8 ((𝑖 ∈ β„• ∧ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚) β†’ (πΉβ€˜π‘–) = ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
323, 23, 31syl2anc 585 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (πΉβ€˜π‘–) = ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
3332, 23eqeltrd 2838 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (πΉβ€˜π‘–) ∈ β„‚)
341, 2, 33serf 13943 . . . . 5 (πœ‘ β†’ seq1( + , 𝐹):β„•βŸΆβ„‚)
3534ffvelcdmda 7040 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐹)β€˜π‘˜) ∈ β„‚)
3612recnd 11190 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ ℝ+) β†’ 𝐴 ∈ β„‚)
3736ralrimiva 3144 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘› ∈ ℝ+ 𝐴 ∈ β„‚)
3837adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ℝ+) β†’ βˆ€π‘› ∈ ℝ+ 𝐴 ∈ β„‚)
39 id 22 . . . . . . . 8 (𝑒 ∈ ℝ+ β†’ 𝑒 ∈ ℝ+)
40 2re 12234 . . . . . . . . . 10 2 ∈ ℝ
41 dchrisum.9 . . . . . . . . . 10 (πœ‘ β†’ 𝑅 ∈ ℝ)
42 remulcl 11143 . . . . . . . . . 10 ((2 ∈ ℝ ∧ 𝑅 ∈ ℝ) β†’ (2 Β· 𝑅) ∈ ℝ)
4340, 41, 42sylancr 588 . . . . . . . . 9 (πœ‘ β†’ (2 Β· 𝑅) ∈ ℝ)
44 rpvmasum.a . . . . . . . . . . . 12 (πœ‘ β†’ 𝑁 ∈ β„•)
45 lbfzo0 13619 . . . . . . . . . . . 12 (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ β„•)
4644, 45sylibr 233 . . . . . . . . . . 11 (πœ‘ β†’ 0 ∈ (0..^𝑁))
47 dchrisum.10 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘’ ∈ (0..^𝑁)(absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
48 oveq2 7370 . . . . . . . . . . . . . . . . 17 (𝑒 = 0 β†’ (0..^𝑒) = (0..^0))
49 fzo0 13603 . . . . . . . . . . . . . . . . 17 (0..^0) = βˆ…
5048, 49eqtrdi 2793 . . . . . . . . . . . . . . . 16 (𝑒 = 0 β†’ (0..^𝑒) = βˆ…)
5150sumeq1d 15593 . . . . . . . . . . . . . . 15 (𝑒 = 0 β†’ Σ𝑛 ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ βˆ… (π‘‹β€˜(πΏβ€˜π‘›)))
52 sum0 15613 . . . . . . . . . . . . . . 15 Σ𝑛 ∈ βˆ… (π‘‹β€˜(πΏβ€˜π‘›)) = 0
5351, 52eqtrdi 2793 . . . . . . . . . . . . . 14 (𝑒 = 0 β†’ Σ𝑛 ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
5453abs00bd 15183 . . . . . . . . . . . . 13 (𝑒 = 0 β†’ (absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) = 0)
5554breq1d 5120 . . . . . . . . . . . 12 (𝑒 = 0 β†’ ((absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅 ↔ 0 ≀ 𝑅))
5655rspcv 3580 . . . . . . . . . . 11 (0 ∈ (0..^𝑁) β†’ (βˆ€π‘’ ∈ (0..^𝑁)(absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅 β†’ 0 ≀ 𝑅))
5746, 47, 56sylc 65 . . . . . . . . . 10 (πœ‘ β†’ 0 ≀ 𝑅)
58 0le2 12262 . . . . . . . . . . 11 0 ≀ 2
59 mulge0 11680 . . . . . . . . . . 11 (((2 ∈ ℝ ∧ 0 ≀ 2) ∧ (𝑅 ∈ ℝ ∧ 0 ≀ 𝑅)) β†’ 0 ≀ (2 Β· 𝑅))
6040, 58, 59mpanl12 701 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≀ 𝑅) β†’ 0 ≀ (2 Β· 𝑅))
6141, 57, 60syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ (2 Β· 𝑅))
6243, 61ge0p1rpd 12994 . . . . . . . 8 (πœ‘ β†’ ((2 Β· 𝑅) + 1) ∈ ℝ+)
63 rpdivcl 12947 . . . . . . . 8 ((𝑒 ∈ ℝ+ ∧ ((2 Β· 𝑅) + 1) ∈ ℝ+) β†’ (𝑒 / ((2 Β· 𝑅) + 1)) ∈ ℝ+)
6439, 62, 63syl2anr 598 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ℝ+) β†’ (𝑒 / ((2 Β· 𝑅) + 1)) ∈ ℝ+)
65 dchrisum.6 . . . . . . . 8 (πœ‘ β†’ (𝑛 ∈ ℝ+ ↦ 𝐴) β‡π‘Ÿ 0)
6665adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ℝ+) β†’ (𝑛 ∈ ℝ+ ↦ 𝐴) β‡π‘Ÿ 0)
6738, 64, 66rlimi 15402 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ ℝ+) β†’ βˆƒπ‘š ∈ ℝ βˆ€π‘› ∈ ℝ+ (π‘š ≀ 𝑛 β†’ (absβ€˜(𝐴 βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))))
68 simpr 486 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ π‘š ∈ ℝ)
69 dchrisum.3 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑀 ∈ β„•)
7069nnred 12175 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑀 ∈ ℝ)
7170adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 𝑀 ∈ ℝ)
7268, 71ifcld 4537 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ)
73 0red 11165 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 0 ∈ ℝ)
7469nngt0d 12209 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 < 𝑀)
7574adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 0 < 𝑀)
76 max1 13111 . . . . . . . . . . . . 13 ((𝑀 ∈ ℝ ∧ π‘š ∈ ℝ) β†’ 𝑀 ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))
7770, 76sylan 581 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 𝑀 ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))
7873, 71, 72, 75, 77ltletrd 11322 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 0 < if(𝑀 ≀ π‘š, π‘š, 𝑀))
7972, 78elrpd 12961 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ+)
8079adantlr 714 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ+)
81 nfv 1918 . . . . . . . . . . 11 Ⅎ𝑛 π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀)
82 nfcv 2908 . . . . . . . . . . . . 13 Ⅎ𝑛abs
83 nfcsb1v 3885 . . . . . . . . . . . . . 14 Ⅎ𝑛⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄
84 nfcv 2908 . . . . . . . . . . . . . 14 Ⅎ𝑛 βˆ’
85 nfcv 2908 . . . . . . . . . . . . . 14 Ⅎ𝑛0
8683, 84, 85nfov 7392 . . . . . . . . . . . . 13 Ⅎ𝑛(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)
8782, 86nffv 6857 . . . . . . . . . . . 12 Ⅎ𝑛(absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0))
88 nfcv 2908 . . . . . . . . . . . 12 Ⅎ𝑛 <
89 nfcv 2908 . . . . . . . . . . . 12 Ⅎ𝑛(𝑒 / ((2 Β· 𝑅) + 1))
9087, 88, 89nfbr 5157 . . . . . . . . . . 11 Ⅎ𝑛(absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))
9181, 90nfim 1900 . . . . . . . . . 10 Ⅎ𝑛(π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)))
92 breq2 5114 . . . . . . . . . . 11 (𝑛 = if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ (π‘š ≀ 𝑛 ↔ π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀)))
93 csbeq1a 3874 . . . . . . . . . . . . 13 (𝑛 = if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ 𝐴 = ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄)
9493fvoveq1d 7384 . . . . . . . . . . . 12 (𝑛 = if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ (absβ€˜(𝐴 βˆ’ 0)) = (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)))
9594breq1d 5120 . . . . . . . . . . 11 (𝑛 = if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ ((absβ€˜(𝐴 βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)) ↔ (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))))
9692, 95imbi12d 345 . . . . . . . . . 10 (𝑛 = if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ ((π‘š ≀ 𝑛 β†’ (absβ€˜(𝐴 βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))) ↔ (π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)))))
9791, 96rspc 3572 . . . . . . . . 9 (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ (π‘š ≀ 𝑛 β†’ (absβ€˜(𝐴 βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))) β†’ (π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)))))
9880, 97syl 17 . . . . . . . 8 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (βˆ€π‘› ∈ ℝ+ (π‘š ≀ 𝑛 β†’ (absβ€˜(𝐴 βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))) β†’ (π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)))))
9970ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ 𝑀 ∈ ℝ)
100 max2 13113 . . . . . . . . . 10 ((𝑀 ∈ ℝ ∧ π‘š ∈ ℝ) β†’ π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))
10199, 100sylancom 589 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))
10213ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ)
10383nfel1 2924 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑛⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ ∈ ℝ
10493eleq1d 2823 . . . . . . . . . . . . . . . . . . 19 (𝑛 = if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ (𝐴 ∈ ℝ ↔ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ ∈ ℝ))
105103, 104rspc 3572 . . . . . . . . . . . . . . . . . 18 (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ β†’ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ ∈ ℝ))
10680, 102, 105sylc 65 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ ∈ ℝ)
107106recnd 11190 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ ∈ β„‚)
108107subid1d 11508 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0) = ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄)
109108fveq2d 6851 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) = (absβ€˜β¦‹if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄))
11072adantlr 714 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ)
11199, 76sylancom 589 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ 𝑀 ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))
112 elicopnf 13369 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ℝ β†’ (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ (𝑀[,)+∞) ↔ (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ ∧ 𝑀 ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))))
11399, 112syl 17 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ (𝑀[,)+∞) ↔ (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ ∧ 𝑀 ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))))
114110, 111, 113mpbir2and 712 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ (𝑀[,)+∞))
11544ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ 𝑁 ∈ β„•)
116 rpvmasum.1 . . . . . . . . . . . . . . . . . 18 1 = (0gβ€˜πΊ)
1178ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ 𝑋 ∈ 𝐷)
118 dchrisum.n1 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋 β‰  1 )
119118ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ 𝑋 β‰  1 )
120 dchrisum.2 . . . . . . . . . . . . . . . . . 18 (𝑛 = π‘₯ β†’ 𝐴 = 𝐡)
12169ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ 𝑀 ∈ β„•)
12212ad4ant14 751 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ 𝑛 ∈ ℝ+) β†’ 𝐴 ∈ ℝ)
123 simpll 766 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ πœ‘)
124 dchrisum.5 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑛 ∈ ℝ+ ∧ π‘₯ ∈ ℝ+) ∧ (𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯)) β†’ 𝐡 ≀ 𝐴)
125123, 124syl3an1 1164 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ (𝑛 ∈ ℝ+ ∧ π‘₯ ∈ ℝ+) ∧ (𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯)) β†’ 𝐡 ≀ 𝐴)
12665ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (𝑛 ∈ ℝ+ ↦ 𝐴) β‡π‘Ÿ 0)
1275, 7, 115, 4, 6, 116, 117, 119, 120, 121, 122, 125, 126, 30dchrisumlema 26852 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ+ β†’ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ ∈ ℝ) ∧ (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ (𝑀[,)+∞) β†’ 0 ≀ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄)))
128127simprd 497 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ (𝑀[,)+∞) β†’ 0 ≀ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄))
129114, 128mpd 15 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ 0 ≀ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄)
130106, 129absidd 15314 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (absβ€˜β¦‹if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) = ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄)
131109, 130eqtrd 2777 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) = ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄)
132131breq1d 5120 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)) ↔ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ < (𝑒 / ((2 Β· 𝑅) + 1))))
133 rpre 12930 . . . . . . . . . . . . . 14 (𝑒 ∈ ℝ+ β†’ 𝑒 ∈ ℝ)
134133ad2antlr 726 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ 𝑒 ∈ ℝ)
13562ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((2 Β· 𝑅) + 1) ∈ ℝ+)
136106, 134, 135ltmuldiv2d 13012 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒 ↔ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ < (𝑒 / ((2 Β· 𝑅) + 1))))
137132, 136bitr4d 282 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)) ↔ (((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒))
13843ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (2 Β· 𝑅) ∈ ℝ)
139135rpred 12964 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((2 Β· 𝑅) + 1) ∈ ℝ)
140138lep1d 12093 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (2 Β· 𝑅) ≀ ((2 Β· 𝑅) + 1))
141138, 139, 106, 129, 140lemul1ad 12101 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ≀ (((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄))
142138, 106remulcld 11192 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∈ ℝ)
143139, 106remulcld 11192 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∈ ℝ)
144 lelttr 11252 . . . . . . . . . . . . 13 ((((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∈ ℝ ∧ (((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∈ ℝ ∧ 𝑒 ∈ ℝ) β†’ ((((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ≀ (((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∧ (((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒) β†’ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒))
145142, 143, 134, 144syl3anc 1372 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ≀ (((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∧ (((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒) β†’ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒))
146141, 145mpand 694 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒 β†’ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒))
147137, 146sylbid 239 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)) β†’ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒))
148 1red 11163 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 1 ∈ ℝ)
14969adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 𝑀 ∈ β„•)
150149nnge1d 12208 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 1 ≀ 𝑀)
151148, 71, 72, 150, 77letrd 11319 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 1 ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))
152 flge1nn 13733 . . . . . . . . . . . . 13 ((if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ ∧ 1 ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀)) β†’ (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) ∈ β„•)
15372, 151, 152syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) ∈ β„•)
154153adantlr 714 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) ∈ β„•)
15544ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ 𝑁 ∈ β„•)
1568ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ 𝑋 ∈ 𝐷)
157118ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ 𝑋 β‰  1 )
15869ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ 𝑀 ∈ β„•)
15912ad4ant14 751 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) ∧ 𝑛 ∈ ℝ+) β†’ 𝐴 ∈ ℝ)
1601243adant1r 1178 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ (𝑛 ∈ ℝ+ ∧ π‘₯ ∈ ℝ+) ∧ (𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯)) β†’ 𝐡 ≀ 𝐴)
1611603adant1r 1178 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) ∧ (𝑛 ∈ ℝ+ ∧ π‘₯ ∈ ℝ+) ∧ (𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯)) β†’ 𝐡 ≀ 𝐴)
16265ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (𝑛 ∈ ℝ+ ↦ 𝐴) β‡π‘Ÿ 0)
16341ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ 𝑅 ∈ ℝ)
16447ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ βˆ€π‘’ ∈ (0..^𝑁)(absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
16579adantr 482 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ+)
16677adantr 482 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ 𝑀 ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))
16772adantr 482 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ)
168 fllep1 13713 . . . . . . . . . . . . . . . 16 (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ≀ ((βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) + 1))
169167, 168syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ≀ ((βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) + 1))
170153adantr 482 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) ∈ β„•)
171 simpr 486 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))
1725, 7, 155, 4, 6, 116, 156, 157, 120, 158, 159, 161, 162, 30, 163, 164, 165, 166, 169, 170, 171dchrisumlem2 26854 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) ≀ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄))
173172adantllr 718 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) ≀ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄))
17434ad3antrrr 729 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ seq1( + , 𝐹):β„•βŸΆβ„‚)
175 eluznn 12850 . . . . . . . . . . . . . . . . . 18 (((βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) ∈ β„• ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ π‘˜ ∈ β„•)
176154, 175sylan 581 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ π‘˜ ∈ β„•)
177174, 176ffvelcdmd 7041 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (seq1( + , 𝐹)β€˜π‘˜) ∈ β„‚)
178154adantr 482 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) ∈ β„•)
179174, 178ffvelcdmd 7041 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))) ∈ β„‚)
180177, 179subcld 11519 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ ((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) ∈ β„‚)
181180abscld 15328 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) ∈ ℝ)
182142adantr 482 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∈ ℝ)
183134adantr 482 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ 𝑒 ∈ ℝ)
184 lelttr 11252 . . . . . . . . . . . . . 14 (((absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) ∈ ℝ ∧ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∈ ℝ ∧ 𝑒 ∈ ℝ) β†’ (((absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) ≀ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∧ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒) β†’ (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) < 𝑒))
185181, 182, 183, 184syl3anc 1372 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (((absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) ≀ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∧ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒) β†’ (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) < 𝑒))
186173, 185mpand 694 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒 β†’ (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) < 𝑒))
187186ralrimdva 3152 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒 β†’ βˆ€π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) < 𝑒))
188 fveq2 6847 . . . . . . . . . . . . 13 (𝑗 = (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) β†’ (β„€β‰₯β€˜π‘—) = (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))
189 fveq2 6847 . . . . . . . . . . . . . . . 16 (𝑗 = (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) β†’ (seq1( + , 𝐹)β€˜π‘—) = (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))
190189oveq2d 7378 . . . . . . . . . . . . . . 15 (𝑗 = (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) β†’ ((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—)) = ((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))))
191190fveq2d 6851 . . . . . . . . . . . . . 14 (𝑗 = (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) β†’ (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) = (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))))
192191breq1d 5120 . . . . . . . . . . . . 13 (𝑗 = (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) β†’ ((absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒 ↔ (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) < 𝑒))
193188, 192raleqbidv 3322 . . . . . . . . . . . 12 (𝑗 = (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒 ↔ βˆ€π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) < 𝑒))
194193rspcev 3584 . . . . . . . . . . 11 (((βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) ∈ β„• ∧ βˆ€π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) < 𝑒) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒)
195154, 187, 194syl6an 683 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒 β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒))
196147, 195syld 47 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒))
197101, 196embantd 59 . . . . . . . 8 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒))
19898, 197syld 47 . . . . . . 7 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (βˆ€π‘› ∈ ℝ+ (π‘š ≀ 𝑛 β†’ (absβ€˜(𝐴 βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒))
199198rexlimdva 3153 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ ℝ+) β†’ (βˆƒπ‘š ∈ ℝ βˆ€π‘› ∈ ℝ+ (π‘š ≀ 𝑛 β†’ (absβ€˜(𝐴 βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒))
20067, 199mpd 15 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ ℝ+) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒)
201200ralrimiva 3144 . . . 4 (πœ‘ β†’ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒)
202 seqex 13915 . . . . 5 seq1( + , 𝐹) ∈ V
203202a1i 11 . . . 4 (πœ‘ β†’ seq1( + , 𝐹) ∈ V)
2041, 35, 201, 203caucvg 15570 . . 3 (πœ‘ β†’ seq1( + , 𝐹) ∈ dom ⇝ )
205202eldm 5861 . . 3 (seq1( + , 𝐹) ∈ dom ⇝ ↔ βˆƒπ‘‘seq1( + , 𝐹) ⇝ 𝑑)
206204, 205sylib 217 . 2 (πœ‘ β†’ βˆƒπ‘‘seq1( + , 𝐹) ⇝ 𝑑)
207 simpr 486 . . . . 5 ((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) β†’ seq1( + , 𝐹) ⇝ 𝑑)
208 elrege0 13378 . . . . . . . 8 ((2 Β· 𝑅) ∈ (0[,)+∞) ↔ ((2 Β· 𝑅) ∈ ℝ ∧ 0 ≀ (2 Β· 𝑅)))
20943, 61, 208sylanbrc 584 . . . . . . 7 (πœ‘ β†’ (2 Β· 𝑅) ∈ (0[,)+∞))
210209adantr 482 . . . . . 6 ((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) β†’ (2 Β· 𝑅) ∈ (0[,)+∞))
211 eqid 2737 . . . . . . . 8 (β„€β‰₯β€˜(βŒŠβ€˜π‘š)) = (β„€β‰₯β€˜(βŒŠβ€˜π‘š))
212 pnfxr 11216 . . . . . . . . . . . 12 +∞ ∈ ℝ*
213 icossre 13352 . . . . . . . . . . . 12 ((𝑀 ∈ ℝ ∧ +∞ ∈ ℝ*) β†’ (𝑀[,)+∞) βŠ† ℝ)
21470, 212, 213sylancl 587 . . . . . . . . . . 11 (πœ‘ β†’ (𝑀[,)+∞) βŠ† ℝ)
215214sselda 3949 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (𝑀[,)+∞)) β†’ π‘š ∈ ℝ)
216215adantlr 714 . . . . . . . . 9 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ π‘š ∈ ℝ)
217216flcld 13710 . . . . . . . 8 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (βŒŠβ€˜π‘š) ∈ β„€)
218 simplr 768 . . . . . . . . . 10 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ seq1( + , 𝐹) ⇝ 𝑑)
21934ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ seq1( + , 𝐹):β„•βŸΆβ„‚)
220 1red 11163 . . . . . . . . . . . . 13 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 1 ∈ ℝ)
22170ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 𝑀 ∈ ℝ)
22269ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 𝑀 ∈ β„•)
223222nnge1d 12208 . . . . . . . . . . . . 13 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 1 ≀ 𝑀)
224 elicopnf 13369 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℝ β†’ (π‘š ∈ (𝑀[,)+∞) ↔ (π‘š ∈ ℝ ∧ 𝑀 ≀ π‘š)))
22570, 224syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘š ∈ (𝑀[,)+∞) ↔ (π‘š ∈ ℝ ∧ 𝑀 ≀ π‘š)))
226225simplbda 501 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 𝑀 ≀ π‘š)
227226adantlr 714 . . . . . . . . . . . . 13 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 𝑀 ≀ π‘š)
228220, 221, 216, 223, 227letrd 11319 . . . . . . . . . . . 12 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 1 ≀ π‘š)
229 flge1nn 13733 . . . . . . . . . . . 12 ((π‘š ∈ ℝ ∧ 1 ≀ π‘š) β†’ (βŒŠβ€˜π‘š) ∈ β„•)
230216, 228, 229syl2anc 585 . . . . . . . . . . 11 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (βŒŠβ€˜π‘š) ∈ β„•)
231219, 230ffvelcdmd 7041 . . . . . . . . . 10 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) ∈ β„‚)
232 nnex 12166 . . . . . . . . . . . 12 β„• ∈ V
233232mptex 7178 . . . . . . . . . . 11 (π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))) ∈ V
234233a1i 11 . . . . . . . . . 10 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))) ∈ V)
235219adantr 482 . . . . . . . . . . 11 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ seq1( + , 𝐹):β„•βŸΆβ„‚)
236 eluznn 12850 . . . . . . . . . . . 12 (((βŒŠβ€˜π‘š) ∈ β„• ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑖 ∈ β„•)
237230, 236sylan 581 . . . . . . . . . . 11 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑖 ∈ β„•)
238235, 237ffvelcdmd 7041 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (seq1( + , 𝐹)β€˜π‘–) ∈ β„‚)
239 fveq2 6847 . . . . . . . . . . . . 13 (π‘˜ = 𝑖 β†’ (seq1( + , 𝐹)β€˜π‘˜) = (seq1( + , 𝐹)β€˜π‘–))
240239oveq2d 7378 . . . . . . . . . . . 12 (π‘˜ = 𝑖 β†’ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)) = ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–)))
241 eqid 2737 . . . . . . . . . . . 12 (π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))) = (π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))
242 ovex 7395 . . . . . . . . . . . 12 ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)) ∈ V
243240, 241, 242fvmpt3i 6958 . . . . . . . . . . 11 (𝑖 ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))β€˜π‘–) = ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–)))
244237, 243syl 17 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))β€˜π‘–) = ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–)))
245211, 217, 218, 231, 234, 238, 244climsubc2 15528 . . . . . . . . 9 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))) ⇝ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑))
246232mptex 7178 . . . . . . . . . 10 (π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))) ∈ V
247246a1i 11 . . . . . . . . 9 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))) ∈ V)
248 fvex 6860 . . . . . . . . . . . . . 14 (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) ∈ V
249248fvconst2 7158 . . . . . . . . . . . . 13 (𝑖 ∈ β„• β†’ ((β„• Γ— {(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))})β€˜π‘–) = (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))
250237, 249syl 17 . . . . . . . . . . . 12 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((β„• Γ— {(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))})β€˜π‘–) = (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))
251250oveq1d 7377 . . . . . . . . . . 11 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (((β„• Γ— {(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))})β€˜π‘–) βˆ’ (seq1( + , 𝐹)β€˜π‘–)) = ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–)))
252244, 251eqtr4d 2780 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))β€˜π‘–) = (((β„• Γ— {(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))})β€˜π‘–) βˆ’ (seq1( + , 𝐹)β€˜π‘–)))
253231adantr 482 . . . . . . . . . . . 12 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) ∈ β„‚)
254250, 253eqeltrd 2838 . . . . . . . . . . 11 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((β„• Γ— {(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))})β€˜π‘–) ∈ β„‚)
255254, 238subcld 11519 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (((β„• Γ— {(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))})β€˜π‘–) βˆ’ (seq1( + , 𝐹)β€˜π‘–)) ∈ β„‚)
256252, 255eqeltrd 2838 . . . . . . . . 9 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))β€˜π‘–) ∈ β„‚)
257240fveq2d 6851 . . . . . . . . . . . 12 (π‘˜ = 𝑖 β†’ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))) = (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–))))
258 eqid 2737 . . . . . . . . . . . 12 (π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))) = (π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))))
259 fvex 6860 . . . . . . . . . . . 12 (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))) ∈ V
260257, 258, 259fvmpt3i 6958 . . . . . . . . . . 11 (𝑖 ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))))β€˜π‘–) = (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–))))
261237, 260syl 17 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))))β€˜π‘–) = (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–))))
262244fveq2d 6851 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (absβ€˜((π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))β€˜π‘–)) = (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–))))
263261, 262eqtr4d 2780 . . . . . . . . 9 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))))β€˜π‘–) = (absβ€˜((π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))β€˜π‘–)))
264211, 245, 247, 217, 256, 263climabs 15493 . . . . . . . 8 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))) ⇝ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑)))
26543ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (2 Β· 𝑅) ∈ ℝ)
266 0red 11165 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 0 ∈ ℝ)
26770adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 𝑀 ∈ ℝ)
26874adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 0 < 𝑀)
269266, 267, 215, 268, 226ltletrd 11322 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 0 < π‘š)
270215, 269elrpd 12961 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ (𝑀[,)+∞)) β†’ π‘š ∈ ℝ+)
271 nfcsb1v 3885 . . . . . . . . . . . . . . . 16 β„²π‘›β¦‹π‘š / π‘›β¦Œπ΄
272271nfel1 2924 . . . . . . . . . . . . . . 15 β„²π‘›β¦‹π‘š / π‘›β¦Œπ΄ ∈ ℝ
273 csbeq1a 3874 . . . . . . . . . . . . . . . 16 (𝑛 = π‘š β†’ 𝐴 = β¦‹π‘š / π‘›β¦Œπ΄)
274273eleq1d 2823 . . . . . . . . . . . . . . 15 (𝑛 = π‘š β†’ (𝐴 ∈ ℝ ↔ β¦‹π‘š / π‘›β¦Œπ΄ ∈ ℝ))
275272, 274rspc 3572 . . . . . . . . . . . . . 14 (π‘š ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ β†’ β¦‹π‘š / π‘›β¦Œπ΄ ∈ ℝ))
27613, 275mpan9 508 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ β¦‹π‘š / π‘›β¦Œπ΄ ∈ ℝ)
277270, 276syldan 592 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ (𝑀[,)+∞)) β†’ β¦‹π‘š / π‘›β¦Œπ΄ ∈ ℝ)
278277adantlr 714 . . . . . . . . . . 11 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ β¦‹π‘š / π‘›β¦Œπ΄ ∈ ℝ)
279265, 278remulcld 11192 . . . . . . . . . 10 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄) ∈ ℝ)
280279recnd 11190 . . . . . . . . 9 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄) ∈ β„‚)
281 1z 12540 . . . . . . . . 9 1 ∈ β„€
2821eqimss2i 4008 . . . . . . . . . 10 (β„€β‰₯β€˜1) βŠ† β„•
283282, 232climconst2 15437 . . . . . . . . 9 ((((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄) ∈ β„‚ ∧ 1 ∈ β„€) β†’ (β„• Γ— {((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄)}) ⇝ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄))
284280, 281, 283sylancl 587 . . . . . . . 8 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (β„• Γ— {((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄)}) ⇝ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄))
285253, 238subcld 11519 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–)) ∈ β„‚)
286285abscld 15328 . . . . . . . . 9 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–))) ∈ ℝ)
287261, 286eqeltrd 2838 . . . . . . . 8 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))))β€˜π‘–) ∈ ℝ)
288 ovex 7395 . . . . . . . . . . 11 ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄) ∈ V
289288fvconst2 7158 . . . . . . . . . 10 (𝑖 ∈ β„• β†’ ((β„• Γ— {((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄)})β€˜π‘–) = ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄))
290237, 289syl 17 . . . . . . . . 9 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((β„• Γ— {((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄)})β€˜π‘–) = ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄))
291279adantr 482 . . . . . . . . 9 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄) ∈ ℝ)
292290, 291eqeltrd 2838 . . . . . . . 8 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((β„• Γ— {((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄)})β€˜π‘–) ∈ ℝ)
293 simplll 774 . . . . . . . . . . 11 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ πœ‘)
294293, 44syl 17 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑁 ∈ β„•)
295293, 8syl 17 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑋 ∈ 𝐷)
296293, 118syl 17 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑋 β‰  1 )
297222adantr 482 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑀 ∈ β„•)
298293, 12sylan 581 . . . . . . . . . 10 (((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) ∧ 𝑛 ∈ ℝ+) β†’ 𝐴 ∈ ℝ)
299293, 124syl3an1 1164 . . . . . . . . . 10 (((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) ∧ (𝑛 ∈ ℝ+ ∧ π‘₯ ∈ ℝ+) ∧ (𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯)) β†’ 𝐡 ≀ 𝐴)
300293, 65syl 17 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (𝑛 ∈ ℝ+ ↦ 𝐴) β‡π‘Ÿ 0)
301293, 41syl 17 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑅 ∈ ℝ)
302293, 47syl 17 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ βˆ€π‘’ ∈ (0..^𝑁)(absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
303270adantlr 714 . . . . . . . . . . 11 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ π‘š ∈ ℝ+)
304303adantr 482 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ π‘š ∈ ℝ+)
305227adantr 482 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑀 ≀ π‘š)
306216adantr 482 . . . . . . . . . . 11 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ π‘š ∈ ℝ)
307 reflcl 13708 . . . . . . . . . . . 12 (π‘š ∈ ℝ β†’ (βŒŠβ€˜π‘š) ∈ ℝ)
308 peano2re 11335 . . . . . . . . . . . 12 ((βŒŠβ€˜π‘š) ∈ ℝ β†’ ((βŒŠβ€˜π‘š) + 1) ∈ ℝ)
309306, 307, 3083syl 18 . . . . . . . . . . 11 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((βŒŠβ€˜π‘š) + 1) ∈ ℝ)
310 flltp1 13712 . . . . . . . . . . . 12 (π‘š ∈ ℝ β†’ π‘š < ((βŒŠβ€˜π‘š) + 1))
311306, 310syl 17 . . . . . . . . . . 11 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ π‘š < ((βŒŠβ€˜π‘š) + 1))
312306, 309, 311ltled 11310 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ π‘š ≀ ((βŒŠβ€˜π‘š) + 1))
313230adantr 482 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (βŒŠβ€˜π‘š) ∈ β„•)
314 simpr 486 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š)))
3155, 7, 294, 4, 6, 116, 295, 296, 120, 297, 298, 299, 300, 30, 301, 302, 304, 305, 312, 313, 314dchrisumlem2 26854 . . . . . . . . 9 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (absβ€˜((seq1( + , 𝐹)β€˜π‘–) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))) ≀ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄))
316253, 238abssubd 15345 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–))) = (absβ€˜((seq1( + , 𝐹)β€˜π‘–) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))))
317261, 316eqtrd 2777 . . . . . . . . 9 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))))β€˜π‘–) = (absβ€˜((seq1( + , 𝐹)β€˜π‘–) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))))
318315, 317, 2903brtr4d 5142 . . . . . . . 8 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))))β€˜π‘–) ≀ ((β„• Γ— {((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄)})β€˜π‘–))
319211, 217, 264, 284, 287, 292, 318climle 15529 . . . . . . 7 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄))
320319ralrimiva 3144 . . . . . 6 ((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) β†’ βˆ€π‘š ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄))
321 oveq1 7369 . . . . . . . . . 10 (𝑐 = (2 Β· 𝑅) β†’ (𝑐 Β· 𝐡) = ((2 Β· 𝑅) Β· 𝐡))
322321breq2d 5122 . . . . . . . . 9 (𝑐 = (2 Β· 𝑅) β†’ ((absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡) ↔ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· 𝐡)))
323322ralbidv 3175 . . . . . . . 8 (𝑐 = (2 Β· 𝑅) β†’ (βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡) ↔ βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· 𝐡)))
324 2fveq3 6852 . . . . . . . . . . 11 (π‘š = π‘₯ β†’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) = (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)))
325324fvoveq1d 7384 . . . . . . . . . 10 (π‘š = π‘₯ β†’ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑)) = (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)))
326 vex 3452 . . . . . . . . . . . . 13 π‘š ∈ V
327326a1i 11 . . . . . . . . . . . 12 (π‘š = π‘₯ β†’ π‘š ∈ V)
328 equequ2 2030 . . . . . . . . . . . . . 14 (π‘š = π‘₯ β†’ (𝑛 = π‘š ↔ 𝑛 = π‘₯))
329328biimpa 478 . . . . . . . . . . . . 13 ((π‘š = π‘₯ ∧ 𝑛 = π‘š) β†’ 𝑛 = π‘₯)
330329, 120syl 17 . . . . . . . . . . . 12 ((π‘š = π‘₯ ∧ 𝑛 = π‘š) β†’ 𝐴 = 𝐡)
331327, 330csbied 3898 . . . . . . . . . . 11 (π‘š = π‘₯ β†’ β¦‹π‘š / π‘›β¦Œπ΄ = 𝐡)
332331oveq2d 7378 . . . . . . . . . 10 (π‘š = π‘₯ β†’ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄) = ((2 Β· 𝑅) Β· 𝐡))
333325, 332breq12d 5123 . . . . . . . . 9 (π‘š = π‘₯ β†’ ((absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄) ↔ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· 𝐡)))
334333cbvralvw 3228 . . . . . . . 8 (βˆ€π‘š ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄) ↔ βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· 𝐡))
335323, 334bitr4di 289 . . . . . . 7 (𝑐 = (2 Β· 𝑅) β†’ (βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡) ↔ βˆ€π‘š ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄)))
336335rspcev 3584 . . . . . 6 (((2 Β· 𝑅) ∈ (0[,)+∞) ∧ βˆ€π‘š ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄)) β†’ βˆƒπ‘ ∈ (0[,)+∞)βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡))
337210, 320, 336syl2anc 585 . . . . 5 ((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) β†’ βˆƒπ‘ ∈ (0[,)+∞)βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡))
338 r19.42v 3188 . . . . 5 (βˆƒπ‘ ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑑 ∧ βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡)) ↔ (seq1( + , 𝐹) ⇝ 𝑑 ∧ βˆƒπ‘ ∈ (0[,)+∞)βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡)))
339207, 337, 338sylanbrc 584 . . . 4 ((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) β†’ βˆƒπ‘ ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑑 ∧ βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡)))
340339ex 414 . . 3 (πœ‘ β†’ (seq1( + , 𝐹) ⇝ 𝑑 β†’ βˆƒπ‘ ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑑 ∧ βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡))))
341340eximdv 1921 . 2 (πœ‘ β†’ (βˆƒπ‘‘seq1( + , 𝐹) ⇝ 𝑑 β†’ βˆƒπ‘‘βˆƒπ‘ ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑑 ∧ βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡))))
342206, 341mpd 15 1 (πœ‘ β†’ βˆƒπ‘‘βˆƒπ‘ ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑑 ∧ βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  Vcvv 3448  β¦‹csb 3860   βŠ† wss 3915  βˆ…c0 4287  ifcif 4491  {csn 4591   class class class wbr 5110   ↦ cmpt 5193   Γ— cxp 5636  dom cdm 5638  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063  +∞cpnf 11193  β„*cxr 11195   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392   / cdiv 11819  β„•cn 12160  2c2 12215  β„€cz 12506  β„€β‰₯cuz 12770  β„+crp 12922  [,)cico 13273  ..^cfzo 13574  βŒŠcfl 13702  seqcseq 13913  abscabs 15126   ⇝ cli 15373   β‡π‘Ÿ 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-limsup 15360  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:  dchrisum  26856
  Copyright terms: Public domain W3C validator