limsupgre

Description: If a sequence of real numbers has upper bounded limit supremum, then all the partial suprema are real. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

	Ref	Expression
Hypotheses	limsupval.1	$⊢ G = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
	limsupgre.z	$⊢ Z = ℤ_{\geq M}$
Assertion	limsupgre	$⊢ (M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \to G : ℝ ⟶ ℝ$

Proof

Step	Hyp	Ref	Expression
1		limsupval.1	$⊢ G = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
2		limsupgre.z	$⊢ Z = ℤ_{\geq M}$
3		xrltso	$⊢ < Or ℝ^{*}$
4	3	supex	$⊢ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in V$
5	4	a1i	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land k \in ℝ) \to sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <) \in V$
6	1	a1i	$⊢ (M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \to G = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
7	1	limsupgval	$⊢ a \in ℝ \to G (a) = sup (F [[a, +∞)] \cap ℝ^{} ℝ^{} <)$
8	7	adantl	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to G (a) = sup (F [[a, +∞)] \cap ℝ^{} ℝ^{} <)$
9		simpl3	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to lim sup (F) < +∞$
10		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
11	2 10	eqsstri	$⊢ Z \subseteq ℤ$
12		zssre	$⊢ ℤ \subseteq ℝ$
13	11 12	sstri	$⊢ Z \subseteq ℝ$
14	13	a1i	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to Z \subseteq ℝ$
15		simpl2	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to F : Z ⟶ ℝ$
16		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
17		fss	$⊢ (F : Z ⟶ ℝ \land ℝ \subseteq ℝ^{}) \to F : Z ⟶ ℝ^{}$
18	15 16 17	sylancl	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to F : Z ⟶ ℝ^{*}$
19		pnfxr	$⊢ +∞ \in ℝ^{*}$
20	19	a1i	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to +∞ \in ℝ^{*}$
21	1	limsuplt	$⊢ (Z \subseteq ℝ \land F : Z ⟶ ℝ^{} \land +∞ \in ℝ^{}) \to (lim sup (F) < +∞ \leftrightarrow \exists n \in ℝ G (n) < +∞)$
22	14 18 20 21	syl3anc	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to (lim sup (F) < +∞ \leftrightarrow \exists n \in ℝ G (n) < +∞)$
23	9 22	mpbid	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to \exists n \in ℝ G (n) < +∞$
24		fzfi	$⊢ (M \dots ⌊n⌋) \in Fin$
25	15	adantr	$⊢ (((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \to F : Z ⟶ ℝ$
26		elfzuz	$⊢ m \in (M \dots ⌊n⌋) \to m \in ℤ_{\geq M}$
27	26 2	eleqtrrdi	$⊢ m \in (M \dots ⌊n⌋) \to m \in Z$
28		ffvelrn	$⊢ (F : Z ⟶ ℝ \land m \in Z) \to F (m) \in ℝ$
29	25 27 28	syl2an	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land m \in (M \dots ⌊n⌋)) \to F (m) \in ℝ$
30	29	ralrimiva	$⊢ (((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \to \forall m \in (M \dots ⌊n⌋) F (m) \in ℝ$
31		fimaxre3	$⊢ ((M \dots ⌊n⌋) \in Fin \land \forall m \in (M \dots ⌊n⌋) F (m) \in ℝ) \to \exists r \in ℝ \forall m \in (M \dots ⌊n⌋) F (m) \leq r$
32	24 30 31	sylancr	$⊢ (((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \to \exists r \in ℝ \forall m \in (M \dots ⌊n⌋) F (m) \leq r$
33		simpr	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to a \in ℝ$
34	33	ad2antrr	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to a \in ℝ$
35	1	limsupgf	$⊢ G : ℝ ⟶ ℝ^{*}$
36	35	ffvelrni	$⊢ a \in ℝ \to G (a) \in ℝ^{*}$
37	34 36	syl	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to G (a) \in ℝ^{*}$
38		simprl	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to r \in ℝ$
39	16 38	sseldi	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to r \in ℝ^{*}$
40		simprl	$⊢ (((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \to n \in ℝ$
41	40	adantr	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to n \in ℝ$
42	35	ffvelrni	$⊢ n \in ℝ \to G (n) \in ℝ^{*}$
43	41 42	syl	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to G (n) \in ℝ^{*}$
44	39 43	ifcld	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to if (G (n) \leq r, r, G (n)) \in ℝ^{*}$
45	19	a1i	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to +∞ \in ℝ^{*}$
46	40	ad2antrr	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to n \in ℝ$
47	13	a1i	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to Z \subseteq ℝ$
48	47	sselda	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to i \in ℝ$
49	43	xrleidd	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to G (n) \leq G (n)$
50	18	ad2antrr	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to F : Z ⟶ ℝ^{*}$
51	1	limsupgle	$⊢ ((Z \subseteq ℝ \land F : Z ⟶ ℝ^{}) \land n \in ℝ \land G (n) \in ℝ^{}) \to (G (n) \leq G (n) \leftrightarrow \forall i \in Z (n \leq i \to F (i) \leq G (n)))$
52	47 50 41 43 51	syl211anc	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to (G (n) \leq G (n) \leftrightarrow \forall i \in Z (n \leq i \to F (i) \leq G (n)))$
53	49 52	mpbid	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to \forall i \in Z (n \leq i \to F (i) \leq G (n))$
54	53	r19.21bi	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to (n \leq i \to F (i) \leq G (n))$
55	54	imp	$⊢ ((((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \land n \leq i) \to F (i) \leq G (n)$
56	46 42	syl	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to G (n) \in ℝ^{*}$
57	39	adantr	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to r \in ℝ^{*}$
58		xrmax1	$⊢ (G (n) \in ℝ^{} \land r \in ℝ^{}) \to G (n) \leq if (G (n) \leq r, r, G (n))$
59	56 57 58	syl2anc	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to G (n) \leq if (G (n) \leq r, r, G (n))$
60	50	ffvelrnda	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to F (i) \in ℝ^{*}$
61	44	adantr	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to if (G (n) \leq r, r, G (n)) \in ℝ^{*}$
62		xrletr	$⊢ (F (i) \in ℝ^{} \land G (n) \in ℝ^{} \land if (G (n) \leq r, r, G (n)) \in ℝ^{*}) \to ((F (i) \leq G (n) \land G (n) \leq if (G (n) \leq r, r, G (n))) \to F (i) \leq if (G (n) \leq r, r, G (n)))$
63	60 56 61 62	syl3anc	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to ((F (i) \leq G (n) \land G (n) \leq if (G (n) \leq r, r, G (n))) \to F (i) \leq if (G (n) \leq r, r, G (n)))$
64	59 63	mpan2d	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to (F (i) \leq G (n) \to F (i) \leq if (G (n) \leq r, r, G (n)))$
65	64	adantr	$⊢ ((((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \land n \leq i) \to (F (i) \leq G (n) \to F (i) \leq if (G (n) \leq r, r, G (n)))$
66	55 65	mpd	$⊢ ((((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \land n \leq i) \to F (i) \leq if (G (n) \leq r, r, G (n))$
67		fveq2	$⊢ m = i \to F (m) = F (i)$
68	67	breq1d	$⊢ m = i \to (F (m) \leq r \leftrightarrow F (i) \leq r)$
69		simprr	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to \forall m \in (M \dots ⌊n⌋) F (m) \leq r$
70	69	ad2antrr	$⊢ ((((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \land i \leq n) \to \forall m \in (M \dots ⌊n⌋) F (m) \leq r$
71		simpr	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to i \in Z$
72	71 2	eleqtrdi	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to i \in ℤ_{\geq M}$
73	41	flcld	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to ⌊n⌋ \in ℤ$
74	73	adantr	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to ⌊n⌋ \in ℤ$
75		elfz5	$⊢ (i \in ℤ_{\geq M} \land ⌊n⌋ \in ℤ) \to (i \in (M \dots ⌊n⌋) \leftrightarrow i \leq ⌊n⌋)$
76	72 74 75	syl2anc	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to (i \in (M \dots ⌊n⌋) \leftrightarrow i \leq ⌊n⌋)$
77	11 71	sseldi	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to i \in ℤ$
78		flge	$⊢ (n \in ℝ \land i \in ℤ) \to (i \leq n \leftrightarrow i \leq ⌊n⌋)$
79	46 77 78	syl2anc	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to (i \leq n \leftrightarrow i \leq ⌊n⌋)$
80	76 79	bitr4d	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to (i \in (M \dots ⌊n⌋) \leftrightarrow i \leq n)$
81	80	biimpar	$⊢ ((((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \land i \leq n) \to i \in (M \dots ⌊n⌋)$
82	68 70 81	rspcdva	$⊢ ((((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \land i \leq n) \to F (i) \leq r$
83		xrmax2	$⊢ (G (n) \in ℝ^{} \land r \in ℝ^{}) \to r \leq if (G (n) \leq r, r, G (n))$
84	43 39 83	syl2anc	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to r \leq if (G (n) \leq r, r, G (n))$
85	84	adantr	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to r \leq if (G (n) \leq r, r, G (n))$
86		xrletr	$⊢ (F (i) \in ℝ^{} \land r \in ℝ^{} \land if (G (n) \leq r, r, G (n)) \in ℝ^{*}) \to ((F (i) \leq r \land r \leq if (G (n) \leq r, r, G (n))) \to F (i) \leq if (G (n) \leq r, r, G (n)))$
87	60 57 61 86	syl3anc	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to ((F (i) \leq r \land r \leq if (G (n) \leq r, r, G (n))) \to F (i) \leq if (G (n) \leq r, r, G (n)))$
88	85 87	mpan2d	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to (F (i) \leq r \to F (i) \leq if (G (n) \leq r, r, G (n)))$
89	88	adantr	$⊢ ((((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \land i \leq n) \to (F (i) \leq r \to F (i) \leq if (G (n) \leq r, r, G (n)))$
90	82 89	mpd	$⊢ ((((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \land i \leq n) \to F (i) \leq if (G (n) \leq r, r, G (n))$
91	46 48 66 90	lecasei	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to F (i) \leq if (G (n) \leq r, r, G (n))$
92	91	a1d	$⊢ (((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \land i \in Z) \to (a \leq i \to F (i) \leq if (G (n) \leq r, r, G (n)))$
93	92	ralrimiva	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to \forall i \in Z (a \leq i \to F (i) \leq if (G (n) \leq r, r, G (n)))$
94	1	limsupgle	$⊢ ((Z \subseteq ℝ \land F : Z ⟶ ℝ^{}) \land a \in ℝ \land if (G (n) \leq r, r, G (n)) \in ℝ^{}) \to (G (a) \leq if (G (n) \leq r, r, G (n)) \leftrightarrow \forall i \in Z (a \leq i \to F (i) \leq if (G (n) \leq r, r, G (n))))$
95	47 50 34 44 94	syl211anc	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to (G (a) \leq if (G (n) \leq r, r, G (n)) \leftrightarrow \forall i \in Z (a \leq i \to F (i) \leq if (G (n) \leq r, r, G (n))))$
96	93 95	mpbird	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to G (a) \leq if (G (n) \leq r, r, G (n))$
97	38	ltpnfd	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to r < +∞$
98		simplrr	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to G (n) < +∞$
99		breq1	$⊢ r = if (G (n) \leq r, r, G (n)) \to (r < +∞ \leftrightarrow if (G (n) \leq r, r, G (n)) < +∞)$
100		breq1	$⊢ G (n) = if (G (n) \leq r, r, G (n)) \to (G (n) < +∞ \leftrightarrow if (G (n) \leq r, r, G (n)) < +∞)$
101	99 100	ifboth	$⊢ (r < +∞ \land G (n) < +∞) \to if (G (n) \leq r, r, G (n)) < +∞$
102	97 98 101	syl2anc	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to if (G (n) \leq r, r, G (n)) < +∞$
103	37 44 45 96 102	xrlelttrd	$⊢ ((((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \land (r \in ℝ \land \forall m \in (M \dots ⌊n⌋) F (m) \leq r)) \to G (a) < +∞$
104	32 103	rexlimddv	$⊢ (((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \land (n \in ℝ \land G (n) < +∞)) \to G (a) < +∞$
105	23 104	rexlimddv	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to G (a) < +∞$
106	8 105	eqbrtrrd	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to sup (F [[a, +∞)] \cap ℝ^{} ℝ^{} <) < +∞$
107		imassrn	$⊢ F [[a, +∞)] \subseteq ran F$
108	15	frnd	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to ran F \subseteq ℝ$
109	107 108	sstrid	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to F [[a, +∞)] \subseteq ℝ$
110	109 16	sstrdi	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to F [[a, +∞)] \subseteq ℝ^{*}$
111		df-ss	$⊢ F [[a, +∞)] \subseteq ℝ^{} \leftrightarrow F [[a, +∞)] \cap ℝ^{} = F [[a, +∞)]$
112	110 111	sylib	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to F [[a, +∞)] \cap ℝ^{*} = F [[a, +∞)]$
113	112 109	eqsstrd	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to F [[a, +∞)] \cap ℝ^{*} \subseteq ℝ$
114		simpl1	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to M \in ℤ$
115		flcl	$⊢ a \in ℝ \to ⌊a⌋ \in ℤ$
116	115	adantl	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to ⌊a⌋ \in ℤ$
117	116	peano2zd	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to ⌊a⌋ + 1 \in ℤ$
118	117 114	ifcld	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M) \in ℤ$
119	114	zred	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to M \in ℝ$
120	117	zred	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to ⌊a⌋ + 1 \in ℝ$
121		max1	$⊢ (M \in ℝ \land ⌊a⌋ + 1 \in ℝ) \to M \leq if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M)$
122	119 120 121	syl2anc	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to M \leq if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M)$
123		eluz2	$⊢ if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M) \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M) \in ℤ \land M \leq if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M))$
124	114 118 122 123	syl3anbrc	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M) \in ℤ_{\geq M}$
125	124 2	eleqtrrdi	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M) \in Z$
126	15	fdmd	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to dom F = Z$
127	125 126	eleqtrrd	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M) \in dom F$
128	118	zred	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M) \in ℝ$
129		fllep1	$⊢ a \in ℝ \to a \leq ⌊a⌋ + 1$
130	129	adantl	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to a \leq ⌊a⌋ + 1$
131		max2	$⊢ (M \in ℝ \land ⌊a⌋ + 1 \in ℝ) \to ⌊a⌋ + 1 \leq if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M)$
132	119 120 131	syl2anc	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to ⌊a⌋ + 1 \leq if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M)$
133	33 120 128 130 132	letrd	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to a \leq if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M)$
134		elicopnf	$⊢ a \in ℝ \to (if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M) \in [a, +∞) \leftrightarrow (if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M) \in ℝ \land a \leq if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M)))$
135	134	adantl	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to (if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M) \in [a, +∞) \leftrightarrow (if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M) \in ℝ \land a \leq if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M)))$
136	128 133 135	mpbir2and	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M) \in [a, +∞)$
137		inelcm	$⊢ (if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M) \in dom F \land if (M \leq ⌊a⌋ + 1, ⌊a⌋ + 1, M) \in [a, +∞)) \to dom F \cap [a, +∞) \neq \emptyset$
138	127 136 137	syl2anc	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to dom F \cap [a, +∞) \neq \emptyset$
139		imadisj	$⊢ F [[a, +∞)] = \emptyset \leftrightarrow dom F \cap [a, +∞) = \emptyset$
140	139	necon3bii	$⊢ F [[a, +∞)] \neq \emptyset \leftrightarrow dom F \cap [a, +∞) \neq \emptyset$
141	138 140	sylibr	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to F [[a, +∞)] \neq \emptyset$
142	112 141	eqnetrd	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to F [[a, +∞)] \cap ℝ^{*} \neq \emptyset$
143		supxrre1	$⊢ (F [[a, +∞)] \cap ℝ^{} \subseteq ℝ \land F [[a, +∞)] \cap ℝ^{} \neq \emptyset) \to (sup (F [[a, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ \leftrightarrow sup (F [[a, +∞)] \cap ℝ^{} ℝ^{} <) < +∞)$
144	113 142 143	syl2anc	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to (sup (F [[a, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ \leftrightarrow sup (F [[a, +∞)] \cap ℝ^{} ℝ^{} <) < +∞)$
145	106 144	mpbird	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to sup (F [[a, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ$
146	8 145	eqeltrd	$⊢ ((M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \land a \in ℝ) \to G (a) \in ℝ$
147	5 6 146	fmpt2d	$⊢ (M \in ℤ \land F : Z ⟶ ℝ \land lim sup (F) < +∞) \to G : ℝ ⟶ ℝ$

Metamath Proof Explorer

Theorem limsupgre

Proof