Theorem limsupreuz

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

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

Proof

Step	Hyp	Ref	Expression
1		limsupreuz.1	⊢ Ⅎ 𝑗 𝐹
2		limsupreuz.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		limsupreuz.3	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		limsupreuz.4	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
5		nfcv	⊢ Ⅎ 𝑙 𝐹
6	4	frexr	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
7	5 2 3 6	limsupre3uzlem	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) )
8		breq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
9	8	rexbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
10	9	ralbidv	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
11		fveq2	⊢ ( 𝑖 = 𝑘 → ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑘 ) )
12	11	rexeqdv	⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
13		nfcv	⊢ Ⅎ 𝑗 𝑥
14		nfcv	⊢ Ⅎ 𝑗 ≤
15		nfcv	⊢ Ⅎ 𝑗 𝑙
16	1 15	nffv	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
17	13 14 16	nfbr	⊢ Ⅎ 𝑗 𝑥 ≤ ( 𝐹 ‘ 𝑙 )
18		nfv	⊢ Ⅎ 𝑙 𝑥 ≤ ( 𝐹 ‘ 𝑗 )
19		fveq2	⊢ ( 𝑙 = 𝑗 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑗 ) )
20	19	breq2d	⊢ ( 𝑙 = 𝑗 → ( 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
21	17 18 20	cbvrexw	⊢ ( ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
22	21	a1i	⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
23	12 22	bitrd	⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
24	23	cbvralvw	⊢ ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
25	24	a1i	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
26	10 25	bitrd	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
27	26	cbvrexvw	⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
28		breq2	⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
29	28	ralbidv	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
30	29	rexbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
31	11	raleqdv	⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
32	16 14 13	nfbr	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥
33		nfv	⊢ Ⅎ 𝑙 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥
34	19	breq1d	⊢ ( 𝑙 = 𝑗 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
35	32 33 34	cbvralw	⊢ ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
36	35	a1i	⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
37	31 36	bitrd	⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
38	37	cbvrexvw	⊢ ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
39	38	a1i	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
40	30 39	bitrd	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
41	40	cbvrexvw	⊢ ( ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
42	27 41	anbi12i	⊢ ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
43	42	a1i	⊢ ( 𝜑 → ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
44	7 43	bitrd	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
45		nfv	⊢ Ⅎ 𝑖 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥
46		nfcv	⊢ Ⅎ 𝑗 𝑖
47	1 46	nffv	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑖 )
48	47 14 13	nfbr	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑖 ) ≤ 𝑥
49		fveq2	⊢ ( 𝑗 = 𝑖 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑖 ) )
50	49	breq1d	⊢ ( 𝑗 = 𝑖 → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ) )
51	45 48 50	cbvralw	⊢ ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 )
52	51	rexbii	⊢ ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 )
53	52	rexbii	⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 )
54	53	a1i	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ) )
55		nfv	⊢ Ⅎ 𝑖 𝜑
56	4	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝐹 : 𝑍 ⟶ ℝ )
57		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ 𝑍 )
58	56 57	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑖 ) ∈ ℝ )
59	55 2 3 58	uzub	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ) )
60		eqcom	⊢ ( 𝑗 = 𝑖 ↔ 𝑖 = 𝑗 )
61	60	imbi1i	⊢ ( ( 𝑗 = 𝑖 → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ) ) ↔ ( 𝑖 = 𝑗 → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ) ) )
62		bicom	⊢ ( ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
63	62	imbi2i	⊢ ( ( 𝑖 = 𝑗 → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ) ) ↔ ( 𝑖 = 𝑗 → ( ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
64	61 63	bitri	⊢ ( ( 𝑗 = 𝑖 → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ) ) ↔ ( 𝑖 = 𝑗 → ( ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
65	50 64	mpbi	⊢ ( 𝑖 = 𝑗 → ( ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
66	48 45 65	cbvralw	⊢ ( ∀ 𝑖 ∈ 𝑍 ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
67	66	rexbii	⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
68	67	a1i	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
69	54 59 68	3bitrd	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
70	69	anbi2d	⊢ ( 𝜑 → ( ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
71	44 70	bitrd	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )