Metamath Proof Explorer


Theorem rlim0

Description: Express the predicate B ( z ) converges to 0 . (Contributed by Mario Carneiro, 16-Sep-2014) (Revised by Mario Carneiro, 28-Feb-2015)

Ref Expression
Hypotheses rlim0.1 φ z A B
rlim0.2 φ A
Assertion rlim0 φ z A B 0 x + y z A y z B < x

Proof

Step Hyp Ref Expression
1 rlim0.1 φ z A B
2 rlim0.2 φ A
3 0cnd φ 0
4 1 2 3 rlim2 φ z A B 0 x + y z A y z B 0 < x
5 subid1 B B 0 = B
6 5 fveq2d B B 0 = B
7 6 breq1d B B 0 < x B < x
8 7 imbi2d B y z B 0 < x y z B < x
9 8 ralimi z A B z A y z B 0 < x y z B < x
10 ralbi z A y z B 0 < x y z B < x z A y z B 0 < x z A y z B < x
11 1 9 10 3syl φ z A y z B 0 < x z A y z B < x
12 11 rexbidv φ y z A y z B 0 < x y z A y z B < x
13 12 ralbidv φ x + y z A y z B 0 < x x + y z A y z B < x
14 4 13 bitrd φ z A B 0 x + y z A y z B < x