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

Theorem supcnvlimsup 40493
 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 472 . . . . . . . 8 ((𝜑𝑛𝑍) → 𝐹:𝑍⟶ℝ)
5 id 22 . . . . . . . . . 10 (𝑛𝑍𝑛𝑍)
61, 5uzssd2 40160 . . . . . . . . 9 (𝑛𝑍 → (ℤ𝑛) ⊆ 𝑍)
76adantl 473 . . . . . . . 8 ((𝜑𝑛𝑍) → (ℤ𝑛) ⊆ 𝑍)
84, 7feqresmpt 6413 . . . . . . 7 ((𝜑𝑛𝑍) → (𝐹 ↾ (ℤ𝑛)) = (𝑚 ∈ (ℤ𝑛) ↦ (𝐹𝑚)))
98rneqd 5508 . . . . . 6 ((𝜑𝑛𝑍) → ran (𝐹 ↾ (ℤ𝑛)) = ran (𝑚 ∈ (ℤ𝑛) ↦ (𝐹𝑚)))
109supeq1d 8519 . . . . 5 ((𝜑𝑛𝑍) → sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ) = sup(ran (𝑚 ∈ (ℤ𝑛) ↦ (𝐹𝑚)), ℝ*, < ))
11 nfcv 2902 . . . . . . . . 9 𝑚𝐹
12 supcnvlimsup.r . . . . . . . . . 10 (𝜑 → (lim sup‘𝐹) ∈ ℝ)
1312renepnfd 10302 . . . . . . . . 9 (𝜑 → (lim sup‘𝐹) ≠ +∞)
1411, 1, 3, 13limsupubuz 40466 . . . . . . . 8 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑚𝑍 (𝐹𝑚) ≤ 𝑥)
1514adantr 472 . . . . . . 7 ((𝜑𝑛𝑍) → ∃𝑥 ∈ ℝ ∀𝑚𝑍 (𝐹𝑚) ≤ 𝑥)
16 ssralv 3807 . . . . . . . . . 10 ((ℤ𝑛) ⊆ 𝑍 → (∀𝑚𝑍 (𝐹𝑚) ≤ 𝑥 → ∀𝑚 ∈ (ℤ𝑛)(𝐹𝑚) ≤ 𝑥))
176, 16syl 17 . . . . . . . . 9 (𝑛𝑍 → (∀𝑚𝑍 (𝐹𝑚) ≤ 𝑥 → ∀𝑚 ∈ (ℤ𝑛)(𝐹𝑚) ≤ 𝑥))
1817adantl 473 . . . . . . . 8 ((𝜑𝑛𝑍) → (∀𝑚𝑍 (𝐹𝑚) ≤ 𝑥 → ∀𝑚 ∈ (ℤ𝑛)(𝐹𝑚) ≤ 𝑥))
1918reximdv 3154 . . . . . . 7 ((𝜑𝑛𝑍) → (∃𝑥 ∈ ℝ ∀𝑚𝑍 (𝐹𝑚) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑚 ∈ (ℤ𝑛)(𝐹𝑚) ≤ 𝑥))
2015, 19mpd 15 . . . . . 6 ((𝜑𝑛𝑍) → ∃𝑥 ∈ ℝ ∀𝑚 ∈ (ℤ𝑛)(𝐹𝑚) ≤ 𝑥)
21 nfv 1992 . . . . . . 7 𝑚(𝜑𝑛𝑍)
221eluzelz2 40143 . . . . . . . . 9 (𝑛𝑍𝑛 ∈ ℤ)
23 uzid 11914 . . . . . . . . 9 (𝑛 ∈ ℤ → 𝑛 ∈ (ℤ𝑛))
24 ne0i 4064 . . . . . . . . 9 (𝑛 ∈ (ℤ𝑛) → (ℤ𝑛) ≠ ∅)
2522, 23, 243syl 18 . . . . . . . 8 (𝑛𝑍 → (ℤ𝑛) ≠ ∅)
2625adantl 473 . . . . . . 7 ((𝜑𝑛𝑍) → (ℤ𝑛) ≠ ∅)
274adantr 472 . . . . . . . 8 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝐹:𝑍⟶ℝ)
287sselda 3744 . . . . . . . 8 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → 𝑚𝑍)
2927, 28ffvelrnd 6524 . . . . . . 7 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → (𝐹𝑚) ∈ ℝ)
3021, 26, 29supxrre3rnmpt 40172 . . . . . 6 ((𝜑𝑛𝑍) → (sup(ran (𝑚 ∈ (ℤ𝑛) ↦ (𝐹𝑚)), ℝ*, < ) ∈ ℝ ↔ ∃𝑥 ∈ ℝ ∀𝑚 ∈ (ℤ𝑛)(𝐹𝑚) ≤ 𝑥))
3120, 30mpbird 247 . . . . 5 ((𝜑𝑛𝑍) → sup(ran (𝑚 ∈ (ℤ𝑛) ↦ (𝐹𝑚)), ℝ*, < ) ∈ ℝ)
3210, 31eqeltrd 2839 . . . 4 ((𝜑𝑛𝑍) → sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ) ∈ ℝ)
33 eqid 2760 . . . 4 (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )) = (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))
3432, 33fmptd 6549 . . 3 (𝜑 → (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )):𝑍⟶ℝ)
35 eqid 2760 . . . . . . . . . 10 (ℤ𝑖) = (ℤ𝑖)
361eluzelz2 40143 . . . . . . . . . 10 (𝑖𝑍𝑖 ∈ ℤ)
3736peano2zd 11697 . . . . . . . . . 10 (𝑖𝑍 → (𝑖 + 1) ∈ ℤ)
3836zred 11694 . . . . . . . . . . 11 (𝑖𝑍𝑖 ∈ ℝ)
39 lep1 11074 . . . . . . . . . . 11 (𝑖 ∈ ℝ → 𝑖 ≤ (𝑖 + 1))
4038, 39syl 17 . . . . . . . . . 10 (𝑖𝑍𝑖 ≤ (𝑖 + 1))
4135, 36, 37, 40eluzd 40151 . . . . . . . . 9 (𝑖𝑍 → (𝑖 + 1) ∈ (ℤ𝑖))
42 uzss 11920 . . . . . . . . 9 ((𝑖 + 1) ∈ (ℤ𝑖) → (ℤ‘(𝑖 + 1)) ⊆ (ℤ𝑖))
4341, 42syl 17 . . . . . . . 8 (𝑖𝑍 → (ℤ‘(𝑖 + 1)) ⊆ (ℤ𝑖))
44 ssres2 5583 . . . . . . . 8 ((ℤ‘(𝑖 + 1)) ⊆ (ℤ𝑖) → (𝐹 ↾ (ℤ‘(𝑖 + 1))) ⊆ (𝐹 ↾ (ℤ𝑖)))
4543, 44syl 17 . . . . . . 7 (𝑖𝑍 → (𝐹 ↾ (ℤ‘(𝑖 + 1))) ⊆ (𝐹 ↾ (ℤ𝑖)))
46 rnss 5509 . . . . . . 7 ((𝐹 ↾ (ℤ‘(𝑖 + 1))) ⊆ (𝐹 ↾ (ℤ𝑖)) → ran (𝐹 ↾ (ℤ‘(𝑖 + 1))) ⊆ ran (𝐹 ↾ (ℤ𝑖)))
4745, 46syl 17 . . . . . 6 (𝑖𝑍 → ran (𝐹 ↾ (ℤ‘(𝑖 + 1))) ⊆ ran (𝐹 ↾ (ℤ𝑖)))
4847adantl 473 . . . . 5 ((𝜑𝑖𝑍) → ran (𝐹 ↾ (ℤ‘(𝑖 + 1))) ⊆ ran (𝐹 ↾ (ℤ𝑖)))
49 rnresss 39882 . . . . . . . 8 ran (𝐹 ↾ (ℤ𝑖)) ⊆ ran 𝐹
5049a1i 11 . . . . . . 7 ((𝜑𝑖𝑍) → ran (𝐹 ↾ (ℤ𝑖)) ⊆ ran 𝐹)
513frnd 39943 . . . . . . . 8 (𝜑 → ran 𝐹 ⊆ ℝ)
5251adantr 472 . . . . . . 7 ((𝜑𝑖𝑍) → ran 𝐹 ⊆ ℝ)
5350, 52sstrd 3754 . . . . . 6 ((𝜑𝑖𝑍) → ran (𝐹 ↾ (ℤ𝑖)) ⊆ ℝ)
54 ressxr 10295 . . . . . . 7 ℝ ⊆ ℝ*
5554a1i 11 . . . . . 6 ((𝜑𝑖𝑍) → ℝ ⊆ ℝ*)
5653, 55sstrd 3754 . . . . 5 ((𝜑𝑖𝑍) → ran (𝐹 ↾ (ℤ𝑖)) ⊆ ℝ*)
57 supxrss 12375 . . . . 5 ((ran (𝐹 ↾ (ℤ‘(𝑖 + 1))) ⊆ ran (𝐹 ↾ (ℤ𝑖)) ∧ ran (𝐹 ↾ (ℤ𝑖)) ⊆ ℝ*) → sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ) ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
5848, 56, 57syl2anc 696 . . . 4 ((𝜑𝑖𝑍) → sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ) ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
59 eqidd 2761 . . . . . . 7 (𝑖𝑍 → (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )) = (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )))
60 fveq2 6353 . . . . . . . . . . 11 (𝑛 = (𝑖 + 1) → (ℤ𝑛) = (ℤ‘(𝑖 + 1)))
6160reseq2d 5551 . . . . . . . . . 10 (𝑛 = (𝑖 + 1) → (𝐹 ↾ (ℤ𝑛)) = (𝐹 ↾ (ℤ‘(𝑖 + 1))))
6261rneqd 5508 . . . . . . . . 9 (𝑛 = (𝑖 + 1) → ran (𝐹 ↾ (ℤ𝑛)) = ran (𝐹 ↾ (ℤ‘(𝑖 + 1))))
6362supeq1d 8519 . . . . . . . 8 (𝑛 = (𝑖 + 1) → sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ) = sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ))
6463adantl 473 . . . . . . 7 ((𝑖𝑍𝑛 = (𝑖 + 1)) → sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ) = sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ))
651peano2uzs 11955 . . . . . . 7 (𝑖𝑍 → (𝑖 + 1) ∈ 𝑍)
66 xrltso 12187 . . . . . . . . 9 < Or ℝ*
6766supex 8536 . . . . . . . 8 sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ) ∈ V
6867a1i 11 . . . . . . 7 (𝑖𝑍 → sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ) ∈ V)
6959, 64, 65, 68fvmptd 6451 . . . . . 6 (𝑖𝑍 → ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘(𝑖 + 1)) = sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ))
7069adantl 473 . . . . 5 ((𝜑𝑖𝑍) → ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘(𝑖 + 1)) = sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ))
71 fveq2 6353 . . . . . . . . . . 11 (𝑛 = 𝑖 → (ℤ𝑛) = (ℤ𝑖))
7271reseq2d 5551 . . . . . . . . . 10 (𝑛 = 𝑖 → (𝐹 ↾ (ℤ𝑛)) = (𝐹 ↾ (ℤ𝑖)))
7372rneqd 5508 . . . . . . . . 9 (𝑛 = 𝑖 → ran (𝐹 ↾ (ℤ𝑛)) = ran (𝐹 ↾ (ℤ𝑖)))
7473supeq1d 8519 . . . . . . . 8 (𝑛 = 𝑖 → sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ) = sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
7574adantl 473 . . . . . . 7 ((𝑖𝑍𝑛 = 𝑖) → sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ) = sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
76 id 22 . . . . . . 7 (𝑖𝑍𝑖𝑍)
7766supex 8536 . . . . . . . 8 sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ) ∈ V
7877a1i 11 . . . . . . 7 (𝑖𝑍 → sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ) ∈ V)
7959, 75, 76, 78fvmptd 6451 . . . . . 6 (𝑖𝑍 → ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖) = sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
8079adantl 473 . . . . 5 ((𝜑𝑖𝑍) → ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖) = sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
8170, 80breq12d 4817 . . . 4 ((𝜑𝑖𝑍) → (((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘(𝑖 + 1)) ≤ ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖) ↔ sup(ran (𝐹 ↾ (ℤ‘(𝑖 + 1))), ℝ*, < ) ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < )))
8258, 81mpbird 247 . . 3 ((𝜑𝑖𝑍) → ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘(𝑖 + 1)) ≤ ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖))
83 nfcv 2902 . . . . . . . 8 𝑗𝐹
843frexr 40120 . . . . . . . 8 (𝜑𝐹:𝑍⟶ℝ*)
8583, 2, 1, 84limsupre3uz 40489 . . . . . . 7 (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔ (∃𝑥 ∈ ℝ ∀𝑖𝑍𝑗 ∈ (ℤ𝑖)𝑥 ≤ (𝐹𝑗) ∧ ∃𝑥 ∈ ℝ ∃𝑖𝑍𝑗 ∈ (ℤ𝑖)(𝐹𝑗) ≤ 𝑥)))
8612, 85mpbid 222 . . . . . 6 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑖𝑍𝑗 ∈ (ℤ𝑖)𝑥 ≤ (𝐹𝑗) ∧ ∃𝑥 ∈ ℝ ∃𝑖𝑍𝑗 ∈ (ℤ𝑖)(𝐹𝑗) ≤ 𝑥))
8786simpld 477 . . . . 5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖𝑍𝑗 ∈ (ℤ𝑖)𝑥 ≤ (𝐹𝑗))
88 simp-4r 827 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑖𝑍) ∧ 𝑗 ∈ (ℤ𝑖)) ∧ 𝑥 ≤ (𝐹𝑗)) → 𝑥 ∈ ℝ)
8988rexrd 10301 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑖𝑍) ∧ 𝑗 ∈ (ℤ𝑖)) ∧ 𝑥 ≤ (𝐹𝑗)) → 𝑥 ∈ ℝ*)
90843ad2ant1 1128 . . . . . . . . . . . 12 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → 𝐹:𝑍⟶ℝ*)
911uztrn2 11917 . . . . . . . . . . . . 13 ((𝑖𝑍𝑗 ∈ (ℤ𝑖)) → 𝑗𝑍)
92913adant1 1125 . . . . . . . . . . . 12 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → 𝑗𝑍)
9390, 92ffvelrnd 6524 . . . . . . . . . . 11 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → (𝐹𝑗) ∈ ℝ*)
9493ad5ant134 1467 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑖𝑍) ∧ 𝑗 ∈ (ℤ𝑖)) ∧ 𝑥 ≤ (𝐹𝑗)) → (𝐹𝑗) ∈ ℝ*)
9556supxrcld 39807 . . . . . . . . . . 11 ((𝜑𝑖𝑍) → sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ) ∈ ℝ*)
9695ad5ant13 1216 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑖𝑍) ∧ 𝑗 ∈ (ℤ𝑖)) ∧ 𝑥 ≤ (𝐹𝑗)) → sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ) ∈ ℝ*)
97 simpr 479 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑖𝑍) ∧ 𝑗 ∈ (ℤ𝑖)) ∧ 𝑥 ≤ (𝐹𝑗)) → 𝑥 ≤ (𝐹𝑗))
98563adant3 1127 . . . . . . . . . . . 12 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → ran (𝐹 ↾ (ℤ𝑖)) ⊆ ℝ*)
99 fvres 6369 . . . . . . . . . . . . . . 15 (𝑗 ∈ (ℤ𝑖) → ((𝐹 ↾ (ℤ𝑖))‘𝑗) = (𝐹𝑗))
10099eqcomd 2766 . . . . . . . . . . . . . 14 (𝑗 ∈ (ℤ𝑖) → (𝐹𝑗) = ((𝐹 ↾ (ℤ𝑖))‘𝑗))
1011003ad2ant3 1130 . . . . . . . . . . . . 13 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → (𝐹𝑗) = ((𝐹 ↾ (ℤ𝑖))‘𝑗))
1023ffnd 6207 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 Fn 𝑍)
103102adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝑍) → 𝐹 Fn 𝑍)
1041, 76uzssd2 40160 . . . . . . . . . . . . . . . . 17 (𝑖𝑍 → (ℤ𝑖) ⊆ 𝑍)
105104adantl 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝑍) → (ℤ𝑖) ⊆ 𝑍)
106 fnssres 6165 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝑍 ∧ (ℤ𝑖) ⊆ 𝑍) → (𝐹 ↾ (ℤ𝑖)) Fn (ℤ𝑖))
107103, 105, 106syl2anc 696 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑍) → (𝐹 ↾ (ℤ𝑖)) Fn (ℤ𝑖))
1081073adant3 1127 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → (𝐹 ↾ (ℤ𝑖)) Fn (ℤ𝑖))
109 simp3 1133 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → 𝑗 ∈ (ℤ𝑖))
110 fnfvelrn 6520 . . . . . . . . . . . . . 14 (((𝐹 ↾ (ℤ𝑖)) Fn (ℤ𝑖) ∧ 𝑗 ∈ (ℤ𝑖)) → ((𝐹 ↾ (ℤ𝑖))‘𝑗) ∈ ran (𝐹 ↾ (ℤ𝑖)))
111108, 109, 110syl2anc 696 . . . . . . . . . . . . 13 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → ((𝐹 ↾ (ℤ𝑖))‘𝑗) ∈ ran (𝐹 ↾ (ℤ𝑖)))
112101, 111eqeltrd 2839 . . . . . . . . . . . 12 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → (𝐹𝑗) ∈ ran (𝐹 ↾ (ℤ𝑖)))
113 eqid 2760 . . . . . . . . . . . 12 sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ) = sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < )
11498, 112, 113supxrubd 39814 . . . . . . . . . . 11 ((𝜑𝑖𝑍𝑗 ∈ (ℤ𝑖)) → (𝐹𝑗) ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
115114ad5ant134 1467 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑖𝑍) ∧ 𝑗 ∈ (ℤ𝑖)) ∧ 𝑥 ≤ (𝐹𝑗)) → (𝐹𝑗) ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
11689, 94, 96, 97, 115xrletrd 12206 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑖𝑍) ∧ 𝑗 ∈ (ℤ𝑖)) ∧ 𝑥 ≤ (𝐹𝑗)) → 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
117116ex 449 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑖𝑍) ∧ 𝑗 ∈ (ℤ𝑖)) → (𝑥 ≤ (𝐹𝑗) → 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < )))
118117rexlimdva 3169 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖𝑍) → (∃𝑗 ∈ (ℤ𝑖)𝑥 ≤ (𝐹𝑗) → 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < )))
119118ralimdva 3100 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (∀𝑖𝑍𝑗 ∈ (ℤ𝑖)𝑥 ≤ (𝐹𝑗) → ∀𝑖𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < )))
120119reximdva 3155 . . . . 5 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑖𝑍𝑗 ∈ (ℤ𝑖)𝑥 ≤ (𝐹𝑗) → ∃𝑥 ∈ ℝ ∀𝑖𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < )))
12187, 120mpd 15 . . . 4 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
122 simpl 474 . . . . . . 7 ((𝑦 = 𝑥𝑖𝑍) → 𝑦 = 𝑥)
12379adantl 473 . . . . . . 7 ((𝑦 = 𝑥𝑖𝑍) → ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖) = sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
124122, 123breq12d 4817 . . . . . 6 ((𝑦 = 𝑥𝑖𝑍) → (𝑦 ≤ ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖) ↔ 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < )))
125124ralbidva 3123 . . . . 5 (𝑦 = 𝑥 → (∀𝑖𝑍 𝑦 ≤ ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖) ↔ ∀𝑖𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < )))
126125cbvrexv 3311 . . . 4 (∃𝑦 ∈ ℝ ∀𝑖𝑍 𝑦 ≤ ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖) ↔ ∃𝑥 ∈ ℝ ∀𝑖𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑖)), ℝ*, < ))
127121, 126sylibr 224 . . 3 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑖𝑍 𝑦 ≤ ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ))‘𝑖))
1281, 2, 34, 82, 127climinf 40359 . 2 (𝜑 → (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )) ⇝ inf(ran (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )), ℝ, < ))
129 fveq2 6353 . . . . . . . 8 (𝑛 = 𝑘 → (ℤ𝑛) = (ℤ𝑘))
130129reseq2d 5551 . . . . . . 7 (𝑛 = 𝑘 → (𝐹 ↾ (ℤ𝑛)) = (𝐹 ↾ (ℤ𝑘)))
131130rneqd 5508 . . . . . 6 (𝑛 = 𝑘 → ran (𝐹 ↾ (ℤ𝑛)) = ran (𝐹 ↾ (ℤ𝑘)))
132131supeq1d 8519 . . . . 5 (𝑛 = 𝑘 → sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < ) = sup(ran (𝐹 ↾ (ℤ𝑘)), ℝ*, < ))
133132cbvmptv 4902 . . . 4 (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )) = (𝑘𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑘)), ℝ*, < ))
134133a1i 11 . . 3 (𝜑 → (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )) = (𝑘𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑘)), ℝ*, < )))
1352, 1, 3, 12limsupvaluz2 40491 . . . 4 (𝜑 → (lim sup‘𝐹) = inf(ran (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )), ℝ, < ))
136135eqcomd 2766 . . 3 (𝜑 → inf(ran (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )), ℝ, < ) = (lim sup‘𝐹))
137134, 136breq12d 4817 . 2 (𝜑 → ((𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )) ⇝ inf(ran (𝑛𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑛)), ℝ*, < )), ℝ, < ) ↔ (𝑘𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑘)), ℝ*, < )) ⇝ (lim sup‘𝐹)))
138128, 137mpbid 222 1 (𝜑 → (𝑘𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑘)), ℝ*, < )) ⇝ (lim sup‘𝐹))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072   = wceq 1632   ∈ wcel 2139   ≠ wne 2932  ∀wral 3050  ∃wrex 3051  Vcvv 3340   ⊆ wss 3715  ∅c0 4058   class class class wbr 4804   ↦ cmpt 4881  ran crn 5267   ↾ cres 5268   Fn wfn 6044  ⟶wf 6045  ‘cfv 6049  (class class class)co 6814  supcsup 8513  infcinf 8514  ℝcr 10147  1c1 10149   + caddc 10151  ℝ*cxr 10285   < clt 10286   ≤ cle 10287  ℤcz 11589  ℤ≥cuz 11899  lim supclsp 14420   ⇝ cli 14434 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225  ax-pre-sup 10226 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-1st 7334  df-2nd 7335  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-oadd 7734  df-er 7913  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-sup 8515  df-inf 8516  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-div 10897  df-nn 11233  df-2 11291  df-3 11292  df-n0 11505  df-z 11590  df-uz 11900  df-rp 12046  df-ico 12394  df-fz 12540  df-fl 12807  df-ceil 12808  df-seq 13016  df-exp 13075  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-limsup 14421  df-clim 14438 This theorem is referenced by:  supcnvlimsupmpt  40494
 Copyright terms: Public domain W3C validator