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	$⊢ \underline{Ⅎ} j F$
	limsupubuz.z	$⊢ Z = ℤ_{\geq M}$
	limsupubuz.f	$⊢ φ \to F : Z ⟶ ℝ$
	limsupubuz.n	$⊢ φ \to lim sup (F) \neq +∞$
Assertion	limsupubuz	$⊢ φ \to \exists x \in ℝ \forall j \in Z F (j) \leq x$

Proof

Step	Hyp	Ref	Expression
1		limsupubuz.j	$⊢ \underline{Ⅎ} j F$
2		limsupubuz.z	$⊢ Z = ℤ_{\geq M}$
3		limsupubuz.f	$⊢ φ \to F : Z ⟶ ℝ$
4		limsupubuz.n	$⊢ φ \to lim sup (F) \neq +∞$
5		nfv	$⊢ Ⅎ l φ$
6		nfcv	$⊢ \underline{Ⅎ} l F$
7		uzssre	$⊢ ℤ_{\geq M} \subseteq ℝ$
8	2 7	eqsstri	$⊢ Z \subseteq ℝ$
9	8	a1i	$⊢ φ \to Z \subseteq ℝ$
10	3	frexr	$⊢ φ \to F : Z ⟶ ℝ^{*}$
11	5 6 9 10 4	limsupub	$⊢ φ \to \exists y \in ℝ \exists k \in ℝ \forall l \in Z (k \leq l \to F (l) \leq y)$
12	11	adantr	$⊢ (φ \land M \in ℤ) \to \exists y \in ℝ \exists k \in ℝ \forall l \in Z (k \leq l \to F (l) \leq y)$
13		nfv	$⊢ Ⅎ l M \in ℤ$
14	5 13	nfan	$⊢ Ⅎ l (φ \land M \in ℤ)$
15		nfv	$⊢ Ⅎ l y \in ℝ$
16	14 15	nfan	$⊢ Ⅎ l ((φ \land M \in ℤ) \land y \in ℝ)$
17		nfv	$⊢ Ⅎ l k \in ℝ$
18	16 17	nfan	$⊢ Ⅎ l (((φ \land M \in ℤ) \land y \in ℝ) \land k \in ℝ)$
19		nfra1	$⊢ Ⅎ l \forall l \in Z (k \leq l \to F (l) \leq y)$
20	18 19	nfan	$⊢ Ⅎ l ((((φ \land M \in ℤ) \land y \in ℝ) \land k \in ℝ) \land \forall l \in Z (k \leq l \to F (l) \leq y))$
21		nfmpt1	$⊢ \underline{Ⅎ} l (l \in (M \dots if (⌈k⌉ \leq M, M, ⌈k⌉)) ⟼ F (l))$
22	21	nfrn	$⊢ \underline{Ⅎ} l ran (l \in (M \dots if (⌈k⌉ \leq M, M, ⌈k⌉)) ⟼ F (l))$
23		nfcv	$⊢ \underline{Ⅎ} l ℝ$
24		nfcv	$⊢ \underline{Ⅎ} l <$
25	22 23 24	nfsup	$⊢ \underline{Ⅎ} l sup (ran (l \in (M \dots if (⌈k⌉ \leq M, M, ⌈k⌉)) ⟼ F (l)) ℝ <)$
26		nfcv	$⊢ \underline{Ⅎ} l \leq$
27		nfcv	$⊢ \underline{Ⅎ} l y$
28	25 26 27	nfbr	$⊢ Ⅎ l sup (ran (l \in (M \dots if (⌈k⌉ \leq M, M, ⌈k⌉)) ⟼ F (l)) ℝ <) \leq y$
29	28 27 25	nfif	$⊢ \underline{Ⅎ} l if (sup (ran (l \in (M \dots if (⌈k⌉ \leq M, M, ⌈k⌉)) ⟼ F (l)) ℝ <) \leq y, y, sup (ran (l \in (M \dots if (⌈k⌉ \leq M, M, ⌈k⌉)) ⟼ F (l)) ℝ <))$
30		breq2	$⊢ l = i \to (k \leq l \leftrightarrow k \leq i)$
31		fveq2	$⊢ l = i \to F (l) = F (i)$
32	31	breq1d	$⊢ l = i \to (F (l) \leq y \leftrightarrow F (i) \leq y)$
33	30 32	imbi12d	$⊢ l = i \to ((k \leq l \to F (l) \leq y) \leftrightarrow (k \leq i \to F (i) \leq y))$
34	33	cbvralvw	$⊢ \forall l \in Z (k \leq l \to F (l) \leq y) \leftrightarrow \forall i \in Z (k \leq i \to F (i) \leq y)$
35	34	biimpi	$⊢ \forall l \in Z (k \leq l \to F (l) \leq y) \to \forall i \in Z (k \leq i \to F (i) \leq y)$
36	35	adantl	$⊢ ((((φ \land M \in ℤ) \land y \in ℝ) \land k \in ℝ) \land \forall l \in Z (k \leq l \to F (l) \leq y)) \to \forall i \in Z (k \leq i \to F (i) \leq y)$
37		simp-4r	$⊢ ((((φ \land M \in ℤ) \land y \in ℝ) \land k \in ℝ) \land \forall i \in Z (k \leq i \to F (i) \leq y)) \to M \in ℤ$
38	36 37	syldan	$⊢ ((((φ \land M \in ℤ) \land y \in ℝ) \land k \in ℝ) \land \forall l \in Z (k \leq l \to F (l) \leq y)) \to M \in ℤ$
39	3	ad4antr	$⊢ ((((φ \land M \in ℤ) \land y \in ℝ) \land k \in ℝ) \land \forall i \in Z (k \leq i \to F (i) \leq y)) \to F : Z ⟶ ℝ$
40	36 39	syldan	$⊢ ((((φ \land M \in ℤ) \land y \in ℝ) \land k \in ℝ) \land \forall l \in Z (k \leq l \to F (l) \leq y)) \to F : Z ⟶ ℝ$
41		simpllr	$⊢ ((((φ \land M \in ℤ) \land y \in ℝ) \land k \in ℝ) \land \forall i \in Z (k \leq i \to F (i) \leq y)) \to y \in ℝ$
42	36 41	syldan	$⊢ ((((φ \land M \in ℤ) \land y \in ℝ) \land k \in ℝ) \land \forall l \in Z (k \leq l \to F (l) \leq y)) \to y \in ℝ$
43		simplr	$⊢ ((((φ \land M \in ℤ) \land y \in ℝ) \land k \in ℝ) \land \forall i \in Z (k \leq i \to F (i) \leq y)) \to k \in ℝ$
44	36 43	syldan	$⊢ ((((φ \land M \in ℤ) \land y \in ℝ) \land k \in ℝ) \land \forall l \in Z (k \leq l \to F (l) \leq y)) \to k \in ℝ$
45	34	biimpri	$⊢ \forall i \in Z (k \leq i \to F (i) \leq y) \to \forall l \in Z (k \leq l \to F (l) \leq y)$
46	36 45	syl	$⊢ ((((φ \land M \in ℤ) \land y \in ℝ) \land k \in ℝ) \land \forall l \in Z (k \leq l \to F (l) \leq y)) \to \forall l \in Z (k \leq l \to F (l) \leq y)$
47		eqid	$⊢ if (⌈k⌉ \leq M, M, ⌈k⌉) = if (⌈k⌉ \leq M, M, ⌈k⌉)$
48		eqid	$⊢ sup (ran (l \in (M \dots if (⌈k⌉ \leq M, M, ⌈k⌉)) ⟼ F (l)) ℝ <) = sup (ran (l \in (M \dots if (⌈k⌉ \leq M, M, ⌈k⌉)) ⟼ F (l)) ℝ <)$
49		eqid	$⊢ if (sup (ran (l \in (M \dots if (⌈k⌉ \leq M, M, ⌈k⌉)) ⟼ F (l)) ℝ <) \leq y, y, sup (ran (l \in (M \dots if (⌈k⌉ \leq M, M, ⌈k⌉)) ⟼ F (l)) ℝ <)) = if (sup (ran (l \in (M \dots if (⌈k⌉ \leq M, M, ⌈k⌉)) ⟼ F (l)) ℝ <) \leq y, y, sup (ran (l \in (M \dots if (⌈k⌉ \leq M, M, ⌈k⌉)) ⟼ F (l)) ℝ <))$
50	20 29 38 2 40 42 44 46 47 48 49	limsupubuzlem	$⊢ ((((φ \land M \in ℤ) \land y \in ℝ) \land k \in ℝ) \land \forall l \in Z (k \leq l \to F (l) \leq y)) \to \exists x \in ℝ \forall l \in Z F (l) \leq x$
51	50	rexlimdva2	$⊢ ((φ \land M \in ℤ) \land y \in ℝ) \to (\exists k \in ℝ \forall l \in Z (k \leq l \to F (l) \leq y) \to \exists x \in ℝ \forall l \in Z F (l) \leq x)$
52	51	rexlimdva	$⊢ (φ \land M \in ℤ) \to (\exists y \in ℝ \exists k \in ℝ \forall l \in Z (k \leq l \to F (l) \leq y) \to \exists x \in ℝ \forall l \in Z F (l) \leq x)$
53	12 52	mpd	$⊢ (φ \land M \in ℤ) \to \exists x \in ℝ \forall l \in Z F (l) \leq x$
54	2	a1i	$⊢ \neg M \in ℤ \to Z = ℤ_{\geq M}$
55		uz0	$⊢ \neg M \in ℤ \to ℤ_{\geq M} = \emptyset$
56	54 55	eqtrd	$⊢ \neg M \in ℤ \to Z = \emptyset$
57		0red	$⊢ Z = \emptyset \to 0 \in ℝ$
58		rzal	$⊢ Z = \emptyset \to \forall l \in Z F (l) \leq 0$
59		brralrspcev	$⊢ (0 \in ℝ \land \forall l \in Z F (l) \leq 0) \to \exists x \in ℝ \forall l \in Z F (l) \leq x$
60	57 58 59	syl2anc	$⊢ Z = \emptyset \to \exists x \in ℝ \forall l \in Z F (l) \leq x$
61	56 60	syl	$⊢ \neg M \in ℤ \to \exists x \in ℝ \forall l \in Z F (l) \leq x$
62	61	adantl	$⊢ (φ \land \neg M \in ℤ) \to \exists x \in ℝ \forall l \in Z F (l) \leq x$
63	53 62	pm2.61dan	$⊢ φ \to \exists x \in ℝ \forall l \in Z F (l) \leq x$
64		nfcv	$⊢ \underline{Ⅎ} j l$
65	1 64	nffv	$⊢ \underline{Ⅎ} j F (l)$
66		nfcv	$⊢ \underline{Ⅎ} j \leq$
67		nfcv	$⊢ \underline{Ⅎ} j x$
68	65 66 67	nfbr	$⊢ Ⅎ j F (l) \leq x$
69		nfv	$⊢ Ⅎ l F (j) \leq x$
70		fveq2	$⊢ l = j \to F (l) = F (j)$
71	70	breq1d	$⊢ l = j \to (F (l) \leq x \leftrightarrow F (j) \leq x)$
72	68 69 71	cbvralw	$⊢ \forall l \in Z F (l) \leq x \leftrightarrow \forall j \in Z F (j) \leq x$
73	72	rexbii	$⊢ \exists x \in ℝ \forall l \in Z F (l) \leq x \leftrightarrow \exists x \in ℝ \forall j \in Z F (j) \leq x$
74	63 73	sylib	$⊢ φ \to \exists x \in ℝ \forall j \in Z F (j) \leq x$

Metamath Proof Explorer

Theorem limsupubuz

Proof