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 44752

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 44393	. . 3 ⊢ (𝜑 → 𝐹:𝑍⟶ℝ^*)
5	1, 2, 4	limsupvaluz 44722	. 2 ⊢ (𝜑 → (lim sup‘𝐹) = inf(ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )), ℝ^, < ))
6	3	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐹:𝑍⟶ℝ)
7		id 22	. . . . . . . . . . 11 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍)
8	2, 7	uzssd2 44425	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 → (ℤ_≥‘𝑛) ⊆ 𝑍)
9	8	adantl 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (ℤ_≥‘𝑛) ⊆ 𝑍)
10	6, 9	feqresmpt 6960	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹 ↾ (ℤ_≥‘𝑛)) = (𝑚 ∈ (ℤ_≥‘𝑛) ↦ (𝐹‘𝑚)))
11	10	rneqd 5936	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ran (𝐹 ↾ (ℤ_≥‘𝑛)) = ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ (𝐹‘𝑚)))
12	11	supeq1d 9443	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ (𝐹‘𝑚)), ℝ^, < ))
13		nfcv 2901	. . . . . . . . . 10 ⊢ Ⅎ𝑚𝐹
14		limsupvaluz2.r	. . . . . . . . . . 11 ⊢ (𝜑 → (lim sup‘𝐹) ∈ ℝ)
15	14	renepnfd 11269	. . . . . . . . . 10 ⊢ (𝜑 → (lim sup‘𝐹) ≠ +∞)
16	13, 2, 3, 15	limsupubuz 44727	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥)
17	16	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥)
18		ssralv 4049	. . . . . . . . . . 11 ⊢ ((ℤ_≥‘𝑛) ⊆ 𝑍 → (∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥 → ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥))
19	8, 18	syl 17	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 → (∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥 → ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥))
20	19	adantl 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥 → ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥))
21	20	reximdv 3168	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑥 ∈ ℝ ∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥))
22	17, 21	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥)
23		nfv 1915	. . . . . . . 8 ⊢ Ⅎ𝑚(𝜑 ∧ 𝑛 ∈ 𝑍)
24	2	eluzelz2 44411	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ)
25		uzid 12841	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ (ℤ_≥‘𝑛))
26		ne0i 4333	. . . . . . . . . 10 ⊢ (𝑛 ∈ (ℤ_≥‘𝑛) → (ℤ_≥‘𝑛) ≠ ∅)
27	24, 25, 26	3syl 18	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝑍 → (ℤ_≥‘𝑛) ≠ ∅)
28	27	adantl 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (ℤ_≥‘𝑛) ≠ ∅)
29	6	adantr 479	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ_≥‘𝑛)) → 𝐹:𝑍⟶ℝ)
30	9	sselda 3981	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ_≥‘𝑛)) → 𝑚 ∈ 𝑍)
31	29, 30	ffvelcdmd 7086	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑚) ∈ ℝ)
32	23, 28, 31	supxrre3rnmpt 44437	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ (𝐹‘𝑚)), ℝ^*, < ) ∈ ℝ ↔ ∃𝑥 ∈ ℝ ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥))
33	22, 32	mpbird 256	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ (𝐹‘𝑚)), ℝ^*, < ) ∈ ℝ)
34	12, 33	eqeltrd 2831	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < ) ∈ ℝ)
35	34	fmpttd 7115	. . . 4 ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < )):𝑍⟶ℝ)
36	35	frnd 6724	. . 3 ⊢ (𝜑 → ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < )) ⊆ ℝ)
37		nfv 1915	. . . 4 ⊢ Ⅎ𝑛𝜑
38		eqid 2730	. . . 4 ⊢ (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )) = (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))
39	1, 2	uzn0d 44433	. . . 4 ⊢ (𝜑 → 𝑍 ≠ ∅)
40	37, 34, 38, 39	rnmptn0 6242	. . 3 ⊢ (𝜑 → ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < )) ≠ ∅)
41		nfcv 2901	. . . . . . . . . 10 ⊢ Ⅎ𝑗𝐹
42	41, 1, 2, 4	limsupre3uz 44750	. . . . . . . . 9 ⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔ (∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 ∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗) ∧ ∃𝑥 ∈ ℝ ∃𝑖 ∈ 𝑍 ∀𝑗 ∈ (ℤ_≥‘𝑖)(𝐹‘𝑗) ≤ 𝑥)))
43	14, 42	mpbid 231	. . . . . . . 8 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 ∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗) ∧ ∃𝑥 ∈ ℝ ∃𝑖 ∈ 𝑍 ∀𝑗 ∈ (ℤ_≥‘𝑖)(𝐹‘𝑗) ≤ 𝑥))
44	43	simpld 493	. . . . . . 7 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 ∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗))
45		simp-4r 780	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → 𝑥 ∈ ℝ)
46	45	rexrd 11268	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → 𝑥 ∈ ℝ^*)
47	4	3ad2ant1 1131	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → 𝐹:𝑍⟶ℝ^*)
48	2	uztrn2 12845	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → 𝑗 ∈ 𝑍)
49	48	3adant1 1128	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → 𝑗 ∈ 𝑍)
50	47, 49	ffvelcdmd 7086	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → (𝐹‘𝑗) ∈ ℝ^*)
51	50	ad5ant134 1365	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → (𝐹‘𝑗) ∈ ℝ^*)
52		rnresss 6016	. . . . . . . . . . . . . . . 16 ⊢ ran (𝐹 ↾ (ℤ_≥‘𝑖)) ⊆ ran 𝐹
53	52	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ran (𝐹 ↾ (ℤ_≥‘𝑖)) ⊆ ran 𝐹)
54	3	frnd 6724	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran 𝐹 ⊆ ℝ)
55	54	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ran 𝐹 ⊆ ℝ)
56	53, 55	sstrd 3991	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ran (𝐹 ↾ (ℤ_≥‘𝑖)) ⊆ ℝ)
57		ressxr 11262	. . . . . . . . . . . . . . 15 ⊢ ℝ ⊆ ℝ^*
58	57	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ℝ ⊆ ℝ^*)
59	56, 58	sstrd 3991	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ran (𝐹 ↾ (ℤ_≥‘𝑖)) ⊆ ℝ^*)
60	59	supxrcld 44097	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) ∈ ℝ^)
61	60	ad5ant13 753	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) ∈ ℝ^)
62		simpr 483	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → 𝑥 ≤ (𝐹‘𝑗))
63	59	3adant3 1130	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → ran (𝐹 ↾ (ℤ_≥‘𝑖)) ⊆ ℝ^*)
64		fvres 6909	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑖) → ((𝐹 ↾ (ℤ_≥‘𝑖))‘𝑗) = (𝐹‘𝑗))
65	64	eqcomd 2736	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (ℤ_≥‘𝑖) → (𝐹‘𝑗) = ((𝐹 ↾ (ℤ_≥‘𝑖))‘𝑗))
66	65	3ad2ant3 1133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → (𝐹‘𝑗) = ((𝐹 ↾ (ℤ_≥‘𝑖))‘𝑗))
67	3	ffnd 6717	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 Fn 𝑍)
68	67	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝐹 Fn 𝑍)
69		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ 𝑍 → 𝑖 ∈ 𝑍)
70	2, 69	uzssd2 44425	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ 𝑍 → (ℤ_≥‘𝑖) ⊆ 𝑍)
71	70	adantl 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (ℤ_≥‘𝑖) ⊆ 𝑍)
72		fnssres 6672	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 Fn 𝑍 ∧ (ℤ_≥‘𝑖) ⊆ 𝑍) → (𝐹 ↾ (ℤ_≥‘𝑖)) Fn (ℤ_≥‘𝑖))
73	68, 71, 72	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹 ↾ (ℤ_≥‘𝑖)) Fn (ℤ_≥‘𝑖))
74	73	3adant3 1130	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → (𝐹 ↾ (ℤ_≥‘𝑖)) Fn (ℤ_≥‘𝑖))
75		simp3 1136	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → 𝑗 ∈ (ℤ_≥‘𝑖))
76		fnfvelrn 7081	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ↾ (ℤ_≥‘𝑖)) Fn (ℤ_≥‘𝑖) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → ((𝐹 ↾ (ℤ_≥‘𝑖))‘𝑗) ∈ ran (𝐹 ↾ (ℤ_≥‘𝑖)))
77	74, 75, 76	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → ((𝐹 ↾ (ℤ_≥‘𝑖))‘𝑗) ∈ ran (𝐹 ↾ (ℤ_≥‘𝑖)))
78	66, 77	eqeltrd 2831	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → (𝐹‘𝑗) ∈ ran (𝐹 ↾ (ℤ_≥‘𝑖)))
79		eqid 2730	. . . . . . . . . . . . 13 ⊢ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < )
80	63, 78, 79	supxrubd 44103	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → (𝐹‘𝑗) ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < ))
81	80	ad5ant134 1365	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → (𝐹‘𝑗) ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < ))
82	46, 51, 61, 62, 81	xrletrd 13145	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < ))
83	82	rexlimdva2 3155	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) → (∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗) → 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < )))
84	83	ralimdva 3165	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑖 ∈ 𝑍 ∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗) → ∀𝑖 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < )))
85	84	reximdva 3166	. . . . . . 7 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 ∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗) → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < )))
86	44, 85	mpd 15	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < ))
87	86	idi 1	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < ))
88		fveq2 6890	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑖 → (ℤ_≥‘𝑛) = (ℤ_≥‘𝑖))
89	88	reseq2d 5980	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑖 → (𝐹 ↾ (ℤ_≥‘𝑛)) = (𝐹 ↾ (ℤ_≥‘𝑖)))
90	89	rneqd 5936	. . . . . . . . . 10 ⊢ (𝑛 = 𝑖 → ran (𝐹 ↾ (ℤ_≥‘𝑛)) = ran (𝐹 ↾ (ℤ_≥‘𝑖)))
91	90	supeq1d 9443	. . . . . . . . 9 ⊢ (𝑛 = 𝑖 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ))
92		eqcom 2737	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑖 ↔ 𝑖 = 𝑛)
93	92	imbi1i 348	. . . . . . . . . 10 ⊢ ((𝑛 = 𝑖 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < )) ↔ (𝑖 = 𝑛 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < )))
94		eqcom 2737	. . . . . . . . . . 11 ⊢ (sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) ↔ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))
95	94	imbi2i 335	. . . . . . . . . 10 ⊢ ((𝑖 = 𝑛 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < )) ↔ (𝑖 = 𝑛 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )))
96	93, 95	bitri 274	. . . . . . . . 9 ⊢ ((𝑛 = 𝑖 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < )) ↔ (𝑖 = 𝑛 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )))
97	91, 96	mpbi 229	. . . . . . . 8 ⊢ (𝑖 = 𝑛 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))
98	97	breq2d 5159	. . . . . . 7 ⊢ (𝑖 = 𝑛 → (𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) ↔ 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )))
99	98	cbvralvw 3232	. . . . . 6 ⊢ (∀𝑖 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) ↔ ∀𝑛 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))
100	99	rexbii 3092	. . . . 5 ⊢ (∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) ↔ ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))
101	87, 100	sylib 217	. . . 4 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < ))
102	34	elexd 3493	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < ) ∈ V)
103	37, 102	rnmptbd2 44251	. . . 4 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))𝑥 ≤ 𝑦))
104	101, 103	mpbid 231	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < ))𝑥 ≤ 𝑦)
105		infxrre 13319	. . 3 ⊢ ((ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )) ⊆ ℝ ∧ ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))𝑥 ≤ 𝑦) → inf(ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )), ℝ^, < ) = inf(ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )), ℝ, < ))
106	36, 40, 104, 105	syl3anc 1369	. 2 ⊢ (𝜑 → inf(ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )), ℝ^, < ) = inf(ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < )), ℝ, < ))
107		fveq2 6890	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → (ℤ_≥‘𝑛) = (ℤ_≥‘𝑘))
108	107	reseq2d 5980	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (𝐹 ↾ (ℤ_≥‘𝑛)) = (𝐹 ↾ (ℤ_≥‘𝑘)))
109	108	rneqd 5936	. . . . . . 7 ⊢ (𝑛 = 𝑘 → ran (𝐹 ↾ (ℤ_≥‘𝑛)) = ran (𝐹 ↾ (ℤ_≥‘𝑘)))
110	109	supeq1d 9443	. . . . . 6 ⊢ (𝑛 = 𝑘 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑘)), ℝ^, < ))
111	110	cbvmptv 5260	. . . . 5 ⊢ (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )) = (𝑘 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑘)), ℝ^, < ))
112	111	rneqi 5935	. . . 4 ⊢ ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )) = ran (𝑘 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑘)), ℝ^, < ))
113	112	infeq1i 9475	. . 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 2774	1 ⊢ (𝜑 → (lim sup‘𝐹) = inf(ran (𝑘 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑘)), ℝ^*, < )), ℝ, < ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1085 = wceq 1539 ∈ wcel 2104 ≠ wne 2938 ∀wral 3059 ∃wrex 3068 Vcvv 3472 ⊆ wss 3947 ∅c0 4321 class class class wbr 5147 ↦ cmpt 5230 ran crn 5676 ↾ cres 5677 Fn wfn 6537 ⟶wf 6538 ‘cfv 6542 supcsup 9437 infcinf 9438 ℝcr 11111 ℝ^*cxr 11251 < clt 11252 ≤ cle 11253 ℤcz 12562 ℤ_≥cuz 12826 lim supclsp 15418

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-er 8705 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-sup 9439 df-inf 9440 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-nn 12217 df-n0 12477 df-z 12563 df-uz 12827 df-ico 13334 df-fz 13489 df-fl 13761 df-ceil 13762 df-limsup 15419

This theorem is referenced by: supcnvlimsup 44754

W3C validator