Metamath Proof Explorer


Theorem clim0

Description: Express the predicate F converges to 0 . (Contributed by NM, 24-Feb-2008) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses clim0.1 Z = M
clim0.2 φ M
clim0.3 φ F V
clim0.4 φ k Z F k = B
Assertion clim0 φ F 0 x + j Z k j B B < x

Proof

Step Hyp Ref Expression
1 clim0.1 Z = M
2 clim0.2 φ M
3 clim0.3 φ F V
4 clim0.4 φ k Z F k = B
5 1 2 3 4 clim2 φ F 0 0 x + j Z k j B B 0 < x
6 0cn 0
7 6 biantrur x + j Z k j B B 0 < x 0 x + j Z k j B B 0 < x
8 subid1 B B 0 = B
9 8 fveq2d B B 0 = B
10 9 breq1d B B 0 < x B < x
11 10 pm5.32i B B 0 < x B B < x
12 11 ralbii k j B B 0 < x k j B B < x
13 12 rexbii j Z k j B B 0 < x j Z k j B B < x
14 13 ralbii x + j Z k j B B 0 < x x + j Z k j B B < x
15 7 14 bitr3i 0 x + j Z k j B B 0 < x x + j Z k j B B < x
16 5 15 bitrdi φ F 0 x + j Z k j B B < x