Theorem limsupreuzmpt

Description: Given a function on the reals, defined on a set of upper integers, its supremum limit is real if and only if two condition holds: 1. there is a real number that is less than or equal to the function, infinitely often; 2. there is a real number that is greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupreuzmpt.j	⊢ Ⅎ 𝑗 𝜑
	limsupreuzmpt.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	limsupreuzmpt.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	limsupreuzmpt.b	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
Assertion	limsupreuzmpt	⊢ ( 𝜑 → ( ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ 𝐵 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		limsupreuzmpt.j	⊢ Ⅎ 𝑗 𝜑
2		limsupreuzmpt.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		limsupreuzmpt.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		limsupreuzmpt.b	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
5		nfmpt1	⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝑍 ↦ 𝐵 )
6	1 4	fmptd2f	⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℝ )
7	5 2 3 6	limsupreuz	⊢ ( 𝜑 → ( ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ≤ 𝑦 ) ) )
8		nfv	⊢ Ⅎ 𝑗 𝑖 ∈ 𝑍
9	1 8	nfan	⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑖 ∈ 𝑍 )
10		simpll	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝜑 )
11	3	uztrn2	⊢ ( ( 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑗 ∈ 𝑍 )
12	11	adantll	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑗 ∈ 𝑍 )
13		eqid	⊢ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) = ( 𝑗 ∈ 𝑍 ↦ 𝐵 )
14	13	a1i	⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) = ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) )
15	14 4	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) = 𝐵 )
16	10 12 15	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) = 𝐵 )
17	16	breq2d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝑦 ≤ ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ↔ 𝑦 ≤ 𝐵 ) )
18	9 17	rexbida	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ 𝐵 ) )
19	18	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ↔ ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ 𝐵 ) )
20	19	rexbidv	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ 𝐵 ) )
21		breq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ≤ 𝐵 ↔ 𝑥 ≤ 𝐵 ) )
22	21	rexbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ 𝐵 ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ 𝐵 ) )
23	22	ralbidv	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ 𝐵 ↔ ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ 𝐵 ) )
24		fveq2	⊢ ( 𝑖 = 𝑘 → ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑘 ) )
25	24	rexeqdv	⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ 𝐵 ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ 𝐵 ) )
26	25	cbvralvw	⊢ ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ 𝐵 ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ 𝐵 )
27	26	a1i	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ 𝐵 ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ 𝐵 ) )
28	23 27	bitrd	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ 𝐵 ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ 𝐵 ) )
29	28	cbvrexvw	⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ 𝐵 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ 𝐵 )
30	29	a1i	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ 𝐵 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ 𝐵 ) )
31	20 30	bitrd	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ 𝐵 ) )
32	15	breq1d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ≤ 𝑦 ↔ 𝐵 ≤ 𝑦 ) )
33	1 32	ralbida	⊢ ( 𝜑 → ( ∀ 𝑗 ∈ 𝑍 ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ≤ 𝑦 ↔ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑦 ) )
34	33	rexbidv	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ≤ 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑦 ) )
35		breq2	⊢ ( 𝑦 = 𝑥 → ( 𝐵 ≤ 𝑦 ↔ 𝐵 ≤ 𝑥 ) )
36	35	ralbidv	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑦 ↔ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 ) )
37	36	cbvrexvw	⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 )
38	37	a1i	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 ) )
39	34 38	bitrd	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 ) )
40	31 39	anbi12d	⊢ ( 𝜑 → ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑗 ) ≤ 𝑦 ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ 𝐵 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 ) ) )
41	7 40	bitrd	⊢ ( 𝜑 → ( ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ 𝐵 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 ) ) )