limsupvaluz2 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > limsupvaluz2		Structured version Visualization version GIF version

Theorem limsupvaluz2 45659

Description: The superior limit, when the domain of a real-valued function is a set of upper integers, and the superior limit is real. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

**Hypotheses**
Ref	Expression
limsupvaluz2.m	⊢ (𝜑 → 𝑀 ∈ ℤ)
limsupvaluz2.z	⊢ 𝑍 = (ℤ_≥‘𝑀)
limsupvaluz2.f	⊢ (𝜑 → 𝐹:𝑍⟶ℝ)
limsupvaluz2.r	⊢ (𝜑 → (lim sup‘𝐹) ∈ ℝ)

**Assertion**
Ref	Expression
limsupvaluz2	⊢ (𝜑 → (lim sup‘𝐹) = inf(ran (𝑘 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑘)), ℝ^*, < )), ℝ, < ))

Distinct variable groups: 𝑘,𝐹 𝑘,𝑍 Allowed substitution hints: 𝜑(𝑘) 𝑀(𝑘)

Proof of Theorem limsupvaluz2 Dummy variables 𝑖 𝑗 𝑥 𝑛 𝑚 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		limsupvaluz2.m	. . 3 ⊢ (𝜑 → 𝑀 ∈ ℤ)
2		limsupvaluz2.z	. . 3 ⊢ 𝑍 = (ℤ_≥‘𝑀)
3		limsupvaluz2.f	. . . 4 ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)
4	3	frexr 45300	. . 3 ⊢ (𝜑 → 𝐹:𝑍⟶ℝ^*)
5	1, 2, 4	limsupvaluz 45629	. 2 ⊢ (𝜑 → (lim sup‘𝐹) = inf(ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )), ℝ^, < ))
6	3	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐹:𝑍⟶ℝ)
7		id 22	. . . . . . . . . . 11 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍)
8	2, 7	uzssd2 45332	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 → (ℤ_≥‘𝑛) ⊆ 𝑍)
9	8	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (ℤ_≥‘𝑛) ⊆ 𝑍)
10	6, 9	feqresmpt 6991	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹 ↾ (ℤ_≥‘𝑛)) = (𝑚 ∈ (ℤ_≥‘𝑛) ↦ (𝐹‘𝑚)))
11	10	rneqd 5963	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ran (𝐹 ↾ (ℤ_≥‘𝑛)) = ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ (𝐹‘𝑚)))
12	11	supeq1d 9515	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ (𝐹‘𝑚)), ℝ^, < ))
13		nfcv 2908	. . . . . . . . . 10 ⊢ Ⅎ𝑚𝐹
14		limsupvaluz2.r	. . . . . . . . . . 11 ⊢ (𝜑 → (lim sup‘𝐹) ∈ ℝ)
15	14	renepnfd 11341	. . . . . . . . . 10 ⊢ (𝜑 → (lim sup‘𝐹) ≠ +∞)
16	13, 2, 3, 15	limsupubuz 45634	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥)
17	16	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥)
18		ssralv 4077	. . . . . . . . . . 11 ⊢ ((ℤ_≥‘𝑛) ⊆ 𝑍 → (∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥 → ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥))
19	8, 18	syl 17	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 → (∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥 → ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥))
20	19	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥 → ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥))
21	20	reximdv 3176	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑥 ∈ ℝ ∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥))
22	17, 21	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥)
23		nfv 1913	. . . . . . . 8 ⊢ Ⅎ𝑚(𝜑 ∧ 𝑛 ∈ 𝑍)
24	2	eluzelz2 45318	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ)
25		uzid 12918	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ (ℤ_≥‘𝑛))
26		ne0i 4364	. . . . . . . . . 10 ⊢ (𝑛 ∈ (ℤ_≥‘𝑛) → (ℤ_≥‘𝑛) ≠ ∅)
27	24, 25, 26	3syl 18	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝑍 → (ℤ_≥‘𝑛) ≠ ∅)
28	27	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (ℤ_≥‘𝑛) ≠ ∅)
29	6	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ_≥‘𝑛)) → 𝐹:𝑍⟶ℝ)
30	9	sselda 4008	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ_≥‘𝑛)) → 𝑚 ∈ 𝑍)
31	29, 30	ffvelcdmd 7119	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑚) ∈ ℝ)
32	23, 28, 31	supxrre3rnmpt 45344	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ (𝐹‘𝑚)), ℝ^*, < ) ∈ ℝ ↔ ∃𝑥 ∈ ℝ ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥))
33	22, 32	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ (𝐹‘𝑚)), ℝ^*, < ) ∈ ℝ)
34	12, 33	eqeltrd 2844	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < ) ∈ ℝ)
35	34	fmpttd 7149	. . . 4 ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < )):𝑍⟶ℝ)
36	35	frnd 6755	. . 3 ⊢ (𝜑 → ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < )) ⊆ ℝ)
37		nfv 1913	. . . 4 ⊢ Ⅎ𝑛𝜑
38		eqid 2740	. . . 4 ⊢ (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )) = (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))
39	1, 2	uzn0d 45340	. . . 4 ⊢ (𝜑 → 𝑍 ≠ ∅)
40	37, 34, 38, 39	rnmptn0 6275	. . 3 ⊢ (𝜑 → ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < )) ≠ ∅)
41		nfcv 2908	. . . . . . . . . 10 ⊢ Ⅎ𝑗𝐹
42	41, 1, 2, 4	limsupre3uz 45657	. . . . . . . . 9 ⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔ (∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 ∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗) ∧ ∃𝑥 ∈ ℝ ∃𝑖 ∈ 𝑍 ∀𝑗 ∈ (ℤ_≥‘𝑖)(𝐹‘𝑗) ≤ 𝑥)))
43	14, 42	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 ∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗) ∧ ∃𝑥 ∈ ℝ ∃𝑖 ∈ 𝑍 ∀𝑗 ∈ (ℤ_≥‘𝑖)(𝐹‘𝑗) ≤ 𝑥))
44	43	simpld 494	. . . . . . 7 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 ∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗))
45		simp-4r 783	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → 𝑥 ∈ ℝ)
46	45	rexrd 11340	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → 𝑥 ∈ ℝ^*)
47	4	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → 𝐹:𝑍⟶ℝ^*)
48	2	uztrn2 12922	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → 𝑗 ∈ 𝑍)
49	48	3adant1 1130	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → 𝑗 ∈ 𝑍)
50	47, 49	ffvelcdmd 7119	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → (𝐹‘𝑗) ∈ ℝ^*)
51	50	ad5ant134 1367	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → (𝐹‘𝑗) ∈ ℝ^*)
52		rnresss 6046	. . . . . . . . . . . . . . . 16 ⊢ ran (𝐹 ↾ (ℤ_≥‘𝑖)) ⊆ ran 𝐹
53	52	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ran (𝐹 ↾ (ℤ_≥‘𝑖)) ⊆ ran 𝐹)
54	3	frnd 6755	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran 𝐹 ⊆ ℝ)
55	54	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ran 𝐹 ⊆ ℝ)
56	53, 55	sstrd 4019	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ran (𝐹 ↾ (ℤ_≥‘𝑖)) ⊆ ℝ)
57		ressxr 11334	. . . . . . . . . . . . . . 15 ⊢ ℝ ⊆ ℝ^*
58	57	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ℝ ⊆ ℝ^*)
59	56, 58	sstrd 4019	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ran (𝐹 ↾ (ℤ_≥‘𝑖)) ⊆ ℝ^*)
60	59	supxrcld 45009	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) ∈ ℝ^)
61	60	ad5ant13 756	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) ∈ ℝ^)
62		simpr 484	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → 𝑥 ≤ (𝐹‘𝑗))
63	59	3adant3 1132	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → ran (𝐹 ↾ (ℤ_≥‘𝑖)) ⊆ ℝ^*)
64		fvres 6939	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑖) → ((𝐹 ↾ (ℤ_≥‘𝑖))‘𝑗) = (𝐹‘𝑗))
65	64	eqcomd 2746	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (ℤ_≥‘𝑖) → (𝐹‘𝑗) = ((𝐹 ↾ (ℤ_≥‘𝑖))‘𝑗))
66	65	3ad2ant3 1135	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → (𝐹‘𝑗) = ((𝐹 ↾ (ℤ_≥‘𝑖))‘𝑗))
67	3	ffnd 6748	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 Fn 𝑍)
68	67	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝐹 Fn 𝑍)
69		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ 𝑍 → 𝑖 ∈ 𝑍)
70	2, 69	uzssd2 45332	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ 𝑍 → (ℤ_≥‘𝑖) ⊆ 𝑍)
71	70	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (ℤ_≥‘𝑖) ⊆ 𝑍)
72		fnssres 6703	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 Fn 𝑍 ∧ (ℤ_≥‘𝑖) ⊆ 𝑍) → (𝐹 ↾ (ℤ_≥‘𝑖)) Fn (ℤ_≥‘𝑖))
73	68, 71, 72	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹 ↾ (ℤ_≥‘𝑖)) Fn (ℤ_≥‘𝑖))
74	73	3adant3 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → (𝐹 ↾ (ℤ_≥‘𝑖)) Fn (ℤ_≥‘𝑖))
75		simp3 1138	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → 𝑗 ∈ (ℤ_≥‘𝑖))
76		fnfvelrn 7114	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ↾ (ℤ_≥‘𝑖)) Fn (ℤ_≥‘𝑖) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → ((𝐹 ↾ (ℤ_≥‘𝑖))‘𝑗) ∈ ran (𝐹 ↾ (ℤ_≥‘𝑖)))
77	74, 75, 76	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → ((𝐹 ↾ (ℤ_≥‘𝑖))‘𝑗) ∈ ran (𝐹 ↾ (ℤ_≥‘𝑖)))
78	66, 77	eqeltrd 2844	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → (𝐹‘𝑗) ∈ ran (𝐹 ↾ (ℤ_≥‘𝑖)))
79		eqid 2740	. . . . . . . . . . . . 13 ⊢ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < )
80	63, 78, 79	supxrubd 45015	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → (𝐹‘𝑗) ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < ))
81	80	ad5ant134 1367	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → (𝐹‘𝑗) ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < ))
82	46, 51, 61, 62, 81	xrletrd 13224	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < ))
83	82	rexlimdva2 3163	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) → (∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗) → 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < )))
84	83	ralimdva 3173	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑖 ∈ 𝑍 ∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗) → ∀𝑖 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < )))
85	84	reximdva 3174	. . . . . . 7 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 ∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗) → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < )))
86	44, 85	mpd 15	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < ))
87	86	idi 1	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < ))
88		fveq2 6920	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑖 → (ℤ_≥‘𝑛) = (ℤ_≥‘𝑖))
89	88	reseq2d 6009	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑖 → (𝐹 ↾ (ℤ_≥‘𝑛)) = (𝐹 ↾ (ℤ_≥‘𝑖)))
90	89	rneqd 5963	. . . . . . . . . 10 ⊢ (𝑛 = 𝑖 → ran (𝐹 ↾ (ℤ_≥‘𝑛)) = ran (𝐹 ↾ (ℤ_≥‘𝑖)))
91	90	supeq1d 9515	. . . . . . . . 9 ⊢ (𝑛 = 𝑖 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ))
92		eqcom 2747	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑖 ↔ 𝑖 = 𝑛)
93	92	imbi1i 349	. . . . . . . . . 10 ⊢ ((𝑛 = 𝑖 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < )) ↔ (𝑖 = 𝑛 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < )))
94		eqcom 2747	. . . . . . . . . . 11 ⊢ (sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) ↔ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))
95	94	imbi2i 336	. . . . . . . . . 10 ⊢ ((𝑖 = 𝑛 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < )) ↔ (𝑖 = 𝑛 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )))
96	93, 95	bitri 275	. . . . . . . . 9 ⊢ ((𝑛 = 𝑖 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < )) ↔ (𝑖 = 𝑛 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )))
97	91, 96	mpbi 230	. . . . . . . 8 ⊢ (𝑖 = 𝑛 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))
98	97	breq2d 5178	. . . . . . 7 ⊢ (𝑖 = 𝑛 → (𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) ↔ 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )))
99	98	cbvralvw 3243	. . . . . 6 ⊢ (∀𝑖 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) ↔ ∀𝑛 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))
100	99	rexbii 3100	. . . . 5 ⊢ (∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) ↔ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))
101	87, 100	sylib 218	. . . 4 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < ))
102	34	elexd 3512	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < ) ∈ V)
103	37, 102	rnmptbd2 45158	. . . 4 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))𝑥 ≤ 𝑦))
104	101, 103	mpbid 232	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < ))𝑥 ≤ 𝑦)
105		infxrre 13398	. . 3 ⊢ ((ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )) ⊆ ℝ ∧ ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))𝑥 ≤ 𝑦) → inf(ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )), ℝ^, < ) = inf(ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )), ℝ, < ))
106	36, 40, 104, 105	syl3anc 1371	. 2 ⊢ (𝜑 → inf(ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )), ℝ^, < ) = inf(ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < )), ℝ, < ))
107		fveq2 6920	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (ℤ_≥‘𝑛) = (ℤ_≥‘𝑘))
108	107	reseq2d 6009	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (𝐹 ↾ (ℤ_≥‘𝑛)) = (𝐹 ↾ (ℤ_≥‘𝑘)))
109	108	rneqd 5963	. . . . . . 7 ⊢ (𝑛 = 𝑘 → ran (𝐹 ↾ (ℤ_≥‘𝑛)) = ran (𝐹 ↾ (ℤ_≥‘𝑘)))
110	109	supeq1d 9515	. . . . . 6 ⊢ (𝑛 = 𝑘 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑘)), ℝ^, < ))
111	110	cbvmptv 5279	. . . . 5 ⊢ (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )) = (𝑘 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑘)), ℝ^, < ))
112	111	rneqi 5962	. . . 4 ⊢ ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )) = ran (𝑘 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑘)), ℝ^, < ))
113	112	infeq1i 9547	. . 3 ⊢ inf(ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )), ℝ, < ) = inf(ran (𝑘 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑘)), ℝ^, < )), ℝ, < )
114	113	a1i 11	. 2 ⊢ (𝜑 → inf(ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )), ℝ, < ) = inf(ran (𝑘 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑘)), ℝ^, < )), ℝ, < ))
115	5, 106, 114	3eqtrd 2784	1 ⊢ (𝜑 → (lim sup‘𝐹) = inf(ran (𝑘 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑘)), ℝ^*, < )), ℝ, < ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 ∀wral 3067 ∃wrex 3076 Vcvv 3488 ⊆ wss 3976 ∅c0 4352 class class class wbr 5166 ↦ cmpt 5249 ran crn 5701 ↾ cres 5702 Fn wfn 6568 ⟶wf 6569 ‘cfv 6573 supcsup 9509 infcinf 9510 ℝcr 11183 ℝ^*cxr 11323 < clt 11324 ≤ cle 11325 ℤcz 12639 ℤ_≥cuz 12903 lim supclsp 15516

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-om 7904 df-1st 8030 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-er 8763 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-sup 9511 df-inf 9512 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-nn 12294 df-n0 12554 df-z 12640 df-uz 12904 df-ico 13413 df-fz 13568 df-fl 13843 df-ceil 13844 df-limsup 15517

This theorem is referenced by: supcnvlimsup 45661

W3C validator