limsupequzlem

Description: Two functions that are eventually equal to one another have the same superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupequzlem.1	$⊢ Ⅎ k φ$
	limsupequzlem.2	$⊢ φ \to M \in ℤ$
	limsupequzlem.4	$⊢ φ \to F Fn ℤ_{\geq M}$
	limsupequzlem.5	$⊢ φ \to N \in ℤ$
	limsupequzlem.6	$⊢ φ \to G Fn ℤ_{\geq N}$
	limsupequzlem.7	$⊢ φ \to K \in ℤ$
	limsupequzlem.8	$⊢ (φ \land k \in ℤ_{\geq K}) \to F (k) = G (k)$
Assertion	limsupequzlem	$⊢ φ \to lim sup (F) = lim sup (G)$

Proof

Step	Hyp	Ref	Expression
1		limsupequzlem.1	$⊢ Ⅎ k φ$
2		limsupequzlem.2	$⊢ φ \to M \in ℤ$
3		limsupequzlem.4	$⊢ φ \to F Fn ℤ_{\geq M}$
4		limsupequzlem.5	$⊢ φ \to N \in ℤ$
5		limsupequzlem.6	$⊢ φ \to G Fn ℤ_{\geq N}$
6		limsupequzlem.7	$⊢ φ \to K \in ℤ$
7		limsupequzlem.8	$⊢ (φ \land k \in ℤ_{\geq K}) \to F (k) = G (k)$
8		eqid	$⊢ ℤ_{\geq K} = ℤ_{\geq K}$
9	6	adantr	$⊢ (φ \land k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{*} <)}) \to K \in ℤ$
10		eluzelz	$⊢ k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{*} <)} \to k \in ℤ$
11	10	adantl	$⊢ (φ \land k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{*} <)}) \to k \in ℤ$
12	6	zred	$⊢ φ \to K \in ℝ$
13	12	adantr	$⊢ (φ \land k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{*} <)}) \to K \in ℝ$
14	13	rexrd	$⊢ (φ \land k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)}) \to K \in ℝ^{}$
15		zssxr	$⊢ ℤ \subseteq ℝ^{*}$
16		tpssi	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to \{M, N, K\} \subseteq ℤ$
17	2 4 6 16	syl3anc	$⊢ φ \to \{M, N, K\} \subseteq ℤ$
18		xrltso	$⊢ < Or ℝ^{*}$
19	18	a1i	$⊢ φ \to < Or ℝ^{*}$
20		tpfi	$⊢ \{M, N, K\} \in Fin$
21	20	a1i	$⊢ φ \to \{M, N, K\} \in Fin$
22	2	tpnzd	$⊢ φ \to \{M, N, K\} \neq \emptyset$
23	15	a1i	$⊢ φ \to ℤ \subseteq ℝ^{*}$
24	17 23	sstrd	$⊢ φ \to \{M, N, K\} \subseteq ℝ^{*}$
25		fisupcl	$⊢ (< Or ℝ^{} \land (\{M, N, K\} \in Fin \land \{M, N, K\} \neq \emptyset \land \{M, N, K\} \subseteq ℝ^{})) \to sup (\{M, N, K\} ℝ^{*} <) \in \{M, N, K\}$
26	19 21 22 24 25	syl13anc	$⊢ φ \to sup (\{M, N, K\} ℝ^{*} <) \in \{M, N, K\}$
27	17 26	sseldd	$⊢ φ \to sup (\{M, N, K\} ℝ^{*} <) \in ℤ$
28	15 27	sselid	$⊢ φ \to sup (\{M, N, K\} ℝ^{} <) \in ℝ^{}$
29	28	adantr	$⊢ (φ \land k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)}) \to sup (\{M, N, K\} ℝ^{} <) \in ℝ^{*}$
30		eluzelre	$⊢ k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{*} <)} \to k \in ℝ$
31	30	adantl	$⊢ (φ \land k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{*} <)}) \to k \in ℝ$
32	31	rexrd	$⊢ (φ \land k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)}) \to k \in ℝ^{}$
33		tpid3g	$⊢ K \in ℤ \to K \in \{M, N, K\}$
34	6 33	syl	$⊢ φ \to K \in \{M, N, K\}$
35		eqid	$⊢ sup (\{M, N, K\} ℝ^{} <) = sup (\{M, N, K\} ℝ^{} <)$
36	24 34 35	supxrubd	$⊢ φ \to K \leq sup (\{M, N, K\} ℝ^{*} <)$
37	36	adantr	$⊢ (φ \land k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)}) \to K \leq sup (\{M, N, K\} ℝ^{} <)$
38		eluzle	$⊢ k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)} \to sup (\{M, N, K\} ℝ^{} <) \leq k$
39	38	adantl	$⊢ (φ \land k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)}) \to sup (\{M, N, K\} ℝ^{} <) \leq k$
40	14 29 32 37 39	xrletrd	$⊢ (φ \land k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{*} <)}) \to K \leq k$
41	8 9 11 40	eluzd	$⊢ (φ \land k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{*} <)}) \to k \in ℤ_{\geq K}$
42	41 7	syldan	$⊢ (φ \land k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{*} <)}) \to F (k) = G (k)$
43	1 42	ralrimia	$⊢ φ \to \forall k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{*} <)} F (k) = G (k)$
44		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
45		tpid1g	$⊢ M \in ℤ \to M \in \{M, N, K\}$
46	2 45	syl	$⊢ φ \to M \in \{M, N, K\}$
47	24 46 35	supxrubd	$⊢ φ \to M \leq sup (\{M, N, K\} ℝ^{*} <)$
48	44 2 27 47	eluzd	$⊢ φ \to sup (\{M, N, K\} ℝ^{*} <) \in ℤ_{\geq M}$
49		uzss	$⊢ sup (\{M, N, K\} ℝ^{} <) \in ℤ_{\geq M} \to ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)} \subseteq ℤ_{\geq M}$
50	48 49	syl	$⊢ φ \to ℤ_{\geq sup (\{M, N, K\} ℝ^{*} <)} \subseteq ℤ_{\geq M}$
51		eqid	$⊢ ℤ_{\geq N} = ℤ_{\geq N}$
52		tpid2g	$⊢ N \in ℤ \to N \in \{M, N, K\}$
53	4 52	syl	$⊢ φ \to N \in \{M, N, K\}$
54	24 53 35	supxrubd	$⊢ φ \to N \leq sup (\{M, N, K\} ℝ^{*} <)$
55	51 4 27 54	eluzd	$⊢ φ \to sup (\{M, N, K\} ℝ^{*} <) \in ℤ_{\geq N}$
56		uzss	$⊢ sup (\{M, N, K\} ℝ^{} <) \in ℤ_{\geq N} \to ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)} \subseteq ℤ_{\geq N}$
57	55 56	syl	$⊢ φ \to ℤ_{\geq sup (\{M, N, K\} ℝ^{*} <)} \subseteq ℤ_{\geq N}$
58		fvreseq0	$⊢ ((F Fn ℤ_{\geq M} \land G Fn ℤ_{\geq N}) \land (ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)} \subseteq ℤ_{\geq M} \land ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)} \subseteq ℤ_{\geq N})) \to ({F ↾}_{ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)}} = {G ↾}_{ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)}} \leftrightarrow \forall k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{*} <)} F (k) = G (k))$
59	3 5 50 57 58	syl22anc	$⊢ φ \to ({F ↾}_{ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)}} = {G ↾}_{ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)}} \leftrightarrow \forall k \in ℤ_{\geq sup (\{M, N, K\} ℝ^{*} <)} F (k) = G (k))$
60	43 59	mpbird	$⊢ φ \to {F ↾}_{ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)}} = {G ↾}_{ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)}}$
61	60	fveq2d	$⊢ φ \to lim sup ({F ↾}_{ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)}}) = lim sup ({G ↾}_{ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)}})$
62		eqid	$⊢ ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)} = ℤ_{\geq sup (\{M, N, K\} ℝ^{} <)}$
63		fvexd	$⊢ φ \to ℤ_{\geq M} \in V$
64	3 63	fnexd	$⊢ φ \to F \in V$
65	3	fndmd	$⊢ φ \to dom F = ℤ_{\geq M}$
66		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
67	65 66	eqsstrdi	$⊢ φ \to dom F \subseteq ℤ$
68	27 62 64 67	limsupresuz2	$⊢ φ \to lim sup ({F ↾}_{ℤ_{\geq sup (\{M, N, K\} ℝ^{*} <)}}) = lim sup (F)$
69		fvexd	$⊢ φ \to ℤ_{\geq N} \in V$
70	5 69	fnexd	$⊢ φ \to G \in V$
71	5	fndmd	$⊢ φ \to dom G = ℤ_{\geq N}$
72		uzssz	$⊢ ℤ_{\geq N} \subseteq ℤ$
73	71 72	eqsstrdi	$⊢ φ \to dom G \subseteq ℤ$
74	27 62 70 73	limsupresuz2	$⊢ φ \to lim sup ({G ↾}_{ℤ_{\geq sup (\{M, N, K\} ℝ^{*} <)}}) = lim sup (G)$
75	61 68 74	3eqtr3d	$⊢ φ \to lim sup (F) = lim sup (G)$

Metamath Proof Explorer

Theorem limsupequzlem

Proof