Theorem climrec

Description: Limit of the reciprocal of a converging sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	climrec.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climrec.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climrec.3	⊢ ( 𝜑 → 𝐺 ⇝ 𝐴 )
	climrec.4	⊢ ( 𝜑 → 𝐴 ≠ 0 )
	climrec.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ( ℂ ∖ { 0 } ) )
	climrec.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) )
	climrec.7	⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
Assertion	climrec	⊢ ( 𝜑 → 𝐻 ⇝ ( 1 / 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		climrec.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		climrec.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		climrec.3	⊢ ( 𝜑 → 𝐺 ⇝ 𝐴 )
4		climrec.4	⊢ ( 𝜑 → 𝐴 ≠ 0 )
5		climrec.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ( ℂ ∖ { 0 } ) )
6		climrec.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) )
7		climrec.7	⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
8		climcl	⊢ ( 𝐺 ⇝ 𝐴 → 𝐴 ∈ ℂ )
9	3 8	syl	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
10	4	neneqd	⊢ ( 𝜑 → ¬ 𝐴 = 0 )
11		c0ex	⊢ 0 ∈ V
12	11	elsn2	⊢ ( 𝐴 ∈ { 0 } ↔ 𝐴 = 0 )
13	10 12	sylnibr	⊢ ( 𝜑 → ¬ 𝐴 ∈ { 0 } )
14	9 13	eldifd	⊢ ( 𝜑 → 𝐴 ∈ ( ℂ ∖ { 0 } ) )
15		eqidd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) = ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) )
16		simpr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑤 = 𝑧 ) → 𝑤 = 𝑧 )
17	16	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑤 = 𝑧 ) → ( 1 / 𝑤 ) = ( 1 / 𝑧 ) )
18		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) → 𝑧 ∈ ( ℂ ∖ { 0 } ) )
19	18	eldifad	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) → 𝑧 ∈ ℂ )
20		eldifsni	⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → 𝑧 ≠ 0 )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) → 𝑧 ≠ 0 )
22	19 21	reccld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) → ( 1 / 𝑧 ) ∈ ℂ )
23	15 17 18 22	fvmptd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) = ( 1 / 𝑧 ) )
24	23 22	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) ∈ ℂ )
25		eqid	⊢ ( if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝑥 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝑥 ) ) · ( ( abs ‘ 𝐴 ) / 2 ) ) = ( if ( 1 ≤ ( ( abs ‘ 𝐴 ) · 𝑥 ) , 1 , ( ( abs ‘ 𝐴 ) · 𝑥 ) ) · ( ( abs ‘ 𝐴 ) / 2 ) )
26	25	reccn2	⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) )
27	14 26	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) )
28		eqidd	⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) = ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) )
29		simpr	⊢ ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 = 𝑧 ) → 𝑤 = 𝑧 )
30	29	oveq2d	⊢ ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 = 𝑧 ) → ( 1 / 𝑤 ) = ( 1 / 𝑧 ) )
31		id	⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → 𝑧 ∈ ( ℂ ∖ { 0 } ) )
32		eldifi	⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → 𝑧 ∈ ℂ )
33	32 20	reccld	⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( 1 / 𝑧 ) ∈ ℂ )
34	28 30 31 33	fvmptd	⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) = ( 1 / 𝑧 ) )
35	34	ad2antlr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) = ( 1 / 𝑧 ) )
36		eqidd	⊢ ( 𝜑 → ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) = ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) )
37		simpr	⊢ ( ( 𝜑 ∧ 𝑤 = 𝐴 ) → 𝑤 = 𝐴 )
38	37	oveq2d	⊢ ( ( 𝜑 ∧ 𝑤 = 𝐴 ) → ( 1 / 𝑤 ) = ( 1 / 𝐴 ) )
39	9 4	reccld	⊢ ( 𝜑 → ( 1 / 𝐴 ) ∈ ℂ )
40	36 38 14 39	fvmptd	⊢ ( 𝜑 → ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) = ( 1 / 𝐴 ) )
41	40	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) = ( 1 / 𝐴 ) )
42	35 41	oveq12d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → ( ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) − ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) ) = ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) )
43	42	fveq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → ( abs ‘ ( ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) − ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) ) ) = ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) )
44	31	ad2antlr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → 𝑧 ∈ ( ℂ ∖ { 0 } ) )
45		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 )
46		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) )
47	44 45 46	mp2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 )
48	43 47	eqbrtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) ) ∧ 𝑧 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ) → ( abs ‘ ( ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) − ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) ) ) < 𝑥 )
49	48	exp41	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) ) → ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) − ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) ) ) < 𝑥 ) ) ) )
50	49	ralimdv2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) → ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) − ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) ) ) < 𝑥 ) ) )
51	50	reximdv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 1 / 𝑧 ) − ( 1 / 𝐴 ) ) ) < 𝑥 ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) − ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) ) ) < 𝑥 ) ) )
52	27 51	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝑧 ) − ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) ) ) < 𝑥 ) )
53		eqidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) = ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) )
54		oveq2	⊢ ( 𝑤 = ( 𝐺 ‘ 𝑘 ) → ( 1 / 𝑤 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) )
55	54	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑤 = ( 𝐺 ‘ 𝑘 ) ) → ( 1 / 𝑤 ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) )
56	5	eldifad	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
57		eldifsni	⊢ ( ( 𝐺 ‘ 𝑘 ) ∈ ( ℂ ∖ { 0 } ) → ( 𝐺 ‘ 𝑘 ) ≠ 0 )
58	5 57	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ≠ 0 )
59	56 58	reccld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 1 / ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ )
60	53 55 5 59	fvmptd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 1 / ( 𝐺 ‘ 𝑘 ) ) )
61	6 60	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ ( 𝐺 ‘ 𝑘 ) ) )
62	1 2 14 24 3 7 52 5 61	climcn1	⊢ ( 𝜑 → 𝐻 ⇝ ( ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑤 ) ) ‘ 𝐴 ) )
63	62 40	breqtrd	⊢ ( 𝜑 → 𝐻 ⇝ ( 1 / 𝐴 ) )