Theorem climmpt 13033

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 458	. 2 |- ( ( M e. ZZ /\ F e. V ) -> F e. V )
3		climmpt.2	. . . 4 |- G = ( k e. Z |-> ( F ` k ) )
4		fvex 5689	. . . . . 6 |- ( ZZ>= ` M ) e. _V
5	1, 4	eqeltri 2503	. . . . 5 |- Z e. _V
6	5	mptex 5935	. . . 4 |- ( k e. Z |-> ( F ` k ) ) e. _V
7	3, 6	eqeltri 2503	. . 3 |- G e. _V
8	7	a1i 11	. 2 |- ( ( M e. ZZ /\ F e. V ) -> G e. _V )
9		simpl 454	. 2 |- ( ( M e. ZZ /\ F e. V ) -> M e. ZZ )
10		fveq2 5679	. . . . 5 |- ( k = m -> ( F ` k ) = ( F ` m ) )
11		fvex 5689	. . . . 5 |- ( F ` m ) e. _V
12	10, 3, 11	fvmpt 5762	. . . 4 |- ( m e. Z -> ( G ` m ) = ( F ` m ) )
13	12	eqcomd 2438	. . 3 |- ( m e. Z -> ( F ` m ) = ( G ` m ) )
14	13	adantl 463	. 2 |- ( ( ( M e. ZZ /\ F e. V ) /\ m e. Z ) -> ( F ` m ) = ( G ` m ) )
15	1, 2, 8, 9, 14	climeq 13029	1 |- ( ( M e. ZZ /\ F e. V ) -> ( F ~~> A <-> G ~~> A ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1362   e. wcel 1755   _Vcvv 2962   class class class wbr 4280   e. cmpt 4338   ` cfv 5406   ZZcz 10634   ZZ>=cuz 10849   ~~> cli 12946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-cnex 9326  ax-resscn 9327  ax-pre-lttri 9344  ax-pre-lttrn 9345

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-po 4628  df-so 4629  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-ov 6083  df-er 7089  df-en 7299  df-dom 7300  df-sdom 7301  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412  df-neg 9586  df-z 10635  df-uz 10850  df-clim 12950

This theorem is referenced by:  climmpt2  13035  climrecl  13045  climge0  13046  caurcvg2  13139  caucvg  13140  climfsum  13266  dstfrvclim1  26708