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

Theorem limsupgtlem 44944
Description: For any positive real, the superior limit of F is larger than any of its values at large enough arguments, up to that positive real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
Hypotheses
Ref Expression
limsupgtlem.m (𝜑𝑀 ∈ ℤ)
limsupgtlem.z 𝑍 = (ℤ𝑀)
limsupgtlem.f (𝜑𝐹:𝑍⟶ℝ)
limsupgtlem.r (𝜑 → (lim sup‘𝐹) ∈ ℝ)
limsupgtlem.x (𝜑𝑋 ∈ ℝ+)
Assertion
Ref Expression
limsupgtlem (𝜑 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)((𝐹𝑘) − 𝑋) < (lim sup‘𝐹))
Distinct variable groups:   𝑗,𝐹,𝑘   𝑗,𝑋,𝑘   𝑗,𝑍,𝑘   𝜑,𝑗,𝑘
Allowed substitution hints:   𝑀(𝑗,𝑘)

Proof of Theorem limsupgtlem
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 nfv 1909 . . . 4 𝑗𝜑
2 limsupgtlem.m . . . . 5 (𝜑𝑀 ∈ ℤ)
3 limsupgtlem.z . . . . 5 𝑍 = (ℤ𝑀)
42, 3uzn0d 44586 . . . 4 (𝜑𝑍 ≠ ∅)
5 rnresss 6007 . . . . . . . 8 ran (𝐹 ↾ (ℤ𝑗)) ⊆ ran 𝐹
65a1i 11 . . . . . . 7 (𝜑 → ran (𝐹 ↾ (ℤ𝑗)) ⊆ ran 𝐹)
7 limsupgtlem.f . . . . . . . . 9 (𝜑𝐹:𝑍⟶ℝ)
87frexr 44546 . . . . . . . 8 (𝜑𝐹:𝑍⟶ℝ*)
98frnd 6715 . . . . . . 7 (𝜑 → ran 𝐹 ⊆ ℝ*)
106, 9sstrd 3984 . . . . . 6 (𝜑 → ran (𝐹 ↾ (ℤ𝑗)) ⊆ ℝ*)
1110supxrcld 44250 . . . . 5 (𝜑 → sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ∈ ℝ*)
1211adantr 480 . . . 4 ((𝜑𝑗𝑍) → sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ∈ ℝ*)
13 limsupgtlem.r . . . . . . 7 (𝜑 → (lim sup‘𝐹) ∈ ℝ)
14 nfcv 2895 . . . . . . . 8 𝑘𝐹
1514, 2, 3, 7limsupreuz 44904 . . . . . . 7 (𝜑 → ((lim sup‘𝐹) ∈ ℝ ↔ (∃𝑥 ∈ ℝ ∀𝑗𝑍𝑘 ∈ (ℤ𝑗)𝑥 ≤ (𝐹𝑘) ∧ ∃𝑥 ∈ ℝ ∀𝑘𝑍 (𝐹𝑘) ≤ 𝑥)))
1613, 15mpbid 231 . . . . . 6 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗𝑍𝑘 ∈ (ℤ𝑗)𝑥 ≤ (𝐹𝑘) ∧ ∃𝑥 ∈ ℝ ∀𝑘𝑍 (𝐹𝑘) ≤ 𝑥))
1716simpld 494 . . . . 5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗𝑍𝑘 ∈ (ℤ𝑗)𝑥 ≤ (𝐹𝑘))
18 rexr 11256 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
1918ad4antlr 730 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑥 ≤ (𝐹𝑘)) → 𝑥 ∈ ℝ*)
207ad2antrr 723 . . . . . . . . . . . . 13 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝐹:𝑍⟶ℝ)
213uztrn2 12837 . . . . . . . . . . . . . 14 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
2221adantll 711 . . . . . . . . . . . . 13 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
2320, 22ffvelcdmd 7077 . . . . . . . . . . . 12 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ ℝ)
2423rexrd 11260 . . . . . . . . . . 11 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ ℝ*)
25243impa 1107 . . . . . . . . . 10 ((𝜑𝑗𝑍𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ ℝ*)
2625ad5ant134 1364 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑥 ≤ (𝐹𝑘)) → (𝐹𝑘) ∈ ℝ*)
2711ad4antr 729 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑥 ≤ (𝐹𝑘)) → sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ∈ ℝ*)
28 simpr 484 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑥 ≤ (𝐹𝑘)) → 𝑥 ≤ (𝐹𝑘))
2910ad2antrr 723 . . . . . . . . . . . 12 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ran (𝐹 ↾ (ℤ𝑗)) ⊆ ℝ*)
30 fvres 6900 . . . . . . . . . . . . . . 15 (𝑘 ∈ (ℤ𝑗) → ((𝐹 ↾ (ℤ𝑗))‘𝑘) = (𝐹𝑘))
3130eqcomd 2730 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ𝑗) → (𝐹𝑘) = ((𝐹 ↾ (ℤ𝑗))‘𝑘))
3231adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) = ((𝐹 ↾ (ℤ𝑗))‘𝑘))
337ffnd 6708 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 Fn 𝑍)
3433adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑍) → 𝐹 Fn 𝑍)
3522ssd 44223 . . . . . . . . . . . . . . . 16 ((𝜑𝑗𝑍) → (ℤ𝑗) ⊆ 𝑍)
36 fnssres 6663 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝑍 ∧ (ℤ𝑗) ⊆ 𝑍) → (𝐹 ↾ (ℤ𝑗)) Fn (ℤ𝑗))
3734, 35, 36syl2anc 583 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑍) → (𝐹 ↾ (ℤ𝑗)) Fn (ℤ𝑗))
3837adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹 ↾ (ℤ𝑗)) Fn (ℤ𝑗))
39 simpr 484 . . . . . . . . . . . . . 14 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ (ℤ𝑗))
4038, 39fnfvelrnd 7074 . . . . . . . . . . . . 13 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝐹 ↾ (ℤ𝑗))‘𝑘) ∈ ran (𝐹 ↾ (ℤ𝑗)))
4132, 40eqeltrd 2825 . . . . . . . . . . . 12 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ ran (𝐹 ↾ (ℤ𝑗)))
42 eqid 2724 . . . . . . . . . . . 12 sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) = sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < )
4329, 41, 42supxrubd 44256 . . . . . . . . . . 11 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ≤ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ))
44433impa 1107 . . . . . . . . . 10 ((𝜑𝑗𝑍𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ≤ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ))
4544ad5ant134 1364 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑥 ≤ (𝐹𝑘)) → (𝐹𝑘) ≤ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ))
4619, 26, 27, 28, 45xrletrd 13137 . . . . . . . 8 (((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑥 ≤ (𝐹𝑘)) → 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ))
4746rexlimdva2 3149 . . . . . . 7 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) → (∃𝑘 ∈ (ℤ𝑗)𝑥 ≤ (𝐹𝑘) → 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < )))
4847ralimdva 3159 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (∀𝑗𝑍𝑘 ∈ (ℤ𝑗)𝑥 ≤ (𝐹𝑘) → ∀𝑗𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < )))
4948reximdva 3160 . . . . 5 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗𝑍𝑘 ∈ (ℤ𝑗)𝑥 ≤ (𝐹𝑘) → ∃𝑥 ∈ ℝ ∀𝑗𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < )))
5017, 49mpd 15 . . . 4 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗𝑍 𝑥 ≤ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ))
51 limsupgtlem.x . . . . 5 (𝜑𝑋 ∈ ℝ+)
5251rphalfcld 13024 . . . 4 (𝜑 → (𝑋 / 2) ∈ ℝ+)
531, 4, 12, 50, 52infrpgernmpt 44626 . . 3 (𝜑 → ∃𝑗𝑍 sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ (inf(ran (𝑗𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < )), ℝ*, < ) +𝑒 (𝑋 / 2)))
54 simp3 1135 . . . . . . 7 ((𝜑𝑗𝑍 ∧ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ (inf(ran (𝑗𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < )), ℝ*, < ) +𝑒 (𝑋 / 2))) → sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ (inf(ran (𝑗𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < )), ℝ*, < ) +𝑒 (𝑋 / 2)))
552, 3, 8limsupvaluz 44875 . . . . . . . . . 10 (𝜑 → (lim sup‘𝐹) = inf(ran (𝑗𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < )), ℝ*, < ))
5655eqcomd 2730 . . . . . . . . 9 (𝜑 → inf(ran (𝑗𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < )), ℝ*, < ) = (lim sup‘𝐹))
5756oveq1d 7416 . . . . . . . 8 (𝜑 → (inf(ran (𝑗𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < )), ℝ*, < ) +𝑒 (𝑋 / 2)) = ((lim sup‘𝐹) +𝑒 (𝑋 / 2)))
58573ad2ant1 1130 . . . . . . 7 ((𝜑𝑗𝑍 ∧ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ (inf(ran (𝑗𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < )), ℝ*, < ) +𝑒 (𝑋 / 2))) → (inf(ran (𝑗𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < )), ℝ*, < ) +𝑒 (𝑋 / 2)) = ((lim sup‘𝐹) +𝑒 (𝑋 / 2)))
5954, 58breqtrd 5164 . . . . . 6 ((𝜑𝑗𝑍 ∧ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ (inf(ran (𝑗𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < )), ℝ*, < ) +𝑒 (𝑋 / 2))) → sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ ((lim sup‘𝐹) +𝑒 (𝑋 / 2)))
60243adantl3 1165 . . . . . . . . . 10 (((𝜑𝑗𝑍 ∧ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ ((lim sup‘𝐹) +𝑒 (𝑋 / 2))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ ℝ*)
61 simpl1 1188 . . . . . . . . . . 11 (((𝜑𝑗𝑍 ∧ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ ((lim sup‘𝐹) +𝑒 (𝑋 / 2))) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝜑)
6261, 11syl 17 . . . . . . . . . 10 (((𝜑𝑗𝑍 ∧ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ ((lim sup‘𝐹) +𝑒 (𝑋 / 2))) ∧ 𝑘 ∈ (ℤ𝑗)) → sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ∈ ℝ*)
633fvexi 6895 . . . . . . . . . . . . . . 15 𝑍 ∈ V
6463a1i 11 . . . . . . . . . . . . . 14 (𝜑𝑍 ∈ V)
657, 64fexd 7220 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ V)
6665limsupcld 44857 . . . . . . . . . . . 12 (𝜑 → (lim sup‘𝐹) ∈ ℝ*)
6751rpred 13012 . . . . . . . . . . . . . 14 (𝜑𝑋 ∈ ℝ)
6867rehalfcld 12455 . . . . . . . . . . . . 13 (𝜑 → (𝑋 / 2) ∈ ℝ)
6968rexrd 11260 . . . . . . . . . . . 12 (𝜑 → (𝑋 / 2) ∈ ℝ*)
7066, 69xaddcld 13276 . . . . . . . . . . 11 (𝜑 → ((lim sup‘𝐹) +𝑒 (𝑋 / 2)) ∈ ℝ*)
7161, 70syl 17 . . . . . . . . . 10 (((𝜑𝑗𝑍 ∧ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ ((lim sup‘𝐹) +𝑒 (𝑋 / 2))) ∧ 𝑘 ∈ (ℤ𝑗)) → ((lim sup‘𝐹) +𝑒 (𝑋 / 2)) ∈ ℝ*)
72433adantl3 1165 . . . . . . . . . 10 (((𝜑𝑗𝑍 ∧ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ ((lim sup‘𝐹) +𝑒 (𝑋 / 2))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ≤ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ))
73 simpl3 1190 . . . . . . . . . 10 (((𝜑𝑗𝑍 ∧ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ ((lim sup‘𝐹) +𝑒 (𝑋 / 2))) ∧ 𝑘 ∈ (ℤ𝑗)) → sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ ((lim sup‘𝐹) +𝑒 (𝑋 / 2)))
7460, 62, 71, 72, 73xrletrd 13137 . . . . . . . . 9 (((𝜑𝑗𝑍 ∧ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ ((lim sup‘𝐹) +𝑒 (𝑋 / 2))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ≤ ((lim sup‘𝐹) +𝑒 (𝑋 / 2)))
7513, 68rexaddd 13209 . . . . . . . . . 10 (𝜑 → ((lim sup‘𝐹) +𝑒 (𝑋 / 2)) = ((lim sup‘𝐹) + (𝑋 / 2)))
7661, 75syl 17 . . . . . . . . 9 (((𝜑𝑗𝑍 ∧ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ ((lim sup‘𝐹) +𝑒 (𝑋 / 2))) ∧ 𝑘 ∈ (ℤ𝑗)) → ((lim sup‘𝐹) +𝑒 (𝑋 / 2)) = ((lim sup‘𝐹) + (𝑋 / 2)))
7774, 76breqtrd 5164 . . . . . . . 8 (((𝜑𝑗𝑍 ∧ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ ((lim sup‘𝐹) +𝑒 (𝑋 / 2))) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ≤ ((lim sup‘𝐹) + (𝑋 / 2)))
7868ad2antrr 723 . . . . . . . . . 10 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝑋 / 2) ∈ ℝ)
7913ad2antrr 723 . . . . . . . . . 10 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (lim sup‘𝐹) ∈ ℝ)
8023, 78, 79lesubaddd 11807 . . . . . . . . 9 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹) ↔ (𝐹𝑘) ≤ ((lim sup‘𝐹) + (𝑋 / 2))))
81803adantl3 1165 . . . . . . . 8 (((𝜑𝑗𝑍 ∧ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ ((lim sup‘𝐹) +𝑒 (𝑋 / 2))) ∧ 𝑘 ∈ (ℤ𝑗)) → (((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹) ↔ (𝐹𝑘) ≤ ((lim sup‘𝐹) + (𝑋 / 2))))
8277, 81mpbird 257 . . . . . . 7 (((𝜑𝑗𝑍 ∧ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ ((lim sup‘𝐹) +𝑒 (𝑋 / 2))) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹))
8382ralrimiva 3138 . . . . . 6 ((𝜑𝑗𝑍 ∧ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ ((lim sup‘𝐹) +𝑒 (𝑋 / 2))) → ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹))
8459, 83syld3an3 1406 . . . . 5 ((𝜑𝑗𝑍 ∧ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ (inf(ran (𝑗𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < )), ℝ*, < ) +𝑒 (𝑋 / 2))) → ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹))
85843exp 1116 . . . 4 (𝜑 → (𝑗𝑍 → (sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ (inf(ran (𝑗𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < )), ℝ*, < ) +𝑒 (𝑋 / 2)) → ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹))))
861, 85reximdai 3250 . . 3 (𝜑 → (∃𝑗𝑍 sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < ) ≤ (inf(ran (𝑗𝑍 ↦ sup(ran (𝐹 ↾ (ℤ𝑗)), ℝ*, < )), ℝ*, < ) +𝑒 (𝑋 / 2)) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)))
8753, 86mpd 15 . 2 (𝜑 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹))
88 simpll 764 . . . . 5 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝜑)
897ffvelcdmda 7076 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
9067adantr 480 . . . . . . . . 9 ((𝜑𝑘𝑍) → 𝑋 ∈ ℝ)
9189, 90resubcld 11638 . . . . . . . 8 ((𝜑𝑘𝑍) → ((𝐹𝑘) − 𝑋) ∈ ℝ)
9291adantr 480 . . . . . . 7 (((𝜑𝑘𝑍) ∧ ((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)) → ((𝐹𝑘) − 𝑋) ∈ ℝ)
9368adantr 480 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝑋 / 2) ∈ ℝ)
9489, 93resubcld 11638 . . . . . . . 8 ((𝜑𝑘𝑍) → ((𝐹𝑘) − (𝑋 / 2)) ∈ ℝ)
9594adantr 480 . . . . . . 7 (((𝜑𝑘𝑍) ∧ ((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)) → ((𝐹𝑘) − (𝑋 / 2)) ∈ ℝ)
9613ad2antrr 723 . . . . . . 7 (((𝜑𝑘𝑍) ∧ ((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)) → (lim sup‘𝐹) ∈ ℝ)
9751rphalfltd 44616 . . . . . . . . . 10 (𝜑 → (𝑋 / 2) < 𝑋)
9897adantr 480 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝑋 / 2) < 𝑋)
9993, 90, 89, 98ltsub2dd 11823 . . . . . . . 8 ((𝜑𝑘𝑍) → ((𝐹𝑘) − 𝑋) < ((𝐹𝑘) − (𝑋 / 2)))
10099adantr 480 . . . . . . 7 (((𝜑𝑘𝑍) ∧ ((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)) → ((𝐹𝑘) − 𝑋) < ((𝐹𝑘) − (𝑋 / 2)))
101 simpr 484 . . . . . . 7 (((𝜑𝑘𝑍) ∧ ((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)) → ((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹))
10292, 95, 96, 100, 101ltletrd 11370 . . . . . 6 (((𝜑𝑘𝑍) ∧ ((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹)) → ((𝐹𝑘) − 𝑋) < (lim sup‘𝐹))
103102ex 412 . . . . 5 ((𝜑𝑘𝑍) → (((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹) → ((𝐹𝑘) − 𝑋) < (lim sup‘𝐹)))
10488, 22, 103syl2anc 583 . . . 4 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹) → ((𝐹𝑘) − 𝑋) < (lim sup‘𝐹)))
105104ralimdva 3159 . . 3 ((𝜑𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹) → ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) − 𝑋) < (lim sup‘𝐹)))
106105reximdva 3160 . 2 (𝜑 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)((𝐹𝑘) − (𝑋 / 2)) ≤ (lim sup‘𝐹) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)((𝐹𝑘) − 𝑋) < (lim sup‘𝐹)))
10787, 106mpd 15 1 (𝜑 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)((𝐹𝑘) − 𝑋) < (lim sup‘𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wcel 2098  wral 3053  wrex 3062  Vcvv 3466  wss 3940   class class class wbr 5138  cmpt 5221  ran crn 5667  cres 5668   Fn wfn 6528  wf 6529  cfv 6533  (class class class)co 7401  supcsup 9430  infcinf 9431  cr 11104   + caddc 11108  *cxr 11243   < clt 11244  cle 11245  cmin 11440   / cdiv 11867  2c2 12263  cz 12554  cuz 12818  +crp 12970   +𝑒 cxad 13086  lim supclsp 15410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182  ax-pre-sup 11183
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-er 8698  df-en 8935  df-dom 8936  df-sdom 8937  df-fin 8938  df-sup 9432  df-inf 9433  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-n0 12469  df-z 12555  df-uz 12819  df-rp 12971  df-xadd 13089  df-ico 13326  df-fz 13481  df-fzo 13624  df-fl 13753  df-ceil 13754  df-limsup 15411
This theorem is referenced by:  limsupgt  44945
  Copyright terms: Public domain W3C validator