Step | Hyp | Ref
| Expression |
1 | | limsupbnd2.5 |
. . 3
⊢ (𝜑 → ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗))) |
2 | | limsupbnd2.4 |
. . . . . . . . 9
⊢ (𝜑 → sup(𝐵, ℝ*, < ) =
+∞) |
3 | | limsupbnd.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
4 | | ressxr 9962 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℝ* |
5 | 3, 4 | syl6ss 3580 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ⊆
ℝ*) |
6 | | supxrunb1 12021 |
. . . . . . . . . 10
⊢ (𝐵 ⊆ ℝ*
→ (∀𝑛 ∈
ℝ ∃𝑗 ∈
𝐵 𝑛 ≤ 𝑗 ↔ sup(𝐵, ℝ*, < ) =
+∞)) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑛 ∈ ℝ ∃𝑗 ∈ 𝐵 𝑛 ≤ 𝑗 ↔ sup(𝐵, ℝ*, < ) =
+∞)) |
8 | 2, 7 | mpbird 246 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑛 ∈ ℝ ∃𝑗 ∈ 𝐵 𝑛 ≤ 𝑗) |
9 | | ifcl 4080 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ) → if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ∈ ℝ) |
10 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑛 = if(𝑘 ≤ 𝑚, 𝑚, 𝑘) → (𝑛 ≤ 𝑗 ↔ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗)) |
11 | 10 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑛 = if(𝑘 ≤ 𝑚, 𝑚, 𝑘) → (∃𝑗 ∈ 𝐵 𝑛 ≤ 𝑗 ↔ ∃𝑗 ∈ 𝐵 if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗)) |
12 | 11 | rspccva 3281 |
. . . . . . . 8
⊢
((∀𝑛 ∈
ℝ ∃𝑗 ∈
𝐵 𝑛 ≤ 𝑗 ∧ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ∈ ℝ) → ∃𝑗 ∈ 𝐵 if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗) |
13 | 8, 9, 12 | syl2an 493 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) → ∃𝑗 ∈ 𝐵 if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗) |
14 | | r19.29 3054 |
. . . . . . . 8
⊢
((∀𝑗 ∈
𝐵 (𝑘 ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗)) ∧ ∃𝑗 ∈ 𝐵 if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗) → ∃𝑗 ∈ 𝐵 ((𝑘 ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗)) ∧ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗)) |
15 | | simplrr 797 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → 𝑘 ∈ ℝ) |
16 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) → 𝑚 ∈ ℝ) |
17 | 16 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → 𝑚 ∈ ℝ) |
18 | | max1 11890 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑘 ≤ if(𝑘 ≤ 𝑚, 𝑚, 𝑘)) |
19 | 15, 17, 18 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → 𝑘 ≤ if(𝑘 ≤ 𝑚, 𝑚, 𝑘)) |
20 | 17, 15, 9 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ∈ ℝ) |
21 | 3 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) → 𝐵 ⊆ ℝ) |
22 | 21 | sselda 3568 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → 𝑗 ∈ ℝ) |
23 | | letr 10010 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℝ ∧ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ∈ ℝ ∧ 𝑗 ∈ ℝ) → ((𝑘 ≤ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ∧ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗) → 𝑘 ≤ 𝑗)) |
24 | 15, 20, 22, 23 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → ((𝑘 ≤ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ∧ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗) → 𝑘 ≤ 𝑗)) |
25 | 19, 24 | mpand 707 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → (if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗 → 𝑘 ≤ 𝑗)) |
26 | 25 | imim1d 80 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → ((𝑘 ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗)) → (if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗)))) |
27 | 26 | impd 446 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → (((𝑘 ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗)) ∧ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗) → 𝐴 ≤ (𝐹‘𝑗))) |
28 | | max2 11892 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℝ ∧ 𝑚 ∈ ℝ) → 𝑚 ≤ if(𝑘 ≤ 𝑚, 𝑚, 𝑘)) |
29 | 15, 17, 28 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → 𝑚 ≤ if(𝑘 ≤ 𝑚, 𝑚, 𝑘)) |
30 | | letr 10010 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℝ ∧ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ∈ ℝ ∧ 𝑗 ∈ ℝ) → ((𝑚 ≤ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ∧ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗) → 𝑚 ≤ 𝑗)) |
31 | 17, 20, 22, 30 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → ((𝑚 ≤ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ∧ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗) → 𝑚 ≤ 𝑗)) |
32 | 29, 31 | mpand 707 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → (if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗 → 𝑚 ≤ 𝑗)) |
33 | 32 | adantld 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → (((𝑘 ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗)) ∧ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗) → 𝑚 ≤ 𝑗)) |
34 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℝ ↦
sup(((𝐹 “ (𝑛[,)+∞)) ∩
ℝ*), ℝ*, < )) = (𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
35 | 34 | limsupgf 14054 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℝ ↦
sup(((𝐹 “ (𝑛[,)+∞)) ∩
ℝ*), ℝ*, <
)):ℝ⟶ℝ* |
36 | 35 | ffvelrni 6266 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℝ → ((𝑛 ∈ ℝ ↦
sup(((𝐹 “ (𝑛[,)+∞)) ∩
ℝ*), ℝ*, < ))‘𝑚) ∈
ℝ*) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚) ∈
ℝ*) |
38 | | xrleid 11859 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ ℝ ↦
sup(((𝐹 “ (𝑛[,)+∞)) ∩
ℝ*), ℝ*, < ))‘𝑚) ∈ ℝ* → ((𝑛 ∈ ℝ ↦
sup(((𝐹 “ (𝑛[,)+∞)) ∩
ℝ*), ℝ*, < ))‘𝑚) ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚) ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚)) |
40 | 39 | adantrr 749 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) → ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚) ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚)) |
41 | | limsupbnd.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝐵⟶ℝ*) |
42 | 41 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) → 𝐹:𝐵⟶ℝ*) |
43 | 16, 36 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) → ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚) ∈
ℝ*) |
44 | 34 | limsupgle 14056 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝑚 ∈ ℝ ∧ ((𝑛 ∈ ℝ ↦
sup(((𝐹 “ (𝑛[,)+∞)) ∩
ℝ*), ℝ*, < ))‘𝑚) ∈ ℝ*) → (((𝑛 ∈ ℝ ↦
sup(((𝐹 “ (𝑛[,)+∞)) ∩
ℝ*), ℝ*, < ))‘𝑚) ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚) ↔ ∀𝑗 ∈ 𝐵 (𝑚 ≤ 𝑗 → (𝐹‘𝑗) ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚)))) |
45 | 21, 42, 16, 43, 44 | syl211anc 1324 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) → (((𝑛 ∈ ℝ ↦
sup(((𝐹 “ (𝑛[,)+∞)) ∩
ℝ*), ℝ*, < ))‘𝑚) ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚) ↔ ∀𝑗 ∈ 𝐵 (𝑚 ≤ 𝑗 → (𝐹‘𝑗) ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚)))) |
46 | 40, 45 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) → ∀𝑗 ∈ 𝐵 (𝑚 ≤ 𝑗 → (𝐹‘𝑗) ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚))) |
47 | 46 | r19.21bi 2916 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → (𝑚 ≤ 𝑗 → (𝐹‘𝑗) ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚))) |
48 | 33, 47 | syld 46 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → (((𝑘 ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗)) ∧ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗) → (𝐹‘𝑗) ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚))) |
49 | 27, 48 | jcad 554 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → (((𝑘 ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗)) ∧ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗) → (𝐴 ≤ (𝐹‘𝑗) ∧ (𝐹‘𝑗) ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚)))) |
50 | | limsupbnd.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
51 | 50 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → 𝐴 ∈
ℝ*) |
52 | 42 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → (𝐹‘𝑗) ∈
ℝ*) |
53 | 43 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚) ∈
ℝ*) |
54 | | xrletr 11865 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ (𝐹‘𝑗) ∈ ℝ*
∧ ((𝑛 ∈ ℝ
↦ sup(((𝐹 “
(𝑛[,)+∞)) ∩
ℝ*), ℝ*, < ))‘𝑚) ∈ ℝ*) → ((𝐴 ≤ (𝐹‘𝑗) ∧ (𝐹‘𝑗) ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚)) → 𝐴 ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚))) |
55 | 51, 52, 53, 54 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → ((𝐴 ≤ (𝐹‘𝑗) ∧ (𝐹‘𝑗) ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚)) → 𝐴 ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚))) |
56 | 49, 55 | syld 46 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) ∧ 𝑗 ∈ 𝐵) → (((𝑘 ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗)) ∧ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗) → 𝐴 ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚))) |
57 | 56 | rexlimdva 3013 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) → (∃𝑗 ∈ 𝐵 ((𝑘 ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗)) ∧ if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗) → 𝐴 ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚))) |
58 | 14, 57 | syl5 33 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) → ((∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗)) ∧ ∃𝑗 ∈ 𝐵 if(𝑘 ≤ 𝑚, 𝑚, 𝑘) ≤ 𝑗) → 𝐴 ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚))) |
59 | 13, 58 | mpan2d 706 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ ℝ ∧ 𝑘 ∈ ℝ)) → (∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗)) → 𝐴 ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚))) |
60 | 59 | anassrs 678 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ) ∧ 𝑘 ∈ ℝ) → (∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗)) → 𝐴 ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚))) |
61 | 60 | rexlimdva 3013 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ) → (∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗)) → 𝐴 ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚))) |
62 | 61 | ralrimdva 2952 |
. . 3
⊢ (𝜑 → (∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐵 (𝑘 ≤ 𝑗 → 𝐴 ≤ (𝐹‘𝑗)) → ∀𝑚 ∈ ℝ 𝐴 ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚))) |
63 | 1, 62 | mpd 15 |
. 2
⊢ (𝜑 → ∀𝑚 ∈ ℝ 𝐴 ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚)) |
64 | 34 | limsuple 14057 |
. . 3
⊢ ((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ* ∧ 𝐴 ∈ ℝ*)
→ (𝐴 ≤ (lim
sup‘𝐹) ↔
∀𝑚 ∈ ℝ
𝐴 ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚))) |
65 | 3, 41, 50, 64 | syl3anc 1318 |
. 2
⊢ (𝜑 → (𝐴 ≤ (lim sup‘𝐹) ↔ ∀𝑚 ∈ ℝ 𝐴 ≤ ((𝑛 ∈ ℝ ↦ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < ))‘𝑚))) |
66 | 63, 65 | mpbird 246 |
1
⊢ (𝜑 → 𝐴 ≤ (lim sup‘𝐹)) |