Step | Hyp | Ref
| Expression |
1 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑙𝜑 |
2 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑙𝐹 |
3 | | limsupubuz.z |
. . . . . . . 8
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | | uzssre 39620 |
. . . . . . . 8
⊢
(ℤ≥‘𝑀) ⊆ ℝ |
5 | 3, 4 | eqsstri 3635 |
. . . . . . 7
⊢ 𝑍 ⊆
ℝ |
6 | 5 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑍 ⊆ ℝ) |
7 | | limsupubuz.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝑍⟶ℝ) |
8 | 7 | frexr 39604 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) |
9 | | limsupubuz.n |
. . . . . 6
⊢ (𝜑 → (lim sup‘𝐹) ≠
+∞) |
10 | 1, 2, 6, 8, 9 | limsupub 39936 |
. . . . 5
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑙 ∈ 𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦)) |
11 | 10 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → ∃𝑦 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑙 ∈ 𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦)) |
12 | | nfv 1843 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑙 𝑀 ∈ ℤ |
13 | 1, 12 | nfan 1828 |
. . . . . . . . . . 11
⊢
Ⅎ𝑙(𝜑 ∧ 𝑀 ∈ ℤ) |
14 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑙 𝑦 ∈ ℝ |
15 | 13, 14 | nfan 1828 |
. . . . . . . . . 10
⊢
Ⅎ𝑙((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑦 ∈ ℝ) |
16 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑙 𝑘 ∈ ℝ |
17 | 15, 16 | nfan 1828 |
. . . . . . . . 9
⊢
Ⅎ𝑙(((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℝ) |
18 | | nfra1 2941 |
. . . . . . . . 9
⊢
Ⅎ𝑙∀𝑙 ∈ 𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦) |
19 | 17, 18 | nfan 1828 |
. . . . . . . 8
⊢
Ⅎ𝑙((((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧ ∀𝑙 ∈ 𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦)) |
20 | | nfmpt1 4747 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑙(𝑙 ∈ (𝑀...if((⌈‘𝑘) ≤ 𝑀, 𝑀, (⌈‘𝑘))) ↦ (𝐹‘𝑙)) |
21 | 20 | nfrn 5368 |
. . . . . . . . . . 11
⊢
Ⅎ𝑙ran
(𝑙 ∈ (𝑀...if((⌈‘𝑘) ≤ 𝑀, 𝑀, (⌈‘𝑘))) ↦ (𝐹‘𝑙)) |
22 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑙ℝ |
23 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑙
< |
24 | 21, 22, 23 | nfsup 8357 |
. . . . . . . . . 10
⊢
Ⅎ𝑙sup(ran (𝑙 ∈ (𝑀...if((⌈‘𝑘) ≤ 𝑀, 𝑀, (⌈‘𝑘))) ↦ (𝐹‘𝑙)), ℝ, < ) |
25 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑙
≤ |
26 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑙𝑦 |
27 | 24, 25, 26 | nfbr 4699 |
. . . . . . . . 9
⊢
Ⅎ𝑙sup(ran
(𝑙 ∈ (𝑀...if((⌈‘𝑘) ≤ 𝑀, 𝑀, (⌈‘𝑘))) ↦ (𝐹‘𝑙)), ℝ, < ) ≤ 𝑦 |
28 | 27, 26, 24 | nfif 4115 |
. . . . . . . 8
⊢
Ⅎ𝑙if(sup(ran (𝑙 ∈ (𝑀...if((⌈‘𝑘) ≤ 𝑀, 𝑀, (⌈‘𝑘))) ↦ (𝐹‘𝑙)), ℝ, < ) ≤ 𝑦, 𝑦, sup(ran (𝑙 ∈ (𝑀...if((⌈‘𝑘) ≤ 𝑀, 𝑀, (⌈‘𝑘))) ↦ (𝐹‘𝑙)), ℝ, < )) |
29 | | breq2 4657 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑖 → (𝑘 ≤ 𝑙 ↔ 𝑘 ≤ 𝑖)) |
30 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = 𝑖 → (𝐹‘𝑙) = (𝐹‘𝑖)) |
31 | 30 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑖 → ((𝐹‘𝑙) ≤ 𝑦 ↔ (𝐹‘𝑖) ≤ 𝑦)) |
32 | 29, 31 | imbi12d 334 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑖 → ((𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦) ↔ (𝑘 ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑦))) |
33 | 32 | cbvralv 3171 |
. . . . . . . . . . 11
⊢
(∀𝑙 ∈
𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦) ↔ ∀𝑖 ∈ 𝑍 (𝑘 ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑦)) |
34 | 33 | biimpi 206 |
. . . . . . . . . 10
⊢
(∀𝑙 ∈
𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦) → ∀𝑖 ∈ 𝑍 (𝑘 ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑦)) |
35 | 34 | adantl 482 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧
∀𝑙 ∈ 𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦)) → ∀𝑖 ∈ 𝑍 (𝑘 ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑦)) |
36 | | simp-4r 807 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧
∀𝑖 ∈ 𝑍 (𝑘 ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑦)) → 𝑀 ∈ ℤ) |
37 | 35, 36 | syldan 487 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧
∀𝑙 ∈ 𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦)) → 𝑀 ∈ ℤ) |
38 | 7 | ad4antr 768 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧
∀𝑖 ∈ 𝑍 (𝑘 ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑦)) → 𝐹:𝑍⟶ℝ) |
39 | 35, 38 | syldan 487 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧
∀𝑙 ∈ 𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦)) → 𝐹:𝑍⟶ℝ) |
40 | | simpllr 799 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧
∀𝑖 ∈ 𝑍 (𝑘 ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑦)) → 𝑦 ∈ ℝ) |
41 | 35, 40 | syldan 487 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧
∀𝑙 ∈ 𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦)) → 𝑦 ∈ ℝ) |
42 | | simplr 792 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧
∀𝑖 ∈ 𝑍 (𝑘 ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑦)) → 𝑘 ∈ ℝ) |
43 | 35, 42 | syldan 487 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧
∀𝑙 ∈ 𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦)) → 𝑘 ∈ ℝ) |
44 | 33 | biimpri 218 |
. . . . . . . . 9
⊢
(∀𝑖 ∈
𝑍 (𝑘 ≤ 𝑖 → (𝐹‘𝑖) ≤ 𝑦) → ∀𝑙 ∈ 𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦)) |
45 | 35, 44 | syl 17 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧
∀𝑙 ∈ 𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦)) → ∀𝑙 ∈ 𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦)) |
46 | | eqid 2622 |
. . . . . . . 8
⊢
if((⌈‘𝑘)
≤ 𝑀, 𝑀, (⌈‘𝑘)) = if((⌈‘𝑘) ≤ 𝑀, 𝑀, (⌈‘𝑘)) |
47 | | eqid 2622 |
. . . . . . . 8
⊢ sup(ran
(𝑙 ∈ (𝑀...if((⌈‘𝑘) ≤ 𝑀, 𝑀, (⌈‘𝑘))) ↦ (𝐹‘𝑙)), ℝ, < ) = sup(ran (𝑙 ∈ (𝑀...if((⌈‘𝑘) ≤ 𝑀, 𝑀, (⌈‘𝑘))) ↦ (𝐹‘𝑙)), ℝ, < ) |
48 | | eqid 2622 |
. . . . . . . 8
⊢
if(sup(ran (𝑙 ∈
(𝑀...if((⌈‘𝑘) ≤ 𝑀, 𝑀, (⌈‘𝑘))) ↦ (𝐹‘𝑙)), ℝ, < ) ≤ 𝑦, 𝑦, sup(ran (𝑙 ∈ (𝑀...if((⌈‘𝑘) ≤ 𝑀, 𝑀, (⌈‘𝑘))) ↦ (𝐹‘𝑙)), ℝ, < )) = if(sup(ran (𝑙 ∈ (𝑀...if((⌈‘𝑘) ≤ 𝑀, 𝑀, (⌈‘𝑘))) ↦ (𝐹‘𝑙)), ℝ, < ) ≤ 𝑦, 𝑦, sup(ran (𝑙 ∈ (𝑀...if((⌈‘𝑘) ≤ 𝑀, 𝑀, (⌈‘𝑘))) ↦ (𝐹‘𝑙)), ℝ, < )) |
49 | 19, 28, 37, 3, 39, 41, 43, 45, 46, 47, 48 | limsupubuzlem 39944 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑦 ∈ ℝ) ∧ 𝑘 ∈ ℝ) ∧
∀𝑙 ∈ 𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦)) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ 𝑍 (𝐹‘𝑙) ≤ 𝑥) |
50 | 49 | exp31 630 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑦 ∈ ℝ) → (𝑘 ∈ ℝ → (∀𝑙 ∈ 𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ 𝑍 (𝐹‘𝑙) ≤ 𝑥))) |
51 | 50 | rexlimdv 3030 |
. . . . 5
⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑦 ∈ ℝ) → (∃𝑘 ∈ ℝ ∀𝑙 ∈ 𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ 𝑍 (𝐹‘𝑙) ≤ 𝑥)) |
52 | 51 | rexlimdva 3031 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → (∃𝑦 ∈ ℝ ∃𝑘 ∈ ℝ ∀𝑙 ∈ 𝑍 (𝑘 ≤ 𝑙 → (𝐹‘𝑙) ≤ 𝑦) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ 𝑍 (𝐹‘𝑙) ≤ 𝑥)) |
53 | 11, 52 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ 𝑍 (𝐹‘𝑙) ≤ 𝑥) |
54 | 3 | a1i 11 |
. . . . . 6
⊢ (¬
𝑀 ∈ ℤ →
𝑍 =
(ℤ≥‘𝑀)) |
55 | | uz0 39639 |
. . . . . 6
⊢ (¬
𝑀 ∈ ℤ →
(ℤ≥‘𝑀) = ∅) |
56 | 54, 55 | eqtrd 2656 |
. . . . 5
⊢ (¬
𝑀 ∈ ℤ →
𝑍 =
∅) |
57 | | 0red 10041 |
. . . . . 6
⊢ (𝑍 = ∅ → 0 ∈
ℝ) |
58 | | rzal 4073 |
. . . . . 6
⊢ (𝑍 = ∅ → ∀𝑙 ∈ 𝑍 (𝐹‘𝑙) ≤ 0) |
59 | | breq2 4657 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝐹‘𝑙) ≤ 𝑥 ↔ (𝐹‘𝑙) ≤ 0)) |
60 | 59 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑥 = 0 → (∀𝑙 ∈ 𝑍 (𝐹‘𝑙) ≤ 𝑥 ↔ ∀𝑙 ∈ 𝑍 (𝐹‘𝑙) ≤ 0)) |
61 | 60 | rspcev 3309 |
. . . . . 6
⊢ ((0
∈ ℝ ∧ ∀𝑙 ∈ 𝑍 (𝐹‘𝑙) ≤ 0) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ 𝑍 (𝐹‘𝑙) ≤ 𝑥) |
62 | 57, 58, 61 | syl2anc 693 |
. . . . 5
⊢ (𝑍 = ∅ → ∃𝑥 ∈ ℝ ∀𝑙 ∈ 𝑍 (𝐹‘𝑙) ≤ 𝑥) |
63 | 56, 62 | syl 17 |
. . . 4
⊢ (¬
𝑀 ∈ ℤ →
∃𝑥 ∈ ℝ
∀𝑙 ∈ 𝑍 (𝐹‘𝑙) ≤ 𝑥) |
64 | 63 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑀 ∈ ℤ) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ 𝑍 (𝐹‘𝑙) ≤ 𝑥) |
65 | 53, 64 | pm2.61dan 832 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑙 ∈ 𝑍 (𝐹‘𝑙) ≤ 𝑥) |
66 | | limsupubuz.j |
. . . . . 6
⊢
Ⅎ𝑗𝐹 |
67 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑗𝑙 |
68 | 66, 67 | nffv 6198 |
. . . . 5
⊢
Ⅎ𝑗(𝐹‘𝑙) |
69 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑗
≤ |
70 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑗𝑥 |
71 | 68, 69, 70 | nfbr 4699 |
. . . 4
⊢
Ⅎ𝑗(𝐹‘𝑙) ≤ 𝑥 |
72 | | nfv 1843 |
. . . 4
⊢
Ⅎ𝑙(𝐹‘𝑗) ≤ 𝑥 |
73 | | fveq2 6191 |
. . . . 5
⊢ (𝑙 = 𝑗 → (𝐹‘𝑙) = (𝐹‘𝑗)) |
74 | 73 | breq1d 4663 |
. . . 4
⊢ (𝑙 = 𝑗 → ((𝐹‘𝑙) ≤ 𝑥 ↔ (𝐹‘𝑗) ≤ 𝑥)) |
75 | 71, 72, 74 | cbvral 3167 |
. . 3
⊢
(∀𝑙 ∈
𝑍 (𝐹‘𝑙) ≤ 𝑥 ↔ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥) |
76 | 75 | rexbii 3041 |
. 2
⊢
(∃𝑥 ∈
ℝ ∀𝑙 ∈
𝑍 (𝐹‘𝑙) ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥) |
77 | 65, 76 | sylib 208 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥) |