Metamath Proof Explorer


Theorem clim2cf

Description: Express the predicate F converges to A . Similar to clim2 , but without the disjoint var constraint F k . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses clim2cf.nf _kF
clim2cf.z Z=M
clim2cf.m φM
clim2cf.f φFV
clim2cf.fv φkZFk=B
clim2cf.a φA
clim2cf.b φkZB
Assertion clim2cf φFAx+jZkjBA<x

Proof

Step Hyp Ref Expression
1 clim2cf.nf _kF
2 clim2cf.z Z=M
3 clim2cf.m φM
4 clim2cf.f φFV
5 clim2cf.fv φkZFk=B
6 clim2cf.a φA
7 clim2cf.b φkZB
8 6 biantrurd φx+jZkjBBA<xAx+jZkjBBA<x
9 2 uztrn2 jZkjkZ
10 7 biantrurd φkZBA<xBBA<x
11 9 10 sylan2 φjZkjBA<xBBA<x
12 11 anassrs φjZkjBA<xBBA<x
13 12 ralbidva φjZkjBA<xkjBBA<x
14 13 rexbidva φjZkjBA<xjZkjBBA<x
15 14 ralbidv φx+jZkjBA<xx+jZkjBBA<x
16 1 2 3 4 5 clim2f φFAAx+jZkjBBA<x
17 8 15 16 3bitr4rd φFAx+jZkjBA<x