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

Theorem supcnvlimsup 40890
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.
StepHypRef Expression
1 supcnvlimsup.z . . 3 𝑍 = (ℤ𝑀)
2 supcnvlimsup.m . . 3 (𝜑𝑀 ∈ ℤ)
3 supcnvlimsup.f . . . . . . . . 9 (𝜑𝐹:𝑍⟶ℝ)
43adantr 474 . . . . . . . 8 ((𝜑𝑛𝑍) → 𝐹:𝑍⟶ℝ)
5 id 22 . . . . . . . . . 10 (𝑛𝑍𝑛𝑍)
61, 5uzssd2 40560 . . . . . . . . 9 (𝑛𝑍 → (ℤ𝑛) ⊆ 𝑍)
76adantl 475 . . . . . . . 8 ((𝜑𝑛𝑍) → (ℤ𝑛) ⊆ 𝑍)
84, 7feqresmpt 6512 . . . . . . 7 ((𝜑𝑛𝑍) → (𝐹 ↾ (ℤ𝑛)) = (𝑚 ∈ (ℤ𝑛) ↦ (𝐹𝑚)))
98rneqd 5600 . . . . . 6 ((𝜑𝑛𝑍) → ran (𝐹 ↾ (ℤ𝑛)) = ran (𝑚 ∈ (ℤ𝑛) ↦ (𝐹𝑚)))
109supeq1d 8642 . . . . 5 ((𝜑𝑛𝑍) → sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ) = sup(ran (𝑚 ∈ (ℤ𝑛) ↦ (𝐹𝑚)), ℝ*, < ))
11 nfcv 2934 . . . . . . . . 9 𝑚𝐹
12 supcnvlimsup.r . . . . . . . . . 10 (𝜑 → (lim sup‘𝐹) ∈ ℝ)
1312renepnfd 10429 . . . . . . . . 9 (𝜑 → (lim sup‘𝐹) ≠ +∞)
1411, 1, 3, 13limsupubuz 40863 . . . . . . . 8 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑚𝑍 (𝐹𝑚) ≤ 𝑥)
1514adantr 474 . . . . . . 7 ((𝜑𝑛𝑍) → ∃𝑥 ∈ ℝ ∀𝑚𝑍 (𝐹𝑚) ≤ 𝑥)
16 ssralv 3885 . . . . . . . . . 10 ((ℤ𝑛) ⊆ 𝑍 → (∀𝑚𝑍 (𝐹𝑚) ≤ 𝑥 → ∀𝑚 ∈ (ℤ𝑛)(𝐹𝑚) ≤ 𝑥))
176, 16syl 17 . . . . . . . . 9 (𝑛𝑍 → (∀𝑚𝑍 (𝐹𝑚) ≤ 𝑥 → ∀𝑚 ∈ (ℤ𝑛)(𝐹𝑚) ≤ 𝑥))
1817adantl 475 . . . . . . . 8 ((𝜑𝑛𝑍) → (∀𝑚𝑍 (𝐹𝑚) ≤ 𝑥 → ∀𝑚 ∈ (ℤ𝑛)(𝐹𝑚) ≤ 𝑥))
1918reximdv 3197 . . . . . . 7 ((𝜑𝑛𝑍) → (∃𝑥 ∈ ℝ ∀𝑚𝑍 (𝐹𝑚) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑚 ∈ (ℤ𝑛)(𝐹𝑚) ≤ 𝑥))
2015, 19mpd 15 . . . . . 6 ((𝜑𝑛𝑍) → ∃𝑥 ∈ ℝ ∀𝑚 ∈ (ℤ𝑛)(𝐹𝑚) ≤ 𝑥)
21 nfv 1957 . . . . . . 7 𝑚(𝜑𝑛𝑍)
221eluzelz2 40543 . . . . . . . . 9 (𝑛𝑍𝑛 ∈ ℤ)
23 uzid 12011 . . . . . . . . 9 (𝑛 ∈ ℤ → 𝑛 ∈ (ℤ𝑛))
24 ne0i 4149 . . . . . . . . 9 (𝑛 ∈ (ℤ𝑛) → (ℤ𝑛) ≠ ∅)
2522, 23, 243syl 18 . . . . . . . 8 (𝑛𝑍 → (ℤ𝑛) ≠ ∅)
2625adantl 475 . . . . . . 7 ((𝜑𝑛𝑍) → (ℤ𝑛) ≠ ∅)
274adantr 474 . . . . . . . 8 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝐹:𝑍⟶ℝ)
287sselda 3821 . . . . . . . 8 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
2927, 28ffvelrnd 6626 . . . . . . 7 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → (𝐹𝑚) ∈ ℝ)
3021, 26, 29supxrre3rnmpt 40572 . . . . . 6 ((𝜑𝑛𝑍) → (sup(ran (𝑚 ∈ (ℤ𝑛) ↦ (𝐹𝑚)), ℝ*, < ) ∈ ℝ ↔ ∃𝑥 ∈ ℝ ∀𝑚 ∈ (ℤ𝑛)(𝐹𝑚) ≤ 𝑥))
3120, 30mpbird 249 . . . . 5 ((𝜑𝑛𝑍) → sup(ran (𝑚 ∈ (ℤ𝑛) ↦ (𝐹𝑚)), ℝ*, < ) ∈ ℝ)
3210, 31eqeltrd 2859 . . . 4 ((𝜑𝑛𝑍) → sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ) ∈ ℝ)
3332fmpttd 6651 . . 3 (𝜑 → (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )):𝑍⟶ℝ)
34 eqid 2778 . . . . . . . . . 10 (ℤ𝑖) = (ℤ𝑖)
351eluzelz2 40543 . . . . . . . . . 10 (𝑖𝑍𝑖 ∈ ℤ)
3635peano2zd 11841 . . . . . . . . . 10 (𝑖𝑍 → (𝑖 + 1) ∈ ℤ)
3735zred 11838 . . . . . . . . . . 11 (𝑖𝑍𝑖 ∈ ℝ)
38 lep1 11218 . . . . . . . . . . 11 (𝑖 ∈ ℝ → 𝑖 ≤ (𝑖 + 1))
3937, 38syl 17 . . . . . . . . . 10 (𝑖𝑍𝑖 ≤ (𝑖 + 1))
4034, 35, 36, 39eluzd 40551 . . . . . . . . 9 (𝑖𝑍 → (𝑖 + 1) ∈ (ℤ𝑖))
41 uzss 12017 . . . . . . . . 9 ((𝑖 + 1) ∈ (ℤ𝑖) → (ℤ‘(𝑖 + 1)) ⊆ (ℤ𝑖))
4240, 41syl 17 . . . . . . . 8 (𝑖𝑍 → (ℤ‘(𝑖 + 1)) ⊆ (ℤ𝑖))
43 ssres2 5676 . . . . . . . 8 ((ℤ‘(𝑖 + 1)) ⊆ (ℤ𝑖) → (𝐹 ↾ (ℤ‘(𝑖 + 1))) ⊆ (𝐹 ↾ (ℤ𝑖)))
4442, 43syl 17 . . . . . . 7 (𝑖𝑍 → (𝐹 ↾ (ℤ‘(𝑖 + 1))) ⊆ (𝐹 ↾ (ℤ𝑖)))
45 rnss 5601 . . . . . . 7 ((𝐹 ↾ (ℤ‘(𝑖 + 1))) ⊆ (𝐹 ↾ (ℤ𝑖)) → ran (𝐹 ↾ (ℤ‘(𝑖 + 1))) ⊆ ran (𝐹 ↾ (ℤ𝑖)))
4644, 45syl 17 . . . . . 6 (𝑖𝑍 → ran (𝐹 ↾ (ℤ‘(𝑖 + 1))) ⊆ ran (𝐹 ↾ (ℤ𝑖)))
4746adantl 475 . . . . 5 ((𝜑𝑖𝑍) → ran (𝐹 ↾ (ℤ‘(𝑖 + 1))) ⊆ ran (𝐹 ↾ (ℤ𝑖)))
48 rnresss 40298 . . . . . . . 8 ran (𝐹 ↾ (ℤ𝑖)) ⊆ ran 𝐹
4948a1i 11 . . . . . . 7 ((𝜑𝑖𝑍) → ran (𝐹 ↾ (ℤ𝑖)) ⊆ ran 𝐹)
503frnd 6300 . . . . . . . 8 (𝜑 → ran 𝐹 ⊆ ℝ)
5150adantr 474 . . . . . . 7 ((𝜑𝑖𝑍) → ran 𝐹 ⊆ ℝ)
5249, 51sstrd 3831 . . . . . 6 ((𝜑𝑖𝑍) → ran (𝐹 ↾ (ℤ𝑖)) ⊆ ℝ)
53 ressxr 10422 . . . . . . 7 ℝ ⊆ ℝ*
5453a1i 11 . . . . . 6 ((𝜑𝑖𝑍) → ℝ ⊆ ℝ*)
5552, 54sstrd 3831 . . . . 5 ((𝜑𝑖𝑍) → ran (𝐹 ↾ (ℤ𝑖)) ⊆ ℝ*)
56 supxrss 12478 . . . . 5 ((ran (𝐹 ↾ (ℤ‘(𝑖 + 1))) ⊆ ran (𝐹 ↾ (ℤ𝑖)) ∧ ran (𝐹 ↾ (ℤ𝑖)) ⊆ ℝ*) → sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ) ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
5747, 55, 56syl2anc 579 . . . 4 ((𝜑𝑖𝑍) → sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ) ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
58 eqidd 2779 . . . . . . 7 (𝑖𝑍 → (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )) = (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )))
59 fveq2 6448 . . . . . . . . . . 11 (𝑛 = (𝑖 + 1) → (ℤ𝑛) = (ℤ‘(𝑖 + 1)))
6059reseq2d 5644 . . . . . . . . . 10 (𝑛 = (𝑖 + 1) → (𝐹 ↾ (ℤ𝑛)) = (𝐹 ↾ (ℤ‘(𝑖 + 1))))
6160rneqd 5600 . . . . . . . . 9 (𝑛 = (𝑖 + 1) → ran (𝐹 ↾ (ℤ𝑛)) = ran (𝐹 ↾ (ℤ‘(𝑖 + 1))))
6261supeq1d 8642 . . . . . . . 8 (𝑛 = (𝑖 + 1) → sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ) = sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ))
6362adantl 475 . . . . . . 7 ((𝑖𝑍𝑛 = (𝑖 + 1)) → sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ) = sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ))
641peano2uzs 12052 . . . . . . 7 (𝑖𝑍 → (𝑖 + 1) ∈ 𝑍)
65 xrltso 12288 . . . . . . . . 9 < Or ℝ*
6665supex 8659 . . . . . . . 8 sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ) ∈ V
6766a1i 11 . . . . . . 7 (𝑖𝑍 → sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ) ∈ V)
6858, 63, 64, 67fvmptd 6550 . . . . . 6 (𝑖𝑍 → ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘(𝑖 + 1)) = sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ))
6968adantl 475 . . . . 5 ((𝜑𝑖𝑍) → ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘(𝑖 + 1)) = sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ))
70 fveq2 6448 . . . . . . . . . . 11 (𝑛 = 𝑖 → (ℤ𝑛) = (ℤ𝑖))
7170reseq2d 5644 . . . . . . . . . 10 (𝑛 = 𝑖 → (𝐹 ↾ (ℤ𝑛)) = (𝐹 ↾ (ℤ𝑖)))
7271rneqd 5600 . . . . . . . . 9 (𝑛 = 𝑖 → ran (𝐹 ↾ (ℤ𝑛)) = ran (𝐹 ↾ (ℤ𝑖)))
7372supeq1d 8642 . . . . . . . 8 (𝑛 = 𝑖 → sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ) = sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
7473adantl 475 . . . . . . 7 ((𝑖𝑍𝑛 = 𝑖) → sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ) = sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
75 id 22 . . . . . . 7 (𝑖𝑍𝑖𝑍)
7665supex 8659 . . . . . . . 8 sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ) ∈ V
7776a1i 11 . . . . . . 7 (𝑖𝑍 → sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ) ∈ V)
7858, 74, 75, 77fvmptd 6550 . . . . . 6 (𝑖𝑍 → ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖) = sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
7978adantl 475 . . . . 5 ((𝜑𝑖𝑍) → ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖) = sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
8069, 79breq12d 4901 . . . 4 ((𝜑𝑖𝑍) → (((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘(𝑖 + 1)) ≤ ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖) ↔ sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ) ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < )))
8157, 80mpbird 249 . . 3 ((𝜑𝑖𝑍) → ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘(𝑖 + 1)) ≤ ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖))
82 nfcv 2934 . . . . . . . 8 𝑗𝐹
833frexr 40522 . . . . . . . 8 (𝜑𝐹:𝑍⟶ℝ*)
8482, 2, 1, 83limsupre3uz 40886 . . . . . . 7 (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔ (∃𝑥 ∈ ℝ ∀𝑖𝑍𝑗 ∈ (ℤ𝑖)𝑥 ≤ (𝐹𝑗) ∧ ∃𝑥 ∈ ℝ ∃𝑖𝑍𝑗 ∈ (ℤ𝑖)(𝐹𝑗) ≤ 𝑥)))
8512, 84mpbid 224 . . . . . 6 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑖𝑍𝑗 ∈ (ℤ𝑖)𝑥 ≤ (𝐹𝑗) ∧ ∃𝑥 ∈ ℝ ∃𝑖𝑍𝑗 ∈ (ℤ𝑖)(𝐹𝑗) ≤ 𝑥))
8685simpld 490 . . . . 5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖𝑍𝑗 ∈ (ℤ𝑖)𝑥 ≤ (𝐹𝑗))
87 simp-4r 774 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑖𝑍) ∧ 𝑗 ∈ (ℤ𝑖)) ∧ 𝑥 ≤ (𝐹𝑗)) → 𝑥 ∈ ℝ)
8887rexrd 10428 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑖𝑍) ∧ 𝑗 ∈ (ℤ𝑖)) ∧ 𝑥 ≤ (𝐹𝑗)) → 𝑥 ∈ ℝ*)
89833ad2ant1 1124 . . . . . . . . . . 11 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → 𝐹:𝑍⟶ℝ*)
901uztrn2 12014 . . . . . . . . . . . 12 ((𝑖𝑍𝑗 ∈ (ℤ𝑖)) → 𝑗𝑍)
91903adant1 1121 . . . . . . . . . . 11 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → 𝑗𝑍)
9289, 91ffvelrnd 6626 . . . . . . . . . 10 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → (𝐹𝑗) ∈ ℝ*)
9392ad5ant134 1432 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑖𝑍) ∧ 𝑗 ∈ (ℤ𝑖)) ∧ 𝑥 ≤ (𝐹𝑗)) → (𝐹𝑗) ∈ ℝ*)
9455supxrcld 40229 . . . . . . . . . 10 ((𝜑𝑖𝑍) → sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ) ∈ ℝ*)
9594ad5ant13 747 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑖𝑍) ∧ 𝑗 ∈ (ℤ𝑖)) ∧ 𝑥 ≤ (𝐹𝑗)) → sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ) ∈ ℝ*)
96 simpr 479 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑖𝑍) ∧ 𝑗 ∈ (ℤ𝑖)) ∧ 𝑥 ≤ (𝐹𝑗)) → 𝑥 ≤ (𝐹𝑗))
97553adant3 1123 . . . . . . . . . . 11 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → ran (𝐹 ↾ (ℤ𝑖)) ⊆ ℝ*)
98 fvres 6467 . . . . . . . . . . . . . 14 (𝑗 ∈ (ℤ𝑖) → ((𝐹 ↾ (ℤ𝑖))‘𝑗) = (𝐹𝑗))
9998eqcomd 2784 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ𝑖) → (𝐹𝑗) = ((𝐹 ↾ (ℤ𝑖))‘𝑗))
100993ad2ant3 1126 . . . . . . . . . . . 12 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → (𝐹𝑗) = ((𝐹 ↾ (ℤ𝑖))‘𝑗))
1013ffnd 6294 . . . . . . . . . . . . . . . 16 (𝜑𝐹 Fn 𝑍)
102101adantr 474 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑍) → 𝐹 Fn 𝑍)
1031, 75uzssd2 40560 . . . . . . . . . . . . . . . 16 (𝑖𝑍 → (ℤ𝑖) ⊆ 𝑍)
104103adantl 475 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑍) → (ℤ𝑖) ⊆ 𝑍)
105 fnssres 6252 . . . . . . . . . . . . . . 15 ((𝐹 Fn 𝑍 ∧ (ℤ𝑖) ⊆ 𝑍) → (𝐹 ↾ (ℤ𝑖)) Fn (ℤ𝑖))
106102, 104, 105syl2anc 579 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑍) → (𝐹 ↾ (ℤ𝑖)) Fn (ℤ𝑖))
1071063adant3 1123 . . . . . . . . . . . . 13 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → (𝐹 ↾ (ℤ𝑖)) Fn (ℤ𝑖))
108 simp3 1129 . . . . . . . . . . . . 13 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → 𝑗 ∈ (ℤ𝑖))
109 fnfvelrn 6622 . . . . . . . . . . . . 13 (((𝐹 ↾ (ℤ𝑖)) Fn (ℤ𝑖) ∧ 𝑗 ∈ (ℤ𝑖)) → ((𝐹 ↾ (ℤ𝑖))‘𝑗) ∈ ran (𝐹 ↾ (ℤ𝑖)))
110107, 108, 109syl2anc 579 . . . . . . . . . . . 12 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → ((𝐹 ↾ (ℤ𝑖))‘𝑗) ∈ ran (𝐹 ↾ (ℤ𝑖)))
111100, 110eqeltrd 2859 . . . . . . . . . . 11 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → (𝐹𝑗) ∈ ran (𝐹 ↾ (ℤ𝑖)))
112 eqid 2778 . . . . . . . . . . 11 sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ) = sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < )
11397, 111, 112supxrubd 40236 . . . . . . . . . 10 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → (𝐹𝑗) ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
114113ad5ant134 1432 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑖𝑍) ∧ 𝑗 ∈ (ℤ𝑖)) ∧ 𝑥 ≤ (𝐹𝑗)) → (𝐹𝑗) ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
11588, 93, 95, 96, 114xrletrd 12309 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑖𝑍) ∧ 𝑗 ∈ (ℤ𝑖)) ∧ 𝑥 ≤ (𝐹𝑗)) → 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
116115rexlimdva2 3216 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖𝑍) → (∃𝑗 ∈ (ℤ𝑖)𝑥 ≤ (𝐹𝑗) → 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < )))
117116ralimdva 3144 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (∀𝑖𝑍𝑗 ∈ (ℤ𝑖)𝑥 ≤ (𝐹𝑗) → ∀𝑖𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < )))
118117reximdva 3198 . . . . 5 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑖𝑍𝑗 ∈ (ℤ𝑖)𝑥 ≤ (𝐹𝑗) → ∃𝑥 ∈ ℝ ∀𝑖𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < )))
11986, 118mpd 15 . . . 4 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
120 simpl 476 . . . . . . 7 ((𝑦 = 𝑥𝑖𝑍) → 𝑦 = 𝑥)
12178adantl 475 . . . . . . 7 ((𝑦 = 𝑥𝑖𝑍) → ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖) = sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
122120, 121breq12d 4901 . . . . . 6 ((𝑦 = 𝑥𝑖𝑍) → (𝑦 ≤ ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖) ↔ 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < )))
123122ralbidva 3167 . . . . 5 (𝑦 = 𝑥 → (∀𝑖𝑍 𝑦 ≤ ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖) ↔ ∀𝑖𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < )))
124123cbvrexv 3368 . . . 4 (∃𝑦 ∈ ℝ ∀𝑖𝑍 𝑦 ≤ ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖) ↔ ∃𝑥 ∈ ℝ ∀𝑖𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
125119, 124sylibr 226 . . 3 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑖𝑍 𝑦 ≤ ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖))
1261, 2, 33, 81, 125climinf 40756 . 2 (𝜑 → (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )) ⇝ inf(ran (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )), ℝ, < ))
127 fveq2 6448 . . . . . . . 8 (𝑛 = 𝑘 → (ℤ𝑛) = (ℤ𝑘))
128127reseq2d 5644 . . . . . . 7 (𝑛 = 𝑘 → (𝐹 ↾ (ℤ𝑛)) = (𝐹 ↾ (ℤ𝑘)))
129128rneqd 5600 . . . . . 6 (𝑛 = 𝑘 → ran (𝐹 ↾ (ℤ𝑛)) = ran (𝐹 ↾ (ℤ𝑘)))
130129supeq1d 8642 . . . . 5 (𝑛 = 𝑘 → sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ) = sup(ran (𝐹 ↾ (ℤ𝑘)), ℝ*, < ))
131130cbvmptv 4987 . . . 4 (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )) = (𝑘𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑘)), ℝ*, < ))
132131a1i 11 . . 3 (𝜑 → (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )) = (𝑘𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑘)), ℝ*, < )))
1332, 1, 3, 12limsupvaluz2 40888 . . . 4 (𝜑 → (lim sup‘𝐹) = inf(ran (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )), ℝ, < ))
134133eqcomd 2784 . . 3 (𝜑 → inf(ran (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )), ℝ, < ) = (lim sup‘𝐹))
135132, 134breq12d 4901 . 2 (𝜑 → ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )) ⇝ inf(ran (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )), ℝ, < ) ↔ (𝑘𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑘)), ℝ*, < )) ⇝ (lim sup‘𝐹)))
136126, 135mpbid 224 1 (𝜑 → (𝑘𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑘)), ℝ*, < )) ⇝ (lim sup‘𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1071   = wceq 1601  wcel 2107  wne 2969  wral 3090  wrex 3091  Vcvv 3398  wss 3792  c0 4141   class class class wbr 4888  cmpt 4967  ran crn 5358  cres 5359   Fn wfn 6132  wf 6133  cfv 6137  (class class class)co 6924  supcsup 8636  infcinf 8637  cr 10273  1c1 10275   + caddc 10277  *cxr 10412   < clt 10413  cle 10414  cz 11732  cuz 11996  lim supclsp 14613  cli 14627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351  ax-pre-sup 10352
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-om 7346  df-1st 7447  df-2nd 7448  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-oadd 7849  df-er 8028  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-sup 8638  df-inf 8639  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-div 11035  df-nn 11379  df-2 11442  df-3 11443  df-n0 11647  df-z 11733  df-uz 11997  df-rp 12142  df-ico 12497  df-fz 12648  df-fl 12916  df-ceil 12917  df-seq 13124  df-exp 13183  df-cj 14250  df-re 14251  df-im 14252  df-sqrt 14386  df-abs 14387  df-limsup 14614  df-clim 14631
This theorem is referenced by:  supcnvlimsupmpt  40891
  Copyright terms: Public domain W3C validator