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 42743

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 2843	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
4		uzss 12340	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (ℤ_≥‘𝑁) ⊆ (ℤ_≥‘𝑀))
5	3, 4	syl 17	. . 3 ⊢ (𝜑 → (ℤ_≥‘𝑁) ⊆ (ℤ_≥‘𝑀))
6	5, 2	sseqtrrdi 3926	. 2 ⊢ (𝜑 → (ℤ_≥‘𝑁) ⊆ 𝑍)
7		climleltrp.k	. . . 4 ⊢ Ⅎ𝑘𝜑
8		climleltrp.f	. . . 4 ⊢ Ⅎ𝑘𝐹
9		uzssz 12338	. . . . 5 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
10	9, 3	sseldi 3873	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℤ)
11		eqid 2738	. . . 4 ⊢ (ℤ_≥‘𝑁) = (ℤ_≥‘𝑁)
12		climleltrp.a	. . . 4 ⊢ (𝜑 → 𝐹 ⇝ 𝐴)
13		eqidd 2739	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑘) = (𝐹‘𝑘))
14		climleltrp.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℝ⁺)
15	7, 8, 10, 11, 12, 13, 14	clim2d 42740	. . 3 ⊢ (𝜑 → ∃𝑗 ∈ (ℤ_≥‘𝑁)∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋))
16		nfv 1920	. . . . . 6 ⊢ Ⅎ𝑘 𝑗 ∈ (ℤ_≥‘𝑁)
17	7, 16	nfan 1905	. . . . 5 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁))
18		simplll 775	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝜑)
19		uzss 12340	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (ℤ_≥‘𝑁) → (ℤ_≥‘𝑗) ⊆ (ℤ_≥‘𝑁))
20	19	ad2antlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) → (ℤ_≥‘𝑗) ⊆ (ℤ_≥‘𝑁))
21		simpr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) → 𝑘 ∈ (ℤ_≥‘𝑗))
22	20, 21	sseldd 3876	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) → 𝑘 ∈ (ℤ_≥‘𝑁))
23	22	adantr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝑘 ∈ (ℤ_≥‘𝑁))
24		simpr 488	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋)
25		climleltrp.r	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑘) ∈ ℝ)
26	13, 25	eqeltrd 2833	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑘) ∈ ℝ)
27	26	adantr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐹‘𝑘) ∈ ℝ)
28		climcl 14939	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ)
29	12, 28	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ ℂ)
30	29	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → 𝐴 ∈ ℂ)
31	26	recnd 10740	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑘) ∈ ℂ)
32	30, 31	pncan3d 11071	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → (𝐴 + ((𝐹‘𝑘) − 𝐴)) = (𝐹‘𝑘))
33	32	eqcomd 2744	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) → (𝐹‘𝑘) = (𝐴 + ((𝐹‘𝑘) − 𝐴)))
34	33	adantr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐹‘𝑘) = (𝐴 + ((𝐹‘𝑘) − 𝐴)))
35	34, 27	eqeltrrd 2834	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐴 + ((𝐹‘𝑘) − 𝐴)) ∈ ℝ)
36		climleltrp.c	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ ℝ)
37	36	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝐶 ∈ ℝ)
38	7, 8, 11, 10, 12, 25	climreclf 42731	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ ℝ)
39	38	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝐴 ∈ ℝ)
40	27, 39	resubcld 11139	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) − 𝐴) ∈ ℝ)
41	37, 40	readdcld 10741	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐶 + ((𝐹‘𝑘) − 𝐴)) ∈ ℝ)
42	14	rpred 12507	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ ℝ)
43	42	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝑋 ∈ ℝ)
44	37, 43	readdcld 10741	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐶 + 𝑋) ∈ ℝ)
45		climleltrp.l	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ≤ 𝐶)
46	45	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝐴 ≤ 𝐶)
47	39, 37, 40, 46	leadd1dd 11325	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐴 + ((𝐹‘𝑘) − 𝐴)) ≤ (𝐶 + ((𝐹‘𝑘) − 𝐴)))
48	31	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐹‘𝑘) ∈ ℂ)
49	30	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → 𝐴 ∈ ℂ)
50	48, 49	subcld 11068	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) − 𝐴) ∈ ℂ)
51	50	abscld 14879	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (abs‘((𝐹‘𝑘) − 𝐴)) ∈ ℝ)
52	40	leabsd 14857	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) − 𝐴) ≤ (abs‘((𝐹‘𝑘) − 𝐴)))
53		simpr 488	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋)
54	40, 51, 43, 52, 53	lelttrd 10869	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) − 𝐴) < 𝑋)
55	40, 43, 37, 54	ltadd2dd 10870	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐶 + ((𝐹‘𝑘) − 𝐴)) < (𝐶 + 𝑋))
56	35, 41, 44, 47, 55	lelttrd 10869	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐴 + ((𝐹‘𝑘) − 𝐴)) < (𝐶 + 𝑋))
57	34, 56	eqbrtrd 5049	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → (𝐹‘𝑘) < (𝐶 + 𝑋))
58	27, 57	jca 515	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑁)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)))
59	18, 23, 24, 58	syl21anc 837	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)))
60	59	adantrl 716	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) ∧ ((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋)) → ((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)))
61	60	ex 416	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) ∧ 𝑘 ∈ (ℤ_≥‘𝑗)) → (((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋))))
62	17, 61	ralimdaa 3128	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑁)) → (∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋))))
63	62	reximdva 3183	. . 3 ⊢ (𝜑 → (∃𝑗 ∈ (ℤ_≥‘𝑁)∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℂ ∧ (abs‘((𝐹‘𝑘) − 𝐴)) < 𝑋) → ∃𝑗 ∈ (ℤ_≥‘𝑁)∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋))))
64	15, 63	mpd 15	. 2 ⊢ (𝜑 → ∃𝑗 ∈ (ℤ_≥‘𝑁)∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)))
65		ssrexv 3942	. 2 ⊢ ((ℤ_≥‘𝑁) ⊆ 𝑍 → (∃𝑗 ∈ (ℤ_≥‘𝑁)∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋))))
66	6, 64, 65	sylc 65	1 ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ_≥‘𝑗)((𝐹‘𝑘) ∈ ℝ ∧ (𝐹‘𝑘) < (𝐶 + 𝑋)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 = wceq 1542 Ⅎwnf 1790 ∈ wcel 2113 Ⅎwnfc 2879 ∀wral 3053 ∃wrex 3054 ⊆ wss 3841 class class class wbr 5027 ‘cfv 6333 (class class class)co 7164 ℂcc 10606 ℝcr 10607 + caddc 10611 < clt 10746 ≤ cle 10747 − cmin 10941 ℤcz 12055 ℤ_≥cuz 12317 ℝ⁺crp 12465 abscabs 14676 ⇝ cli 14924

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-rep 5151 ax-sep 5164 ax-nul 5171 ax-pow 5229 ax-pr 5293 ax-un 7473 ax-cnex 10664 ax-resscn 10665 ax-1cn 10666 ax-icn 10667 ax-addcl 10668 ax-addrcl 10669 ax-mulcl 10670 ax-mulrcl 10671 ax-mulcom 10672 ax-addass 10673 ax-mulass 10674 ax-distr 10675 ax-i2m1 10676 ax-1ne0 10677 ax-1rid 10678 ax-rnegex 10679 ax-rrecex 10680 ax-cnre 10681 ax-pre-lttri 10682 ax-pre-lttrn 10683 ax-pre-ltadd 10684 ax-pre-mulgt0 10685 ax-pre-sup 10686

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3399 df-sbc 3680 df-csb 3789 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-pss 3860 df-nul 4210 df-if 4412 df-pw 4487 df-sn 4514 df-pr 4516 df-tp 4518 df-op 4520 df-uni 4794 df-iun 4880 df-br 5028 df-opab 5090 df-mpt 5108 df-tr 5134 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6123 df-ord 6169 df-on 6170 df-lim 6171 df-suc 6172 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-f1 6338 df-fo 6339 df-f1o 6340 df-fv 6341 df-riota 7121 df-ov 7167 df-oprab 7168 df-mpo 7169 df-om 7594 df-2nd 7708 df-wrecs 7969 df-recs 8030 df-rdg 8068 df-er 8313 df-pm 8433 df-en 8549 df-dom 8550 df-sdom 8551 df-sup 8972 df-inf 8973 df-pnf 10748 df-mnf 10749 df-xr 10750 df-ltxr 10751 df-le 10752 df-sub 10943 df-neg 10944 df-div 11369 df-nn 11710 df-2 11772 df-3 11773 df-n0 11970 df-z 12056 df-uz 12318 df-rp 12466 df-fl 13246 df-seq 13454 df-exp 13515 df-cj 14541 df-re 14542 df-im 14543 df-sqrt 14677 df-abs 14678 df-clim 14928 df-rlim 14929

This theorem is referenced by: smflimlem2 43830

W3C validator