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	bilani	$⊢ ((((φ \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)$
36		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 ℤ$
37	35 36	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 ℤ$
38	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 ⟶ ℝ$
39	35 38	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 ⟶ ℝ$
40		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 ℝ$
41	35 40	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 ℝ$
42		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 ℝ$
43	35 42	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 ℝ$
44	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)$
45	35 44	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)$
46		eqid	$⊢ if (⌈k⌉ \leq M, M, ⌈k⌉) = if (⌈k⌉ \leq M, M, ⌈k⌉)$
47		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)) ℝ <)$
48		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)) ℝ <))$
49	20 29 37 2 39 41 43 45 46 47 48	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$
50	49	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)$
51	50	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)$
52	12 51	mpd	$⊢ (φ \land M \in ℤ) \to \exists x \in ℝ \forall l \in Z F (l) \leq x$
53	2	a1i	$⊢ \neg M \in ℤ \to Z = ℤ_{\geq M}$
54		uz0	$⊢ \neg M \in ℤ \to ℤ_{\geq M} = \emptyset$
55	53 54	eqtrd	$⊢ \neg M \in ℤ \to Z = \emptyset$
56		0red	$⊢ Z = \emptyset \to 0 \in ℝ$
57		rzal	$⊢ Z = \emptyset \to \forall l \in Z F (l) \leq 0$
58		brralrspcev	$⊢ (0 \in ℝ \land \forall l \in Z F (l) \leq 0) \to \exists x \in ℝ \forall l \in Z F (l) \leq x$
59	56 57 58	syl2anc	$⊢ Z = \emptyset \to \exists x \in ℝ \forall l \in Z F (l) \leq x$
60	55 59	syl	$⊢ \neg M \in ℤ \to \exists x \in ℝ \forall l \in Z F (l) \leq x$
61	60	adantl	$⊢ (φ \land \neg M \in ℤ) \to \exists x \in ℝ \forall l \in Z F (l) \leq x$
62	52 61	pm2.61dan	$⊢ φ \to \exists x \in ℝ \forall l \in Z F (l) \leq x$
63		nfcv	$⊢ \underline{Ⅎ} j l$
64	1 63	nffv	$⊢ \underline{Ⅎ} j F (l)$
65		nfcv	$⊢ \underline{Ⅎ} j \leq$
66		nfcv	$⊢ \underline{Ⅎ} j x$
67	64 65 66	nfbr	$⊢ Ⅎ j F (l) \leq x$
68		nfv	$⊢ Ⅎ l F (j) \leq x$
69		fveq2	$⊢ l = j \to F (l) = F (j)$
70	69	breq1d	$⊢ l = j \to (F (l) \leq x \leftrightarrow F (j) \leq x)$
71	67 68 70	cbvralw	$⊢ \forall l \in Z F (l) \leq x \leftrightarrow \forall j \in Z F (j) \leq x$
72	71	rexbii	$⊢ \exists x \in ℝ \forall l \in Z F (l) \leq x \leftrightarrow \exists x \in ℝ \forall j \in Z F (j) \leq x$
73	62 72	sylib	$⊢ φ \to \exists x \in ℝ \forall j \in Z F (j) \leq x$

Metamath Proof Explorer

Theorem limsupubuz

Proof