climdivf

Description: Limit of the ratio of two converging sequences. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	climdivf.1	\|- F/ k ph
	climdivf.2	\|- F/_ k F
	climdivf.3	\|- F/_ k G
	climdivf.4	\|- F/_ k H
	climdivf.5	\|- Z = ( ZZ>= ` M )
	climdivf.6	\|- ( ph -> M e. ZZ )
	climdivf.7	\|- ( ph -> F ~~> A )
	climdivf.8	\|- ( ph -> H e. X )
	climdivf.9	\|- ( ph -> G ~~> B )
	climdivf.10	\|- ( ph -> B =/= 0 )
	climdivf.11	\|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
	climdivf.12	\|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. ( CC \ { 0 } ) )
	climdivf.13	\|- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) / ( G ` k ) ) )
Assertion	climdivf	\|- ( ph -> H ~~> ( A / B ) )

Proof

Step	Hyp	Ref	Expression
1		climdivf.1	\|- F/ k ph
2		climdivf.2	\|- F/_ k F
3		climdivf.3	\|- F/_ k G
4		climdivf.4	\|- F/_ k H
5		climdivf.5	\|- Z = ( ZZ>= ` M )
6		climdivf.6	\|- ( ph -> M e. ZZ )
7		climdivf.7	\|- ( ph -> F ~~> A )
8		climdivf.8	\|- ( ph -> H e. X )
9		climdivf.9	\|- ( ph -> G ~~> B )
10		climdivf.10	\|- ( ph -> B =/= 0 )
11		climdivf.11	\|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
12		climdivf.12	\|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. ( CC \ { 0 } ) )
13		climdivf.13	\|- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) / ( G ` k ) ) )
14		nfmpt1	\|- F/_ k ( k e. Z \|-> ( 1 / ( G ` k ) ) )
15		simpr	\|- ( ( ph /\ k e. Z ) -> k e. Z )
16	12	eldifad	\|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
17		eldifsni	\|- ( ( G ` k ) e. ( CC \ { 0 } ) -> ( G ` k ) =/= 0 )
18	12 17	syl	\|- ( ( ph /\ k e. Z ) -> ( G ` k ) =/= 0 )
19	16 18	reccld	\|- ( ( ph /\ k e. Z ) -> ( 1 / ( G ` k ) ) e. CC )
20		eqid	\|- ( k e. Z \|-> ( 1 / ( G ` k ) ) ) = ( k e. Z \|-> ( 1 / ( G ` k ) ) )
21	20	fvmpt2	\|- ( ( k e. Z /\ ( 1 / ( G ` k ) ) e. CC ) -> ( ( k e. Z \|-> ( 1 / ( G ` k ) ) ) ` k ) = ( 1 / ( G ` k ) ) )
22	15 19 21	syl2anc	\|- ( ( ph /\ k e. Z ) -> ( ( k e. Z \|-> ( 1 / ( G ` k ) ) ) ` k ) = ( 1 / ( G ` k ) ) )
23	5	fvexi	\|- Z e. _V
24	23	mptex	\|- ( k e. Z \|-> ( 1 / ( G ` k ) ) ) e. _V
25	24	a1i	\|- ( ph -> ( k e. Z \|-> ( 1 / ( G ` k ) ) ) e. _V )
26	1 3 14 5 6 9 10 12 22 25	climrecf	\|- ( ph -> ( k e. Z \|-> ( 1 / ( G ` k ) ) ) ~~> ( 1 / B ) )
27	22 19	eqeltrd	\|- ( ( ph /\ k e. Z ) -> ( ( k e. Z \|-> ( 1 / ( G ` k ) ) ) ` k ) e. CC )
28	11 16 18	divrecd	\|- ( ( ph /\ k e. Z ) -> ( ( F ` k ) / ( G ` k ) ) = ( ( F ` k ) x. ( 1 / ( G ` k ) ) ) )
29	22	eqcomd	\|- ( ( ph /\ k e. Z ) -> ( 1 / ( G ` k ) ) = ( ( k e. Z \|-> ( 1 / ( G ` k ) ) ) ` k ) )
30	29	oveq2d	\|- ( ( ph /\ k e. Z ) -> ( ( F ` k ) x. ( 1 / ( G ` k ) ) ) = ( ( F ` k ) x. ( ( k e. Z \|-> ( 1 / ( G ` k ) ) ) ` k ) ) )
31	13 28 30	3eqtrd	\|- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) x. ( ( k e. Z \|-> ( 1 / ( G ` k ) ) ) ` k ) ) )
32	1 2 14 4 5 6 7 8 26 11 27 31	climmulf	\|- ( ph -> H ~~> ( A x. ( 1 / B ) ) )
33		climcl	\|- ( F ~~> A -> A e. CC )
34	7 33	syl	\|- ( ph -> A e. CC )
35		climcl	\|- ( G ~~> B -> B e. CC )
36	9 35	syl	\|- ( ph -> B e. CC )
37	34 36 10	divrecd	\|- ( ph -> ( A / B ) = ( A x. ( 1 / B ) ) )
38	32 37	breqtrrd	\|- ( ph -> H ~~> ( A / B ) )

Metamath Proof Explorer

Theorem climdivf

Proof