Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  divsqrsumo1 Structured version   Unicode version

Theorem divsqrsumo1 22479
 Description: The sum has the asymptotic expansion , for some . (Contributed by Mario Carneiro, 10-May-2016.)
Hypotheses
Ref Expression
divsqrsum.2
divsqrsum2.1
Assertion
Ref Expression
divsqrsumo1
Distinct variable groups:   ,,   ,   ,   ,,
Allowed substitution hints:   ()   (,)   (,)

Proof of Theorem divsqrsumo1
StepHypRef Expression
1 rpssre 11088 . . 3
21a1i 11 . 2
3 divsqrsum.2 . . . . . . 7
43divsqrsumf 22476 . . . . . 6
54ffvelrni 5927 . . . . 5
6 rpsup 11792 . . . . . . 7
76a1i 11 . . . . . 6
84a1i 11 . . . . . . . 8
98feqmptd 5829 . . . . . . 7
10 divsqrsum2.1 . . . . . . 7
119, 10eqbrtrrd 4398 . . . . . 6
125adantl 466 . . . . . 6
137, 11, 12rlimrecl 13146 . . . . 5
14 resubcl 9760 . . . . 5
155, 13, 14syl2anr 478 . . . 4
1615recnd 9499 . . 3
17 rpsqrcl 12842 . . . . 5
1817adantl 466 . . . 4
1918rpcnd 11116 . . 3
2016, 19mulcld 9493 . 2
21 1red 9488 . 2
2216, 19absmuld 13028 . . . . 5
2318rprege0d 11121 . . . . . . 7
24 absid 12873 . . . . . . 7
2523, 24syl 16 . . . . . 6
2625oveq2d 6192 . . . . 5
2722, 26eqtrd 2490 . . . 4
283, 10divsqrsum2 22478 . . . . 5
2916abscld 13010 . . . . . 6
30 1red 9488 . . . . . 6
3129, 30, 18lemuldivd 11159 . . . . 5
3228, 31mpbird 232 . . . 4
3327, 32eqbrtrd 4396 . . 3