climleltrp

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

	Ref	Expression
Hypotheses	climleltrp.k	$⊢ Ⅎ k φ$
	climleltrp.f	$⊢ \underline{Ⅎ} k F$
	climleltrp.z	$⊢ Z = ℤ_{\geq M}$
	climleltrp.n	$⊢ φ \to N \in Z$
	climleltrp.r	$⊢ (φ \land k \in ℤ_{\geq N}) \to F (k) \in ℝ$
	climleltrp.a	$⊢ φ \to F ⇝ A$
	climleltrp.c	$⊢ φ \to C \in ℝ$
	climleltrp.l	$⊢ φ \to A \leq C$
	climleltrp.x	$⊢ φ \to X \in ℝ^{+}$
Assertion	climleltrp	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℝ \land F (k) < C + X)$

Proof

Step	Hyp	Ref	Expression
1		climleltrp.k	$⊢ Ⅎ k φ$
2		climleltrp.f	$⊢ \underline{Ⅎ} k F$
3		climleltrp.z	$⊢ Z = ℤ_{\geq M}$
4		climleltrp.n	$⊢ φ \to N \in Z$
5		climleltrp.r	$⊢ (φ \land k \in ℤ_{\geq N}) \to F (k) \in ℝ$
6		climleltrp.a	$⊢ φ \to F ⇝ A$
7		climleltrp.c	$⊢ φ \to C \in ℝ$
8		climleltrp.l	$⊢ φ \to A \leq C$
9		climleltrp.x	$⊢ φ \to X \in ℝ^{+}$
10	4 3	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq M}$
11		uzss	$⊢ N \in ℤ_{\geq M} \to ℤ_{\geq N} \subseteq ℤ_{\geq M}$
12	10 11	syl	$⊢ φ \to ℤ_{\geq N} \subseteq ℤ_{\geq M}$
13	12 3	sseqtrrdi	$⊢ φ \to ℤ_{\geq N} \subseteq Z$
14		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
15	14 10	sseldi	$⊢ φ \to N \in ℤ$
16		eqid	$⊢ ℤ_{\geq N} = ℤ_{\geq N}$
17		eqidd	$⊢ (φ \land k \in ℤ_{\geq N}) \to F (k) = F (k)$
18	1 2 15 16 6 17 9	clim2d	$⊢ φ \to \exists j \in ℤ_{\geq N} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X)$
19		nfv	$⊢ Ⅎ k j \in ℤ_{\geq N}$
20	1 19	nfan	$⊢ Ⅎ k (φ \land j \in ℤ_{\geq N})$
21		simplll	$⊢ (((φ \land j \in ℤ_{\geq N}) \land k \in ℤ_{\geq j}) \land \|F (k) - A\| < X) \to φ$
22		uzss	$⊢ j \in ℤ_{\geq N} \to ℤ_{\geq j} \subseteq ℤ_{\geq N}$
23	22	ad2antlr	$⊢ ((φ \land j \in ℤ_{\geq N}) \land k \in ℤ_{\geq j}) \to ℤ_{\geq j} \subseteq ℤ_{\geq N}$
24		simpr	$⊢ ((φ \land j \in ℤ_{\geq N}) \land k \in ℤ_{\geq j}) \to k \in ℤ_{\geq j}$
25	23 24	sseldd	$⊢ ((φ \land j \in ℤ_{\geq N}) \land k \in ℤ_{\geq j}) \to k \in ℤ_{\geq N}$
26	25	adantr	$⊢ (((φ \land j \in ℤ_{\geq N}) \land k \in ℤ_{\geq j}) \land \|F (k) - A\| < X) \to k \in ℤ_{\geq N}$
27		simpr	$⊢ (((φ \land j \in ℤ_{\geq N}) \land k \in ℤ_{\geq j}) \land \|F (k) - A\| < X) \to \|F (k) - A\| < X$
28	17 5	eqeltrd	$⊢ (φ \land k \in ℤ_{\geq N}) \to F (k) \in ℝ$
29	28	adantr	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to F (k) \in ℝ$
30		climcl	$⊢ F ⇝ A \to A \in ℂ$
31	6 30	syl	$⊢ φ \to A \in ℂ$
32	31	adantr	$⊢ (φ \land k \in ℤ_{\geq N}) \to A \in ℂ$
33	28	recnd	$⊢ (φ \land k \in ℤ_{\geq N}) \to F (k) \in ℂ$
34	32 33	pncan3d	$⊢ (φ \land k \in ℤ_{\geq N}) \to A + F (k) - A = F (k)$
35	34	eqcomd	$⊢ (φ \land k \in ℤ_{\geq N}) \to F (k) = A + F (k) - A$
36	35	adantr	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to F (k) = A + F (k) - A$
37	36 29	eqeltrrd	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to A + F (k) - A \in ℝ$
38	7	ad2antrr	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to C \in ℝ$
39	1 2 16 15 6 5	climreclf	$⊢ φ \to A \in ℝ$
40	39	ad2antrr	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to A \in ℝ$
41	29 40	resubcld	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to F (k) - A \in ℝ$
42	38 41	readdcld	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to C + F (k) - A \in ℝ$
43	9	rpred	$⊢ φ \to X \in ℝ$
44	43	ad2antrr	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to X \in ℝ$
45	38 44	readdcld	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to C + X \in ℝ$
46	8	ad2antrr	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to A \leq C$
47	40 38 41 46	leadd1dd	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to A + F (k) - A \leq C + F (k) - A$
48	33	adantr	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to F (k) \in ℂ$
49	32	adantr	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to A \in ℂ$
50	48 49	subcld	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to F (k) - A \in ℂ$
51	50	abscld	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to \|F (k) - A\| \in ℝ$
52	41	leabsd	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to F (k) - A \leq \|F (k) - A\|$
53		simpr	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to \|F (k) - A\| < X$
54	41 51 44 52 53	lelttrd	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to F (k) - A < X$
55	41 44 38 54	ltadd2dd	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to C + F (k) - A < C + X$
56	37 42 45 47 55	lelttrd	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to A + F (k) - A < C + X$
57	36 56	eqbrtrd	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to F (k) < C + X$
58	29 57	jca	$⊢ ((φ \land k \in ℤ_{\geq N}) \land \|F (k) - A\| < X) \to (F (k) \in ℝ \land F (k) < C + X)$
59	21 26 27 58	syl21anc	$⊢ (((φ \land j \in ℤ_{\geq N}) \land k \in ℤ_{\geq j}) \land \|F (k) - A\| < X) \to (F (k) \in ℝ \land F (k) < C + X)$
60	59	adantrl	$⊢ (((φ \land j \in ℤ_{\geq N}) \land k \in ℤ_{\geq j}) \land (F (k) \in ℂ \land \|F (k) - A\| < X)) \to (F (k) \in ℝ \land F (k) < C + X)$
61	60	ex	$⊢ ((φ \land j \in ℤ_{\geq N}) \land k \in ℤ_{\geq j}) \to ((F (k) \in ℂ \land \|F (k) - A\| < X) \to (F (k) \in ℝ \land F (k) < C + X))$
62	20 61	ralimdaa	$⊢ (φ \land j \in ℤ_{\geq N}) \to (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X) \to \forall k \in ℤ_{\geq j} (F (k) \in ℝ \land F (k) < C + X))$
63	62	reximdva	$⊢ φ \to (\exists j \in ℤ_{\geq N} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < X) \to \exists j \in ℤ_{\geq N} \forall k \in ℤ_{\geq j} (F (k) \in ℝ \land F (k) < C + X))$
64	18 63	mpd	$⊢ φ \to \exists j \in ℤ_{\geq N} \forall k \in ℤ_{\geq j} (F (k) \in ℝ \land F (k) < C + X)$
65		ssrexv	$⊢ ℤ_{\geq N} \subseteq Z \to (\exists j \in ℤ_{\geq N} \forall k \in ℤ_{\geq j} (F (k) \in ℝ \land F (k) < C + X) \to \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℝ \land F (k) < C + X))$
66	13 64 65	sylc	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℝ \land F (k) < C + X)$

Metamath Proof Explorer

Theorem climleltrp

Proof