limsupubuzlem

Description: If the limsup is not +oo , then the function is bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupubuzlem.j	$⊢ Ⅎ j φ$
	limsupubuzlem.e	$⊢ \underline{Ⅎ} j X$
	limsupubuzlem.m	$⊢ φ \to M \in ℤ$
	limsupubuzlem.z	$⊢ Z = ℤ_{\geq M}$
	limsupubuzlem.f	$⊢ φ \to F : Z ⟶ ℝ$
	limsupubuzlem.y	$⊢ φ \to Y \in ℝ$
	limsupubuzlem.k	$⊢ φ \to K \in ℝ$
	limsupubuzlem.b	$⊢ φ \to \forall j \in Z (K \leq j \to F (j) \leq Y)$
	limsupubuzlem.n	$⊢ N = if (⌈K⌉ \leq M, M, ⌈K⌉)$
	limsupubuzlem.w	$⊢ W = sup (ran (j \in (M \dots N) ⟼ F (j)) ℝ <)$
	limsupubuzlem.x	$⊢ X = if (W \leq Y, Y, W)$
Assertion	limsupubuzlem	$⊢ φ \to \exists x \in ℝ \forall j \in Z F (j) \leq x$

Proof

Step	Hyp	Ref	Expression
1		limsupubuzlem.j	$⊢ Ⅎ j φ$
2		limsupubuzlem.e	$⊢ \underline{Ⅎ} j X$
3		limsupubuzlem.m	$⊢ φ \to M \in ℤ$
4		limsupubuzlem.z	$⊢ Z = ℤ_{\geq M}$
5		limsupubuzlem.f	$⊢ φ \to F : Z ⟶ ℝ$
6		limsupubuzlem.y	$⊢ φ \to Y \in ℝ$
7		limsupubuzlem.k	$⊢ φ \to K \in ℝ$
8		limsupubuzlem.b	$⊢ φ \to \forall j \in Z (K \leq j \to F (j) \leq Y)$
9		limsupubuzlem.n	$⊢ N = if (⌈K⌉ \leq M, M, ⌈K⌉)$
10		limsupubuzlem.w	$⊢ W = sup (ran (j \in (M \dots N) ⟼ F (j)) ℝ <)$
11		limsupubuzlem.x	$⊢ X = if (W \leq Y, Y, W)$
12	10	a1i	$⊢ φ \to W = sup (ran (j \in (M \dots N) ⟼ F (j)) ℝ <)$
13		ltso	$⊢ < Or ℝ$
14	13	a1i	$⊢ φ \to < Or ℝ$
15		fzfid	$⊢ φ \to (M \dots N) \in Fin$
16		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
17	9	a1i	$⊢ φ \to N = if (⌈K⌉ \leq M, M, ⌈K⌉)$
18		ceilcl	$⊢ K \in ℝ \to ⌈K⌉ \in ℤ$
19	7 18	syl	$⊢ φ \to ⌈K⌉ \in ℤ$
20	3 19	ifcld	$⊢ φ \to if (⌈K⌉ \leq M, M, ⌈K⌉) \in ℤ$
21	17 20	eqeltrd	$⊢ φ \to N \in ℤ$
22	19	zred	$⊢ φ \to ⌈K⌉ \in ℝ$
23	3	zred	$⊢ φ \to M \in ℝ$
24		max2	$⊢ (⌈K⌉ \in ℝ \land M \in ℝ) \to M \leq if (⌈K⌉ \leq M, M, ⌈K⌉)$
25	22 23 24	syl2anc	$⊢ φ \to M \leq if (⌈K⌉ \leq M, M, ⌈K⌉)$
26	17	eqcomd	$⊢ φ \to if (⌈K⌉ \leq M, M, ⌈K⌉) = N$
27	25 26	breqtrd	$⊢ φ \to M \leq N$
28	16 3 21 27	eluzd	$⊢ φ \to N \in ℤ_{\geq M}$
29		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
30	28 29	syl	$⊢ φ \to N \in (M \dots N)$
31	30	ne0d	$⊢ φ \to (M \dots N) \neq \emptyset$
32	5	adantr	$⊢ (φ \land j \in (M \dots N)) \to F : Z ⟶ ℝ$
33	3	adantr	$⊢ (φ \land j \in (M \dots N)) \to M \in ℤ$
34		elfzelz	$⊢ j \in (M \dots N) \to j \in ℤ$
35	34	adantl	$⊢ (φ \land j \in (M \dots N)) \to j \in ℤ$
36		elfzle1	$⊢ j \in (M \dots N) \to M \leq j$
37	36	adantl	$⊢ (φ \land j \in (M \dots N)) \to M \leq j$
38	16 33 35 37	eluzd	$⊢ (φ \land j \in (M \dots N)) \to j \in ℤ_{\geq M}$
39	38 4	eleqtrrdi	$⊢ (φ \land j \in (M \dots N)) \to j \in Z$
40	32 39	ffvelrnd	$⊢ (φ \land j \in (M \dots N)) \to F (j) \in ℝ$
41	1 14 15 31 40	fisupclrnmpt	$⊢ φ \to sup (ran (j \in (M \dots N) ⟼ F (j)) ℝ <) \in ℝ$
42	12 41	eqeltrd	$⊢ φ \to W \in ℝ$
43	6 42	ifcld	$⊢ φ \to if (W \leq Y, Y, W) \in ℝ$
44	11 43	eqeltrid	$⊢ φ \to X \in ℝ$
45	5	ffvelrnda	$⊢ (φ \land j \in Z) \to F (j) \in ℝ$
46	45	adantr	$⊢ ((φ \land j \in Z) \land j \leq N) \to F (j) \in ℝ$
47	42	ad2antrr	$⊢ ((φ \land j \in Z) \land j \leq N) \to W \in ℝ$
48	44	ad2antrr	$⊢ ((φ \land j \in Z) \land j \leq N) \to X \in ℝ$
49		simpll	$⊢ ((φ \land j \in Z) \land j \leq N) \to φ$
50	3	ad2antrr	$⊢ ((φ \land j \in Z) \land j \leq N) \to M \in ℤ$
51	21	ad2antrr	$⊢ ((φ \land j \in Z) \land j \leq N) \to N \in ℤ$
52	4	eluzelz2	$⊢ j \in Z \to j \in ℤ$
53	52	ad2antlr	$⊢ ((φ \land j \in Z) \land j \leq N) \to j \in ℤ$
54	4	eleq2i	$⊢ j \in Z \leftrightarrow j \in ℤ_{\geq M}$
55	54	biimpi	$⊢ j \in Z \to j \in ℤ_{\geq M}$
56		eluzle	$⊢ j \in ℤ_{\geq M} \to M \leq j$
57	55 56	syl	$⊢ j \in Z \to M \leq j$
58	57	ad2antlr	$⊢ ((φ \land j \in Z) \land j \leq N) \to M \leq j$
59		simpr	$⊢ ((φ \land j \in Z) \land j \leq N) \to j \leq N$
60	50 51 53 58 59	elfzd	$⊢ ((φ \land j \in Z) \land j \leq N) \to j \in (M \dots N)$
61	1 15 40	fimaxre4	$⊢ φ \to \exists b \in ℝ \forall j \in (M \dots N) F (j) \leq b$
62	1 40 61	suprubrnmpt	$⊢ (φ \land j \in (M \dots N)) \to F (j) \leq sup (ran (j \in (M \dots N) ⟼ F (j)) ℝ <)$
63	62 10	breqtrrdi	$⊢ (φ \land j \in (M \dots N)) \to F (j) \leq W$
64	49 60 63	syl2anc	$⊢ ((φ \land j \in Z) \land j \leq N) \to F (j) \leq W$
65		max1	$⊢ (W \in ℝ \land Y \in ℝ) \to W \leq if (W \leq Y, Y, W)$
66	42 6 65	syl2anc	$⊢ φ \to W \leq if (W \leq Y, Y, W)$
67	66 11	breqtrrdi	$⊢ φ \to W \leq X$
68	67	ad2antrr	$⊢ ((φ \land j \in Z) \land j \leq N) \to W \leq X$
69	46 47 48 64 68	letrd	$⊢ ((φ \land j \in Z) \land j \leq N) \to F (j) \leq X$
70	7	ad2antrr	$⊢ ((φ \land j \in Z) \land \neg j \leq N) \to K \in ℝ$
71		uzssre	$⊢ ℤ_{\geq M} \subseteq ℝ$
72	4 71	eqsstri	$⊢ Z \subseteq ℝ$
73	72	sseli	$⊢ j \in Z \to j \in ℝ$
74	73	ad2antlr	$⊢ ((φ \land j \in Z) \land \neg j \leq N) \to j \in ℝ$
75	71 28	sselid	$⊢ φ \to N \in ℝ$
76	75	ad2antrr	$⊢ ((φ \land j \in Z) \land \neg j \leq N) \to N \in ℝ$
77		ceilge	$⊢ K \in ℝ \to K \leq ⌈K⌉$
78	7 77	syl	$⊢ φ \to K \leq ⌈K⌉$
79		max1	$⊢ (⌈K⌉ \in ℝ \land M \in ℝ) \to ⌈K⌉ \leq if (⌈K⌉ \leq M, M, ⌈K⌉)$
80	22 23 79	syl2anc	$⊢ φ \to ⌈K⌉ \leq if (⌈K⌉ \leq M, M, ⌈K⌉)$
81	80 26	breqtrd	$⊢ φ \to ⌈K⌉ \leq N$
82	7 22 75 78 81	letrd	$⊢ φ \to K \leq N$
83	82	ad2antrr	$⊢ ((φ \land j \in Z) \land \neg j \leq N) \to K \leq N$
84		simpr	$⊢ ((φ \land j \in Z) \land \neg j \leq N) \to \neg j \leq N$
85	76 74	ltnled	$⊢ ((φ \land j \in Z) \land \neg j \leq N) \to (N < j \leftrightarrow \neg j \leq N)$
86	84 85	mpbird	$⊢ ((φ \land j \in Z) \land \neg j \leq N) \to N < j$
87	70 76 74 83 86	lelttrd	$⊢ ((φ \land j \in Z) \land \neg j \leq N) \to K < j$
88	70 74 87	ltled	$⊢ ((φ \land j \in Z) \land \neg j \leq N) \to K \leq j$
89	45	adantr	$⊢ ((φ \land j \in Z) \land K \leq j) \to F (j) \in ℝ$
90	6	ad2antrr	$⊢ ((φ \land j \in Z) \land K \leq j) \to Y \in ℝ$
91	44	ad2antrr	$⊢ ((φ \land j \in Z) \land K \leq j) \to X \in ℝ$
92		simpr	$⊢ ((φ \land j \in Z) \land K \leq j) \to K \leq j$
93	8	r19.21bi	$⊢ (φ \land j \in Z) \to (K \leq j \to F (j) \leq Y)$
94	93	adantr	$⊢ ((φ \land j \in Z) \land K \leq j) \to (K \leq j \to F (j) \leq Y)$
95	92 94	mpd	$⊢ ((φ \land j \in Z) \land K \leq j) \to F (j) \leq Y$
96		max2	$⊢ (W \in ℝ \land Y \in ℝ) \to Y \leq if (W \leq Y, Y, W)$
97	42 6 96	syl2anc	$⊢ φ \to Y \leq if (W \leq Y, Y, W)$
98	97 11	breqtrrdi	$⊢ φ \to Y \leq X$
99	98	ad2antrr	$⊢ ((φ \land j \in Z) \land K \leq j) \to Y \leq X$
100	89 90 91 95 99	letrd	$⊢ ((φ \land j \in Z) \land K \leq j) \to F (j) \leq X$
101	88 100	syldan	$⊢ ((φ \land j \in Z) \land \neg j \leq N) \to F (j) \leq X$
102	69 101	pm2.61dan	$⊢ (φ \land j \in Z) \to F (j) \leq X$
103	102	ex	$⊢ φ \to (j \in Z \to F (j) \leq X)$
104	1 103	ralrimi	$⊢ φ \to \forall j \in Z F (j) \leq X$
105		nfv	$⊢ Ⅎ x \forall j \in Z F (j) \leq X$
106		nfcv	$⊢ \underline{Ⅎ} j x$
107	106 2	nfeq	$⊢ Ⅎ j x = X$
108		breq2	$⊢ x = X \to (F (j) \leq x \leftrightarrow F (j) \leq X)$
109	107 108	ralbid	$⊢ x = X \to (\forall j \in Z F (j) \leq x \leftrightarrow \forall j \in Z F (j) \leq X)$
110	105 109	rspce	$⊢ (X \in ℝ \land \forall j \in Z F (j) \leq X) \to \exists x \in ℝ \forall j \in Z F (j) \leq x$
111	44 104 110	syl2anc	$⊢ φ \to \exists x \in ℝ \forall j \in Z F (j) \leq x$

Metamath Proof Explorer

Theorem limsupubuzlem

Proof