smflimsuplem4

Description: If H converges, the limsup of F is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smflimsuplem4.1	$⊢ Ⅎ n φ$
	smflimsuplem4.m	$⊢ φ \to M \in ℤ$
	smflimsuplem4.z	$⊢ Z = ℤ_{\geq M}$
	smflimsuplem4.s	$⊢ φ \to S \in SAlg$
	smflimsuplem4.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smflimsuplem4.e	$⊢ E = (n \in Z ⟼ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\})$
	smflimsuplem4.h	$⊢ H = (n \in Z ⟼ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)))$
	smflimsuplem4.n	$⊢ φ \to N \in Z$
	smflimsuplem4.i	$⊢ φ \to x \in ⋂_{n \in ℤ_{\geq N}} dom H (n)$
	smflimsuplem4.c	$⊢ φ \to (n \in Z ⟼ H (n) (x)) \in dom ⇝$
Assertion	smflimsuplem4	$⊢ φ \to lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		smflimsuplem4.1	$⊢ Ⅎ n φ$
2		smflimsuplem4.m	$⊢ φ \to M \in ℤ$
3		smflimsuplem4.z	$⊢ Z = ℤ_{\geq M}$
4		smflimsuplem4.s	$⊢ φ \to S \in SAlg$
5		smflimsuplem4.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
6		smflimsuplem4.e	$⊢ E = (n \in Z ⟼ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\})$
7		smflimsuplem4.h	$⊢ H = (n \in Z ⟼ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)))$
8		smflimsuplem4.n	$⊢ φ \to N \in Z$
9		smflimsuplem4.i	$⊢ φ \to x \in ⋂_{n \in ℤ_{\geq N}} dom H (n)$
10		smflimsuplem4.c	$⊢ φ \to (n \in Z ⟼ H (n) (x)) \in dom ⇝$
11		nfv	$⊢ Ⅎ m φ$
12	3 8	eluzelz2d	$⊢ φ \to N \in ℤ$
13		eqid	$⊢ ℤ_{\geq N} = ℤ_{\geq N}$
14		fvexd	$⊢ (φ \land m \in Z) \to F (m) (x) \in V$
15		fvexd	$⊢ (φ \land m \in ℤ_{\geq N}) \to F (m) (x) \in V$
16	11 2 12 3 13 14 15	limsupequzmpt	$⊢ φ \to lim sup ((m \in Z ⟼ F (m) (x))) = lim sup ((m \in ℤ_{\geq N} ⟼ F (m) (x)))$
17	4	adantr	$⊢ (φ \land m \in ℤ_{\geq N}) \to S \in SAlg$
18	3 8	uzssd2	$⊢ φ \to ℤ_{\geq N} \subseteq Z$
19	18	sselda	$⊢ (φ \land m \in ℤ_{\geq N}) \to m \in Z$
20	5	ffvelrnda	$⊢ (φ \land m \in Z) \to F (m) \in SMblFn (S)$
21	19 20	syldan	$⊢ (φ \land m \in ℤ_{\geq N}) \to F (m) \in SMblFn (S)$
22		eqid	$⊢ dom F (m) = dom F (m)$
23	17 21 22	smff	$⊢ (φ \land m \in ℤ_{\geq N}) \to F (m) : dom F (m) ⟶ ℝ$
24	3 6 7 19	smflimsuplem1	$⊢ (φ \land m \in ℤ_{\geq N}) \to dom H (m) \subseteq dom F (m)$
25	9	adantr	$⊢ (φ \land m \in ℤ_{\geq N}) \to x \in ⋂_{n \in ℤ_{\geq N}} dom H (n)$
26		simpr	$⊢ (φ \land m \in ℤ_{\geq N}) \to m \in ℤ_{\geq N}$
27		fveq2	$⊢ n = m \to H (n) = H (m)$
28	27	dmeqd	$⊢ n = m \to dom H (n) = dom H (m)$
29	28	eleq2d	$⊢ n = m \to (x \in dom H (n) \leftrightarrow x \in dom H (m))$
30	25 26 29	eliind	$⊢ (φ \land m \in ℤ_{\geq N}) \to x \in dom H (m)$
31	24 30	sseldd	$⊢ (φ \land m \in ℤ_{\geq N}) \to x \in dom F (m)$
32	23 31	ffvelrnd	$⊢ (φ \land m \in ℤ_{\geq N}) \to F (m) (x) \in ℝ$
33	32	rexrd	$⊢ (φ \land m \in ℤ_{\geq N}) \to F (m) (x) \in ℝ^{*}$
34	11 12 13 33	limsupvaluzmpt	$⊢ φ \to lim sup ((m \in ℤ_{\geq N} ⟼ F (m) (x))) = sup (ran (n \in ℤ_{\geq N} ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)) ℝ^{} <)$
35	16 34	eqtrd	$⊢ φ \to lim sup ((m \in Z ⟼ F (m) (x))) = sup (ran (n \in ℤ_{\geq N} ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)) ℝ^{} <)$
36	18	adantr	$⊢ (φ \land n \in ℤ_{\geq N}) \to ℤ_{\geq N} \subseteq Z$
37		simpr	$⊢ (φ \land n \in ℤ_{\geq N}) \to n \in ℤ_{\geq N}$
38	36 37	sseldd	$⊢ (φ \land n \in ℤ_{\geq N}) \to n \in Z$
39	7	a1i	$⊢ φ \to H = (n \in Z ⟼ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)))$
40		fvex	$⊢ E (n) \in V$
41	40	mptex	$⊢ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)) \in V$
42	41	a1i	$⊢ (φ \land n \in Z) \to (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)) \in V$
43	39 42	fvmpt2d	$⊢ (φ \land n \in Z) \to H (n) = (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <))$
44	38 43	syldan	$⊢ (φ \land n \in ℤ_{\geq N}) \to H (n) = (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <))$
45	44	dmeqd	$⊢ (φ \land n \in ℤ_{\geq N}) \to dom H (n) = dom (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <))$
46		xrltso	$⊢ < Or ℝ^{*}$
47	46	supex	$⊢ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in V$
48		eqid	$⊢ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)) = (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <))$
49	47 48	dmmpti	$⊢ dom (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)) = E (n)$
50	49	a1i	$⊢ (φ \land n \in ℤ_{\geq N}) \to dom (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)) = E (n)$
51	45 50	eqtrd	$⊢ (φ \land n \in ℤ_{\geq N}) \to dom H (n) = E (n)$
52	1 51	iineq2d	$⊢ φ \to ⋂_{n \in ℤ_{\geq N}} dom H (n) = ⋂_{n \in ℤ_{\geq N}} E (n)$
53	9 52	eleqtrd	$⊢ φ \to x \in ⋂_{n \in ℤ_{\geq N}} E (n)$
54	53	adantr	$⊢ (φ \land n \in ℤ_{\geq N}) \to x \in ⋂_{n \in ℤ_{\geq N}} E (n)$
55		eliinid	$⊢ (x \in ⋂_{n \in ℤ_{\geq N}} E (n) \land n \in ℤ_{\geq N}) \to x \in E (n)$
56	54 37 55	syl2anc	$⊢ (φ \land n \in ℤ_{\geq N}) \to x \in E (n)$
57	47	a1i	$⊢ ((φ \land n \in ℤ_{\geq N}) \land x \in E (n)) \to sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in V$
58	44 57	fvmpt2d	$⊢ ((φ \land n \in ℤ_{\geq N}) \land x \in E (n)) \to H (n) (x) = sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)$
59	56 58	mpdan	$⊢ (φ \land n \in ℤ_{\geq N}) \to H (n) (x) = sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)$
60		eqid	$⊢ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\} = \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\}$
61	3	eluzelz2	$⊢ n \in Z \to n \in ℤ$
62		eqid	$⊢ ℤ_{\geq n} = ℤ_{\geq n}$
63	61 62	uzn0d	$⊢ n \in Z \to ℤ_{\geq n} \neq \emptyset$
64		fvex	$⊢ F (m) \in V$
65	64	dmex	$⊢ dom F (m) \in V$
66	65	rgenw	$⊢ \forall m \in ℤ_{\geq n} dom F (m) \in V$
67	66	a1i	$⊢ n \in Z \to \forall m \in ℤ_{\geq n} dom F (m) \in V$
68	63 67	iinexd	$⊢ n \in Z \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
69	68	adantl	$⊢ (φ \land n \in Z) \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
70	60 69	rabexd	$⊢ (φ \land n \in Z) \to \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\} \in V$
71	38 70	syldan	$⊢ (φ \land n \in ℤ_{\geq N}) \to \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\} \in V$
72	6	fvmpt2	$⊢ (n \in Z \land \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\} \in V) \to E (n) = \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\}$
73	38 71 72	syl2anc	$⊢ (φ \land n \in ℤ_{\geq N}) \to E (n) = \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\}$
74	56 73	eleqtrd	$⊢ (φ \land n \in ℤ_{\geq N}) \to x \in \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\}$
75		rabid	$⊢ x \in \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\} \leftrightarrow (x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \land sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ)$
76	74 75	sylib	$⊢ (φ \land n \in ℤ_{\geq N}) \to (x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \land sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ)$
77	76	simprd	$⊢ (φ \land n \in ℤ_{\geq N}) \to sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ$
78	59 77	eqeltrd	$⊢ (φ \land n \in ℤ_{\geq N}) \to H (n) (x) \in ℝ$
79	1 59	mpteq2da	$⊢ φ \to (n \in ℤ_{\geq N} ⟼ H (n) (x)) = (n \in ℤ_{\geq N} ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <))$
80		nfv	$⊢ Ⅎ k φ$
81		fveq2	$⊢ n = k \to ℤ_{\geq n} = ℤ_{\geq k}$
82	81	mpteq1d	$⊢ n = k \to (m \in ℤ_{\geq n} ⟼ F (m) (x)) = (m \in ℤ_{\geq k} ⟼ F (m) (x))$
83	82	rneqd	$⊢ n = k \to ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) = ran (m \in ℤ_{\geq k} ⟼ F (m) (x))$
84	83	supeq1d	$⊢ n = k \to sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) = sup (ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) ℝ^{} <)$
85		nfv	$⊢ Ⅎ m (n \in ℤ_{\geq N} \land k = n + 1)$
86		eluzelz	$⊢ n \in ℤ_{\geq N} \to n \in ℤ$
87	86	adantr	$⊢ (n \in ℤ_{\geq N} \land k = n + 1) \to n \in ℤ$
88		simpr	$⊢ (n \in ℤ_{\geq N} \land k = n + 1) \to k = n + 1$
89	87	peano2zd	$⊢ (n \in ℤ_{\geq N} \land k = n + 1) \to n + 1 \in ℤ$
90	88 89	eqeltrd	$⊢ (n \in ℤ_{\geq N} \land k = n + 1) \to k \in ℤ$
91	87	zred	$⊢ (n \in ℤ_{\geq N} \land k = n + 1) \to n \in ℝ$
92	90	zred	$⊢ (n \in ℤ_{\geq N} \land k = n + 1) \to k \in ℝ$
93	91	ltp1d	$⊢ (n \in ℤ_{\geq N} \land k = n + 1) \to n < n + 1$
94	88	eqcomd	$⊢ (n \in ℤ_{\geq N} \land k = n + 1) \to n + 1 = k$
95	93 94	breqtrd	$⊢ (n \in ℤ_{\geq N} \land k = n + 1) \to n < k$
96	91 92 95	ltled	$⊢ (n \in ℤ_{\geq N} \land k = n + 1) \to n \leq k$
97	62 87 90 96	eluzd	$⊢ (n \in ℤ_{\geq N} \land k = n + 1) \to k \in ℤ_{\geq n}$
98		uzss	$⊢ k \in ℤ_{\geq n} \to ℤ_{\geq k} \subseteq ℤ_{\geq n}$
99	97 98	syl	$⊢ (n \in ℤ_{\geq N} \land k = n + 1) \to ℤ_{\geq k} \subseteq ℤ_{\geq n}$
100		fvexd	$⊢ ((n \in ℤ_{\geq N} \land k = n + 1) \land m \in ℤ_{\geq k}) \to F (m) (x) \in V$
101	85 99 100	rnmptss2	$⊢ (n \in ℤ_{\geq N} \land k = n + 1) \to ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) \subseteq ran (m \in ℤ_{\geq n} ⟼ F (m) (x))$
102	101	3adant1	$⊢ (φ \land n \in ℤ_{\geq N} \land k = n + 1) \to ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) \subseteq ran (m \in ℤ_{\geq n} ⟼ F (m) (x))$
103		nfv	$⊢ Ⅎ m (φ \land n \in ℤ_{\geq N})$
104		eqid	$⊢ (m \in ℤ_{\geq n} ⟼ F (m) (x)) = (m \in ℤ_{\geq n} ⟼ F (m) (x))$
105		simpll	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to φ$
106	38 105	syldanl	$⊢ ((φ \land n \in ℤ_{\geq N}) \land m \in ℤ_{\geq n}) \to φ$
107	13	uztrn2	$⊢ (n \in ℤ_{\geq N} \land m \in ℤ_{\geq n}) \to m \in ℤ_{\geq N}$
108	107	adantll	$⊢ ((φ \land n \in ℤ_{\geq N}) \land m \in ℤ_{\geq n}) \to m \in ℤ_{\geq N}$
109	106 108 32	syl2anc	$⊢ ((φ \land n \in ℤ_{\geq N}) \land m \in ℤ_{\geq n}) \to F (m) (x) \in ℝ$
110	103 104 109	rnmptssd	$⊢ (φ \land n \in ℤ_{\geq N}) \to ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) \subseteq ℝ$
111		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
112	111	a1i	$⊢ (φ \land n \in ℤ_{\geq N}) \to ℝ \subseteq ℝ^{*}$
113	110 112	sstrd	$⊢ (φ \land n \in ℤ_{\geq N}) \to ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) \subseteq ℝ^{*}$
114	113	3adant3	$⊢ (φ \land n \in ℤ_{\geq N} \land k = n + 1) \to ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) \subseteq ℝ^{*}$
115		supxrss	$⊢ (ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) \subseteq ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) \land ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) \subseteq ℝ^{}) \to sup (ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) ℝ^{} <) \leq sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)$
116	102 114 115	syl2anc	$⊢ (φ \land n \in ℤ_{\geq N} \land k = n + 1) \to sup (ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) ℝ^{} <) \leq sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)$
117	3	fvexi	$⊢ Z \in V$
118	117	a1i	$⊢ φ \to Z \in V$
119		fvexd	$⊢ (φ \land n \in Z) \to H (n) (x) \in V$
120		fvexd	$⊢ φ \to ℤ_{\geq N} \in V$
121	1 37	ssdf	$⊢ φ \to ℤ_{\geq N} \subseteq ℤ_{\geq N}$
122		fvexd	$⊢ (φ \land n \in ℤ_{\geq N}) \to H (n) (x) \in V$
123		eqidd	$⊢ (φ \land n \in ℤ_{\geq N}) \to H (n) (x) = H (n) (x)$
124	1 12 13 118 18 119 120 121 122 123	climeldmeqmpt	$⊢ φ \to ((n \in Z ⟼ H (n) (x)) \in dom ⇝ \leftrightarrow (n \in ℤ_{\geq N} ⟼ H (n) (x)) \in dom ⇝)$
125	10 124	mpbid	$⊢ φ \to (n \in ℤ_{\geq N} ⟼ H (n) (x)) \in dom ⇝$
126	79 125	eqeltrrd	$⊢ φ \to (n \in ℤ_{\geq N} ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)) \in dom ⇝$
127	1 80 12 13 77 84 116 126	climinf2mpt	$⊢ φ \to (n \in ℤ_{\geq N} ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)) ⇝ sup (ran (n \in ℤ_{\geq N} ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)) ℝ^{*} <)$
128	79 127	eqbrtrd	$⊢ φ \to (n \in ℤ_{\geq N} ⟼ H (n) (x)) ⇝ sup (ran (n \in ℤ_{\geq N} ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)) ℝ^{} <)$
129	1 12 13 78 128	climreclmpt	$⊢ φ \to sup (ran (n \in ℤ_{\geq N} ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)) ℝ^{} <) \in ℝ$
130	35 129	eqeltrd	$⊢ φ \to lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ$

Metamath Proof Explorer

Theorem smflimsuplem4

Proof