xlimpnfvlem2

Description: Lemma for xlimpnfv : the "if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	xlimpnfvlem2.k	$⊢ Ⅎ k φ$
	xlimpnfvlem2.j	$⊢ Ⅎ j φ$
	xlimpnfvlem2.m	$⊢ φ \to M \in ℤ$
	xlimpnfvlem2.z	$⊢ Z = ℤ_{\geq M}$
	xlimpnfvlem2.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
	xlimpnfvlem2.g	$⊢ φ \to \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x < F (k)$
Assertion	xlimpnfvlem2	$⊢ φ \to F \underset{*}{⇝} +∞$

Proof

Step	Hyp	Ref	Expression
1		xlimpnfvlem2.k	$⊢ Ⅎ k φ$
2		xlimpnfvlem2.j	$⊢ Ⅎ j φ$
3		xlimpnfvlem2.m	$⊢ φ \to M \in ℤ$
4		xlimpnfvlem2.z	$⊢ Z = ℤ_{\geq M}$
5		xlimpnfvlem2.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
6		xlimpnfvlem2.g	$⊢ φ \to \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x < F (k)$
7		letopon	$⊢ ordTop (\leq) \in TopOn (ℝ^{*})$
8	7	a1i	$⊢ φ \to ordTop (\leq) \in TopOn (ℝ^{*})$
9	8	elfvexd	$⊢ φ \to ℝ^{*} \in V$
10		cnex	$⊢ ℂ \in V$
11	10	a1i	$⊢ φ \to ℂ \in V$
12	4	uzsscn2	$⊢ Z \subseteq ℂ$
13	12	a1i	$⊢ φ \to Z \subseteq ℂ$
14		elpm2r	$⊢ ((ℝ^{} \in V \land ℂ \in V) \land (F : Z ⟶ ℝ^{} \land Z \subseteq ℂ)) \to F \in (ℝ^{*} ↑_{𝑝𝑚} ℂ)$
15	9 11 5 13 14	syl22anc	$⊢ φ \to F \in (ℝ^{*} ↑_{𝑝𝑚} ℂ)$
16		pnfxr	$⊢ +∞ \in ℝ^{*}$
17	16	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
18		pnfnei	$⊢ (u \in ordTop (\leq) \land +∞ \in u) \to \exists x \in ℝ (x, +∞] \subseteq u$
19	18	adantll	$⊢ ((φ \land u \in ordTop (\leq)) \land +∞ \in u) \to \exists x \in ℝ (x, +∞] \subseteq u$
20		nfv	$⊢ Ⅎ j x \in ℝ$
21	2 20	nfan	$⊢ Ⅎ j (φ \land x \in ℝ)$
22		nfv	$⊢ Ⅎ j (x, +∞] \subseteq u$
23	21 22	nfan	$⊢ Ⅎ j ((φ \land x \in ℝ) \land (x, +∞] \subseteq u)$
24		simprr	$⊢ (((φ \land x \in ℝ) \land (x, +∞] \subseteq u) \land (j \in Z \land \forall k \in ℤ_{\geq j} x < F (k))) \to \forall k \in ℤ_{\geq j} x < F (k)$
25		nfv	$⊢ Ⅎ k x \in ℝ$
26	1 25	nfan	$⊢ Ⅎ k (φ \land x \in ℝ)$
27		nfv	$⊢ Ⅎ k (x, +∞] \subseteq u$
28	26 27	nfan	$⊢ Ⅎ k ((φ \land x \in ℝ) \land (x, +∞] \subseteq u)$
29		nfv	$⊢ Ⅎ k j \in Z$
30	28 29	nfan	$⊢ Ⅎ k (((φ \land x \in ℝ) \land (x, +∞] \subseteq u) \land j \in Z)$
31	4	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
32	31	3adant1	$⊢ (φ \land j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
33	5	fdmd	$⊢ φ \to dom F = Z$
34	33	3ad2ant1	$⊢ (φ \land j \in Z \land k \in ℤ_{\geq j}) \to dom F = Z$
35	32 34	eleqtrrd	$⊢ (φ \land j \in Z \land k \in ℤ_{\geq j}) \to k \in dom F$
36	35	ad5ant134	$⊢ ((((φ \land (x, +∞] \subseteq u) \land j \in Z) \land k \in ℤ_{\geq j}) \land x < F (k)) \to k \in dom F$
37	36	adantl4r	$⊢ (((((φ \land x \in ℝ) \land (x, +∞] \subseteq u) \land j \in Z) \land k \in ℤ_{\geq j}) \land x < F (k)) \to k \in dom F$
38		simp-4r	$⊢ ((((φ \land (x, +∞] \subseteq u) \land j \in Z) \land k \in ℤ_{\geq j}) \land x < F (k)) \to (x, +∞] \subseteq u$
39	38	adantl4r	$⊢ (((((φ \land x \in ℝ) \land (x, +∞] \subseteq u) \land j \in Z) \land k \in ℤ_{\geq j}) \land x < F (k)) \to (x, +∞] \subseteq u$
40		simp-4r	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land x < F (k)) \to x \in ℝ$
41		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
42	40 41	syl	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land x < F (k)) \to x \in ℝ^{*}$
43	16	a1i	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land x < F (k)) \to +∞ \in ℝ^{*}$
44		simp-4l	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land x < F (k)) \to φ$
45	31	ad4ant23	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land x < F (k)) \to k \in Z$
46	5	ffvelcdmda	$⊢ (φ \land k \in Z) \to F (k) \in ℝ^{*}$
47	44 45 46	syl2anc	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land x < F (k)) \to F (k) \in ℝ^{*}$
48		simpr	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land x < F (k)) \to x < F (k)$
49	5	3ad2ant1	$⊢ (φ \land j \in Z \land k \in ℤ_{\geq j}) \to F : Z ⟶ ℝ^{*}$
50	49 32	ffvelcdmd	$⊢ (φ \land j \in Z \land k \in ℤ_{\geq j}) \to F (k) \in ℝ^{*}$
51	50	pnfged	$⊢ (φ \land j \in Z \land k \in ℤ_{\geq j}) \to F (k) \leq +∞$
52	51	ad5ant134	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land x < F (k)) \to F (k) \leq +∞$
53	42 43 47 48 52	eliocd	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land x < F (k)) \to F (k) \in (x, +∞]$
54	53	adantl3r	$⊢ (((((φ \land x \in ℝ) \land (x, +∞] \subseteq u) \land j \in Z) \land k \in ℤ_{\geq j}) \land x < F (k)) \to F (k) \in (x, +∞]$
55	39 54	sseldd	$⊢ (((((φ \land x \in ℝ) \land (x, +∞] \subseteq u) \land j \in Z) \land k \in ℤ_{\geq j}) \land x < F (k)) \to F (k) \in u$
56	37 55	jca	$⊢ (((((φ \land x \in ℝ) \land (x, +∞] \subseteq u) \land j \in Z) \land k \in ℤ_{\geq j}) \land x < F (k)) \to (k \in dom F \land F (k) \in u)$
57	56	ex	$⊢ ((((φ \land x \in ℝ) \land (x, +∞] \subseteq u) \land j \in Z) \land k \in ℤ_{\geq j}) \to (x < F (k) \to (k \in dom F \land F (k) \in u))$
58	30 57	ralimdaa	$⊢ (((φ \land x \in ℝ) \land (x, +∞] \subseteq u) \land j \in Z) \to (\forall k \in ℤ_{\geq j} x < F (k) \to \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
59	58	adantrr	$⊢ (((φ \land x \in ℝ) \land (x, +∞] \subseteq u) \land (j \in Z \land \forall k \in ℤ_{\geq j} x < F (k))) \to (\forall k \in ℤ_{\geq j} x < F (k) \to \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
60	24 59	mpd	$⊢ (((φ \land x \in ℝ) \land (x, +∞] \subseteq u) \land (j \in Z \land \forall k \in ℤ_{\geq j} x < F (k))) \to \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)$
61	60	3impb	$⊢ (((φ \land x \in ℝ) \land (x, +∞] \subseteq u) \land j \in Z \land \forall k \in ℤ_{\geq j} x < F (k)) \to \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)$
62	6	r19.21bi	$⊢ (φ \land x \in ℝ) \to \exists j \in Z \forall k \in ℤ_{\geq j} x < F (k)$
63	62	adantr	$⊢ ((φ \land x \in ℝ) \land (x, +∞] \subseteq u) \to \exists j \in Z \forall k \in ℤ_{\geq j} x < F (k)$
64	23 61 63	reximdd	$⊢ ((φ \land x \in ℝ) \land (x, +∞] \subseteq u) \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)$
65	4	rexuz3	$⊢ M \in ℤ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
66	3 65	syl	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
67	66	ad2antrr	$⊢ ((φ \land x \in ℝ) \land (x, +∞] \subseteq u) \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
68	64 67	mpbid	$⊢ ((φ \land x \in ℝ) \land (x, +∞] \subseteq u) \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)$
69	68	rexlimdva2	$⊢ φ \to (\exists x \in ℝ (x, +∞] \subseteq u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
70	69	ad2antrr	$⊢ ((φ \land u \in ordTop (\leq)) \land +∞ \in u) \to (\exists x \in ℝ (x, +∞] \subseteq u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
71	19 70	mpd	$⊢ ((φ \land u \in ordTop (\leq)) \land +∞ \in u) \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)$
72	71	ex	$⊢ (φ \land u \in ordTop (\leq)) \to (+∞ \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
73	72	ralrimiva	$⊢ φ \to \forall u \in ordTop (\leq) (+∞ \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))$
74	15 17 73	3jca	$⊢ φ \to (F \in (ℝ^{} ↑_{𝑝𝑚} ℂ) \land +∞ \in ℝ^{} \land \forall u \in ordTop (\leq) (+∞ \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u)))$
75		nfcv	$⊢ \underline{Ⅎ} k F$
76	75 8	lmbr3	$⊢ φ \to (F \underset{t}{⇝} (ordTop (\leq)) +∞ \leftrightarrow (F \in (ℝ^{} ↑_{𝑝𝑚} ℂ) \land +∞ \in ℝ^{} \land \forall u \in ordTop (\leq) (+∞ \in u \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in u))))$
77	74 76	mpbird	$⊢ φ \to F \underset{t}{⇝} (ordTop (\leq)) +∞$
78		df-xlim	$⊢ \underset{*}{⇝} = \underset{t}{⇝} (ordTop (\leq))$
79	78	breqi	$⊢ F \underset{*}{⇝} +∞ \leftrightarrow F \underset{t}{⇝} (ordTop (\leq)) +∞$
80	79	a1i	$⊢ φ \to (F \underset{*}{⇝} +∞ \leftrightarrow F \underset{t}{⇝} (ordTop (\leq)) +∞)$
81	77 80	mpbird	$⊢ φ \to F \underset{*}{⇝} +∞$

Metamath Proof Explorer

Theorem xlimpnfvlem2

Proof