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

Theorem dchrisumlem3 27437
Description: Lemma for dchrisum 27438. 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 12890 . . . 4 β„• = (β„€β‰₯β€˜1)
2 1zzd 12618 . . . . . 6 (πœ‘ β†’ 1 ∈ β„€)
3 simpr 483 . . . . . . . 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 479 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ 𝑋 ∈ 𝐷)
103nnzd 12610 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ 𝑖 ∈ β„€)
114, 5, 6, 7, 9, 10dchrzrhcl 27191 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (π‘‹β€˜(πΏβ€˜π‘–)) ∈ β„‚)
12 dchrisum.4 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ ℝ+) β†’ 𝐴 ∈ ℝ)
1312ralrimiva 3136 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ)
14 nnrp 13012 . . . . . . . . . . 11 (𝑖 ∈ β„• β†’ 𝑖 ∈ ℝ+)
15 nfcsb1v 3911 . . . . . . . . . . . . . 14 Ⅎ𝑛⦋𝑖 / π‘›β¦Œπ΄
1615nfel1 2909 . . . . . . . . . . . . 13 Ⅎ𝑛⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ
17 csbeq1a 3900 . . . . . . . . . . . . . 14 (𝑛 = 𝑖 β†’ 𝐴 = ⦋𝑖 / π‘›β¦Œπ΄)
1817eleq1d 2810 . . . . . . . . . . . . 13 (𝑛 = 𝑖 β†’ (𝐴 ∈ ℝ ↔ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ))
1916, 18rspc 3591 . . . . . . . . . . . 12 (𝑖 ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ))
2019impcom 406 . . . . . . . . . . 11 ((βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ ∧ 𝑖 ∈ ℝ+) β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ)
2113, 14, 20syl2an 594 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ ℝ)
2221recnd 11267 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ⦋𝑖 / π‘›β¦Œπ΄ ∈ β„‚)
2311, 22mulcld 11259 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚)
24 nfcv 2892 . . . . . . . . 9 Ⅎ𝑛𝑖
25 nfcv 2892 . . . . . . . . . 10 Ⅎ𝑛(π‘‹β€˜(πΏβ€˜π‘–))
26 nfcv 2892 . . . . . . . . . 10 Ⅎ𝑛 Β·
2725, 26, 15nfov 7443 . . . . . . . . 9 Ⅎ𝑛((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄)
28 2fveq3 6895 . . . . . . . . . 10 (𝑛 = 𝑖 β†’ (π‘‹β€˜(πΏβ€˜π‘›)) = (π‘‹β€˜(πΏβ€˜π‘–)))
2928, 17oveq12d 7431 . . . . . . . . 9 (𝑛 = 𝑖 β†’ ((π‘‹β€˜(πΏβ€˜π‘›)) Β· 𝐴) = ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
30 dchrisum.7 . . . . . . . . 9 𝐹 = (𝑛 ∈ β„• ↦ ((π‘‹β€˜(πΏβ€˜π‘›)) Β· 𝐴))
3124, 27, 29, 30fvmptf 7019 . . . . . . . 8 ((𝑖 ∈ β„• ∧ ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄) ∈ β„‚) β†’ (πΉβ€˜π‘–) = ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
323, 23, 31syl2anc 582 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (πΉβ€˜π‘–) = ((π‘‹β€˜(πΏβ€˜π‘–)) Β· ⦋𝑖 / π‘›β¦Œπ΄))
3332, 23eqeltrd 2825 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ β„•) β†’ (πΉβ€˜π‘–) ∈ β„‚)
341, 2, 33serf 14022 . . . . 5 (πœ‘ β†’ seq1( + , 𝐹):β„•βŸΆβ„‚)
3534ffvelcdmda 7087 . . . 4 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐹)β€˜π‘˜) ∈ β„‚)
3612recnd 11267 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ ℝ+) β†’ 𝐴 ∈ β„‚)
3736ralrimiva 3136 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘› ∈ ℝ+ 𝐴 ∈ β„‚)
3837adantr 479 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ℝ+) β†’ βˆ€π‘› ∈ ℝ+ 𝐴 ∈ β„‚)
39 id 22 . . . . . . . 8 (𝑒 ∈ ℝ+ β†’ 𝑒 ∈ ℝ+)
40 2re 12311 . . . . . . . . . 10 2 ∈ ℝ
41 dchrisum.9 . . . . . . . . . 10 (πœ‘ β†’ 𝑅 ∈ ℝ)
42 remulcl 11218 . . . . . . . . . 10 ((2 ∈ ℝ ∧ 𝑅 ∈ ℝ) β†’ (2 Β· 𝑅) ∈ ℝ)
4340, 41, 42sylancr 585 . . . . . . . . 9 (πœ‘ β†’ (2 Β· 𝑅) ∈ ℝ)
44 rpvmasum.a . . . . . . . . . . . 12 (πœ‘ β†’ 𝑁 ∈ β„•)
45 lbfzo0 13699 . . . . . . . . . . . 12 (0 ∈ (0..^𝑁) ↔ 𝑁 ∈ β„•)
4644, 45sylibr 233 . . . . . . . . . . 11 (πœ‘ β†’ 0 ∈ (0..^𝑁))
47 dchrisum.10 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘’ ∈ (0..^𝑁)(absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
48 oveq2 7421 . . . . . . . . . . . . . . . . 17 (𝑒 = 0 β†’ (0..^𝑒) = (0..^0))
49 fzo0 13683 . . . . . . . . . . . . . . . . 17 (0..^0) = βˆ…
5048, 49eqtrdi 2781 . . . . . . . . . . . . . . . 16 (𝑒 = 0 β†’ (0..^𝑒) = βˆ…)
5150sumeq1d 15674 . . . . . . . . . . . . . . 15 (𝑒 = 0 β†’ Σ𝑛 ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›)) = Σ𝑛 ∈ βˆ… (π‘‹β€˜(πΏβ€˜π‘›)))
52 sum0 15694 . . . . . . . . . . . . . . 15 Σ𝑛 ∈ βˆ… (π‘‹β€˜(πΏβ€˜π‘›)) = 0
5351, 52eqtrdi 2781 . . . . . . . . . . . . . 14 (𝑒 = 0 β†’ Σ𝑛 ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›)) = 0)
5453abs00bd 15265 . . . . . . . . . . . . 13 (𝑒 = 0 β†’ (absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) = 0)
5554breq1d 5154 . . . . . . . . . . . 12 (𝑒 = 0 β†’ ((absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅 ↔ 0 ≀ 𝑅))
5655rspcv 3599 . . . . . . . . . . 11 (0 ∈ (0..^𝑁) β†’ (βˆ€π‘’ ∈ (0..^𝑁)(absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅 β†’ 0 ≀ 𝑅))
5746, 47, 56sylc 65 . . . . . . . . . 10 (πœ‘ β†’ 0 ≀ 𝑅)
58 0le2 12339 . . . . . . . . . . 11 0 ≀ 2
59 mulge0 11757 . . . . . . . . . . 11 (((2 ∈ ℝ ∧ 0 ≀ 2) ∧ (𝑅 ∈ ℝ ∧ 0 ≀ 𝑅)) β†’ 0 ≀ (2 Β· 𝑅))
6040, 58, 59mpanl12 700 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≀ 𝑅) β†’ 0 ≀ (2 Β· 𝑅))
6141, 57, 60syl2anc 582 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ (2 Β· 𝑅))
6243, 61ge0p1rpd 13073 . . . . . . . 8 (πœ‘ β†’ ((2 Β· 𝑅) + 1) ∈ ℝ+)
63 rpdivcl 13026 . . . . . . . 8 ((𝑒 ∈ ℝ+ ∧ ((2 Β· 𝑅) + 1) ∈ ℝ+) β†’ (𝑒 / ((2 Β· 𝑅) + 1)) ∈ ℝ+)
6439, 62, 63syl2anr 595 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ℝ+) β†’ (𝑒 / ((2 Β· 𝑅) + 1)) ∈ ℝ+)
65 dchrisum.6 . . . . . . . 8 (πœ‘ β†’ (𝑛 ∈ ℝ+ ↦ 𝐴) β‡π‘Ÿ 0)
6665adantr 479 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ ℝ+) β†’ (𝑛 ∈ ℝ+ ↦ 𝐴) β‡π‘Ÿ 0)
6738, 64, 66rlimi 15484 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ ℝ+) β†’ βˆƒπ‘š ∈ ℝ βˆ€π‘› ∈ ℝ+ (π‘š ≀ 𝑛 β†’ (absβ€˜(𝐴 βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))))
68 simpr 483 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ π‘š ∈ ℝ)
69 dchrisum.3 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑀 ∈ β„•)
7069nnred 12252 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑀 ∈ ℝ)
7170adantr 479 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 𝑀 ∈ ℝ)
7268, 71ifcld 4571 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ)
73 0red 11242 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 0 ∈ ℝ)
7469nngt0d 12286 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 < 𝑀)
7574adantr 479 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 0 < 𝑀)
76 max1 13191 . . . . . . . . . . . . 13 ((𝑀 ∈ ℝ ∧ π‘š ∈ ℝ) β†’ 𝑀 ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))
7770, 76sylan 578 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 𝑀 ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))
7873, 71, 72, 75, 77ltletrd 11399 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 0 < if(𝑀 ≀ π‘š, π‘š, 𝑀))
7972, 78elrpd 13040 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ+)
8079adantlr 713 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ+)
81 nfv 1909 . . . . . . . . . . 11 Ⅎ𝑛 π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀)
82 nfcv 2892 . . . . . . . . . . . . 13 Ⅎ𝑛abs
83 nfcsb1v 3911 . . . . . . . . . . . . . 14 Ⅎ𝑛⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄
84 nfcv 2892 . . . . . . . . . . . . . 14 Ⅎ𝑛 βˆ’
85 nfcv 2892 . . . . . . . . . . . . . 14 Ⅎ𝑛0
8683, 84, 85nfov 7443 . . . . . . . . . . . . 13 Ⅎ𝑛(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)
8782, 86nffv 6900 . . . . . . . . . . . 12 Ⅎ𝑛(absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0))
88 nfcv 2892 . . . . . . . . . . . 12 Ⅎ𝑛 <
89 nfcv 2892 . . . . . . . . . . . 12 Ⅎ𝑛(𝑒 / ((2 Β· 𝑅) + 1))
9087, 88, 89nfbr 5191 . . . . . . . . . . 11 Ⅎ𝑛(absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))
9181, 90nfim 1891 . . . . . . . . . 10 Ⅎ𝑛(π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)))
92 breq2 5148 . . . . . . . . . . 11 (𝑛 = if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ (π‘š ≀ 𝑛 ↔ π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀)))
93 csbeq1a 3900 . . . . . . . . . . . . 13 (𝑛 = if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ 𝐴 = ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄)
9493fvoveq1d 7435 . . . . . . . . . . . 12 (𝑛 = if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ (absβ€˜(𝐴 βˆ’ 0)) = (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)))
9594breq1d 5154 . . . . . . . . . . 11 (𝑛 = if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ ((absβ€˜(𝐴 βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)) ↔ (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))))
9692, 95imbi12d 343 . . . . . . . . . 10 (𝑛 = if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ ((π‘š ≀ 𝑛 β†’ (absβ€˜(𝐴 βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))) ↔ (π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)))))
9791, 96rspc 3591 . . . . . . . . 9 (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ (π‘š ≀ 𝑛 β†’ (absβ€˜(𝐴 βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))) β†’ (π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)))))
9880, 97syl 17 . . . . . . . 8 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (βˆ€π‘› ∈ ℝ+ (π‘š ≀ 𝑛 β†’ (absβ€˜(𝐴 βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))) β†’ (π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)))))
9970ad2antrr 724 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ 𝑀 ∈ ℝ)
100 max2 13193 . . . . . . . . . 10 ((𝑀 ∈ ℝ ∧ π‘š ∈ ℝ) β†’ π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))
10199, 100sylancom 586 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))
10213ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ)
10383nfel1 2909 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑛⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ ∈ ℝ
10493eleq1d 2810 . . . . . . . . . . . . . . . . . . 19 (𝑛 = if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ (𝐴 ∈ ℝ ↔ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ ∈ ℝ))
105103, 104rspc 3591 . . . . . . . . . . . . . . . . . 18 (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ β†’ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ ∈ ℝ))
10680, 102, 105sylc 65 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ ∈ ℝ)
107106recnd 11267 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ ∈ β„‚)
108107subid1d 11585 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0) = ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄)
109108fveq2d 6894 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) = (absβ€˜β¦‹if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄))
11072adantlr 713 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ)
11199, 76sylancom 586 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ 𝑀 ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))
112 elicopnf 13449 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ℝ β†’ (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ (𝑀[,)+∞) ↔ (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ ∧ 𝑀 ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))))
11399, 112syl 17 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ (𝑀[,)+∞) ↔ (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ ∧ 𝑀 ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))))
114110, 111, 113mpbir2and 711 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ (𝑀[,)+∞))
11544ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ 𝑁 ∈ β„•)
116 rpvmasum.1 . . . . . . . . . . . . . . . . . 18 1 = (0gβ€˜πΊ)
1178ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ 𝑋 ∈ 𝐷)
118 dchrisum.n1 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑋 β‰  1 )
119118ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ 𝑋 β‰  1 )
120 dchrisum.2 . . . . . . . . . . . . . . . . . 18 (𝑛 = π‘₯ β†’ 𝐴 = 𝐡)
12169ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ 𝑀 ∈ β„•)
12212ad4ant14 750 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ 𝑛 ∈ ℝ+) β†’ 𝐴 ∈ ℝ)
123 simpll 765 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ πœ‘)
124 dchrisum.5 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑛 ∈ ℝ+ ∧ π‘₯ ∈ ℝ+) ∧ (𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯)) β†’ 𝐡 ≀ 𝐴)
125123, 124syl3an1 1160 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ (𝑛 ∈ ℝ+ ∧ π‘₯ ∈ ℝ+) ∧ (𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯)) β†’ 𝐡 ≀ 𝐴)
12665ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (𝑛 ∈ ℝ+ ↦ 𝐴) β‡π‘Ÿ 0)
1275, 7, 115, 4, 6, 116, 117, 119, 120, 121, 122, 125, 126, 30dchrisumlema 27434 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ+ β†’ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ ∈ ℝ) ∧ (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ (𝑀[,)+∞) β†’ 0 ≀ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄)))
128127simprd 494 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ (𝑀[,)+∞) β†’ 0 ≀ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄))
129114, 128mpd 15 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ 0 ≀ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄)
130106, 129absidd 15396 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (absβ€˜β¦‹if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) = ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄)
131109, 130eqtrd 2765 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) = ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄)
132131breq1d 5154 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)) ↔ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ < (𝑒 / ((2 Β· 𝑅) + 1))))
133 rpre 13009 . . . . . . . . . . . . . 14 (𝑒 ∈ ℝ+ β†’ 𝑒 ∈ ℝ)
134133ad2antlr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ 𝑒 ∈ ℝ)
13562ad2antrr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((2 Β· 𝑅) + 1) ∈ ℝ+)
136106, 134, 135ltmuldiv2d 13091 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒 ↔ ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ < (𝑒 / ((2 Β· 𝑅) + 1))))
137132, 136bitr4d 281 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)) ↔ (((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒))
13843ad2antrr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (2 Β· 𝑅) ∈ ℝ)
139135rpred 13043 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((2 Β· 𝑅) + 1) ∈ ℝ)
140138lep1d 12170 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (2 Β· 𝑅) ≀ ((2 Β· 𝑅) + 1))
141138, 139, 106, 129, 140lemul1ad 12178 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ≀ (((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄))
142138, 106remulcld 11269 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∈ ℝ)
143139, 106remulcld 11269 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∈ ℝ)
144 lelttr 11329 . . . . . . . . . . . . 13 ((((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∈ ℝ ∧ (((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∈ ℝ ∧ 𝑒 ∈ ℝ) β†’ ((((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ≀ (((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∧ (((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒) β†’ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒))
145142, 143, 134, 144syl3anc 1368 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ≀ (((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∧ (((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒) β†’ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒))
146141, 145mpand 693 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((((2 Β· 𝑅) + 1) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒 β†’ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒))
147137, 146sylbid 239 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)) β†’ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒))
148 1red 11240 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 1 ∈ ℝ)
14969adantr 479 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 𝑀 ∈ β„•)
150149nnge1d 12285 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 1 ≀ 𝑀)
151148, 71, 72, 150, 77letrd 11396 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ 1 ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))
152 flge1nn 13813 . . . . . . . . . . . . 13 ((if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ ∧ 1 ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀)) β†’ (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) ∈ β„•)
15372, 151, 152syl2anc 582 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ ℝ) β†’ (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) ∈ β„•)
154153adantlr 713 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) ∈ β„•)
15544ad2antrr 724 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ 𝑁 ∈ β„•)
1568ad2antrr 724 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ 𝑋 ∈ 𝐷)
157118ad2antrr 724 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ 𝑋 β‰  1 )
15869ad2antrr 724 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ 𝑀 ∈ β„•)
15912ad4ant14 750 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) ∧ 𝑛 ∈ ℝ+) β†’ 𝐴 ∈ ℝ)
1601243adant1r 1174 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ (𝑛 ∈ ℝ+ ∧ π‘₯ ∈ ℝ+) ∧ (𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯)) β†’ 𝐡 ≀ 𝐴)
1611603adant1r 1174 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) ∧ (𝑛 ∈ ℝ+ ∧ π‘₯ ∈ ℝ+) ∧ (𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯)) β†’ 𝐡 ≀ 𝐴)
16265ad2antrr 724 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (𝑛 ∈ ℝ+ ↦ 𝐴) β‡π‘Ÿ 0)
16341ad2antrr 724 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ 𝑅 ∈ ℝ)
16447ad2antrr 724 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ βˆ€π‘’ ∈ (0..^𝑁)(absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
16579adantr 479 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ+)
16677adantr 479 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ 𝑀 ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀))
16772adantr 479 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ)
168 fllep1 13793 . . . . . . . . . . . . . . . 16 (if(𝑀 ≀ π‘š, π‘š, 𝑀) ∈ ℝ β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ≀ ((βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) + 1))
169167, 168syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ if(𝑀 ≀ π‘š, π‘š, 𝑀) ≀ ((βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) + 1))
170153adantr 479 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) ∈ β„•)
171 simpr 483 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))
1725, 7, 155, 4, 6, 116, 156, 157, 120, 158, 159, 161, 162, 30, 163, 164, 165, 166, 169, 170, 171dchrisumlem2 27436 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) ≀ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄))
173172adantllr 717 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) ≀ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄))
17434ad3antrrr 728 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ seq1( + , 𝐹):β„•βŸΆβ„‚)
175 eluznn 12927 . . . . . . . . . . . . . . . . . 18 (((βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) ∈ β„• ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ π‘˜ ∈ β„•)
176154, 175sylan 578 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ π‘˜ ∈ β„•)
177174, 176ffvelcdmd 7088 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (seq1( + , 𝐹)β€˜π‘˜) ∈ β„‚)
178154adantr 479 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) ∈ β„•)
179174, 178ffvelcdmd 7088 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))) ∈ β„‚)
180177, 179subcld 11596 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ ((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) ∈ β„‚)
181180abscld 15410 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) ∈ ℝ)
182142adantr 479 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∈ ℝ)
183134adantr 479 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ 𝑒 ∈ ℝ)
184 lelttr 11329 . . . . . . . . . . . . . 14 (((absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) ∈ ℝ ∧ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∈ ℝ ∧ 𝑒 ∈ ℝ) β†’ (((absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) ≀ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∧ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒) β†’ (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) < 𝑒))
185181, 182, 183, 184syl3anc 1368 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (((absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) ≀ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) ∧ ((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒) β†’ (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) < 𝑒))
186173, 185mpand 693 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) ∧ π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))) β†’ (((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒 β†’ (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) < 𝑒))
187186ralrimdva 3144 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒 β†’ βˆ€π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) < 𝑒))
188 fveq2 6890 . . . . . . . . . . . . 13 (𝑗 = (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) β†’ (β„€β‰₯β€˜π‘—) = (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))
189 fveq2 6890 . . . . . . . . . . . . . . . 16 (𝑗 = (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) β†’ (seq1( + , 𝐹)β€˜π‘—) = (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))
190189oveq2d 7429 . . . . . . . . . . . . . . 15 (𝑗 = (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) β†’ ((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—)) = ((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))))
191190fveq2d 6894 . . . . . . . . . . . . . 14 (𝑗 = (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) β†’ (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) = (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))))
192191breq1d 5154 . . . . . . . . . . . . 13 (𝑗 = (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) β†’ ((absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒 ↔ (absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) < 𝑒))
193188, 192raleqbidv 3330 . . . . . . . . . . . 12 (𝑗 = (βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) β†’ (βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒 ↔ βˆ€π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) < 𝑒))
194193rspcev 3603 . . . . . . . . . . 11 (((βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)) ∈ β„• ∧ βˆ€π‘˜ ∈ (β„€β‰₯β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀)))(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜if(𝑀 ≀ π‘š, π‘š, 𝑀))))) < 𝑒) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒)
195154, 187, 194syl6an 682 . . . . . . . . . 10 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (((2 Β· 𝑅) Β· ⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄) < 𝑒 β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒))
196147, 195syld 47 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1)) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒))
197101, 196embantd 59 . . . . . . . 8 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ ((π‘š ≀ if(𝑀 ≀ π‘š, π‘š, 𝑀) β†’ (absβ€˜(⦋if(𝑀 ≀ π‘š, π‘š, 𝑀) / π‘›β¦Œπ΄ βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒))
19898, 197syld 47 . . . . . . 7 (((πœ‘ ∧ 𝑒 ∈ ℝ+) ∧ π‘š ∈ ℝ) β†’ (βˆ€π‘› ∈ ℝ+ (π‘š ≀ 𝑛 β†’ (absβ€˜(𝐴 βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒))
199198rexlimdva 3145 . . . . . 6 ((πœ‘ ∧ 𝑒 ∈ ℝ+) β†’ (βˆƒπ‘š ∈ ℝ βˆ€π‘› ∈ ℝ+ (π‘š ≀ 𝑛 β†’ (absβ€˜(𝐴 βˆ’ 0)) < (𝑒 / ((2 Β· 𝑅) + 1))) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒))
20067, 199mpd 15 . . . . 5 ((πœ‘ ∧ 𝑒 ∈ ℝ+) β†’ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒)
201200ralrimiva 3136 . . . 4 (πœ‘ β†’ βˆ€π‘’ ∈ ℝ+ βˆƒπ‘— ∈ β„• βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(absβ€˜((seq1( + , 𝐹)β€˜π‘˜) βˆ’ (seq1( + , 𝐹)β€˜π‘—))) < 𝑒)
202 seqex 13995 . . . . 5 seq1( + , 𝐹) ∈ V
203202a1i 11 . . . 4 (πœ‘ β†’ seq1( + , 𝐹) ∈ V)
2041, 35, 201, 203caucvg 15652 . . 3 (πœ‘ β†’ seq1( + , 𝐹) ∈ dom ⇝ )
205202eldm 5898 . . 3 (seq1( + , 𝐹) ∈ dom ⇝ ↔ βˆƒπ‘‘seq1( + , 𝐹) ⇝ 𝑑)
206204, 205sylib 217 . 2 (πœ‘ β†’ βˆƒπ‘‘seq1( + , 𝐹) ⇝ 𝑑)
207 simpr 483 . . . . 5 ((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) β†’ seq1( + , 𝐹) ⇝ 𝑑)
208 elrege0 13458 . . . . . . . 8 ((2 Β· 𝑅) ∈ (0[,)+∞) ↔ ((2 Β· 𝑅) ∈ ℝ ∧ 0 ≀ (2 Β· 𝑅)))
20943, 61, 208sylanbrc 581 . . . . . . 7 (πœ‘ β†’ (2 Β· 𝑅) ∈ (0[,)+∞))
210209adantr 479 . . . . . 6 ((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) β†’ (2 Β· 𝑅) ∈ (0[,)+∞))
211 eqid 2725 . . . . . . . 8 (β„€β‰₯β€˜(βŒŠβ€˜π‘š)) = (β„€β‰₯β€˜(βŒŠβ€˜π‘š))
212 pnfxr 11293 . . . . . . . . . . . 12 +∞ ∈ ℝ*
213 icossre 13432 . . . . . . . . . . . 12 ((𝑀 ∈ ℝ ∧ +∞ ∈ ℝ*) β†’ (𝑀[,)+∞) βŠ† ℝ)
21470, 212, 213sylancl 584 . . . . . . . . . . 11 (πœ‘ β†’ (𝑀[,)+∞) βŠ† ℝ)
215214sselda 3973 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (𝑀[,)+∞)) β†’ π‘š ∈ ℝ)
216215adantlr 713 . . . . . . . . 9 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ π‘š ∈ ℝ)
217216flcld 13790 . . . . . . . 8 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (βŒŠβ€˜π‘š) ∈ β„€)
218 simplr 767 . . . . . . . . . 10 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ seq1( + , 𝐹) ⇝ 𝑑)
21934ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ seq1( + , 𝐹):β„•βŸΆβ„‚)
220 1red 11240 . . . . . . . . . . . . 13 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 1 ∈ ℝ)
22170ad2antrr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 𝑀 ∈ ℝ)
22269ad2antrr 724 . . . . . . . . . . . . . 14 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 𝑀 ∈ β„•)
223222nnge1d 12285 . . . . . . . . . . . . 13 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 1 ≀ 𝑀)
224 elicopnf 13449 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℝ β†’ (π‘š ∈ (𝑀[,)+∞) ↔ (π‘š ∈ ℝ ∧ 𝑀 ≀ π‘š)))
22570, 224syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘š ∈ (𝑀[,)+∞) ↔ (π‘š ∈ ℝ ∧ 𝑀 ≀ π‘š)))
226225simplbda 498 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 𝑀 ≀ π‘š)
227226adantlr 713 . . . . . . . . . . . . 13 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 𝑀 ≀ π‘š)
228220, 221, 216, 223, 227letrd 11396 . . . . . . . . . . . 12 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 1 ≀ π‘š)
229 flge1nn 13813 . . . . . . . . . . . 12 ((π‘š ∈ ℝ ∧ 1 ≀ π‘š) β†’ (βŒŠβ€˜π‘š) ∈ β„•)
230216, 228, 229syl2anc 582 . . . . . . . . . . 11 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (βŒŠβ€˜π‘š) ∈ β„•)
231219, 230ffvelcdmd 7088 . . . . . . . . . 10 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) ∈ β„‚)
232 nnex 12243 . . . . . . . . . . . 12 β„• ∈ V
233232mptex 7229 . . . . . . . . . . 11 (π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))) ∈ V
234233a1i 11 . . . . . . . . . 10 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))) ∈ V)
235219adantr 479 . . . . . . . . . . 11 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ seq1( + , 𝐹):β„•βŸΆβ„‚)
236 eluznn 12927 . . . . . . . . . . . 12 (((βŒŠβ€˜π‘š) ∈ β„• ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑖 ∈ β„•)
237230, 236sylan 578 . . . . . . . . . . 11 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑖 ∈ β„•)
238235, 237ffvelcdmd 7088 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (seq1( + , 𝐹)β€˜π‘–) ∈ β„‚)
239 fveq2 6890 . . . . . . . . . . . . 13 (π‘˜ = 𝑖 β†’ (seq1( + , 𝐹)β€˜π‘˜) = (seq1( + , 𝐹)β€˜π‘–))
240239oveq2d 7429 . . . . . . . . . . . 12 (π‘˜ = 𝑖 β†’ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)) = ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–)))
241 eqid 2725 . . . . . . . . . . . 12 (π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))) = (π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))
242 ovex 7446 . . . . . . . . . . . 12 ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)) ∈ V
243240, 241, 242fvmpt3i 7003 . . . . . . . . . . 11 (𝑖 ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))β€˜π‘–) = ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–)))
244237, 243syl 17 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))β€˜π‘–) = ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–)))
245211, 217, 218, 231, 234, 238, 244climsubc2 15610 . . . . . . . . 9 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))) ⇝ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑))
246232mptex 7229 . . . . . . . . . 10 (π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))) ∈ V
247246a1i 11 . . . . . . . . 9 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))) ∈ V)
248 fvex 6903 . . . . . . . . . . . . . 14 (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) ∈ V
249248fvconst2 7210 . . . . . . . . . . . . 13 (𝑖 ∈ β„• β†’ ((β„• Γ— {(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))})β€˜π‘–) = (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))
250237, 249syl 17 . . . . . . . . . . . 12 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((β„• Γ— {(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))})β€˜π‘–) = (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))
251250oveq1d 7428 . . . . . . . . . . 11 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (((β„• Γ— {(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))})β€˜π‘–) βˆ’ (seq1( + , 𝐹)β€˜π‘–)) = ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–)))
252244, 251eqtr4d 2768 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))β€˜π‘–) = (((β„• Γ— {(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))})β€˜π‘–) βˆ’ (seq1( + , 𝐹)β€˜π‘–)))
253231adantr 479 . . . . . . . . . . . 12 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) ∈ β„‚)
254250, 253eqeltrd 2825 . . . . . . . . . . 11 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((β„• Γ— {(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))})β€˜π‘–) ∈ β„‚)
255254, 238subcld 11596 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (((β„• Γ— {(seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š))})β€˜π‘–) βˆ’ (seq1( + , 𝐹)β€˜π‘–)) ∈ β„‚)
256252, 255eqeltrd 2825 . . . . . . . . 9 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))β€˜π‘–) ∈ β„‚)
257240fveq2d 6894 . . . . . . . . . . . 12 (π‘˜ = 𝑖 β†’ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))) = (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–))))
258 eqid 2725 . . . . . . . . . . . 12 (π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))) = (π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))))
259 fvex 6903 . . . . . . . . . . . 12 (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))) ∈ V
260257, 258, 259fvmpt3i 7003 . . . . . . . . . . 11 (𝑖 ∈ β„• β†’ ((π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))))β€˜π‘–) = (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–))))
261237, 260syl 17 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))))β€˜π‘–) = (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–))))
262244fveq2d 6894 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (absβ€˜((π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))β€˜π‘–)) = (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–))))
263261, 262eqtr4d 2768 . . . . . . . . 9 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))))β€˜π‘–) = (absβ€˜((π‘˜ ∈ β„• ↦ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))β€˜π‘–)))
264211, 245, 247, 217, 256, 263climabs 15575 . . . . . . . 8 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜)))) ⇝ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑)))
26543ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (2 Β· 𝑅) ∈ ℝ)
266 0red 11242 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 0 ∈ ℝ)
26770adantr 479 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 𝑀 ∈ ℝ)
26874adantr 479 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 0 < 𝑀)
269266, 267, 215, 268, 226ltletrd 11399 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ (𝑀[,)+∞)) β†’ 0 < π‘š)
270215, 269elrpd 13040 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ (𝑀[,)+∞)) β†’ π‘š ∈ ℝ+)
271 nfcsb1v 3911 . . . . . . . . . . . . . . . 16 β„²π‘›β¦‹π‘š / π‘›β¦Œπ΄
272271nfel1 2909 . . . . . . . . . . . . . . 15 β„²π‘›β¦‹π‘š / π‘›β¦Œπ΄ ∈ ℝ
273 csbeq1a 3900 . . . . . . . . . . . . . . . 16 (𝑛 = π‘š β†’ 𝐴 = β¦‹π‘š / π‘›β¦Œπ΄)
274273eleq1d 2810 . . . . . . . . . . . . . . 15 (𝑛 = π‘š β†’ (𝐴 ∈ ℝ ↔ β¦‹π‘š / π‘›β¦Œπ΄ ∈ ℝ))
275272, 274rspc 3591 . . . . . . . . . . . . . 14 (π‘š ∈ ℝ+ β†’ (βˆ€π‘› ∈ ℝ+ 𝐴 ∈ ℝ β†’ β¦‹π‘š / π‘›β¦Œπ΄ ∈ ℝ))
27613, 275mpan9 505 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ ℝ+) β†’ β¦‹π‘š / π‘›β¦Œπ΄ ∈ ℝ)
277270, 276syldan 589 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ (𝑀[,)+∞)) β†’ β¦‹π‘š / π‘›β¦Œπ΄ ∈ ℝ)
278277adantlr 713 . . . . . . . . . . 11 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ β¦‹π‘š / π‘›β¦Œπ΄ ∈ ℝ)
279265, 278remulcld 11269 . . . . . . . . . 10 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄) ∈ ℝ)
280279recnd 11267 . . . . . . . . 9 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄) ∈ β„‚)
281 1z 12617 . . . . . . . . 9 1 ∈ β„€
2821eqimss2i 4035 . . . . . . . . . 10 (β„€β‰₯β€˜1) βŠ† β„•
283282, 232climconst2 15519 . . . . . . . . 9 ((((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄) ∈ β„‚ ∧ 1 ∈ β„€) β†’ (β„• Γ— {((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄)}) ⇝ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄))
284280, 281, 283sylancl 584 . . . . . . . 8 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (β„• Γ— {((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄)}) ⇝ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄))
285253, 238subcld 11596 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–)) ∈ β„‚)
286285abscld 15410 . . . . . . . . 9 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–))) ∈ ℝ)
287261, 286eqeltrd 2825 . . . . . . . 8 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))))β€˜π‘–) ∈ ℝ)
288 ovex 7446 . . . . . . . . . . 11 ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄) ∈ V
289288fvconst2 7210 . . . . . . . . . 10 (𝑖 ∈ β„• β†’ ((β„• Γ— {((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄)})β€˜π‘–) = ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄))
290237, 289syl 17 . . . . . . . . 9 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((β„• Γ— {((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄)})β€˜π‘–) = ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄))
291279adantr 479 . . . . . . . . 9 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄) ∈ ℝ)
292290, 291eqeltrd 2825 . . . . . . . 8 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((β„• Γ— {((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄)})β€˜π‘–) ∈ ℝ)
293 simplll 773 . . . . . . . . . . 11 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ πœ‘)
294293, 44syl 17 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑁 ∈ β„•)
295293, 8syl 17 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑋 ∈ 𝐷)
296293, 118syl 17 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑋 β‰  1 )
297222adantr 479 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑀 ∈ β„•)
298293, 12sylan 578 . . . . . . . . . 10 (((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) ∧ 𝑛 ∈ ℝ+) β†’ 𝐴 ∈ ℝ)
299293, 124syl3an1 1160 . . . . . . . . . 10 (((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) ∧ (𝑛 ∈ ℝ+ ∧ π‘₯ ∈ ℝ+) ∧ (𝑀 ≀ 𝑛 ∧ 𝑛 ≀ π‘₯)) β†’ 𝐡 ≀ 𝐴)
300293, 65syl 17 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (𝑛 ∈ ℝ+ ↦ 𝐴) β‡π‘Ÿ 0)
301293, 41syl 17 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑅 ∈ ℝ)
302293, 47syl 17 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ βˆ€π‘’ ∈ (0..^𝑁)(absβ€˜Ξ£π‘› ∈ (0..^𝑒)(π‘‹β€˜(πΏβ€˜π‘›))) ≀ 𝑅)
303270adantlr 713 . . . . . . . . . . 11 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ π‘š ∈ ℝ+)
304303adantr 479 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ π‘š ∈ ℝ+)
305227adantr 479 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑀 ≀ π‘š)
306216adantr 479 . . . . . . . . . . 11 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ π‘š ∈ ℝ)
307 reflcl 13788 . . . . . . . . . . . 12 (π‘š ∈ ℝ β†’ (βŒŠβ€˜π‘š) ∈ ℝ)
308 peano2re 11412 . . . . . . . . . . . 12 ((βŒŠβ€˜π‘š) ∈ ℝ β†’ ((βŒŠβ€˜π‘š) + 1) ∈ ℝ)
309306, 307, 3083syl 18 . . . . . . . . . . 11 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((βŒŠβ€˜π‘š) + 1) ∈ ℝ)
310 flltp1 13792 . . . . . . . . . . . 12 (π‘š ∈ ℝ β†’ π‘š < ((βŒŠβ€˜π‘š) + 1))
311306, 310syl 17 . . . . . . . . . . 11 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ π‘š < ((βŒŠβ€˜π‘š) + 1))
312306, 309, 311ltled 11387 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ π‘š ≀ ((βŒŠβ€˜π‘š) + 1))
313230adantr 479 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (βŒŠβ€˜π‘š) ∈ β„•)
314 simpr 483 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š)))
3155, 7, 294, 4, 6, 116, 295, 296, 120, 297, 298, 299, 300, 30, 301, 302, 304, 305, 312, 313, 314dchrisumlem2 27436 . . . . . . . . 9 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (absβ€˜((seq1( + , 𝐹)β€˜π‘–) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))) ≀ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄))
316253, 238abssubd 15427 . . . . . . . . . 10 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘–))) = (absβ€˜((seq1( + , 𝐹)β€˜π‘–) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))))
317261, 316eqtrd 2765 . . . . . . . . 9 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))))β€˜π‘–) = (absβ€˜((seq1( + , 𝐹)β€˜π‘–) βˆ’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)))))
318315, 317, 2903brtr4d 5176 . . . . . . . 8 ((((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) ∧ 𝑖 ∈ (β„€β‰₯β€˜(βŒŠβ€˜π‘š))) β†’ ((π‘˜ ∈ β„• ↦ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ (seq1( + , 𝐹)β€˜π‘˜))))β€˜π‘–) ≀ ((β„• Γ— {((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄)})β€˜π‘–))
319211, 217, 264, 284, 287, 292, 318climle 15611 . . . . . . 7 (((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) ∧ π‘š ∈ (𝑀[,)+∞)) β†’ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄))
320319ralrimiva 3136 . . . . . 6 ((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) β†’ βˆ€π‘š ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄))
321 oveq1 7420 . . . . . . . . . 10 (𝑐 = (2 Β· 𝑅) β†’ (𝑐 Β· 𝐡) = ((2 Β· 𝑅) Β· 𝐡))
322321breq2d 5156 . . . . . . . . 9 (𝑐 = (2 Β· 𝑅) β†’ ((absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡) ↔ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· 𝐡)))
323322ralbidv 3168 . . . . . . . 8 (𝑐 = (2 Β· 𝑅) β†’ (βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡) ↔ βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· 𝐡)))
324 2fveq3 6895 . . . . . . . . . . 11 (π‘š = π‘₯ β†’ (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) = (seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)))
325324fvoveq1d 7435 . . . . . . . . . 10 (π‘š = π‘₯ β†’ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑)) = (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)))
326 vex 3467 . . . . . . . . . . . . 13 π‘š ∈ V
327326a1i 11 . . . . . . . . . . . 12 (π‘š = π‘₯ β†’ π‘š ∈ V)
328 equequ2 2021 . . . . . . . . . . . . . 14 (π‘š = π‘₯ β†’ (𝑛 = π‘š ↔ 𝑛 = π‘₯))
329328biimpa 475 . . . . . . . . . . . . 13 ((π‘š = π‘₯ ∧ 𝑛 = π‘š) β†’ 𝑛 = π‘₯)
330329, 120syl 17 . . . . . . . . . . . 12 ((π‘š = π‘₯ ∧ 𝑛 = π‘š) β†’ 𝐴 = 𝐡)
331327, 330csbied 3924 . . . . . . . . . . 11 (π‘š = π‘₯ β†’ β¦‹π‘š / π‘›β¦Œπ΄ = 𝐡)
332331oveq2d 7429 . . . . . . . . . 10 (π‘š = π‘₯ β†’ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄) = ((2 Β· 𝑅) Β· 𝐡))
333325, 332breq12d 5157 . . . . . . . . 9 (π‘š = π‘₯ β†’ ((absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄) ↔ (absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· 𝐡)))
334333cbvralvw 3225 . . . . . . . 8 (βˆ€π‘š ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄) ↔ βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· 𝐡))
335323, 334bitr4di 288 . . . . . . 7 (𝑐 = (2 Β· 𝑅) β†’ (βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡) ↔ βˆ€π‘š ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄)))
336335rspcev 3603 . . . . . 6 (((2 Β· 𝑅) ∈ (0[,)+∞) ∧ βˆ€π‘š ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘š)) βˆ’ 𝑑)) ≀ ((2 Β· 𝑅) Β· β¦‹π‘š / π‘›β¦Œπ΄)) β†’ βˆƒπ‘ ∈ (0[,)+∞)βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡))
337210, 320, 336syl2anc 582 . . . . 5 ((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) β†’ βˆƒπ‘ ∈ (0[,)+∞)βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡))
338 r19.42v 3181 . . . . 5 (βˆƒπ‘ ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑑 ∧ βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡)) ↔ (seq1( + , 𝐹) ⇝ 𝑑 ∧ βˆƒπ‘ ∈ (0[,)+∞)βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡)))
339207, 337, 338sylanbrc 581 . . . 4 ((πœ‘ ∧ seq1( + , 𝐹) ⇝ 𝑑) β†’ βˆƒπ‘ ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑑 ∧ βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡)))
340339ex 411 . . 3 (πœ‘ β†’ (seq1( + , 𝐹) ⇝ 𝑑 β†’ βˆƒπ‘ ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑑 ∧ βˆ€π‘₯ ∈ (𝑀[,)+∞)(absβ€˜((seq1( + , 𝐹)β€˜(βŒŠβ€˜π‘₯)) βˆ’ 𝑑)) ≀ (𝑐 Β· 𝐡))))
341340eximdv 1912 . 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 394   ∧ w3a 1084   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098   β‰  wne 2930  βˆ€wral 3051  βˆƒwrex 3060  Vcvv 3463  β¦‹csb 3886   βŠ† wss 3941  βˆ…c0 4319  ifcif 4525  {csn 4625   class class class wbr 5144   ↦ cmpt 5227   Γ— cxp 5671  dom cdm 5673  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7413  β„‚cc 11131  β„cr 11132  0cc0 11133  1c1 11134   + caddc 11136   Β· cmul 11138  +∞cpnf 11270  β„*cxr 11272   < clt 11273   ≀ cle 11274   βˆ’ cmin 11469   / cdiv 11896  β„•cn 12237  2c2 12292  β„€cz 12583  β„€β‰₯cuz 12847  β„+crp 13001  [,)cico 13353  ..^cfzo 13654  βŒŠcfl 13782  seqcseq 13993  abscabs 15208   ⇝ cli 15455   β‡π‘Ÿ crli 15456  Ξ£csu 15659  Basecbs 17174  0gc0g 17415  β„€RHomczrh 21424  β„€/nβ„€czn 21427  DChrcdchr 27178
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-inf2 9659  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210  ax-pre-sup 11211  ax-addf 11212  ax-mulf 11213
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4905  df-int 4946  df-iun 4994  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-se 5629  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7679  df-om 7866  df-1st 7987  df-2nd 7988  df-tpos 8225  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-oadd 8484  df-er 8718  df-ec 8720  df-qs 8724  df-map 8840  df-pm 8841  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-sup 9460  df-inf 9461  df-oi 9528  df-card 9957  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-div 11897  df-nn 12238  df-2 12300  df-3 12301  df-4 12302  df-5 12303  df-6 12304  df-7 12305  df-8 12306  df-9 12307  df-n0 12498  df-xnn0 12570  df-z 12584  df-dec 12703  df-uz 12848  df-rp 13002  df-ico 13357  df-fz 13512  df-fzo 13655  df-fl 13784  df-mod 13862  df-seq 13994  df-exp 14054  df-hash 14317  df-cj 15073  df-re 15074  df-im 15075  df-sqrt 15209  df-abs 15210  df-limsup 15442  df-clim 15459  df-rlim 15460  df-sum 15660  df-dvds 16226  df-gcd 16464  df-phi 16729  df-struct 17110  df-sets 17127  df-slot 17145  df-ndx 17157  df-base 17175  df-ress 17204  df-plusg 17240  df-mulr 17241  df-starv 17242  df-sca 17243  df-vsca 17244  df-ip 17245  df-tset 17246  df-ple 17247  df-ds 17249  df-unif 17250  df-0g 17417  df-imas 17484  df-qus 17485  df-mgm 18594  df-sgrp 18673  df-mnd 18689  df-mhm 18734  df-grp 18892  df-minusg 18893  df-sbg 18894  df-mulg 19023  df-subg 19077  df-nsg 19078  df-eqg 19079  df-ghm 19167  df-cmn 19736  df-abl 19737  df-mgp 20074  df-rng 20092  df-ur 20121  df-ring 20174  df-cring 20175  df-oppr 20272  df-dvdsr 20295  df-unit 20296  df-invr 20326  df-rhm 20410  df-subrng 20482  df-subrg 20507  df-lmod 20744  df-lss 20815  df-lsp 20855  df-sra 21057  df-rgmod 21058  df-lidl 21103  df-rsp 21104  df-2idl 21143  df-cnfld 21279  df-zring 21372  df-zrh 21428  df-zn 21431  df-dchr 27179
This theorem is referenced by:  dchrisum  27438
  Copyright terms: Public domain W3C validator