Proof of Theorem limsupub
Step | Hyp | Ref
| Expression |
1 | | limsupub.e |
. . . . 5
⊢
Ⅎ𝑗𝐹 |
2 | | limsupub.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
3 | 2 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) → 𝐴 ⊆ ℝ) |
4 | | limsupub.f |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) |
5 | 4 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) → 𝐹:𝐴⟶ℝ*) |
6 | | limsupub.j |
. . . . . . . . . 10
⊢
Ⅎ𝑗𝜑 |
7 | | nfv 1922 |
. . . . . . . . . 10
⊢
Ⅎ𝑗 𝑥 ∈ ℝ |
8 | 6, 7 | nfan 1907 |
. . . . . . . . 9
⊢
Ⅎ𝑗(𝜑 ∧ 𝑥 ∈ ℝ) |
9 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) → 𝑘 ≤ 𝑗) |
10 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 < (𝐹‘𝑗)) → 𝑥 ∈ ℝ) |
11 | | rexr 10903 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 < (𝐹‘𝑗)) → 𝑥 ∈ ℝ*) |
13 | 4 | ffvelrnda 6922 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐹‘𝑗) ∈
ℝ*) |
14 | 13 | ad4ant13 751 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 < (𝐹‘𝑗)) → (𝐹‘𝑗) ∈
ℝ*) |
15 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 < (𝐹‘𝑗)) → 𝑥 < (𝐹‘𝑗)) |
16 | 12, 14, 15 | xrltled 12764 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ 𝑥 < (𝐹‘𝑗)) → 𝑥 ≤ (𝐹‘𝑗)) |
17 | 16 | adantrl 716 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) → 𝑥 ≤ (𝐹‘𝑗)) |
18 | 9, 17 | jca 515 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) ∧ (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) → (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) |
19 | 18 | ex 416 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) → ((𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)) → (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)))) |
20 | 19 | ex 416 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑗 ∈ 𝐴 → ((𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)) → (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))))) |
21 | 8, 20 | reximdai 3238 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)) → ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)))) |
22 | 21 | ralimdv 3102 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)) → ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)))) |
23 | 22 | ralimdva 3101 |
. . . . . 6
⊢ (𝜑 → (∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)) → ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗)))) |
24 | 23 | imp 410 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) → ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 ≤ (𝐹‘𝑗))) |
25 | 1, 3, 5, 24 | limsuppnfd 42946 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) → (lim sup‘𝐹) = +∞) |
26 | | limsupub.n |
. . . . . 6
⊢ (𝜑 → (lim sup‘𝐹) ≠
+∞) |
27 | 26 | neneqd 2946 |
. . . . 5
⊢ (𝜑 → ¬ (lim sup‘𝐹) = +∞) |
28 | 27 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) → ¬ (lim sup‘𝐹) = +∞) |
29 | 25, 28 | pm2.65da 817 |
. . 3
⊢ (𝜑 → ¬ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) |
30 | | imnan 403 |
. . . . . . . . 9
⊢ ((𝑘 ≤ 𝑗 → ¬ 𝑥 < (𝐹‘𝑗)) ↔ ¬ (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) |
31 | 30 | ralbii 3089 |
. . . . . . . 8
⊢
(∀𝑗 ∈
𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 < (𝐹‘𝑗)) ↔ ∀𝑗 ∈ 𝐴 ¬ (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) |
32 | | ralnex 3162 |
. . . . . . . 8
⊢
(∀𝑗 ∈
𝐴 ¬ (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)) ↔ ¬ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) |
33 | 31, 32 | bitri 278 |
. . . . . . 7
⊢
(∀𝑗 ∈
𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 < (𝐹‘𝑗)) ↔ ¬ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) |
34 | 33 | rexbii 3176 |
. . . . . 6
⊢
(∃𝑘 ∈
ℝ ∀𝑗 ∈
𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 < (𝐹‘𝑗)) ↔ ∃𝑘 ∈ ℝ ¬ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) |
35 | | rexnal 3164 |
. . . . . 6
⊢
(∃𝑘 ∈
ℝ ¬ ∃𝑗
∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)) ↔ ¬ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) |
36 | 34, 35 | bitri 278 |
. . . . 5
⊢
(∃𝑘 ∈
ℝ ∀𝑗 ∈
𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 < (𝐹‘𝑗)) ↔ ¬ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) |
37 | 36 | rexbii 3176 |
. . . 4
⊢
(∃𝑥 ∈
ℝ ∃𝑘 ∈
ℝ ∀𝑗 ∈
𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 < (𝐹‘𝑗)) ↔ ∃𝑥 ∈ ℝ ¬ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) |
38 | | rexnal 3164 |
. . . 4
⊢
(∃𝑥 ∈
ℝ ¬ ∀𝑘
∈ ℝ ∃𝑗
∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗)) ↔ ¬ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) |
39 | 37, 38 | bitri 278 |
. . 3
⊢
(∃𝑥 ∈
ℝ ∃𝑘 ∈
ℝ ∀𝑗 ∈
𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 < (𝐹‘𝑗)) ↔ ¬ ∀𝑥 ∈ ℝ ∀𝑘 ∈ ℝ ∃𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 ∧ 𝑥 < (𝐹‘𝑗))) |
40 | 29, 39 | sylibr 237 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 < (𝐹‘𝑗))) |
41 | | nfv 1922 |
. . . . . 6
⊢
Ⅎ𝑗 𝑘 ∈ ℝ |
42 | 8, 41 | nfan 1907 |
. . . . 5
⊢
Ⅎ𝑗((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) |
43 | 13 | ad4ant14 752 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) → (𝐹‘𝑗) ∈
ℝ*) |
44 | | simpllr 776 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) → 𝑥 ∈ ℝ) |
45 | 44 | rexrd 10907 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) → 𝑥 ∈ ℝ*) |
46 | 43, 45 | xrlenltd 10923 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) → ((𝐹‘𝑗) ≤ 𝑥 ↔ ¬ 𝑥 < (𝐹‘𝑗))) |
47 | 46 | imbi2d 344 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ 𝑗 ∈ 𝐴) → ((𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥) ↔ (𝑘 ≤ 𝑗 → ¬ 𝑥 < (𝐹‘𝑗)))) |
48 | 42, 47 | ralbida 3155 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ∈ ℝ) → (∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥) ↔ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 < (𝐹‘𝑗)))) |
49 | 48 | rexbidva 3223 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥) ↔ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 < (𝐹‘𝑗)))) |
50 | 49 | rexbidva 3223 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥) ↔ ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → ¬ 𝑥 < (𝐹‘𝑗)))) |
51 | 40, 50 | mpbird 260 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑗 ∈ 𝐴 (𝑘 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑥)) |