Theorem liminfpnfuz

Description: The inferior limit of a function is +oo if and only if every real number is the lower bound of the restriction of the function to a set of upper integers. (Contributed by Glauco Siliprandi, 23-Apr-2023)

	Ref	Expression
Hypotheses	liminfpnfuz.1	⊢ Ⅎ 𝑗 𝐹
	liminfpnfuz.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	liminfpnfuz.3	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	liminfpnfuz.4	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
Assertion	liminfpnfuz	⊢ ( 𝜑 → ( ( lim inf ‘ 𝐹 ) = +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )

Proof

Step	Hyp	Ref	Expression
1		liminfpnfuz.1	⊢ Ⅎ 𝑗 𝐹
2		liminfpnfuz.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		liminfpnfuz.3	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		liminfpnfuz.4	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
5		nfv	⊢ Ⅎ 𝑙 𝜑
6		nfcv	⊢ Ⅎ 𝑙 𝐹
7	5 6 2 3 4	liminfvaluz3	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = -𝑒 ( lim sup ‘ ( 𝑙 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑙 ) ) ) )
8		nfcv	⊢ Ⅎ 𝑗 𝑙
9	1 8	nffv	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
10	9	nfxneg	⊢ Ⅎ 𝑗 -𝑒 ( 𝐹 ‘ 𝑙 )
11		nfcv	⊢ Ⅎ 𝑙 -𝑒 ( 𝐹 ‘ 𝑗 )
12		fveq2	⊢ ( 𝑙 = 𝑗 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑗 ) )
13	12	xnegeqd	⊢ ( 𝑙 = 𝑗 → -𝑒 ( 𝐹 ‘ 𝑙 ) = -𝑒 ( 𝐹 ‘ 𝑗 ) )
14	10 11 13	cbvmpt	⊢ ( 𝑙 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑙 ) ) = ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) )
15	14	fveq2i	⊢ ( lim sup ‘ ( 𝑙 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑙 ) ) ) = ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) )
16	15	xnegeqi	⊢ -𝑒 ( lim sup ‘ ( 𝑙 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑙 ) ) ) = -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) )
17	7 16	eqtrdi	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) )
18	17	eqeq1d	⊢ ( 𝜑 → ( ( lim inf ‘ 𝐹 ) = +∞ ↔ -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = +∞ ) )
19		xnegmnf	⊢ -𝑒 -∞ = +∞
20	19	eqcomi	⊢ +∞ = -𝑒 -∞
21	20	a1i	⊢ ( 𝜑 → +∞ = -𝑒 -∞ )
22	21	eqeq2d	⊢ ( 𝜑 → ( -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = +∞ ↔ -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -𝑒 -∞ ) )
23	3	fvexi	⊢ 𝑍 ∈ V
24	23	mptex	⊢ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ∈ V
25	24	a1i	⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ∈ V )
26	25	limsupcld	⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ* )
27		mnfxr	⊢ -∞ ∈ ℝ*
28		xneg11	⊢ ( ( ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ* ∧ -∞ ∈ ℝ* ) → ( -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -𝑒 -∞ ↔ ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -∞ ) )
29	26 27 28	sylancl	⊢ ( 𝜑 → ( -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -𝑒 -∞ ↔ ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -∞ ) )
30	22 29	bitrd	⊢ ( 𝜑 → ( -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = +∞ ↔ ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -∞ ) )
31	3	uztrn2	⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑗 ∈ 𝑍 )
32		xnegex	⊢ -𝑒 ( 𝐹 ‘ 𝑗 ) ∈ V
33		fvmpt4	⊢ ( ( 𝑗 ∈ 𝑍 ∧ -𝑒 ( 𝐹 ‘ 𝑗 ) ∈ V ) → ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) = -𝑒 ( 𝐹 ‘ 𝑗 ) )
34	31 32 33	sylancl	⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) = -𝑒 ( 𝐹 ‘ 𝑗 ) )
35	34	breq1d	⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ↔ -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
36	35	ralbidva	⊢ ( 𝑘 ∈ 𝑍 → ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
37	36	rexbiia	⊢ ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
38	37	ralbii	⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
39	38	a1i	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
40		nfmpt1	⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) )
41	4	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑙 ) ∈ ℝ* )
42	41	xnegcld	⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑍 ) → -𝑒 ( 𝐹 ‘ 𝑙 ) ∈ ℝ* )
43	14	eqcomi	⊢ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) = ( 𝑙 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑙 ) )
44	42 43	fmptd	⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) : 𝑍 ⟶ ℝ* )
45	40 2 3 44	limsupmnfuz	⊢ ( 𝜑 → ( ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ) )
46	1 3 4	xlimpnfxnegmnf	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
47	39 45 46	3bitr4d	⊢ ( 𝜑 → ( ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ) = -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
48	18 30 47	3bitrd	⊢ ( 𝜑 → ( ( lim inf ‘ 𝐹 ) = +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )