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

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

Proof of Theorem divsqrtsumo1
StepHypRef Expression
1 rpssre 11319 . . 3
21a1i 11 . 2
3 divsqrtsum.2 . . . . . . 7
43divsqrsumf 23918 . . . . . 6
54ffvelrni 6026 . . . . 5
6 rpsup 12100 . . . . . . 7
76a1i 11 . . . . . 6
84a1i 11 . . . . . . . 8
98feqmptd 5923 . . . . . . 7
10 divsqrsum2.1 . . . . . . 7
119, 10eqbrtrrd 4428 . . . . . 6
125adantl 468 . . . . . 6
137, 11, 12rlimrecl 13656 . . . . 5
14 resubcl 9943 . . . . 5
155, 13, 14syl2anr 481 . . . 4
1615recnd 9674 . . 3
17 rpsqrtcl 13340 . . . . 5
1817adantl 468 . . . 4
1918rpcnd 11350 . . 3
2016, 19mulcld 9668 . 2
21 1red 9663 . 2
2216, 19absmuld 13528 . . . . 5
2318rprege0d 11355 . . . . . . 7
24 absid 13371 . . . . . . 7
2523, 24syl 17 . . . . . 6
2625oveq2d 6311 . . . . 5
2722, 26eqtrd 2487 . . . 4
283, 10divsqrtsum2 23920 . . . . 5
2916abscld 13510 . . . . . 6
30 1red 9663 . . . . . 6
3129, 30, 18lemuldivd 11394 . . . . 5
3228, 31mpbird 236 . . . 4
3327, 32eqbrtrd 4426 . . 3