Theorem climmpt 13628

Description: Exhibit a function G with the same convergence properties as the not-quite-function F. (Contributed by Mario Carneiro, 31-Jan-2014.)

Hypotheses

Ref	Expression
2clim.1	|- Z = ( ZZ>= ` M )
climmpt.2	|- G = ( k e. Z |-> ( F ` k ) )

Assertion

Ref	Expression
climmpt	|- ( ( M e. ZZ /\ F e. V ) -> ( F ~~> A <-> G ~~> A ) )

Distinct variable groups:   A, k   k, F   k, Z

Allowed substitution hints:   G( k)   M( k)   V( k)

Proof of Theorem climmpt

Dummy variable m is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2clim.1	. 2 |- Z = ( ZZ>= ` M )
2		simpr 463	. 2 |- ( ( M e. ZZ /\ F e. V ) -> F e. V )
3		climmpt.2	. . . 4 |- G = ( k e. Z |-> ( F ` k ) )
4		fvex 5873	. . . . . 6 |- ( ZZ>= ` M ) e. _V
5	1, 4	eqeltri 2524	. . . . 5 |- Z e. _V
6	5	mptex 6134	. . . 4 |- ( k e. Z |-> ( F ` k ) ) e. _V
7	3, 6	eqeltri 2524	. . 3 |- G e. _V
8	7	a1i 11	. 2 |- ( ( M e. ZZ /\ F e. V ) -> G e. _V )
9		simpl 459	. 2 |- ( ( M e. ZZ /\ F e. V ) -> M e. ZZ )
10		fveq2 5863	. . . . 5 |- ( k = m -> ( F ` k ) = ( F ` m ) )
11		fvex 5873	. . . . 5 |- ( F ` m ) e. _V
12	10, 3, 11	fvmpt 5946	. . . 4 |- ( m e. Z -> ( G ` m ) = ( F ` m ) )
13	12	eqcomd 2456	. . 3 |- ( m e. Z -> ( F ` m ) = ( G ` m ) )
14	13	adantl 468	. 2 |- ( ( ( M e. ZZ /\ F e. V ) /\ m e. Z ) -> ( F ` m ) = ( G ` m ) )
15	1, 2, 8, 9, 14	climeq 13624	1 |- ( ( M e. ZZ /\ F e. V ) -> ( F ~~> A <-> G ~~> A ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1443   e. wcel 1886   _Vcvv 3044   class class class wbr 4401   |-> cmpt 4460   ` cfv 5581   ZZcz 10934   ZZ>=cuz 11156   ~~> cli 13541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-cnex 9592  ax-resscn 9593  ax-pre-lttri 9610  ax-pre-lttrn 9611

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-po 4754  df-so 4755  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-ov 6291  df-er 7360  df-en 7567  df-dom 7568  df-sdom 7569  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-neg 9860  df-z 10935  df-uz 11157  df-clim 13545

This theorem is referenced by:  climmpt2  13630  climrecl  13640  climge0  13641  caurcvg2  13737  caucvg  13738  climfsum  13873  dstfrvclim1  29303  divcnvg  37701