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

Theorem divsqrsumo1 20823
 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 10623 . . 3
21a1i 11 . 2
3 divsqrsum.2 . . . . . . 7
43divsqrsumf 20820 . . . . . 6
54ffvelrni 5870 . . . . 5
6 rpsup 11248 . . . . . . 7
76a1i 11 . . . . . 6
84a1i 11 . . . . . . . 8
98feqmptd 5780 . . . . . . 7
10 divsqrsum2.1 . . . . . . 7
119, 10eqbrtrrd 4235 . . . . . 6
125adantl 454 . . . . . 6
137, 11, 12rlimrecl 12375 . . . . 5
14 resubcl 9366 . . . . 5
155, 13, 14syl2anr 466 . . . 4
1615recnd 9115 . . 3
17 rpsqrcl 12071 . . . . 5
1817adantl 454 . . . 4
1918rpcnd 10651 . . 3
2016, 19mulcld 9109 . 2
21 1re 9091 . . 3
2221a1i 11 . 2
2316, 19absmuld 12257 . . . . 5
2418rprege0d 10656 . . . . . . 7
25 absid 12102 . . . . . . 7
2624, 25syl 16 . . . . . 6
2726oveq2d 6098 . . . . 5
2823, 27eqtrd 2469 . . . 4
293, 10divsqrsum2 20822 . . . . 5
3016abscld 12239 . . . . . 6
3121a1i 11 . . . . . 6
3230, 31, 18lemuldivd 10694 . . . . 5
3329, 32mpbird 225 . . . 4
3428, 33eqbrtrd 4233 . . 3