climleltrp - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > climleltrp		Structured version Visualization version GIF version

Theorem climleltrp 45681

Description: The limit of complex number sequence 𝐹 is eventually approximated. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

**Hypotheses**
Ref	Expression
climleltrp.k	⊢ Ⅎ𝑘𝜑
climleltrp.f	⊢ Ⅎ𝑘𝐹
climleltrp.z	⊢ 𝑍 = (ℤ_≥‘𝑀)
climleltrp.n	⊢ (𝜑 → 𝑁 ∈ 𝑍)
climleltrp.r	⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑘) ∈ ℝ)
climleltrp.a	⊢ (𝜑 → 𝐹 ⇝ 𝐴)
climleltrp.c	⊢ (𝜑 → 𝐶 ∈ ℝ)
climleltrp.l	⊢ (𝜑 → 𝐴 ≤ 𝐶)
climleltrp.x	⊢ (𝜑 → 𝑋 ∈ ℝ⁺)

**Assertion**
Ref	Expression
climleltrp	⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)))

Distinct variable groups: 𝐴,𝑗,𝑘 𝑗,𝐹 𝑗,𝑁,𝑘 𝑗,𝑋,𝑘 𝑗,𝑍 𝜑,𝑗 Allowed substitution hints: 𝜑(𝑘) 𝐶(𝑗,𝑘) 𝐹(𝑘) 𝑀(𝑗,𝑘) 𝑍(𝑘)

**Proof of Theorem climleltrp**
Step	Hyp	Ref	Expression
1		climleltrp.n	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ 𝑍)
2		climleltrp.z	. . . . 5 ⊢ 𝑍 = (ℤ_≥‘𝑀)
3	1, 2	eleqtrdi 2839	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
4		uzss 12823	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (ℤ_≥‘𝑁) ⊆ (ℤ_≥‘𝑀))
5	3, 4	syl 17	. . 3 ⊢ (𝜑 → (ℤ_≥‘𝑁) ⊆ (ℤ_≥‘𝑀))
6	5, 2	sseqtrrdi 3991	. 2 ⊢ (𝜑 → (ℤ_≥‘𝑁) ⊆ 𝑍)
7		climleltrp.k	. . . 4 ⊢ Ⅎ𝑘𝜑
8		climleltrp.f	. . . 4 ⊢ Ⅎ𝑘𝐹
9		uzssz 12821	. . . . 5 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
10	9, 3	sselid 3947	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℤ)
11		eqid 2730	. . . 4 ⊢ (ℤ_≥‘𝑁) = (ℤ_≥‘𝑁)
12		climleltrp.a	. . . 4 ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
13		eqidd 2731	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑘) = (𝐹‘𝑘))
14		climleltrp.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℝ⁺)
15	7, 8, 10, 11, 12, 13, 14	clim2d 45678	. . 3 ⊢ (𝜑 → ∃𝑗 ∈ (ℤ_≥‘𝑁)∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋))
16		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑘 𝑗 ∈ (ℤ_≥‘𝑁)
17	7, 16	nfan 1899	. . . . 5 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁))
18		simplll 774	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝜑)
19		uzss 12823	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (ℤ_≥‘𝑁) → (ℤ_≥‘𝑗) ⊆ (ℤ_≥‘𝑁))
20	19	ad2antlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) → (ℤ_≥‘𝑗) ⊆ (ℤ_≥‘𝑁))
21		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) → 𝑘 ∈ (ℤ_≥‘𝑗))
22	20, 21	sseldd 3950	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) → 𝑘 ∈ (ℤ_≥‘𝑁))
23	22	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝑘 ∈ (ℤ_≥‘𝑁))
24		simpr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋)
25		climleltrp.r	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑘) ∈ ℝ)
26	13, 25	eqeltrd 2829	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑘) ∈ ℝ)
27	26	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐹‘𝑘) ∈ ℝ)
28		climcl 15472	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ)
29	12, 28	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ ℂ)
30	29	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → 𝐴 ∈ ℂ)
31	26	recnd 11209	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑘) ∈ ℂ)
32	30, 31	pncan3d 11543	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → (𝐴 + ((𝐹‘𝑘) − 𝐴)) = (𝐹‘𝑘))
33	32	eqcomd 2736	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑘) = (𝐴 + ((𝐹‘𝑘) − 𝐴)))
34	33	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐹‘𝑘) = (𝐴 + ((𝐹‘𝑘) − 𝐴)))
35	34, 27	eqeltrrd 2830	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐴 + ((𝐹‘𝑘) − 𝐴)) ∈ ℝ)
36		climleltrp.c	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ ℝ)
37	36	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝐶 ∈ ℝ)
38	7, 8, 11, 10, 12, 25	climreclf 45669	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ ℝ)
39	38	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝐴 ∈ ℝ)
40	27, 39	resubcld 11613	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) − 𝐴) ∈ ℝ)
41	37, 40	readdcld 11210	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐶 + ((𝐹‘𝑘) − 𝐴)) ∈ ℝ)
42	14	rpred 13002	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ ℝ)
43	42	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝑋 ∈ ℝ)
44	37, 43	readdcld 11210	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐶 + 𝑋) ∈ ℝ)
45		climleltrp.l	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ≤ 𝐶)
46	45	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝐴 ≤ 𝐶)
47	39, 37, 40, 46	leadd1dd 11799	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐴 + ((𝐹‘𝑘) − 𝐴)) ≤ (𝐶 + ((𝐹‘𝑘) − 𝐴)))
48	31	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐹‘𝑘) ∈ ℂ)
49	30	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝐴 ∈ ℂ)
50	48, 49	subcld 11540	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) − 𝐴) ∈ ℂ)
51	50	abscld 15412	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (abs‘((𝐹‘𝑘) − 𝐴)) ∈ ℝ)
52	40	leabsd 15388	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) − 𝐴) ≤ (abs‘((𝐹‘𝑘) − 𝐴)))
53		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋)
54	40, 51, 43, 52, 53	lelttrd 11339	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) − 𝐴) < 𝑋)
55	40, 43, 37, 54	ltadd2dd 11340	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐶 + ((𝐹‘𝑘) − 𝐴)) < (𝐶 + 𝑋))
56	35, 41, 44, 47, 55	lelttrd 11339	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐴 + ((𝐹‘𝑘) − 𝐴)) < (𝐶 + 𝑋))
57	34, 56	eqbrtrd 5132	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐹‘𝑘) < (𝐶 + 𝑋))
58	27, 57	jca 511	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)))
59	18, 23, 24, 58	syl21anc 837	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)))
60	59	adantrl 716	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) ∧ ((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋)) → ((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)))
61	60	ex 412	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) → (((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋))))
62	17, 61	ralimdaa 3239	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → (∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋))))
63	62	reximdva 3147	. . 3 ⊢ (𝜑 → (∃𝑗 ∈ (ℤ_≥‘𝑁)∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ∃𝑗 ∈ (ℤ_≥‘𝑁)∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋))))
64	15, 63	mpd 15	. 2 ⊢ (𝜑 → ∃𝑗 ∈ (ℤ_≥‘𝑁)∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)))
65		ssrexv 4019	. 2 ⊢ ((ℤ_≥‘𝑁) ⊆ 𝑍 → (∃𝑗 ∈ (ℤ_≥‘𝑁)∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋))))
66	6, 64, 65	sylc 65	1 ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 Ⅎwnf 1783 ∈ wcel 2109 Ⅎwnfc 2877 ∀wral 3045 ∃wrex 3054 ⊆ wss 3917 class class class wbr 5110 ‘cfv 6514 (class class class)co 7390 ℂcc 11073 ℝcr 11074 + caddc 11078 < clt 11215 ≤ cle 11216 − cmin 11412 ℤcz 12536 ℤ_≥cuz 12800 ℝ⁺crp 12958 abscabs 15207 ⇝ cli 15457

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7846 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-er 8674 df-pm 8805 df-en 8922 df-dom 8923 df-sdom 8924 df-sup 9400 df-inf 9401 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-div 11843 df-nn 12194 df-2 12256 df-3 12257 df-n0 12450 df-z 12537 df-uz 12801 df-rp 12959 df-fl 13761 df-seq 13974 df-exp 14034 df-cj 15072 df-re 15073 df-im 15074 df-sqrt 15208 df-abs 15209 df-clim 15461 df-rlim 15462

This theorem is referenced by: smflimlem2 46777

W3C validator