| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | limsupbnd1.4 | . 2
⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴)) | 
| 2 |  | limsupbnd.1 | . . . . . 6
⊢ (𝜑 → 𝐵 ⊆ ℝ) | 
| 3 | 2 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → 𝐵 ⊆ ℝ) | 
| 4 |  | limsupbnd.2 | . . . . . 6
⊢ (𝜑 → 𝐹:𝐵⟶ℝ*) | 
| 5 | 4 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → 𝐹:𝐵⟶ℝ*) | 
| 6 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → 𝑘 ∈ ℝ) | 
| 7 |  | limsupbnd.3 | . . . . . 6
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 8 | 7 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → 𝐴 ∈
ℝ*) | 
| 9 |  | eqid 2736 | . . . . . 6
⊢ (𝑛 ∈ ℝ ↦
sup(((𝐹 “ (𝑛[,)+∞)) ∩
ℝ*), ℝ*, < )) = (𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < )) | 
| 10 | 9 | limsupgle 15514 | . . . . 5
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝑘 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (((𝑛 ∈ ℝ
↦ sup(((𝐹 “
(𝑛[,)+∞)) ∩
ℝ*), ℝ*, < ))‘𝑘) ≤ 𝐴 ↔ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴))) | 
| 11 | 3, 5, 6, 8, 10 | syl211anc 1377 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑘) ≤ 𝐴 ↔ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴))) | 
| 12 |  | reex 11247 | . . . . . . . . . . . 12
⊢ ℝ
∈ V | 
| 13 | 12 | ssex 5320 | . . . . . . . . . . 11
⊢ (𝐵 ⊆ ℝ → 𝐵 ∈ V) | 
| 14 | 2, 13 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ V) | 
| 15 |  | xrex 13030 | . . . . . . . . . . 11
⊢
ℝ* ∈ V | 
| 16 | 15 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → ℝ* ∈
V) | 
| 17 |  | fex2 7959 | . . . . . . . . . 10
⊢ ((𝐹:𝐵⟶ℝ* ∧ 𝐵 ∈ V ∧
ℝ* ∈ V) → 𝐹 ∈ V) | 
| 18 | 4, 14, 16, 17 | syl3anc 1372 | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ V) | 
| 19 |  | limsupcl 15510 | . . . . . . . . 9
⊢ (𝐹 ∈ V → (lim
sup‘𝐹) ∈
ℝ*) | 
| 20 | 18, 19 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (lim sup‘𝐹) ∈
ℝ*) | 
| 21 | 20 | xrleidd 13195 | . . . . . . 7
⊢ (𝜑 → (lim sup‘𝐹) ≤ (lim sup‘𝐹)) | 
| 22 | 9 | limsuple 15515 | . . . . . . . 8
⊢ ((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ* ∧ (lim
sup‘𝐹) ∈
ℝ*) → ((lim sup‘𝐹) ≤ (lim sup‘𝐹) ↔ ∀𝑘 ∈ ℝ (lim sup‘𝐹) ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑘))) | 
| 23 | 2, 4, 20, 22 | syl3anc 1372 | . . . . . . 7
⊢ (𝜑 → ((lim sup‘𝐹) ≤ (lim sup‘𝐹) ↔ ∀𝑘 ∈ ℝ (lim
sup‘𝐹) ≤ ((𝑛 ∈ ℝ ↦
sup(((𝐹 “ (𝑛[,)+∞)) ∩
ℝ*), ℝ*, < ))‘𝑘))) | 
| 24 | 21, 23 | mpbid 232 | . . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ ℝ (lim sup‘𝐹) ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑘)) | 
| 25 | 24 | r19.21bi 3250 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (lim sup‘𝐹) ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑘)) | 
| 26 | 20 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (lim sup‘𝐹) ∈
ℝ*) | 
| 27 | 9 | limsupgf 15512 | . . . . . . . 8
⊢ (𝑛 ∈ ℝ ↦
sup(((𝐹 “ (𝑛[,)+∞)) ∩
ℝ*), ℝ*, <
)):ℝ⟶ℝ* | 
| 28 | 27 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, <
)):ℝ⟶ℝ*) | 
| 29 | 28 | ffvelcdmda 7103 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑘) ∈
ℝ*) | 
| 30 |  | xrletr 13201 | . . . . . 6
⊢ (((lim
sup‘𝐹) ∈
ℝ* ∧ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑘) ∈ ℝ* ∧ 𝐴 ∈ ℝ*)
→ (((lim sup‘𝐹)
≤ ((𝑛 ∈ ℝ
↦ sup(((𝐹 “
(𝑛[,)+∞)) ∩
ℝ*), ℝ*, < ))‘𝑘) ∧ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑘) ≤ 𝐴) → (lim sup‘𝐹) ≤ 𝐴)) | 
| 31 | 26, 29, 8, 30 | syl3anc 1372 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (((lim
sup‘𝐹) ≤ ((𝑛 ∈ ℝ ↦
sup(((𝐹 “ (𝑛[,)+∞)) ∩
ℝ*), ℝ*, < ))‘𝑘) ∧ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑘) ≤ 𝐴) → (lim sup‘𝐹) ≤ 𝐴)) | 
| 32 | 25, 31 | mpand 695 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑘) ≤ 𝐴 → (lim sup‘𝐹) ≤ 𝐴)) | 
| 33 | 11, 32 | sylbird 260 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ) → (∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴) → (lim sup‘𝐹) ≤ 𝐴)) | 
| 34 | 33 | rexlimdva 3154 | . 2
⊢ (𝜑 → (∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴) → (lim sup‘𝐹) ≤ 𝐴)) | 
| 35 | 1, 34 | mpd 15 | 1
⊢ (𝜑 → (lim sup‘𝐹) ≤ 𝐴) |