limsupre3uz

Description: Given a function on the extended reals, 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 eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupre3uz.1	⊢ Ⅎ 𝑗 𝐹
	limsupre3uz.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	limsupre3uz.3	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
	limsupre3uz.4	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ^* )
Assertion	limsupre3uz	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		limsupre3uz.1	⊢ Ⅎ 𝑗 𝐹
2		limsupre3uz.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		limsupre3uz.3	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
4		limsupre3uz.4	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ^* )
5		nfcv	⊢ Ⅎ 𝑙 𝐹
6	5 2 3 4	limsupre3uzlem	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) )
7		breq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
8	7	rexbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
9	8	ralbidv	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
10		fveq2	⊢ ( 𝑖 = 𝑘 → ( ℤ_≥ ‘ 𝑖 ) = ( ℤ_≥ ‘ 𝑘 ) )
11	10	rexeqdv	⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑙 ∈ ( ℤ_≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
12		nfcv	⊢ Ⅎ 𝑗 𝑥
13		nfcv	⊢ Ⅎ 𝑗 ≤
14		nfcv	⊢ Ⅎ 𝑗 𝑙
15	1 14	nffv	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
16	12 13 15	nfbr	⊢ Ⅎ 𝑗 𝑥 ≤ ( 𝐹 ‘ 𝑙 )
17		nfv	⊢ Ⅎ 𝑙 𝑥 ≤ ( 𝐹 ‘ 𝑗 )
18		fveq2	⊢ ( 𝑙 = 𝑗 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑗 ) )
19	18	breq2d	⊢ ( 𝑙 = 𝑗 → ( 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
20	16 17 19	cbvrexw	⊢ ( ∃ 𝑙 ∈ ( ℤ_≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
21	20	a1i	⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ ( ℤ_≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
22	11 21	bitrd	⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
23	22	cbvralvw	⊢ ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
24	23	a1i	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
25	9 24	bitrd	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
26	25	cbvrexvw	⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
27		breq2	⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
28	27	ralbidv	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
29	28	rexbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
30	10	raleqdv	⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
31	15 13 12	nfbr	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥
32		nfv	⊢ Ⅎ 𝑙 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥
33	18	breq1d	⊢ ( 𝑙 = 𝑗 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
34	31 32 33	cbvralw	⊢ ( ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
35	34	a1i	⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
36	30 35	bitrd	⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
37	36	cbvrexvw	⊢ ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
38	37	a1i	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
39	29 38	bitrd	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
40	39	cbvrexvw	⊢ ( ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
41	26 40	anbi12i	⊢ ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
42	41	a1i	⊢ ( 𝜑 → ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ_≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
43	6 42	bitrd	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ_≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )

Metamath Proof Explorer

Theorem limsupre3uz

Proof