MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  limsupgre Structured version   Visualization version   GIF version

Theorem limsupgre 14596
Description: If a sequence of real numbers has upper bounded limit supremum, then all the partial suprema are real. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.)
Hypotheses
Ref Expression
limsupval.1 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
limsupgre.z 𝑍 = (ℤ𝑀)
Assertion
Ref Expression
limsupgre ((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) → 𝐺:ℝ⟶ℝ)
Distinct variable groups:   𝑘,𝐹   𝑘,𝑀   𝑘,𝑍
Allowed substitution hint:   𝐺(𝑘)

Proof of Theorem limsupgre
Dummy variables 𝑎 𝑖 𝑚 𝑛 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xrltso 12267 . . . 4 < Or ℝ*
21supex 8644 . . 3 sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ V
32a1i 11 . 2 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑘 ∈ ℝ) → sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ V)
4 limsupval.1 . . 3 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
54a1i 11 . 2 ((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) → 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )))
64limsupgval 14591 . . . 4 (𝑎 ∈ ℝ → (𝐺𝑎) = sup(((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*), ℝ*, < ))
76adantl 475 . . 3 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐺𝑎) = sup(((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*), ℝ*, < ))
8 simpl3 1250 . . . . . . 7 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (lim sup‘𝐹) < +∞)
9 limsupgre.z . . . . . . . . . . 11 𝑍 = (ℤ𝑀)
10 uzssz 11995 . . . . . . . . . . 11 (ℤ𝑀) ⊆ ℤ
119, 10eqsstri 3860 . . . . . . . . . 10 𝑍 ⊆ ℤ
12 zssre 11718 . . . . . . . . . 10 ℤ ⊆ ℝ
1311, 12sstri 3836 . . . . . . . . 9 𝑍 ⊆ ℝ
1413a1i 11 . . . . . . . 8 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑍 ⊆ ℝ)
15 simpl2 1248 . . . . . . . . 9 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝐹:𝑍⟶ℝ)
16 ressxr 10407 . . . . . . . . 9 ℝ ⊆ ℝ*
17 fss 6295 . . . . . . . . 9 ((𝐹:𝑍⟶ℝ ∧ ℝ ⊆ ℝ*) → 𝐹:𝑍⟶ℝ*)
1815, 16, 17sylancl 580 . . . . . . . 8 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝐹:𝑍⟶ℝ*)
19 pnfxr 10417 . . . . . . . . 9 +∞ ∈ ℝ*
2019a1i 11 . . . . . . . 8 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → +∞ ∈ ℝ*)
214limsuplt 14594 . . . . . . . 8 ((𝑍 ⊆ ℝ ∧ 𝐹:𝑍⟶ℝ* ∧ +∞ ∈ ℝ*) → ((lim sup‘𝐹) < +∞ ↔ ∃𝑛 ∈ ℝ (𝐺𝑛) < +∞))
2214, 18, 20, 21syl3anc 1494 . . . . . . 7 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ((lim sup‘𝐹) < +∞ ↔ ∃𝑛 ∈ ℝ (𝐺𝑛) < +∞))
238, 22mpbid 224 . . . . . 6 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ∃𝑛 ∈ ℝ (𝐺𝑛) < +∞)
24 fzfi 13073 . . . . . . . 8 (𝑀...(⌊‘𝑛)) ∈ Fin
2515adantr 474 . . . . . . . . . 10 ((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) → 𝐹:𝑍⟶ℝ)
26 elfzuz 12638 . . . . . . . . . . 11 (𝑚 ∈ (𝑀...(⌊‘𝑛)) → 𝑚 ∈ (ℤ𝑀))
2726, 9syl6eleqr 2917 . . . . . . . . . 10 (𝑚 ∈ (𝑀...(⌊‘𝑛)) → 𝑚𝑍)
28 ffvelrn 6611 . . . . . . . . . 10 ((𝐹:𝑍⟶ℝ ∧ 𝑚𝑍) → (𝐹𝑚) ∈ ℝ)
2925, 27, 28syl2an 589 . . . . . . . . 9 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ 𝑚 ∈ (𝑀...(⌊‘𝑛))) → (𝐹𝑚) ∈ ℝ)
3029ralrimiva 3175 . . . . . . . 8 ((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) → ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ∈ ℝ)
31 fimaxre3 11307 . . . . . . . 8 (((𝑀...(⌊‘𝑛)) ∈ Fin ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ∈ ℝ) → ∃𝑟 ∈ ℝ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)
3224, 30, 31sylancr 581 . . . . . . 7 ((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) → ∃𝑟 ∈ ℝ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)
33 simpr 479 . . . . . . . . . 10 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
3433ad2antrr 717 . . . . . . . . 9 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → 𝑎 ∈ ℝ)
354limsupgf 14590 . . . . . . . . . 10 𝐺:ℝ⟶ℝ*
3635ffvelrni 6612 . . . . . . . . 9 (𝑎 ∈ ℝ → (𝐺𝑎) ∈ ℝ*)
3734, 36syl 17 . . . . . . . 8 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → (𝐺𝑎) ∈ ℝ*)
38 simprl 787 . . . . . . . . . 10 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → 𝑟 ∈ ℝ)
3916, 38sseldi 3825 . . . . . . . . 9 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → 𝑟 ∈ ℝ*)
40 simprl 787 . . . . . . . . . . 11 ((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) → 𝑛 ∈ ℝ)
4140adantr 474 . . . . . . . . . 10 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → 𝑛 ∈ ℝ)
4235ffvelrni 6612 . . . . . . . . . 10 (𝑛 ∈ ℝ → (𝐺𝑛) ∈ ℝ*)
4341, 42syl 17 . . . . . . . . 9 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → (𝐺𝑛) ∈ ℝ*)
4439, 43ifcld 4353 . . . . . . . 8 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)) ∈ ℝ*)
4519a1i 11 . . . . . . . 8 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → +∞ ∈ ℝ*)
4640ad2antrr 717 . . . . . . . . . . . 12 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → 𝑛 ∈ ℝ)
4713a1i 11 . . . . . . . . . . . . 13 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → 𝑍 ⊆ ℝ)
4847sselda 3827 . . . . . . . . . . . 12 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → 𝑖 ∈ ℝ)
4943xrleidd 12278 . . . . . . . . . . . . . . . 16 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → (𝐺𝑛) ≤ (𝐺𝑛))
5018ad2antrr 717 . . . . . . . . . . . . . . . . 17 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → 𝐹:𝑍⟶ℝ*)
514limsupgle 14592 . . . . . . . . . . . . . . . . 17 (((𝑍 ⊆ ℝ ∧ 𝐹:𝑍⟶ℝ*) ∧ 𝑛 ∈ ℝ ∧ (𝐺𝑛) ∈ ℝ*) → ((𝐺𝑛) ≤ (𝐺𝑛) ↔ ∀𝑖𝑍 (𝑛𝑖 → (𝐹𝑖) ≤ (𝐺𝑛))))
5247, 50, 41, 43, 51syl211anc 1499 . . . . . . . . . . . . . . . 16 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → ((𝐺𝑛) ≤ (𝐺𝑛) ↔ ∀𝑖𝑍 (𝑛𝑖 → (𝐹𝑖) ≤ (𝐺𝑛))))
5349, 52mpbid 224 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → ∀𝑖𝑍 (𝑛𝑖 → (𝐹𝑖) ≤ (𝐺𝑛)))
5453r19.21bi 3141 . . . . . . . . . . . . . 14 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → (𝑛𝑖 → (𝐹𝑖) ≤ (𝐺𝑛)))
5554imp 397 . . . . . . . . . . . . 13 (((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) ∧ 𝑛𝑖) → (𝐹𝑖) ≤ (𝐺𝑛))
5646, 42syl 17 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → (𝐺𝑛) ∈ ℝ*)
5739adantr 474 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → 𝑟 ∈ ℝ*)
58 xrmax1 12301 . . . . . . . . . . . . . . . 16 (((𝐺𝑛) ∈ ℝ*𝑟 ∈ ℝ*) → (𝐺𝑛) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)))
5956, 57, 58syl2anc 579 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → (𝐺𝑛) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)))
6050ffvelrnda 6613 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → (𝐹𝑖) ∈ ℝ*)
6144adantr 474 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)) ∈ ℝ*)
62 xrletr 12284 . . . . . . . . . . . . . . . 16 (((𝐹𝑖) ∈ ℝ* ∧ (𝐺𝑛) ∈ ℝ* ∧ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)) ∈ ℝ*) → (((𝐹𝑖) ≤ (𝐺𝑛) ∧ (𝐺𝑛) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛))) → (𝐹𝑖) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛))))
6360, 56, 61, 62syl3anc 1494 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → (((𝐹𝑖) ≤ (𝐺𝑛) ∧ (𝐺𝑛) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛))) → (𝐹𝑖) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛))))
6459, 63mpan2d 685 . . . . . . . . . . . . . 14 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → ((𝐹𝑖) ≤ (𝐺𝑛) → (𝐹𝑖) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛))))
6564adantr 474 . . . . . . . . . . . . 13 (((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) ∧ 𝑛𝑖) → ((𝐹𝑖) ≤ (𝐺𝑛) → (𝐹𝑖) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛))))
6655, 65mpd 15 . . . . . . . . . . . 12 (((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) ∧ 𝑛𝑖) → (𝐹𝑖) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)))
67 fveq2 6437 . . . . . . . . . . . . . . 15 (𝑚 = 𝑖 → (𝐹𝑚) = (𝐹𝑖))
6867breq1d 4885 . . . . . . . . . . . . . 14 (𝑚 = 𝑖 → ((𝐹𝑚) ≤ 𝑟 ↔ (𝐹𝑖) ≤ 𝑟))
69 simprr 789 . . . . . . . . . . . . . . 15 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)
7069ad2antrr 717 . . . . . . . . . . . . . 14 (((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) ∧ 𝑖𝑛) → ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)
71 simpr 479 . . . . . . . . . . . . . . . . . 18 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → 𝑖𝑍)
7271, 9syl6eleq 2916 . . . . . . . . . . . . . . . . 17 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → 𝑖 ∈ (ℤ𝑀))
7341flcld 12901 . . . . . . . . . . . . . . . . . 18 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → (⌊‘𝑛) ∈ ℤ)
7473adantr 474 . . . . . . . . . . . . . . . . 17 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → (⌊‘𝑛) ∈ ℤ)
75 elfz5 12634 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (ℤ𝑀) ∧ (⌊‘𝑛) ∈ ℤ) → (𝑖 ∈ (𝑀...(⌊‘𝑛)) ↔ 𝑖 ≤ (⌊‘𝑛)))
7672, 74, 75syl2anc 579 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → (𝑖 ∈ (𝑀...(⌊‘𝑛)) ↔ 𝑖 ≤ (⌊‘𝑛)))
7711, 71sseldi 3825 . . . . . . . . . . . . . . . . 17 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → 𝑖 ∈ ℤ)
78 flge 12908 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℝ ∧ 𝑖 ∈ ℤ) → (𝑖𝑛𝑖 ≤ (⌊‘𝑛)))
7946, 77, 78syl2anc 579 . . . . . . . . . . . . . . . 16 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → (𝑖𝑛𝑖 ≤ (⌊‘𝑛)))
8076, 79bitr4d 274 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → (𝑖 ∈ (𝑀...(⌊‘𝑛)) ↔ 𝑖𝑛))
8180biimpar 471 . . . . . . . . . . . . . 14 (((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) ∧ 𝑖𝑛) → 𝑖 ∈ (𝑀...(⌊‘𝑛)))
8268, 70, 81rspcdva 3532 . . . . . . . . . . . . 13 (((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) ∧ 𝑖𝑛) → (𝐹𝑖) ≤ 𝑟)
83 xrmax2 12302 . . . . . . . . . . . . . . . . 17 (((𝐺𝑛) ∈ ℝ*𝑟 ∈ ℝ*) → 𝑟 ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)))
8443, 39, 83syl2anc 579 . . . . . . . . . . . . . . . 16 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → 𝑟 ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)))
8584adantr 474 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → 𝑟 ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)))
86 xrletr 12284 . . . . . . . . . . . . . . . 16 (((𝐹𝑖) ∈ ℝ*𝑟 ∈ ℝ* ∧ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)) ∈ ℝ*) → (((𝐹𝑖) ≤ 𝑟𝑟 ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛))) → (𝐹𝑖) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛))))
8760, 57, 61, 86syl3anc 1494 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → (((𝐹𝑖) ≤ 𝑟𝑟 ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛))) → (𝐹𝑖) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛))))
8885, 87mpan2d 685 . . . . . . . . . . . . . 14 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → ((𝐹𝑖) ≤ 𝑟 → (𝐹𝑖) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛))))
8988adantr 474 . . . . . . . . . . . . 13 (((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) ∧ 𝑖𝑛) → ((𝐹𝑖) ≤ 𝑟 → (𝐹𝑖) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛))))
9082, 89mpd 15 . . . . . . . . . . . 12 (((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) ∧ 𝑖𝑛) → (𝐹𝑖) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)))
9146, 48, 66, 90lecasei 10469 . . . . . . . . . . 11 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → (𝐹𝑖) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)))
9291a1d 25 . . . . . . . . . 10 ((((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) ∧ 𝑖𝑍) → (𝑎𝑖 → (𝐹𝑖) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛))))
9392ralrimiva 3175 . . . . . . . . 9 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → ∀𝑖𝑍 (𝑎𝑖 → (𝐹𝑖) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛))))
944limsupgle 14592 . . . . . . . . . 10 (((𝑍 ⊆ ℝ ∧ 𝐹:𝑍⟶ℝ*) ∧ 𝑎 ∈ ℝ ∧ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)) ∈ ℝ*) → ((𝐺𝑎) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)) ↔ ∀𝑖𝑍 (𝑎𝑖 → (𝐹𝑖) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)))))
9547, 50, 34, 44, 94syl211anc 1499 . . . . . . . . 9 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → ((𝐺𝑎) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)) ↔ ∀𝑖𝑍 (𝑎𝑖 → (𝐹𝑖) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)))))
9693, 95mpbird 249 . . . . . . . 8 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → (𝐺𝑎) ≤ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)))
9738ltpnfd 12248 . . . . . . . . 9 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → 𝑟 < +∞)
98 simplrr 796 . . . . . . . . 9 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → (𝐺𝑛) < +∞)
99 breq1 4878 . . . . . . . . . 10 (𝑟 = if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)) → (𝑟 < +∞ ↔ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)) < +∞))
100 breq1 4878 . . . . . . . . . 10 ((𝐺𝑛) = if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)) → ((𝐺𝑛) < +∞ ↔ if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)) < +∞))
10199, 100ifboth 4346 . . . . . . . . 9 ((𝑟 < +∞ ∧ (𝐺𝑛) < +∞) → if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)) < +∞)
10297, 98, 101syl2anc 579 . . . . . . . 8 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → if((𝐺𝑛) ≤ 𝑟, 𝑟, (𝐺𝑛)) < +∞)
10337, 44, 45, 96, 102xrlelttrd 12286 . . . . . . 7 (((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹𝑚) ≤ 𝑟)) → (𝐺𝑎) < +∞)
10432, 103rexlimddv 3245 . . . . . 6 ((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺𝑛) < +∞)) → (𝐺𝑎) < +∞)
10523, 104rexlimddv 3245 . . . . 5 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐺𝑎) < +∞)
1067, 105eqbrtrrd 4899 . . . 4 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → sup(((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*), ℝ*, < ) < +∞)
107 imassrn 5722 . . . . . . . . 9 (𝐹 “ (𝑎[,)+∞)) ⊆ ran 𝐹
10815frnd 6289 . . . . . . . . 9 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ran 𝐹 ⊆ ℝ)
109107, 108syl5ss 3838 . . . . . . . 8 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐹 “ (𝑎[,)+∞)) ⊆ ℝ)
110109, 16syl6ss 3839 . . . . . . 7 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐹 “ (𝑎[,)+∞)) ⊆ ℝ*)
111 df-ss 3812 . . . . . . 7 ((𝐹 “ (𝑎[,)+∞)) ⊆ ℝ* ↔ ((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*) = (𝐹 “ (𝑎[,)+∞)))
112110, 111sylib 210 . . . . . 6 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*) = (𝐹 “ (𝑎[,)+∞)))
113112, 109eqsstrd 3864 . . . . 5 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*) ⊆ ℝ)
114 simpl1 1246 . . . . . . . . . . 11 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑀 ∈ ℤ)
115 flcl 12898 . . . . . . . . . . . . . 14 (𝑎 ∈ ℝ → (⌊‘𝑎) ∈ ℤ)
116115adantl 475 . . . . . . . . . . . . 13 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (⌊‘𝑎) ∈ ℤ)
117116peano2zd 11820 . . . . . . . . . . . 12 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ((⌊‘𝑎) + 1) ∈ ℤ)
118117, 114ifcld 4353 . . . . . . . . . . 11 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ ℤ)
119114zred 11817 . . . . . . . . . . . 12 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑀 ∈ ℝ)
120117zred 11817 . . . . . . . . . . . 12 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ((⌊‘𝑎) + 1) ∈ ℝ)
121 max1 12311 . . . . . . . . . . . 12 ((𝑀 ∈ ℝ ∧ ((⌊‘𝑎) + 1) ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀))
122119, 120, 121syl2anc 579 . . . . . . . . . . 11 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀))
123 eluz2 11981 . . . . . . . . . . 11 (if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ ℤ ∧ 𝑀 ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀)))
124114, 118, 122, 123syl3anbrc 1447 . . . . . . . . . 10 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ (ℤ𝑀))
125124, 9syl6eleqr 2917 . . . . . . . . 9 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ 𝑍)
12615fdmd 6291 . . . . . . . . 9 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → dom 𝐹 = 𝑍)
127125, 126eleqtrrd 2909 . . . . . . . 8 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ dom 𝐹)
128118zred 11817 . . . . . . . . 9 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ ℝ)
129 fllep1 12904 . . . . . . . . . . 11 (𝑎 ∈ ℝ → 𝑎 ≤ ((⌊‘𝑎) + 1))
130129adantl 475 . . . . . . . . . 10 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑎 ≤ ((⌊‘𝑎) + 1))
131 max2 12313 . . . . . . . . . . 11 ((𝑀 ∈ ℝ ∧ ((⌊‘𝑎) + 1) ∈ ℝ) → ((⌊‘𝑎) + 1) ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀))
132119, 120, 131syl2anc 579 . . . . . . . . . 10 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ((⌊‘𝑎) + 1) ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀))
13333, 120, 128, 130, 132letrd 10520 . . . . . . . . 9 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑎 ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀))
134 elicopnf 12565 . . . . . . . . . 10 (𝑎 ∈ ℝ → (if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ (𝑎[,)+∞) ↔ (if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ ℝ ∧ 𝑎 ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀))))
135134adantl 475 . . . . . . . . 9 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ (𝑎[,)+∞) ↔ (if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ ℝ ∧ 𝑎 ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀))))
136128, 133, 135mpbir2and 704 . . . . . . . 8 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ (𝑎[,)+∞))
137 inelcm 4258 . . . . . . . 8 ((if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ dom 𝐹 ∧ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ (𝑎[,)+∞)) → (dom 𝐹 ∩ (𝑎[,)+∞)) ≠ ∅)
138127, 136, 137syl2anc 579 . . . . . . 7 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (dom 𝐹 ∩ (𝑎[,)+∞)) ≠ ∅)
139 imadisj 5729 . . . . . . . 8 ((𝐹 “ (𝑎[,)+∞)) = ∅ ↔ (dom 𝐹 ∩ (𝑎[,)+∞)) = ∅)
140139necon3bii 3051 . . . . . . 7 ((𝐹 “ (𝑎[,)+∞)) ≠ ∅ ↔ (dom 𝐹 ∩ (𝑎[,)+∞)) ≠ ∅)
141138, 140sylibr 226 . . . . . 6 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐹 “ (𝑎[,)+∞)) ≠ ∅)
142112, 141eqnetrd 3066 . . . . 5 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*) ≠ ∅)
143 supxrre1 12455 . . . . 5 ((((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*) ⊆ ℝ ∧ ((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*) ≠ ∅) → (sup(((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ ↔ sup(((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*), ℝ*, < ) < +∞))
144113, 142, 143syl2anc 579 . . . 4 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (sup(((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ ↔ sup(((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*), ℝ*, < ) < +∞))
145106, 144mpbird 249 . . 3 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → sup(((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ)
1467, 145eqeltrd 2906 . 2 (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐺𝑎) ∈ ℝ)
1473, 5, 146fmpt2d 6647 1 ((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) → 𝐺:ℝ⟶ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  w3a 1111   = wceq 1656  wcel 2164  wne 2999  wral 3117  wrex 3118  Vcvv 3414  cin 3797  wss 3798  c0 4146  ifcif 4308   class class class wbr 4875  cmpt 4954  dom cdm 5346  ran crn 5347  cima 5349  wf 6123  cfv 6127  (class class class)co 6910  Fincfn 8228  supcsup 8621  cr 10258  1c1 10260   + caddc 10262  +∞cpnf 10395  *cxr 10397   < clt 10398  cle 10399  cz 11711  cuz 11975  [,)cico 12472  ...cfz 12626  cfl 12893  lim supclsp 14585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214  ax-cnex 10315  ax-resscn 10316  ax-1cn 10317  ax-icn 10318  ax-addcl 10319  ax-addrcl 10320  ax-mulcl 10321  ax-mulrcl 10322  ax-mulcom 10323  ax-addass 10324  ax-mulass 10325  ax-distr 10326  ax-i2m1 10327  ax-1ne0 10328  ax-1rid 10329  ax-rnegex 10330  ax-rrecex 10331  ax-cnre 10332  ax-pre-lttri 10333  ax-pre-lttrn 10334  ax-pre-ltadd 10335  ax-pre-mulgt0 10336  ax-pre-sup 10337
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-tp 4404  df-op 4406  df-uni 4661  df-int 4700  df-iun 4744  df-br 4876  df-opab 4938  df-mpt 4955  df-tr 4978  df-id 5252  df-eprel 5257  df-po 5265  df-so 5266  df-fr 5305  df-we 5307  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-pred 5924  df-ord 5970  df-on 5971  df-lim 5972  df-suc 5973  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-riota 6871  df-ov 6913  df-oprab 6914  df-mpt2 6915  df-om 7332  df-1st 7433  df-2nd 7434  df-wrecs 7677  df-recs 7739  df-rdg 7777  df-1o 7831  df-oadd 7835  df-er 8014  df-en 8229  df-dom 8230  df-sdom 8231  df-fin 8232  df-sup 8623  df-inf 8624  df-pnf 10400  df-mnf 10401  df-xr 10402  df-ltxr 10403  df-le 10404  df-sub 10594  df-neg 10595  df-nn 11358  df-n0 11626  df-z 11712  df-uz 11976  df-ico 12476  df-fz 12627  df-fl 12895  df-limsup 14586
This theorem is referenced by:  mbflimsup  23839
  Copyright terms: Public domain W3C validator