| Step | Hyp | Ref
| Expression |
| 1 | | limsupubuzlem.x |
. . 3
⊢ 𝑋 = if(𝑊 ≤ 𝑌, 𝑌, 𝑊) |
| 2 | | limsupubuzlem.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ ℝ) |
| 3 | | limsupubuzlem.w |
. . . . . 6
⊢ 𝑊 = sup(ran (𝑗 ∈ (𝑀...𝑁) ↦ (𝐹‘𝑗)), ℝ, < ) |
| 4 | 3 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑊 = sup(ran (𝑗 ∈ (𝑀...𝑁) ↦ (𝐹‘𝑗)), ℝ, < )) |
| 5 | | limsupubuzlem.j |
. . . . . 6
⊢
Ⅎ𝑗𝜑 |
| 6 | | ltso 11341 |
. . . . . . 7
⊢ < Or
ℝ |
| 7 | 6 | a1i 11 |
. . . . . 6
⊢ (𝜑 → < Or
ℝ) |
| 8 | | fzfid 14014 |
. . . . . 6
⊢ (𝜑 → (𝑀...𝑁) ∈ Fin) |
| 9 | | eqid 2737 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
| 10 | | limsupubuzlem.m |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 11 | | limsupubuzlem.n |
. . . . . . . . . . 11
⊢ 𝑁 = if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾)) |
| 12 | 11 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 = if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾))) |
| 13 | | limsupubuzlem.k |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ ℝ) |
| 14 | | ceilcl 13882 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℝ →
(⌈‘𝐾) ∈
ℤ) |
| 15 | 13, 14 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌈‘𝐾) ∈
ℤ) |
| 16 | 10, 15 | ifcld 4572 |
. . . . . . . . . 10
⊢ (𝜑 → if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾)) ∈ ℤ) |
| 17 | 12, 16 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 18 | 15 | zred 12722 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌈‘𝐾) ∈
ℝ) |
| 19 | 10 | zred 12722 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 20 | | max2 13229 |
. . . . . . . . . . 11
⊢
(((⌈‘𝐾)
∈ ℝ ∧ 𝑀
∈ ℝ) → 𝑀
≤ if((⌈‘𝐾)
≤ 𝑀, 𝑀, (⌈‘𝐾))) |
| 21 | 18, 19, 20 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ≤ if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾))) |
| 22 | 12 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (𝜑 → if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾)) = 𝑁) |
| 23 | 21, 22 | breqtrd 5169 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
| 24 | 9, 10, 17, 23 | eluzd 45420 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
| 25 | | eluzfz2 13572 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
| 26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
| 27 | 26 | ne0d 4342 |
. . . . . 6
⊢ (𝜑 → (𝑀...𝑁) ≠ ∅) |
| 28 | | limsupubuzlem.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝑍⟶ℝ) |
| 29 | 28 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐹:𝑍⟶ℝ) |
| 30 | 10 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℤ) |
| 31 | | elfzelz 13564 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (𝑀...𝑁) → 𝑗 ∈ ℤ) |
| 32 | 31 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝑗 ∈ ℤ) |
| 33 | | elfzle1 13567 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝑗) |
| 34 | 33 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝑀 ≤ 𝑗) |
| 35 | 9, 30, 32, 34 | eluzd 45420 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝑗 ∈ (ℤ≥‘𝑀)) |
| 36 | | limsupubuzlem.z |
. . . . . . . 8
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 37 | 35, 36 | eleqtrrdi 2852 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝑗 ∈ 𝑍) |
| 38 | 29, 37 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ∈ ℝ) |
| 39 | 5, 7, 8, 27, 38 | fisupclrnmpt 45409 |
. . . . 5
⊢ (𝜑 → sup(ran (𝑗 ∈ (𝑀...𝑁) ↦ (𝐹‘𝑗)), ℝ, < ) ∈
ℝ) |
| 40 | 4, 39 | eqeltrd 2841 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ ℝ) |
| 41 | 2, 40 | ifcld 4572 |
. . 3
⊢ (𝜑 → if(𝑊 ≤ 𝑌, 𝑌, 𝑊) ∈ ℝ) |
| 42 | 1, 41 | eqeltrid 2845 |
. 2
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 43 | 28 | ffvelcdmda 7104 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) ∈ ℝ) |
| 44 | 43 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → (𝐹‘𝑗) ∈ ℝ) |
| 45 | 40 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑊 ∈ ℝ) |
| 46 | 42 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑋 ∈ ℝ) |
| 47 | | simpll 767 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝜑) |
| 48 | 10 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑀 ∈ ℤ) |
| 49 | 17 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑁 ∈ ℤ) |
| 50 | 36 | eluzelz2 45414 |
. . . . . . . . 9
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ) |
| 51 | 50 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑗 ∈ ℤ) |
| 52 | 36 | eleq2i 2833 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ 𝑍 ↔ 𝑗 ∈ (ℤ≥‘𝑀)) |
| 53 | 52 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ (ℤ≥‘𝑀)) |
| 54 | | eluzle 12891 |
. . . . . . . . . 10
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑗) |
| 55 | 53, 54 | syl 17 |
. . . . . . . . 9
⊢ (𝑗 ∈ 𝑍 → 𝑀 ≤ 𝑗) |
| 56 | 55 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑀 ≤ 𝑗) |
| 57 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑗 ≤ 𝑁) |
| 58 | 48, 49, 51, 56, 57 | elfzd 13555 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑗 ∈ (𝑀...𝑁)) |
| 59 | 5, 8, 38 | fimaxre4 45412 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑗 ∈ (𝑀...𝑁)(𝐹‘𝑗) ≤ 𝑏) |
| 60 | 5, 38, 59 | suprubrnmpt 45260 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ≤ sup(ran (𝑗 ∈ (𝑀...𝑁) ↦ (𝐹‘𝑗)), ℝ, < )) |
| 61 | 60, 3 | breqtrrdi 5185 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ≤ 𝑊) |
| 62 | 47, 58, 61 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → (𝐹‘𝑗) ≤ 𝑊) |
| 63 | | max1 13227 |
. . . . . . . . 9
⊢ ((𝑊 ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑊 ≤ if(𝑊 ≤ 𝑌, 𝑌, 𝑊)) |
| 64 | 40, 2, 63 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ≤ if(𝑊 ≤ 𝑌, 𝑌, 𝑊)) |
| 65 | 64, 1 | breqtrrdi 5185 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ≤ 𝑋) |
| 66 | 65 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑊 ≤ 𝑋) |
| 67 | 44, 45, 46, 62, 66 | letrd 11418 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → (𝐹‘𝑗) ≤ 𝑋) |
| 68 | 13 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝐾 ∈ ℝ) |
| 69 | | uzssre 12900 |
. . . . . . . . . 10
⊢
(ℤ≥‘𝑀) ⊆ ℝ |
| 70 | 36, 69 | eqsstri 4030 |
. . . . . . . . 9
⊢ 𝑍 ⊆
ℝ |
| 71 | 70 | sseli 3979 |
. . . . . . . 8
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℝ) |
| 72 | 71 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝑗 ∈ ℝ) |
| 73 | 69, 24 | sselid 3981 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 74 | 73 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝑁 ∈ ℝ) |
| 75 | | ceilge 13885 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℝ → 𝐾 ≤ (⌈‘𝐾)) |
| 76 | 13, 75 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ≤ (⌈‘𝐾)) |
| 77 | | max1 13227 |
. . . . . . . . . . . 12
⊢
(((⌈‘𝐾)
∈ ℝ ∧ 𝑀
∈ ℝ) → (⌈‘𝐾) ≤ if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾))) |
| 78 | 18, 19, 77 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌈‘𝐾) ≤ if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾))) |
| 79 | 78, 22 | breqtrd 5169 |
. . . . . . . . . 10
⊢ (𝜑 → (⌈‘𝐾) ≤ 𝑁) |
| 80 | 13, 18, 73, 76, 79 | letrd 11418 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ≤ 𝑁) |
| 81 | 80 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝐾 ≤ 𝑁) |
| 82 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → ¬ 𝑗 ≤ 𝑁) |
| 83 | 74, 72 | ltnled 11408 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → (𝑁 < 𝑗 ↔ ¬ 𝑗 ≤ 𝑁)) |
| 84 | 82, 83 | mpbird 257 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝑁 < 𝑗) |
| 85 | 68, 74, 72, 81, 84 | lelttrd 11419 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝐾 < 𝑗) |
| 86 | 68, 72, 85 | ltled 11409 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝐾 ≤ 𝑗) |
| 87 | 43 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → (𝐹‘𝑗) ∈ ℝ) |
| 88 | 2 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝑌 ∈ ℝ) |
| 89 | 42 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝑋 ∈ ℝ) |
| 90 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝐾 ≤ 𝑗) |
| 91 | | limsupubuzlem.b |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑗 ∈ 𝑍 (𝐾 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑌)) |
| 92 | 91 | r19.21bi 3251 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐾 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑌)) |
| 93 | 92 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → (𝐾 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑌)) |
| 94 | 90, 93 | mpd 15 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → (𝐹‘𝑗) ≤ 𝑌) |
| 95 | | max2 13229 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑌 ≤ if(𝑊 ≤ 𝑌, 𝑌, 𝑊)) |
| 96 | 40, 2, 95 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ≤ if(𝑊 ≤ 𝑌, 𝑌, 𝑊)) |
| 97 | 96, 1 | breqtrrdi 5185 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ≤ 𝑋) |
| 98 | 97 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝑌 ≤ 𝑋) |
| 99 | 87, 88, 89, 94, 98 | letrd 11418 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → (𝐹‘𝑗) ≤ 𝑋) |
| 100 | 86, 99 | syldan 591 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → (𝐹‘𝑗) ≤ 𝑋) |
| 101 | 67, 100 | pm2.61dan 813 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) ≤ 𝑋) |
| 102 | 101 | ex 412 |
. . 3
⊢ (𝜑 → (𝑗 ∈ 𝑍 → (𝐹‘𝑗) ≤ 𝑋)) |
| 103 | 5, 102 | ralrimi 3257 |
. 2
⊢ (𝜑 → ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑋) |
| 104 | | nfv 1914 |
. . 3
⊢
Ⅎ𝑥∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑋 |
| 105 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑗𝑥 |
| 106 | | limsupubuzlem.e |
. . . . 5
⊢
Ⅎ𝑗𝑋 |
| 107 | 105, 106 | nfeq 2919 |
. . . 4
⊢
Ⅎ𝑗 𝑥 = 𝑋 |
| 108 | | breq2 5147 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝐹‘𝑗) ≤ 𝑥 ↔ (𝐹‘𝑗) ≤ 𝑋)) |
| 109 | 107, 108 | ralbid 3273 |
. . 3
⊢ (𝑥 = 𝑋 → (∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥 ↔ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑋)) |
| 110 | 104, 109 | rspce 3611 |
. 2
⊢ ((𝑋 ∈ ℝ ∧
∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑋) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥) |
| 111 | 42, 103, 110 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥) |