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

Theorem explecnv 13656
 Description: A sequence of terms converges to zero when it is less than powers of a number whose absolute value is smaller than 1. (Contributed by NM, 19-Jul-2008.) (Revised by Mario Carneiro, 26-Apr-2014.)
Hypotheses
Ref Expression
explecnv.1
explecnv.2
explecnv.3
explecnv.5
explecnv.4
explecnv.6
explecnv.7
Assertion
Ref Expression
explecnv
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem explecnv
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqid 2467 . . 3
2 0z 10887 . . . 4
3 explecnv.3 . . . 4
4 ifcl 3987 . . . 4
52, 3, 4sylancr 663 . . 3
6 explecnv.5 . . . . 5
76recnd 9634 . . . 4
8 explecnv.4 . . . 4
97, 8expcnv 13655 . . 3
10 explecnv.1 . . . . . 6
11 fvex 5882 . . . . . 6
1210, 11eqeltri 2551 . . . . 5
1312mptex 6142 . . . 4
1413a1i 11 . . 3
15 nn0uz 11128 . . . . . . . . . . 11
1610, 15ineq12i 3703 . . . . . . . . . 10
17 uzin 11126 . . . . . . . . . . 11
183, 2, 17sylancl 662 . . . . . . . . . 10
1916, 18syl5req 2521 . . . . . . . . 9
2019eleq2d 2537 . . . . . . . 8
2120biimpa 484 . . . . . . 7
22 elin 3692 . . . . . . 7
2321, 22sylib 196 . . . . . 6
2423simprd 463 . . . . 5
25 oveq2 6303 . . . . . 6
26 eqid 2467 . . . . . 6
27 ovex 6320 . . . . . 6
2825, 26, 27fvmpt 5957 . . . . 5
2924, 28syl 16 . . . 4
306adantr 465 . . . . 5
3130, 24reexpcld 12307 . . . 4
3229, 31eqeltrd 2555 . . 3
3323simpld 459 . . . . 5
34 fveq2 5872 . . . . . . 7
3534fveq2d 5876 . . . . . 6
36 eqid 2467 . . . . . 6
37 fvex 5882 . . . . . 6
3835, 36, 37fvmpt 5957 . . . . 5
3933, 38syl 16 . . . 4
40 explecnv.6 . . . . . 6
4133, 40syldan 470 . . . . 5
4241abscld 13247 . . . 4
4339, 42eqeltrd 2555 . . 3
44 explecnv.7 . . . . 5
4533, 44syldan 470 . . . 4
4645, 39, 293brtr4d 4483 . . 3
4741absge0d 13255 . . . 4
4847, 39breqtrrd 4479 . . 3
491, 5, 9, 14, 32, 43, 46, 48climsqz2 13444 . 2
50 explecnv.2 . . 3