Theorem limsupubuz

Description: For a real-valued function on a set of upper integers, if the superior limit is not +oo , then the function is bounded above. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupubuz.j	⊢ Ⅎ 𝑗 𝐹
	limsupubuz.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	limsupubuz.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
	limsupubuz.n	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≠ +∞ )
Assertion	limsupubuz	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		limsupubuz.j	⊢ Ⅎ 𝑗 𝐹
2		limsupubuz.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		limsupubuz.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
4		limsupubuz.n	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≠ +∞ )
5		nfv	⊢ Ⅎ 𝑙 𝜑
6		nfcv	⊢ Ⅎ 𝑙 𝐹
7		uzssre	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℝ
8	2 7	eqsstri	⊢ 𝑍 ⊆ ℝ
9	8	a1i	⊢ ( 𝜑 → 𝑍 ⊆ ℝ )
10	3	frexr	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
11	5 6 9 10 4	limsupub	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) )
13		nfv	⊢ Ⅎ 𝑙 𝑀 ∈ ℤ
14	5 13	nfan	⊢ Ⅎ 𝑙 ( 𝜑 ∧ 𝑀 ∈ ℤ )
15		nfv	⊢ Ⅎ 𝑙 𝑦 ∈ ℝ
16	14 15	nfan	⊢ Ⅎ 𝑙 ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ )
17		nfv	⊢ Ⅎ 𝑙 𝑘 ∈ ℝ
18	16 17	nfan	⊢ Ⅎ 𝑙 ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ )
19		nfra1	⊢ Ⅎ 𝑙 ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 )
20	18 19	nfan	⊢ Ⅎ 𝑙 ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) )
21		nfmpt1	⊢ Ⅎ 𝑙 ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) )
22	21	nfrn	⊢ Ⅎ 𝑙 ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) )
23		nfcv	⊢ Ⅎ 𝑙 ℝ
24		nfcv	⊢ Ⅎ 𝑙 <
25	22 23 24	nfsup	⊢ Ⅎ 𝑙 sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < )
26		nfcv	⊢ Ⅎ 𝑙 ≤
27		nfcv	⊢ Ⅎ 𝑙 𝑦
28	25 26 27	nfbr	⊢ Ⅎ 𝑙 sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < ) ≤ 𝑦
29	28 27 25	nfif	⊢ Ⅎ 𝑙 if ( sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < ) ≤ 𝑦 , 𝑦 , sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < ) )
30		breq2	⊢ ( 𝑙 = 𝑖 → ( 𝑘 ≤ 𝑙 ↔ 𝑘 ≤ 𝑖 ) )
31		fveq2	⊢ ( 𝑙 = 𝑖 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑖 ) )
32	31	breq1d	⊢ ( 𝑙 = 𝑖 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) )
33	30 32	imbi12d	⊢ ( 𝑙 = 𝑖 → ( ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ( 𝑘 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) ) )
34	33	cbvralvw	⊢ ( ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ∀ 𝑖 ∈ 𝑍 ( 𝑘 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) )
35	34	bilani	⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) → ∀ 𝑖 ∈ 𝑍 ( 𝑘 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) )
36		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑖 ∈ 𝑍 ( 𝑘 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) ) → 𝑀 ∈ ℤ )
37	35 36	syldan	⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) → 𝑀 ∈ ℤ )
38	3	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑖 ∈ 𝑍 ( 𝑘 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) ) → 𝐹 : 𝑍 ⟶ ℝ )
39	35 38	syldan	⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) → 𝐹 : 𝑍 ⟶ ℝ )
40		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑖 ∈ 𝑍 ( 𝑘 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) ) → 𝑦 ∈ ℝ )
41	35 40	syldan	⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) → 𝑦 ∈ ℝ )
42		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑖 ∈ 𝑍 ( 𝑘 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) ) → 𝑘 ∈ ℝ )
43	35 42	syldan	⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) → 𝑘 ∈ ℝ )
44	34	biimpri	⊢ ( ∀ 𝑖 ∈ 𝑍 ( 𝑘 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ 𝑦 ) → ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) )
45	35 44	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) → ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) )
46		eqid	⊢ if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) = if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) )
47		eqid	⊢ sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < ) = sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < )
48		eqid	⊢ if ( sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < ) ≤ 𝑦 , 𝑦 , sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < ) ) = if ( sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < ) ≤ 𝑦 , 𝑦 , sup ( ran ( 𝑙 ∈ ( 𝑀 ... if ( ( ⌈ ‘ 𝑘 ) ≤ 𝑀 , 𝑀 , ( ⌈ ‘ 𝑘 ) ) ) ↦ ( 𝐹 ‘ 𝑙 ) ) , ℝ , < ) )
49	20 29 37 2 39 41 43 45 46 47 48	limsupubuzlem	⊢ ( ( ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
50	49	rexlimdva2	⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
51	50	rexlimdva	⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( ∃ 𝑦 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
52	12 51	mpd	⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
53	2	a1i	⊢ ( ¬ 𝑀 ∈ ℤ → 𝑍 = ( ℤ≥ ‘ 𝑀 ) )
54		uz0	⊢ ( ¬ 𝑀 ∈ ℤ → ( ℤ≥ ‘ 𝑀 ) = ∅ )
55	53 54	eqtrd	⊢ ( ¬ 𝑀 ∈ ℤ → 𝑍 = ∅ )
56		0red	⊢ ( 𝑍 = ∅ → 0 ∈ ℝ )
57		rzal	⊢ ( 𝑍 = ∅ → ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 0 )
58		brralrspcev	⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 0 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
59	56 57 58	syl2anc	⊢ ( 𝑍 = ∅ → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
60	55 59	syl	⊢ ( ¬ 𝑀 ∈ ℤ → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
61	60	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝑀 ∈ ℤ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
62	52 61	pm2.61dan	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
63		nfcv	⊢ Ⅎ 𝑗 𝑙
64	1 63	nffv	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
65		nfcv	⊢ Ⅎ 𝑗 ≤
66		nfcv	⊢ Ⅎ 𝑗 𝑥
67	64 65 66	nfbr	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥
68		nfv	⊢ Ⅎ 𝑙 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥
69		fveq2	⊢ ( 𝑙 = 𝑗 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑗 ) )
70	69	breq1d	⊢ ( 𝑙 = 𝑗 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
71	67 68 70	cbvralw	⊢ ( ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
72	71	rexbii	⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑙 ∈ 𝑍 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
73	62 72	sylib	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )