supcnvlimsup - Mathbox for Glauco Siliprandi

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

Theorem supcnvlimsup 39972

Description: If a function on a set of upper integers has a real superior limit, the supremum of the rightmost parts of the function, converges to that superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

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

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

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

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

Step	Hyp	Ref	Expression
1		supcnvlimsup.z	. . 3 ⊢ 𝑍 = (ℤ_≥‘𝑀)
2		supcnvlimsup.m	. . 3 ⊢ (𝜑 → 𝑀 ∈ ℤ)
3		supcnvlimsup.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝑍⟶ℝ)
4	3	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐹:𝑍⟶ℝ)
5		id 22	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍)
6	1, 5	uzssd2 39644	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝑍 → (ℤ_≥‘𝑛) ⊆ 𝑍)
7	6	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (ℤ_≥‘𝑛) ⊆ 𝑍)
8	4, 7	feqresmpt 6250	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹 ↾ (ℤ_≥‘𝑛)) = (𝑚 ∈ (ℤ_≥‘𝑛) ↦ (𝐹‘𝑚)))
9	8	rneqd 5353	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ran (𝐹 ↾ (ℤ_≥‘𝑛)) = ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ (𝐹‘𝑚)))
10	9	supeq1d 8352	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ (𝐹‘𝑚)), ℝ^, < ))
11		nfcv 2764	. . . . . . . . 9 ⊢ Ⅎ𝑚𝐹
12		supcnvlimsup.r	. . . . . . . . . 10 ⊢ (𝜑 → (lim sup‘𝐹) ∈ ℝ)
13	12	renepnfd 10090	. . . . . . . . 9 ⊢ (𝜑 → (lim sup‘𝐹) ≠ +∞)
14	11, 1, 3, 13	limsupubuz 39945	. . . . . . . 8 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥)
15	14	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥)
16		ssralv 3666	. . . . . . . . . 10 ⊢ ((ℤ_≥‘𝑛) ⊆ 𝑍 → (∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥 → ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥))
17	6, 16	syl 17	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝑍 → (∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥 → ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥))
18	17	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥 → ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥))
19	18	reximdv 3016	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑥 ∈ ℝ ∀𝑚 ∈ 𝑍 (𝐹‘𝑚) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥))
20	15, 19	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥)
21		nfv 1843	. . . . . . 7 ⊢ Ⅎ𝑚(𝜑 ∧ 𝑛 ∈ 𝑍)
22	1	eluzelz2 39627	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ)
23		uzid 11702	. . . . . . . . 9 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ (ℤ_≥‘𝑛))
24		ne0i 3921	. . . . . . . . 9 ⊢ (𝑛 ∈ (ℤ_≥‘𝑛) → (ℤ_≥‘𝑛) ≠ ∅)
25	22, 23, 24	3syl 18	. . . . . . . 8 ⊢ (𝑛 ∈ 𝑍 → (ℤ_≥‘𝑛) ≠ ∅)
26	25	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (ℤ_≥‘𝑛) ≠ ∅)
27	4	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ_≥‘𝑛)) → 𝐹:𝑍⟶ℝ)
28	7	sselda 3603	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ_≥‘𝑛)) → 𝑚 ∈ 𝑍)
29	27, 28	ffvelrnd 6360	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ_≥‘𝑛)) → (𝐹‘𝑚) ∈ ℝ)
30	21, 26, 29	supxrre3rnmpt 39656	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ (𝐹‘𝑚)), ℝ^*, < ) ∈ ℝ ↔ ∃𝑥 ∈ ℝ ∀𝑚 ∈ (ℤ_≥‘𝑛)(𝐹‘𝑚) ≤ 𝑥))
31	20, 30	mpbird 247	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → sup(ran (𝑚 ∈ (ℤ_≥‘𝑛) ↦ (𝐹‘𝑚)), ℝ^*, < ) ∈ ℝ)
32	10, 31	eqeltrd 2701	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < ) ∈ ℝ)
33		eqid 2622	. . . 4 ⊢ (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )) = (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))
34	32, 33	fmptd 6385	. . 3 ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < )):𝑍⟶ℝ)
35		eqid 2622	. . . . . . . . . 10 ⊢ (ℤ_≥‘𝑖) = (ℤ_≥‘𝑖)
36	1	eluzelz2 39627	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑍 → 𝑖 ∈ ℤ)
37	36	peano2zd 11485	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑍 → (𝑖 + 1) ∈ ℤ)
38	36	zred 11482	. . . . . . . . . . 11 ⊢ (𝑖 ∈ 𝑍 → 𝑖 ∈ ℝ)
39		lep1 10862	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ℝ → 𝑖 ≤ (𝑖 + 1))
40	38, 39	syl 17	. . . . . . . . . 10 ⊢ (𝑖 ∈ 𝑍 → 𝑖 ≤ (𝑖 + 1))
41	35, 36, 37, 40	eluzd 39635	. . . . . . . . 9 ⊢ (𝑖 ∈ 𝑍 → (𝑖 + 1) ∈ (ℤ_≥‘𝑖))
42		uzss 11708	. . . . . . . . 9 ⊢ ((𝑖 + 1) ∈ (ℤ_≥‘𝑖) → (ℤ_≥‘(𝑖 + 1)) ⊆ (ℤ_≥‘𝑖))
43	41, 42	syl 17	. . . . . . . 8 ⊢ (𝑖 ∈ 𝑍 → (ℤ_≥‘(𝑖 + 1)) ⊆ (ℤ_≥‘𝑖))
44		ssres2 5425	. . . . . . . 8 ⊢ ((ℤ_≥‘(𝑖 + 1)) ⊆ (ℤ_≥‘𝑖) → (𝐹 ↾ (ℤ_≥‘(𝑖 + 1))) ⊆ (𝐹 ↾ (ℤ_≥‘𝑖)))
45	43, 44	syl 17	. . . . . . 7 ⊢ (𝑖 ∈ 𝑍 → (𝐹 ↾ (ℤ_≥‘(𝑖 + 1))) ⊆ (𝐹 ↾ (ℤ_≥‘𝑖)))
46		rnss 5354	. . . . . . 7 ⊢ ((𝐹 ↾ (ℤ_≥‘(𝑖 + 1))) ⊆ (𝐹 ↾ (ℤ_≥‘𝑖)) → ran (𝐹 ↾ (ℤ_≥‘(𝑖 + 1))) ⊆ ran (𝐹 ↾ (ℤ_≥‘𝑖)))
47	45, 46	syl 17	. . . . . 6 ⊢ (𝑖 ∈ 𝑍 → ran (𝐹 ↾ (ℤ_≥‘(𝑖 + 1))) ⊆ ran (𝐹 ↾ (ℤ_≥‘𝑖)))
48	47	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ran (𝐹 ↾ (ℤ_≥‘(𝑖 + 1))) ⊆ ran (𝐹 ↾ (ℤ_≥‘𝑖)))
49		rnresss 39365	. . . . . . . 8 ⊢ ran (𝐹 ↾ (ℤ_≥‘𝑖)) ⊆ ran 𝐹
50	49	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ran (𝐹 ↾ (ℤ_≥‘𝑖)) ⊆ ran 𝐹)
51	3	frnd 39426	. . . . . . . 8 ⊢ (𝜑 → ran 𝐹 ⊆ ℝ)
52	51	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ran 𝐹 ⊆ ℝ)
53	50, 52	sstrd 3613	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ran (𝐹 ↾ (ℤ_≥‘𝑖)) ⊆ ℝ)
54		ressxr 10083	. . . . . . 7 ⊢ ℝ ⊆ ℝ^*
55	54	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ℝ ⊆ ℝ^*)
56	53, 55	sstrd 3613	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ran (𝐹 ↾ (ℤ_≥‘𝑖)) ⊆ ℝ^*)
57		supxrss 12162	. . . . 5 ⊢ ((ran (𝐹 ↾ (ℤ_≥‘(𝑖 + 1))) ⊆ ran (𝐹 ↾ (ℤ_≥‘𝑖)) ∧ ran (𝐹 ↾ (ℤ_≥‘𝑖)) ⊆ ℝ^) → sup(ran (𝐹 ↾ (ℤ_≥‘(𝑖 + 1))), ℝ^, < ) ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < ))
58	48, 56, 57	syl2anc 693	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → sup(ran (𝐹 ↾ (ℤ_≥‘(𝑖 + 1))), ℝ^, < ) ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ))
59		eqidd 2623	. . . . . . 7 ⊢ (𝑖 ∈ 𝑍 → (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )) = (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )))
60		fveq2 6191	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑖 + 1) → (ℤ_≥‘𝑛) = (ℤ_≥‘(𝑖 + 1)))
61	60	reseq2d 5396	. . . . . . . . . 10 ⊢ (𝑛 = (𝑖 + 1) → (𝐹 ↾ (ℤ_≥‘𝑛)) = (𝐹 ↾ (ℤ_≥‘(𝑖 + 1))))
62	61	rneqd 5353	. . . . . . . . 9 ⊢ (𝑛 = (𝑖 + 1) → ran (𝐹 ↾ (ℤ_≥‘𝑛)) = ran (𝐹 ↾ (ℤ_≥‘(𝑖 + 1))))
63	62	supeq1d 8352	. . . . . . . 8 ⊢ (𝑛 = (𝑖 + 1) → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘(𝑖 + 1))), ℝ^, < ))
64	63	adantl 482	. . . . . . 7 ⊢ ((𝑖 ∈ 𝑍 ∧ 𝑛 = (𝑖 + 1)) → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘(𝑖 + 1))), ℝ^, < ))
65	1	peano2uzs 11742	. . . . . . 7 ⊢ (𝑖 ∈ 𝑍 → (𝑖 + 1) ∈ 𝑍)
66		xrltso 11974	. . . . . . . . 9 ⊢ < Or ℝ^*
67	66	supex 8369	. . . . . . . 8 ⊢ sup(ran (𝐹 ↾ (ℤ_≥‘(𝑖 + 1))), ℝ^*, < ) ∈ V
68	67	a1i 11	. . . . . . 7 ⊢ (𝑖 ∈ 𝑍 → sup(ran (𝐹 ↾ (ℤ_≥‘(𝑖 + 1))), ℝ^*, < ) ∈ V)
69	59, 64, 65, 68	fvmptd 6288	. . . . . 6 ⊢ (𝑖 ∈ 𝑍 → ((𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))‘(𝑖 + 1)) = sup(ran (𝐹 ↾ (ℤ_≥‘(𝑖 + 1))), ℝ^, < ))
70	69	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ((𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))‘(𝑖 + 1)) = sup(ran (𝐹 ↾ (ℤ_≥‘(𝑖 + 1))), ℝ^, < ))
71		fveq2 6191	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑖 → (ℤ_≥‘𝑛) = (ℤ_≥‘𝑖))
72	71	reseq2d 5396	. . . . . . . . . 10 ⊢ (𝑛 = 𝑖 → (𝐹 ↾ (ℤ_≥‘𝑛)) = (𝐹 ↾ (ℤ_≥‘𝑖)))
73	72	rneqd 5353	. . . . . . . . 9 ⊢ (𝑛 = 𝑖 → ran (𝐹 ↾ (ℤ_≥‘𝑛)) = ran (𝐹 ↾ (ℤ_≥‘𝑖)))
74	73	supeq1d 8352	. . . . . . . 8 ⊢ (𝑛 = 𝑖 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ))
75	74	adantl 482	. . . . . . 7 ⊢ ((𝑖 ∈ 𝑍 ∧ 𝑛 = 𝑖) → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ))
76		id 22	. . . . . . 7 ⊢ (𝑖 ∈ 𝑍 → 𝑖 ∈ 𝑍)
77	66	supex 8369	. . . . . . . 8 ⊢ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < ) ∈ V
78	77	a1i 11	. . . . . . 7 ⊢ (𝑖 ∈ 𝑍 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < ) ∈ V)
79	59, 75, 76, 78	fvmptd 6288	. . . . . 6 ⊢ (𝑖 ∈ 𝑍 → ((𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))‘𝑖) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ))
80	79	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ((𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))‘𝑖) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ))
81	70, 80	breq12d 4666	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (((𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))‘(𝑖 + 1)) ≤ ((𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))‘𝑖) ↔ sup(ran (𝐹 ↾ (ℤ_≥‘(𝑖 + 1))), ℝ^, < ) ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < )))
82	58, 81	mpbird 247	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ((𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))‘(𝑖 + 1)) ≤ ((𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))‘𝑖))
83		nfcv 2764	. . . . . . . 8 ⊢ Ⅎ𝑗𝐹
84	3	frexr 39604	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝑍⟶ℝ^*)
85	83, 2, 1, 84	limsupre3uz 39968	. . . . . . 7 ⊢ (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔ (∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 ∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗) ∧ ∃𝑥 ∈ ℝ ∃𝑖 ∈ 𝑍 ∀𝑗 ∈ (ℤ_≥‘𝑖)(𝐹‘𝑗) ≤ 𝑥)))
86	12, 85	mpbid 222	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 ∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗) ∧ ∃𝑥 ∈ ℝ ∃𝑖 ∈ 𝑍 ∀𝑗 ∈ (ℤ_≥‘𝑖)(𝐹‘𝑗) ≤ 𝑥))
87	86	simpld 475	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 ∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗))
88		simp-4r 807	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → 𝑥 ∈ ℝ)
89	88	rexrd 10089	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → 𝑥 ∈ ℝ^*)
90	84	3ad2ant1 1082	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → 𝐹:𝑍⟶ℝ^*)
91	1	uztrn2 11705	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → 𝑗 ∈ 𝑍)
92	91	3adant1 1079	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → 𝑗 ∈ 𝑍)
93	90, 92	ffvelrnd 6360	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → (𝐹‘𝑗) ∈ ℝ^*)
94	93	ad5ant134 1313	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → (𝐹‘𝑗) ∈ ℝ^*)
95	56	supxrcld 39290	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) ∈ ℝ^)
96	95	ad5ant13 1301	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) ∈ ℝ^)
97		simpr 477	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → 𝑥 ≤ (𝐹‘𝑗))
98	56	3adant3 1081	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → ran (𝐹 ↾ (ℤ_≥‘𝑖)) ⊆ ℝ^*)
99		fvres 6207	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (ℤ_≥‘𝑖) → ((𝐹 ↾ (ℤ_≥‘𝑖))‘𝑗) = (𝐹‘𝑗))
100	99	eqcomd 2628	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘𝑖) → (𝐹‘𝑗) = ((𝐹 ↾ (ℤ_≥‘𝑖))‘𝑗))
101	100	3ad2ant3 1084	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → (𝐹‘𝑗) = ((𝐹 ↾ (ℤ_≥‘𝑖))‘𝑗))
102	3	ffnd 6046	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹 Fn 𝑍)
103	102	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝐹 Fn 𝑍)
104	1, 76	uzssd2 39644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ 𝑍 → (ℤ_≥‘𝑖) ⊆ 𝑍)
105	104	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (ℤ_≥‘𝑖) ⊆ 𝑍)
106		fnssres 6004	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Fn 𝑍 ∧ (ℤ_≥‘𝑖) ⊆ 𝑍) → (𝐹 ↾ (ℤ_≥‘𝑖)) Fn (ℤ_≥‘𝑖))
107	103, 105, 106	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹 ↾ (ℤ_≥‘𝑖)) Fn (ℤ_≥‘𝑖))
108	107	3adant3 1081	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → (𝐹 ↾ (ℤ_≥‘𝑖)) Fn (ℤ_≥‘𝑖))
109		simp3 1063	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → 𝑗 ∈ (ℤ_≥‘𝑖))
110		fnfvelrn 6356	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ↾ (ℤ_≥‘𝑖)) Fn (ℤ_≥‘𝑖) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → ((𝐹 ↾ (ℤ_≥‘𝑖))‘𝑗) ∈ ran (𝐹 ↾ (ℤ_≥‘𝑖)))
111	108, 109, 110	syl2anc 693	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → ((𝐹 ↾ (ℤ_≥‘𝑖))‘𝑗) ∈ ran (𝐹 ↾ (ℤ_≥‘𝑖)))
112	101, 111	eqeltrd 2701	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → (𝐹‘𝑗) ∈ ran (𝐹 ↾ (ℤ_≥‘𝑖)))
113		eqid 2622	. . . . . . . . . . . 12 ⊢ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < )
114	98, 112, 113	supxrubd 39297	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → (𝐹‘𝑗) ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < ))
115	114	ad5ant134 1313	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → (𝐹‘𝑗) ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < ))
116	89, 94, 96, 97, 115	xrletrd 11993	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) ∧ 𝑥 ≤ (𝐹‘𝑗)) → 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < ))
117	116	ex 450	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (ℤ_≥‘𝑖)) → (𝑥 ≤ (𝐹‘𝑗) → 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < )))
118	117	rexlimdva 3031	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ 𝑍) → (∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗) → 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < )))
119	118	ralimdva 2962	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑖 ∈ 𝑍 ∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗) → ∀𝑖 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < )))
120	119	reximdva 3017	. . . . 5 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 ∃𝑗 ∈ (ℤ_≥‘𝑖)𝑥 ≤ (𝐹‘𝑗) → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < )))
121	87, 120	mpd 15	. . . 4 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^*, < ))
122		simpl 473	. . . . . . 7 ⊢ ((𝑦 = 𝑥 ∧ 𝑖 ∈ 𝑍) → 𝑦 = 𝑥)
123	79	adantl 482	. . . . . . 7 ⊢ ((𝑦 = 𝑥 ∧ 𝑖 ∈ 𝑍) → ((𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))‘𝑖) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ))
124	122, 123	breq12d 4666	. . . . . 6 ⊢ ((𝑦 = 𝑥 ∧ 𝑖 ∈ 𝑍) → (𝑦 ≤ ((𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))‘𝑖) ↔ 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < )))
125	124	ralbidva 2985	. . . . 5 ⊢ (𝑦 = 𝑥 → (∀𝑖 ∈ 𝑍 𝑦 ≤ ((𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))‘𝑖) ↔ ∀𝑖 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < )))
126	125	cbvrexv 3172	. . . 4 ⊢ (∃𝑦 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑦 ≤ ((𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ))‘𝑖) ↔ ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ_≥‘𝑖)), ℝ^, < ))
127	121, 126	sylibr 224	. . 3 ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑖 ∈ 𝑍 𝑦 ≤ ((𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < ))‘𝑖))
128	1, 2, 34, 82, 127	climinf 39838	. 2 ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )) ⇝ inf(ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )), ℝ, < ))
129		fveq2 6191	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (ℤ_≥‘𝑛) = (ℤ_≥‘𝑘))
130	129	reseq2d 5396	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝐹 ↾ (ℤ_≥‘𝑛)) = (𝐹 ↾ (ℤ_≥‘𝑘)))
131	130	rneqd 5353	. . . . . 6 ⊢ (𝑛 = 𝑘 → ran (𝐹 ↾ (ℤ_≥‘𝑛)) = ran (𝐹 ↾ (ℤ_≥‘𝑘)))
132	131	supeq1d 8352	. . . . 5 ⊢ (𝑛 = 𝑘 → sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < ) = sup(ran (𝐹 ↾ (ℤ_≥‘𝑘)), ℝ^, < ))
133	132	cbvmptv 4750	. . . 4 ⊢ (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )) = (𝑘 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑘)), ℝ^, < ))
134	133	a1i 11	. . 3 ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )) = (𝑘 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑘)), ℝ^, < )))
135	2, 1, 3, 12	limsupvaluz2 39970	. . . 4 ⊢ (𝜑 → (lim sup‘𝐹) = inf(ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < )), ℝ, < ))
136	135	eqcomd 2628	. . 3 ⊢ (𝜑 → inf(ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^*, < )), ℝ, < ) = (lim sup‘𝐹))
137	134, 136	breq12d 4666	. 2 ⊢ (𝜑 → ((𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )) ⇝ inf(ran (𝑛 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑛)), ℝ^, < )), ℝ, < ) ↔ (𝑘 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑘)), ℝ^*, < )) ⇝ (lim sup‘𝐹)))
138	128, 137	mpbid 222	1 ⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ sup(ran (𝐹 ↾ (ℤ_≥‘𝑘)), ℝ^*, < )) ⇝ (lim sup‘𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 Vcvv 3200 ⊆ wss 3574 ∅c0 3915 class class class wbr 4653 ↦ cmpt 4729 ran crn 5115 ↾ cres 5116 Fn wfn 5883 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 supcsup 8346 infcinf 8347 ℝcr 9935 1c1 9937 + caddc 9939 ℝ^*cxr 10073 < clt 10074 ≤ cle 10075 ℤcz 11377 ℤ_≥cuz 11687 lim supclsp 14201 ⇝ cli 14215

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-ico 12181 df-fz 12327 df-fl 12593 df-ceil 12594 df-seq 12802 df-exp 12861 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-limsup 14202 df-clim 14219

This theorem is referenced by: supcnvlimsupmpt 39973

W3C validator