dfxlim2v

Description: An alternative definition for the convergence relation in the extended real numbers. This resembles what's found in most textbooks: three distinct definitions for the same symbol (limit of a sequence). (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	dfxlim2v.1	$⊢ φ \to M \in ℤ$
	dfxlim2v.2	$⊢ Z = ℤ_{\geq M}$
	dfxlim2v.3	$⊢ φ \to F : Z ⟶ ℝ^{*}$
Assertion	dfxlim2v	$⊢ φ \to (F \underset{*}{⇝} A \leftrightarrow (F ⇝ A \lor (A = −∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \lor (A = +∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k))))$

Proof

Step	Hyp	Ref	Expression
1		dfxlim2v.1	$⊢ φ \to M \in ℤ$
2		dfxlim2v.2	$⊢ Z = ℤ_{\geq M}$
3		dfxlim2v.3	$⊢ φ \to F : Z ⟶ ℝ^{*}$
4		simplr	$⊢ ((φ \land F \underset{}{⇝} A) \land A \in ℝ) \to F \underset{}{⇝} A$
5	1	adantr	$⊢ (φ \land A \in ℝ) \to M \in ℤ$
6	3	adantr	$⊢ (φ \land A \in ℝ) \to F : Z ⟶ ℝ^{*}$
7		simpr	$⊢ (φ \land A \in ℝ) \to A \in ℝ$
8	5 2 6 7	xlimclim2	$⊢ (φ \land A \in ℝ) \to (F \underset{*}{⇝} A \leftrightarrow F ⇝ A)$
9	8	adantlr	$⊢ ((φ \land F \underset{}{⇝} A) \land A \in ℝ) \to (F \underset{}{⇝} A \leftrightarrow F ⇝ A)$
10	4 9	mpbid	$⊢ ((φ \land F \underset{*}{⇝} A) \land A \in ℝ) \to F ⇝ A$
11	10	3mix1d	$⊢ ((φ \land F \underset{*}{⇝} A) \land A \in ℝ) \to (F ⇝ A \lor (A = −∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \lor (A = +∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)))$
12		simpr	$⊢ ((φ \land F \underset{*}{⇝} A) \land A = −∞) \to A = −∞$
13		simpl	$⊢ (F \underset{}{⇝} A \land A = −∞) \to F \underset{}{⇝} A$
14		simpr	$⊢ (F \underset{*}{⇝} A \land A = −∞) \to A = −∞$
15	13 14	breqtrd	$⊢ (F \underset{}{⇝} A \land A = −∞) \to F \underset{}{⇝} −∞$
16	15	adantll	$⊢ ((φ \land F \underset{}{⇝} A) \land A = −∞) \to F \underset{}{⇝} −∞$
17		nfcv	$⊢ \underline{Ⅎ} k F$
18	17 1 2 3	xlimmnf	$⊢ φ \to (F \underset{*}{⇝} −∞ \leftrightarrow \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x)$
19	18	ad2antrr	$⊢ ((φ \land F \underset{}{⇝} A) \land A = −∞) \to (F \underset{}{⇝} −∞ \leftrightarrow \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x)$
20	16 19	mpbid	$⊢ ((φ \land F \underset{*}{⇝} A) \land A = −∞) \to \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x$
21		3mix2	$⊢ (A = −∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \to (F ⇝ A \lor (A = −∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \lor (A = +∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)))$
22	12 20 21	syl2anc	$⊢ ((φ \land F \underset{*}{⇝} A) \land A = −∞) \to (F ⇝ A \lor (A = −∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \lor (A = +∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)))$
23	22	adantlr	$⊢ (((φ \land F \underset{*}{⇝} A) \land \neg A \in ℝ) \land A = −∞) \to (F ⇝ A \lor (A = −∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \lor (A = +∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)))$
24		simpll	$⊢ (((φ \land F \underset{}{⇝} A) \land \neg A \in ℝ) \land \neg A = −∞) \to (φ \land F \underset{}{⇝} A)$
25		xlimcl	$⊢ F \underset{}{⇝} A \to A \in ℝ^{}$
26	25	ad3antlr	$⊢ (((φ \land F \underset{}{⇝} A) \land \neg A \in ℝ) \land \neg A = −∞) \to A \in ℝ^{}$
27		simplr	$⊢ (((φ \land F \underset{*}{⇝} A) \land \neg A \in ℝ) \land \neg A = −∞) \to \neg A \in ℝ$
28		neqne	$⊢ \neg A = −∞ \to A \neq −∞$
29	28	adantl	$⊢ (((φ \land F \underset{*}{⇝} A) \land \neg A \in ℝ) \land \neg A = −∞) \to A \neq −∞$
30	26 27 29	xrnmnfpnf	$⊢ (((φ \land F \underset{*}{⇝} A) \land \neg A \in ℝ) \land \neg A = −∞) \to A = +∞$
31		simpr	$⊢ ((φ \land F \underset{*}{⇝} A) \land A = +∞) \to A = +∞$
32		simpl	$⊢ (F \underset{}{⇝} A \land A = +∞) \to F \underset{}{⇝} A$
33		simpr	$⊢ (F \underset{*}{⇝} A \land A = +∞) \to A = +∞$
34	32 33	breqtrd	$⊢ (F \underset{}{⇝} A \land A = +∞) \to F \underset{}{⇝} +∞$
35	34	adantll	$⊢ ((φ \land F \underset{}{⇝} A) \land A = +∞) \to F \underset{}{⇝} +∞$
36	17 1 2 3	xlimpnf	$⊢ φ \to (F \underset{*}{⇝} +∞ \leftrightarrow \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k))$
37	36	ad2antrr	$⊢ ((φ \land F \underset{}{⇝} A) \land A = +∞) \to (F \underset{}{⇝} +∞ \leftrightarrow \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k))$
38	35 37	mpbid	$⊢ ((φ \land F \underset{*}{⇝} A) \land A = +∞) \to \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)$
39		3mix3	$⊢ (A = +∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)) \to (F ⇝ A \lor (A = −∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \lor (A = +∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)))$
40	31 38 39	syl2anc	$⊢ ((φ \land F \underset{*}{⇝} A) \land A = +∞) \to (F ⇝ A \lor (A = −∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \lor (A = +∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)))$
41	24 30 40	syl2anc	$⊢ (((φ \land F \underset{*}{⇝} A) \land \neg A \in ℝ) \land \neg A = −∞) \to (F ⇝ A \lor (A = −∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \lor (A = +∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)))$
42	23 41	pm2.61dan	$⊢ ((φ \land F \underset{*}{⇝} A) \land \neg A \in ℝ) \to (F ⇝ A \lor (A = −∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \lor (A = +∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)))$
43	11 42	pm2.61dan	$⊢ (φ \land F \underset{*}{⇝} A) \to (F ⇝ A \lor (A = −∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \lor (A = +∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)))$
44	1	adantr	$⊢ (φ \land F ⇝ A) \to M \in ℤ$
45	3	adantr	$⊢ (φ \land F ⇝ A) \to F : Z ⟶ ℝ^{*}$
46		simpr	$⊢ (φ \land F ⇝ A) \to F ⇝ A$
47	44 2 45 46	climxlim2	$⊢ (φ \land F ⇝ A) \to F \underset{*}{⇝} A$
48	18	biimpar	$⊢ (φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \to F \underset{*}{⇝} −∞$
49	48	adantrl	$⊢ (φ \land (A = −∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x)) \to F \underset{*}{⇝} −∞$
50		simprl	$⊢ (φ \land (A = −∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x)) \to A = −∞$
51	49 50	breqtrrd	$⊢ (φ \land (A = −∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x)) \to F \underset{*}{⇝} A$
52	36	biimpar	$⊢ (φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)) \to F \underset{*}{⇝} +∞$
53	52	adantrl	$⊢ (φ \land (A = +∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k))) \to F \underset{*}{⇝} +∞$
54		simprl	$⊢ (φ \land (A = +∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k))) \to A = +∞$
55	53 54	breqtrrd	$⊢ (φ \land (A = +∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k))) \to F \underset{*}{⇝} A$
56	47 51 55	3jaodan	$⊢ (φ \land (F ⇝ A \lor (A = −∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \lor (A = +∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)))) \to F \underset{*}{⇝} A$
57	43 56	impbida	$⊢ φ \to (F \underset{*}{⇝} A \leftrightarrow (F ⇝ A \lor (A = −∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \lor (A = +∞ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k))))$

Metamath Proof Explorer

Theorem dfxlim2v

Proof