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 10799 |
. . . . . . 7
⊢ < Or
ℝ |
7 | 6 | a1i 11 |
. . . . . 6
⊢ (𝜑 → < Or
ℝ) |
8 | | fzfid 13432 |
. . . . . 6
⊢ (𝜑 → (𝑀...𝑁) ∈ Fin) |
9 | | eqid 2738 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
10 | | limsupubuzlem.m |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
11 | | limsupubuzlem.n |
. . . . . . . . . . 11
⊢ 𝑁 = if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾)) |
12 | 11 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 = if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾))) |
13 | | limsupubuzlem.k |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ ℝ) |
14 | | ceilcl 13303 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℝ →
(⌈‘𝐾) ∈
ℤ) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌈‘𝐾) ∈
ℤ) |
16 | 10, 15 | ifcld 4460 |
. . . . . . . . . 10
⊢ (𝜑 → if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾)) ∈ ℤ) |
17 | 12, 16 | eqeltrd 2833 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℤ) |
18 | 15 | zred 12168 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌈‘𝐾) ∈
ℝ) |
19 | 10 | zred 12168 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
20 | | max2 12663 |
. . . . . . . . . . 11
⊢
(((⌈‘𝐾)
∈ ℝ ∧ 𝑀
∈ ℝ) → 𝑀
≤ if((⌈‘𝐾)
≤ 𝑀, 𝑀, (⌈‘𝐾))) |
21 | 18, 19, 20 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ≤ if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾))) |
22 | 12 | eqcomd 2744 |
. . . . . . . . . 10
⊢ (𝜑 → if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾)) = 𝑁) |
23 | 21, 22 | breqtrd 5056 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
24 | 9, 10, 17, 23 | eluzd 42487 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
25 | | eluzfz2 13006 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
27 | 26 | ne0d 4224 |
. . . . . 6
⊢ (𝜑 → (𝑀...𝑁) ≠ ∅) |
28 | | limsupubuzlem.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝑍⟶ℝ) |
29 | 28 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐹:𝑍⟶ℝ) |
30 | 10 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℤ) |
31 | | elfzelz 12998 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (𝑀...𝑁) → 𝑗 ∈ ℤ) |
32 | 31 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝑗 ∈ ℤ) |
33 | | elfzle1 13001 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝑗) |
34 | 33 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝑀 ≤ 𝑗) |
35 | 9, 30, 32, 34 | eluzd 42487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝑗 ∈ (ℤ≥‘𝑀)) |
36 | | limsupubuzlem.z |
. . . . . . . 8
⊢ 𝑍 =
(ℤ≥‘𝑀) |
37 | 35, 36 | eleqtrrdi 2844 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝑗 ∈ 𝑍) |
38 | 29, 37 | ffvelrnd 6862 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ∈ ℝ) |
39 | 5, 7, 8, 27, 38 | fisupclrnmpt 42476 |
. . . . 5
⊢ (𝜑 → sup(ran (𝑗 ∈ (𝑀...𝑁) ↦ (𝐹‘𝑗)), ℝ, < ) ∈
ℝ) |
40 | 4, 39 | eqeltrd 2833 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ ℝ) |
41 | 2, 40 | ifcld 4460 |
. . 3
⊢ (𝜑 → if(𝑊 ≤ 𝑌, 𝑌, 𝑊) ∈ ℝ) |
42 | 1, 41 | eqeltrid 2837 |
. 2
⊢ (𝜑 → 𝑋 ∈ ℝ) |
43 | 28 | ffvelrnda 6861 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) ∈ ℝ) |
44 | 43 | adantr 484 |
. . . . . 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 42481 |
. . . . . . . . 9
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ) |
51 | 50 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑗 ∈ ℤ) |
52 | 36 | eleq2i 2824 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ 𝑍 ↔ 𝑗 ∈ (ℤ≥‘𝑀)) |
53 | 52 | biimpi 219 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ (ℤ≥‘𝑀)) |
54 | | eluzle 12337 |
. . . . . . . . . 10
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑗) |
55 | 53, 54 | syl 17 |
. . . . . . . . 9
⊢ (𝑗 ∈ 𝑍 → 𝑀 ≤ 𝑗) |
56 | 55 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑀 ≤ 𝑗) |
57 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑗 ≤ 𝑁) |
58 | 48, 49, 51, 56, 57 | elfzd 12989 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑗 ∈ (𝑀...𝑁)) |
59 | 5, 8, 38 | fimaxre4 42479 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑗 ∈ (𝑀...𝑁)(𝐹‘𝑗) ≤ 𝑏) |
60 | 5, 38, 59 | suprubrnmpt 42336 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ≤ sup(ran (𝑗 ∈ (𝑀...𝑁) ↦ (𝐹‘𝑗)), ℝ, < )) |
61 | 60, 3 | breqtrrdi 5072 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ≤ 𝑊) |
62 | 47, 58, 61 | syl2anc 587 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → (𝐹‘𝑗) ≤ 𝑊) |
63 | | max1 12661 |
. . . . . . . . 9
⊢ ((𝑊 ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑊 ≤ if(𝑊 ≤ 𝑌, 𝑌, 𝑊)) |
64 | 40, 2, 63 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ≤ if(𝑊 ≤ 𝑌, 𝑌, 𝑊)) |
65 | 64, 1 | breqtrrdi 5072 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ≤ 𝑋) |
66 | 65 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑊 ≤ 𝑋) |
67 | 44, 45, 46, 62, 66 | letrd 10875 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → (𝐹‘𝑗) ≤ 𝑋) |
68 | 13 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝐾 ∈ ℝ) |
69 | | uzssre 12346 |
. . . . . . . . . 10
⊢
(ℤ≥‘𝑀) ⊆ ℝ |
70 | 36, 69 | eqsstri 3911 |
. . . . . . . . 9
⊢ 𝑍 ⊆
ℝ |
71 | 70 | sseli 3873 |
. . . . . . . 8
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℝ) |
72 | 71 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝑗 ∈ ℝ) |
73 | 69, 24 | sseldi 3875 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℝ) |
74 | 73 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝑁 ∈ ℝ) |
75 | | ceilge 13305 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℝ → 𝐾 ≤ (⌈‘𝐾)) |
76 | 13, 75 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ≤ (⌈‘𝐾)) |
77 | | max1 12661 |
. . . . . . . . . . . 12
⊢
(((⌈‘𝐾)
∈ ℝ ∧ 𝑀
∈ ℝ) → (⌈‘𝐾) ≤ if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾))) |
78 | 18, 19, 77 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌈‘𝐾) ≤ if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾))) |
79 | 78, 22 | breqtrd 5056 |
. . . . . . . . . 10
⊢ (𝜑 → (⌈‘𝐾) ≤ 𝑁) |
80 | 13, 18, 73, 76, 79 | letrd 10875 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ≤ 𝑁) |
81 | 80 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝐾 ≤ 𝑁) |
82 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → ¬ 𝑗 ≤ 𝑁) |
83 | 74, 72 | ltnled 10865 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → (𝑁 < 𝑗 ↔ ¬ 𝑗 ≤ 𝑁)) |
84 | 82, 83 | mpbird 260 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝑁 < 𝑗) |
85 | 68, 74, 72, 81, 84 | lelttrd 10876 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝐾 < 𝑗) |
86 | 68, 72, 85 | ltled 10866 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝐾 ≤ 𝑗) |
87 | 43 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → (𝐹‘𝑗) ∈ ℝ) |
88 | 2 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝑌 ∈ ℝ) |
89 | 42 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝑋 ∈ ℝ) |
90 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝐾 ≤ 𝑗) |
91 | | limsupubuzlem.b |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑗 ∈ 𝑍 (𝐾 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑌)) |
92 | 91 | r19.21bi 3121 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐾 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑌)) |
93 | 92 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → (𝐾 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑌)) |
94 | 90, 93 | mpd 15 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → (𝐹‘𝑗) ≤ 𝑌) |
95 | | max2 12663 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑌 ≤ if(𝑊 ≤ 𝑌, 𝑌, 𝑊)) |
96 | 40, 2, 95 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ≤ if(𝑊 ≤ 𝑌, 𝑌, 𝑊)) |
97 | 96, 1 | breqtrrdi 5072 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ≤ 𝑋) |
98 | 97 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝑌 ≤ 𝑋) |
99 | 87, 88, 89, 94, 98 | letrd 10875 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → (𝐹‘𝑗) ≤ 𝑋) |
100 | 86, 99 | syldan 594 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → (𝐹‘𝑗) ≤ 𝑋) |
101 | 67, 100 | pm2.61dan 813 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) ≤ 𝑋) |
102 | 101 | ex 416 |
. . 3
⊢ (𝜑 → (𝑗 ∈ 𝑍 → (𝐹‘𝑗) ≤ 𝑋)) |
103 | 5, 102 | ralrimi 3128 |
. 2
⊢ (𝜑 → ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑋) |
104 | | nfv 1921 |
. . 3
⊢
Ⅎ𝑥∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑋 |
105 | | nfcv 2899 |
. . . . 5
⊢
Ⅎ𝑗𝑥 |
106 | | limsupubuzlem.e |
. . . . 5
⊢
Ⅎ𝑗𝑋 |
107 | 105, 106 | nfeq 2912 |
. . . 4
⊢
Ⅎ𝑗 𝑥 = 𝑋 |
108 | | breq2 5034 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝐹‘𝑗) ≤ 𝑥 ↔ (𝐹‘𝑗) ≤ 𝑋)) |
109 | 107, 108 | ralbid 3145 |
. . 3
⊢ (𝑥 = 𝑋 → (∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥 ↔ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑋)) |
110 | 104, 109 | rspce 3515 |
. 2
⊢ ((𝑋 ∈ ℝ ∧
∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑋) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥) |
111 | 42, 103, 110 | syl2anc 587 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥) |