xlimpnfv

Description: A function converges to plus infinity if it eventually becomes (and stays) larger than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022)

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

Proof

Step	Hyp	Ref	Expression
1		xlimpnfv.m	$⊢ φ \to M \in ℤ$
2		xlimpnfv.z	$⊢ Z = ℤ_{\geq M}$
3		xlimpnfv.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
4	1	ad2antrr	$⊢ ((φ \land F \underset{*}{⇝} +∞) \land x \in ℝ) \to M \in ℤ$
5	3	ad2antrr	$⊢ ((φ \land F \underset{}{⇝} +∞) \land x \in ℝ) \to F : Z ⟶ ℝ^{}$
6		simplr	$⊢ ((φ \land F \underset{}{⇝} +∞) \land x \in ℝ) \to F \underset{}{⇝} +∞$
7		simpr	$⊢ ((φ \land F \underset{*}{⇝} +∞) \land x \in ℝ) \to x \in ℝ$
8	4 2 5 6 7	xlimpnfvlem1	$⊢ ((φ \land F \underset{*}{⇝} +∞) \land x \in ℝ) \to \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)$
9	8	ralrimiva	$⊢ (φ \land F \underset{*}{⇝} +∞) \to \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)$
10		nfv	$⊢ Ⅎ k φ$
11		nfcv	$⊢ \underline{Ⅎ} k ℝ$
12		nfcv	$⊢ \underline{Ⅎ} k Z$
13		nfra1	$⊢ Ⅎ k \forall k \in ℤ_{\geq j} x \leq F (k)$
14	12 13	nfrex	$⊢ Ⅎ k \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)$
15	11 14	nfralw	$⊢ Ⅎ k \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)$
16	10 15	nfan	$⊢ Ⅎ k (φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k))$
17		nfv	$⊢ Ⅎ j φ$
18		nfcv	$⊢ \underline{Ⅎ} j ℝ$
19		nfre1	$⊢ Ⅎ j \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)$
20	18 19	nfralw	$⊢ Ⅎ j \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)$
21	17 20	nfan	$⊢ Ⅎ j (φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k))$
22	1	adantr	$⊢ (φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)) \to M \in ℤ$
23	3	adantr	$⊢ (φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)) \to F : Z ⟶ ℝ^{*}$
24		nfv	$⊢ Ⅎ j y \in ℝ$
25	21 24	nfan	$⊢ Ⅎ j ((φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)) \land y \in ℝ)$
26		simp-4r	$⊢ ((((φ \land y \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land y + 1 \leq F (k)) \to y \in ℝ$
27		rexr	$⊢ y \in ℝ \to y \in ℝ^{*}$
28	26 27	syl	$⊢ ((((φ \land y \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land y + 1 \leq F (k)) \to y \in ℝ^{*}$
29		peano2re	$⊢ y \in ℝ \to y + 1 \in ℝ$
30	29	rexrd	$⊢ y \in ℝ \to y + 1 \in ℝ^{*}$
31	26 30	syl	$⊢ ((((φ \land y \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land y + 1 \leq F (k)) \to y + 1 \in ℝ^{*}$
32	3	3ad2ant1	$⊢ (φ \land j \in Z \land k \in ℤ_{\geq j}) \to F : Z ⟶ ℝ^{*}$
33	2	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
34	33	3adant1	$⊢ (φ \land j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
35	32 34	ffvelrnd	$⊢ (φ \land j \in Z \land k \in ℤ_{\geq j}) \to F (k) \in ℝ^{*}$
36	35	ad5ant134	$⊢ ((((φ \land y \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land y + 1 \leq F (k)) \to F (k) \in ℝ^{*}$
37	26	ltp1d	$⊢ ((((φ \land y \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land y + 1 \leq F (k)) \to y < y + 1$
38		simpr	$⊢ ((((φ \land y \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land y + 1 \leq F (k)) \to y + 1 \leq F (k)$
39	28 31 36 37 38	xrltletrd	$⊢ ((((φ \land y \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land y + 1 \leq F (k)) \to y < F (k)$
40	39	ex	$⊢ (((φ \land y \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \to (y + 1 \leq F (k) \to y < F (k))$
41	40	ralimdva	$⊢ ((φ \land y \in ℝ) \land j \in Z) \to (\forall k \in ℤ_{\geq j} y + 1 \leq F (k) \to \forall k \in ℤ_{\geq j} y < F (k))$
42	41	imp	$⊢ (((φ \land y \in ℝ) \land j \in Z) \land \forall k \in ℤ_{\geq j} y + 1 \leq F (k)) \to \forall k \in ℤ_{\geq j} y < F (k)$
43	42	adantl3r	$⊢ ((((φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)) \land y \in ℝ) \land j \in Z) \land \forall k \in ℤ_{\geq j} y + 1 \leq F (k)) \to \forall k \in ℤ_{\geq j} y < F (k)$
44	43	3impa	$⊢ (((φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)) \land y \in ℝ) \land j \in Z \land \forall k \in ℤ_{\geq j} y + 1 \leq F (k)) \to \forall k \in ℤ_{\geq j} y < F (k)$
45	29	adantl	$⊢ (\forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k) \land y \in ℝ) \to y + 1 \in ℝ$
46		simpl	$⊢ (\forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k) \land y \in ℝ) \to \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)$
47		breq1	$⊢ x = y + 1 \to (x \leq F (k) \leftrightarrow y + 1 \leq F (k))$
48	47	ralbidv	$⊢ x = y + 1 \to (\forall k \in ℤ_{\geq j} x \leq F (k) \leftrightarrow \forall k \in ℤ_{\geq j} y + 1 \leq F (k))$
49	48	rexbidv	$⊢ x = y + 1 \to (\exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k) \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} y + 1 \leq F (k))$
50	49	rspcva	$⊢ (y + 1 \in ℝ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)) \to \exists j \in Z \forall k \in ℤ_{\geq j} y + 1 \leq F (k)$
51	45 46 50	syl2anc	$⊢ (\forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k) \land y \in ℝ) \to \exists j \in Z \forall k \in ℤ_{\geq j} y + 1 \leq F (k)$
52	51	adantll	$⊢ ((φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)) \land y \in ℝ) \to \exists j \in Z \forall k \in ℤ_{\geq j} y + 1 \leq F (k)$
53	25 44 52	reximdd	$⊢ ((φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)) \land y \in ℝ) \to \exists j \in Z \forall k \in ℤ_{\geq j} y < F (k)$
54	53	ralrimiva	$⊢ (φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)) \to \forall y \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} y < F (k)$
55	16 21 22 2 23 54	xlimpnfvlem2	$⊢ (φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k)) \to F \underset{*}{⇝} +∞$
56	9 55	impbida	$⊢ φ \to (F \underset{*}{⇝} +∞ \leftrightarrow \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} x \leq F (k))$

Metamath Proof Explorer

Theorem xlimpnfv

Proof