climxlim2lem

Description: In this lemma for climxlim2 there is the additional assumption that the converging function is complex-valued on the whole domain. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	climxlim2lem.1	$⊢ φ \to M \in ℤ$
	climxlim2lem.2	$⊢ Z = ℤ_{\geq M}$
	climxlim2lem.3	$⊢ φ \to F : Z ⟶ ℝ^{*}$
	climxlim2lem.4	$⊢ φ \to F : Z ⟶ ℂ$
	climxlim2lem.5	$⊢ φ \to F ⇝ A$
Assertion	climxlim2lem	$⊢ φ \to F \underset{*}{⇝} A$

Proof

Step	Hyp	Ref	Expression
1		climxlim2lem.1	$⊢ φ \to M \in ℤ$
2		climxlim2lem.2	$⊢ Z = ℤ_{\geq M}$
3		climxlim2lem.3	$⊢ φ \to F : Z ⟶ ℝ^{*}$
4		climxlim2lem.4	$⊢ φ \to F : Z ⟶ ℂ$
5		climxlim2lem.5	$⊢ φ \to F ⇝ A$
6	5	adantr	$⊢ (φ \land A \in ℝ) \to F ⇝ A$
7	1	adantr	$⊢ (φ \land A \in ℝ) \to M \in ℤ$
8	3	adantr	$⊢ (φ \land A \in ℝ) \to F : Z ⟶ ℝ^{*}$
9		simpr	$⊢ (φ \land A \in ℝ) \to A \in ℝ$
10	7 2 8 9	xlimclim2	$⊢ (φ \land A \in ℝ) \to (F \underset{*}{⇝} A \leftrightarrow F ⇝ A)$
11	6 10	mpbird	$⊢ (φ \land A \in ℝ) \to F \underset{*}{⇝} A$
12	4	ffvelrnda	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
13	12	anim1i	$⊢ ((φ \land k \in Z) \land F (k) \neq A) \to (F (k) \in ℂ \land F (k) \neq A)$
14	13	adantllr	$⊢ (((φ \land \forall y \in ℝ^{*} ((y \in ℂ \land y \neq A) \to x \leq \|y - A\|)) \land k \in Z) \land F (k) \neq A) \to (F (k) \in ℂ \land F (k) \neq A)$
15	3	adantr	$⊢ (φ \land \forall y \in ℝ^{} ((y \in ℂ \land y \neq A) \to x \leq \|y - A\|)) \to F : Z ⟶ ℝ^{}$
16	15	ffvelrnda	$⊢ ((φ \land \forall y \in ℝ^{} ((y \in ℂ \land y \neq A) \to x \leq \|y - A\|)) \land k \in Z) \to F (k) \in ℝ^{}$
17		simplr	$⊢ ((φ \land \forall y \in ℝ^{} ((y \in ℂ \land y \neq A) \to x \leq \|y - A\|)) \land k \in Z) \to \forall y \in ℝ^{} ((y \in ℂ \land y \neq A) \to x \leq \|y - A\|)$
18		eleq1	$⊢ y = F (k) \to (y \in ℂ \leftrightarrow F (k) \in ℂ)$
19		neeq1	$⊢ y = F (k) \to (y \neq A \leftrightarrow F (k) \neq A)$
20	18 19	anbi12d	$⊢ y = F (k) \to ((y \in ℂ \land y \neq A) \leftrightarrow (F (k) \in ℂ \land F (k) \neq A))$
21		fvoveq1	$⊢ y = F (k) \to \|y - A\| = \|F (k) - A\|$
22	21	breq2d	$⊢ y = F (k) \to (x \leq \|y - A\| \leftrightarrow x \leq \|F (k) - A\|)$
23	20 22	imbi12d	$⊢ y = F (k) \to (((y \in ℂ \land y \neq A) \to x \leq \|y - A\|) \leftrightarrow ((F (k) \in ℂ \land F (k) \neq A) \to x \leq \|F (k) - A\|))$
24	23	rspcva	$⊢ (F (k) \in ℝ^{} \land \forall y \in ℝ^{} ((y \in ℂ \land y \neq A) \to x \leq \|y - A\|)) \to ((F (k) \in ℂ \land F (k) \neq A) \to x \leq \|F (k) - A\|)$
25	16 17 24	syl2anc	$⊢ ((φ \land \forall y \in ℝ^{*} ((y \in ℂ \land y \neq A) \to x \leq \|y - A\|)) \land k \in Z) \to ((F (k) \in ℂ \land F (k) \neq A) \to x \leq \|F (k) - A\|)$
26	25	adantr	$⊢ (((φ \land \forall y \in ℝ^{*} ((y \in ℂ \land y \neq A) \to x \leq \|y - A\|)) \land k \in Z) \land F (k) \neq A) \to ((F (k) \in ℂ \land F (k) \neq A) \to x \leq \|F (k) - A\|)$
27	14 26	mpd	$⊢ (((φ \land \forall y \in ℝ^{*} ((y \in ℂ \land y \neq A) \to x \leq \|y - A\|)) \land k \in Z) \land F (k) \neq A) \to x \leq \|F (k) - A\|$
28	27	ex	$⊢ ((φ \land \forall y \in ℝ^{*} ((y \in ℂ \land y \neq A) \to x \leq \|y - A\|)) \land k \in Z) \to (F (k) \neq A \to x \leq \|F (k) - A\|)$
29	28	ralrimiva	$⊢ (φ \land \forall y \in ℝ^{*} ((y \in ℂ \land y \neq A) \to x \leq \|y - A\|)) \to \forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|)$
30	29	ad4ant14	$⊢ (((φ \land \neg A \in ℝ) \land x \in ℝ^{+}) \land \forall y \in ℝ^{*} ((y \in ℂ \land y \neq A) \to x \leq \|y - A\|)) \to \forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|)$
31		climcl	$⊢ F ⇝ A \to A \in ℂ$
32	5 31	syl	$⊢ φ \to A \in ℂ$
33	32	adantr	$⊢ (φ \land \neg A \in ℝ) \to A \in ℂ$
34		simpr	$⊢ (φ \land \neg A \in ℝ) \to \neg A \in ℝ$
35		prfi	$⊢ \{+∞, −∞\} \in Fin$
36	35	a1i	$⊢ (φ \land \neg A \in ℝ) \to \{+∞, −∞\} \in Fin$
37		df-xr	$⊢ ℝ^{*} = ℝ \cup \{+∞, −∞\}$
38	33 34 36 37	cnrefiisp	$⊢ (φ \land \neg A \in ℝ) \to \exists x \in ℝ^{+} \forall y \in ℝ^{*} ((y \in ℂ \land y \neq A) \to x \leq \|y - A\|)$
39	30 38	reximddv3	$⊢ (φ \land \neg A \in ℝ) \to \exists x \in ℝ^{+} \forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|)$
40		nfv	$⊢ Ⅎ k (φ \land x \in ℝ^{+})$
41		nfra1	$⊢ Ⅎ k \forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|)$
42	40 41	nfan	$⊢ Ⅎ k ((φ \land x \in ℝ^{+}) \land \forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|))$
43		nfv	$⊢ Ⅎ k j \in Z$
44	42 43	nfan	$⊢ Ⅎ k (((φ \land x \in ℝ^{+}) \land \forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|)) \land j \in Z)$
45		nfra1	$⊢ Ⅎ k \forall k \in ℤ_{\geq j} \|F (k) - A\| < x$
46	44 45	nfan	$⊢ Ⅎ k ((((φ \land x \in ℝ^{+}) \land \forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|)) \land j \in Z) \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x)$
47		simpll	$⊢ ((\forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|) \land j \in Z) \land k \in ℤ_{\geq j}) \to \forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|)$
48	2	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
49	48	adantll	$⊢ ((\forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|) \land j \in Z) \land k \in ℤ_{\geq j}) \to k \in Z$
50		rspa	$⊢ (\forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|) \land k \in Z) \to (F (k) \neq A \to x \leq \|F (k) - A\|)$
51	47 49 50	syl2anc	$⊢ ((\forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|) \land j \in Z) \land k \in ℤ_{\geq j}) \to (F (k) \neq A \to x \leq \|F (k) - A\|)$
52		neqne	$⊢ \neg F (k) = A \to F (k) \neq A$
53	51 52	impel	$⊢ (((\forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|) \land j \in Z) \land k \in ℤ_{\geq j}) \land \neg F (k) = A) \to x \leq \|F (k) - A\|$
54	53	ad5ant2345	$⊢ (((((φ \land x \in ℝ^{+}) \land \forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|)) \land j \in Z) \land k \in ℤ_{\geq j}) \land \neg F (k) = A) \to x \leq \|F (k) - A\|$
55	54	adantllr	$⊢ ((((((φ \land x \in ℝ^{+}) \land \forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|)) \land j \in Z) \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \land k \in ℤ_{\geq j}) \land \neg F (k) = A) \to x \leq \|F (k) - A\|$
56		rspa	$⊢ (\forall k \in ℤ_{\geq j} \|F (k) - A\| < x \land k \in ℤ_{\geq j}) \to \|F (k) - A\| < x$
57	56	adantll	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \land k \in ℤ_{\geq j}) \to \|F (k) - A\| < x$
58	4	ad2antrr	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to F : Z ⟶ ℂ$
59	48	adantll	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to k \in Z$
60	58 59	ffvelrnd	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to F (k) \in ℂ$
61	60	adantlr	$⊢ (((φ \land j \in Z) \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \land k \in ℤ_{\geq j}) \to F (k) \in ℂ$
62	32	ad3antrrr	$⊢ (((φ \land j \in Z) \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \land k \in ℤ_{\geq j}) \to A \in ℂ$
63	61 62	subcld	$⊢ (((φ \land j \in Z) \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \land k \in ℤ_{\geq j}) \to F (k) - A \in ℂ$
64	63	abscld	$⊢ (((φ \land j \in Z) \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \land k \in ℤ_{\geq j}) \to \|F (k) - A\| \in ℝ$
65	64	adantl3r	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \land k \in ℤ_{\geq j}) \to \|F (k) - A\| \in ℝ$
66		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
67	66	ad3antrrr	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \land k \in ℤ_{\geq j}) \to x \in ℝ^{+}$
68	67	rpred	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \land k \in ℤ_{\geq j}) \to x \in ℝ$
69	65 68	ltnled	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \land k \in ℤ_{\geq j}) \to (\|F (k) - A\| < x \leftrightarrow \neg x \leq \|F (k) - A\|)$
70	57 69	mpbid	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \land k \in ℤ_{\geq j}) \to \neg x \leq \|F (k) - A\|$
71	70	adantl3r	$⊢ (((((φ \land x \in ℝ^{+}) \land \forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|)) \land j \in Z) \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \land k \in ℤ_{\geq j}) \to \neg x \leq \|F (k) - A\|$
72	71	adantr	$⊢ ((((((φ \land x \in ℝ^{+}) \land \forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|)) \land j \in Z) \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \land k \in ℤ_{\geq j}) \land \neg F (k) = A) \to \neg x \leq \|F (k) - A\|$
73	55 72	condan	$⊢ (((((φ \land x \in ℝ^{+}) \land \forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|)) \land j \in Z) \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \land k \in ℤ_{\geq j}) \to F (k) = A$
74	46 73	ralrimia	$⊢ ((((φ \land x \in ℝ^{+}) \land \forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|)) \land j \in Z) \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \to \forall k \in ℤ_{\geq j} F (k) = A$
75		nfcv	$⊢ \underline{Ⅎ} k F$
76	75 1 2 4	climuz	$⊢ φ \to (F ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x))$
77	5 76	mpbid	$⊢ φ \to (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x)$
78	77	simprd	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x$
79	78	r19.21bi	$⊢ (φ \land x \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x$
80	79	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land \forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|)) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x$
81	74 80	reximddv3	$⊢ ((φ \land x \in ℝ^{+}) \land \forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|)) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) = A$
82	81	adantllr	$⊢ (((φ \land \neg A \in ℝ) \land x \in ℝ^{+}) \land \forall k \in Z (F (k) \neq A \to x \leq \|F (k) - A\|)) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) = A$
83	39 82	rexlimddv2	$⊢ (φ \land \neg A \in ℝ) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) = A$
84		nfv	$⊢ Ⅎ k ((φ \land \neg A \in ℝ) \land j \in Z)$
85		nfra1	$⊢ Ⅎ k \forall k \in ℤ_{\geq j} F (k) = A$
86	84 85	nfan	$⊢ Ⅎ k (((φ \land \neg A \in ℝ) \land j \in Z) \land \forall k \in ℤ_{\geq j} F (k) = A)$
87	3	ad3antrrr	$⊢ (((φ \land \neg A \in ℝ) \land j \in Z) \land \forall k \in ℤ_{\geq j} F (k) = A) \to F : Z ⟶ ℝ^{*}$
88		simplr	$⊢ (((φ \land \neg A \in ℝ) \land j \in Z) \land \forall k \in ℤ_{\geq j} F (k) = A) \to j \in Z$
89	2	uzid3	$⊢ j \in Z \to j \in ℤ_{\geq j}$
90		fveq2	$⊢ k = j \to F (k) = F (j)$
91	90	eqeq1d	$⊢ k = j \to (F (k) = A \leftrightarrow F (j) = A)$
92	91	rspcva	$⊢ (j \in ℤ_{\geq j} \land \forall k \in ℤ_{\geq j} F (k) = A) \to F (j) = A$
93	89 92	sylan	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} F (k) = A) \to F (j) = A$
94	93	3adant1	$⊢ (φ \land j \in Z \land \forall k \in ℤ_{\geq j} F (k) = A) \to F (j) = A$
95	3	ffvelrnda	$⊢ (φ \land j \in Z) \to F (j) \in ℝ^{*}$
96	95	3adant3	$⊢ (φ \land j \in Z \land \forall k \in ℤ_{\geq j} F (k) = A) \to F (j) \in ℝ^{*}$
97	94 96	eqeltrrd	$⊢ (φ \land j \in Z \land \forall k \in ℤ_{\geq j} F (k) = A) \to A \in ℝ^{*}$
98	97	ad4ant134	$⊢ (((φ \land \neg A \in ℝ) \land j \in Z) \land \forall k \in ℤ_{\geq j} F (k) = A) \to A \in ℝ^{*}$
99		rspa	$⊢ (\forall k \in ℤ_{\geq j} F (k) = A \land k \in ℤ_{\geq j}) \to F (k) = A$
100	99	adantll	$⊢ ((((φ \land \neg A \in ℝ) \land j \in Z) \land \forall k \in ℤ_{\geq j} F (k) = A) \land k \in ℤ_{\geq j}) \to F (k) = A$
101	86 75 2 87 88 98 100	xlimconst2	$⊢ (((φ \land \neg A \in ℝ) \land j \in Z) \land \forall k \in ℤ_{\geq j} F (k) = A) \to F \underset{*}{⇝} A$
102	83 101	rexlimddv2	$⊢ (φ \land \neg A \in ℝ) \to F \underset{*}{⇝} A$
103	11 102	pm2.61dan	$⊢ φ \to F \underset{*}{⇝} A$

Metamath Proof Explorer

Theorem climxlim2lem

Proof