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 10319 |
. . . . . . 7
⊢ < Or
ℝ |
7 | 6 | a1i 11 |
. . . . . 6
⊢ (𝜑 → < Or
ℝ) |
8 | | fzfid 12979 |
. . . . . 6
⊢ (𝜑 → (𝑀...𝑁) ∈ Fin) |
9 | | eqid 2770 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
10 | | limsupubuzlem.m |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
11 | | limsupubuzlem.n |
. . . . . . . . . . 11
⊢ 𝑁 = if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾)) |
12 | 11 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 = if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾))) |
13 | | limsupubuzlem.k |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ ℝ) |
14 | | ceilcl 12850 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℝ →
(⌈‘𝐾) ∈
ℤ) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌈‘𝐾) ∈
ℤ) |
16 | 10, 15 | ifcld 4268 |
. . . . . . . . . 10
⊢ (𝜑 → if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾)) ∈ ℤ) |
17 | 12, 16 | eqeltrd 2849 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℤ) |
18 | 15 | zred 11683 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌈‘𝐾) ∈
ℝ) |
19 | 10 | zred 11683 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
20 | | max2 12222 |
. . . . . . . . . . 11
⊢
(((⌈‘𝐾)
∈ ℝ ∧ 𝑀
∈ ℝ) → 𝑀
≤ if((⌈‘𝐾)
≤ 𝑀, 𝑀, (⌈‘𝐾))) |
21 | 18, 19, 20 | syl2anc 565 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ≤ if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾))) |
22 | 12 | eqcomd 2776 |
. . . . . . . . . 10
⊢ (𝜑 → if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾)) = 𝑁) |
23 | 21, 22 | breqtrd 4810 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
24 | 9, 10, 17, 23 | eluzd 40145 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
25 | | eluzfz2 12555 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
27 | | ne0i 4067 |
. . . . . . 7
⊢ (𝑁 ∈ (𝑀...𝑁) → (𝑀...𝑁) ≠ ∅) |
28 | 26, 27 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑀...𝑁) ≠ ∅) |
29 | | limsupubuzlem.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝑍⟶ℝ) |
30 | 29 | adantr 466 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐹:𝑍⟶ℝ) |
31 | 10 | adantr 466 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℤ) |
32 | | elfzelz 12548 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (𝑀...𝑁) → 𝑗 ∈ ℤ) |
33 | 32 | adantl 467 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝑗 ∈ ℤ) |
34 | | elfzle1 12550 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝑗) |
35 | 34 | adantl 467 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝑀 ≤ 𝑗) |
36 | 9, 31, 33, 35 | eluzd 40145 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝑗 ∈ (ℤ≥‘𝑀)) |
37 | | limsupubuzlem.z |
. . . . . . . 8
⊢ 𝑍 =
(ℤ≥‘𝑀) |
38 | 36, 37 | syl6eleqr 2860 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝑗 ∈ 𝑍) |
39 | 30, 38 | ffvelrnd 6503 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ∈ ℝ) |
40 | 5, 7, 8, 28, 39 | fisupclrnmpt 40132 |
. . . . 5
⊢ (𝜑 → sup(ran (𝑗 ∈ (𝑀...𝑁) ↦ (𝐹‘𝑗)), ℝ, < ) ∈
ℝ) |
41 | 4, 40 | eqeltrd 2849 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ ℝ) |
42 | 2, 41 | ifcld 4268 |
. . 3
⊢ (𝜑 → if(𝑊 ≤ 𝑌, 𝑌, 𝑊) ∈ ℝ) |
43 | 1, 42 | syl5eqel 2853 |
. 2
⊢ (𝜑 → 𝑋 ∈ ℝ) |
44 | 29 | ffvelrnda 6502 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) ∈ ℝ) |
45 | 44 | adantr 466 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → (𝐹‘𝑗) ∈ ℝ) |
46 | 41 | ad2antrr 697 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑊 ∈ ℝ) |
47 | 43 | ad2antrr 697 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑋 ∈ ℝ) |
48 | | simpll 742 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝜑) |
49 | 10 | ad2antrr 697 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑀 ∈ ℤ) |
50 | 17 | ad2antrr 697 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑁 ∈ ℤ) |
51 | 37 | eluzelz2 40137 |
. . . . . . . . 9
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ) |
52 | 51 | ad2antlr 698 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑗 ∈ ℤ) |
53 | 37 | eleq2i 2841 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ 𝑍 ↔ 𝑗 ∈ (ℤ≥‘𝑀)) |
54 | 53 | biimpi 206 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ (ℤ≥‘𝑀)) |
55 | | eluzle 11900 |
. . . . . . . . . 10
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑗) |
56 | 54, 55 | syl 17 |
. . . . . . . . 9
⊢ (𝑗 ∈ 𝑍 → 𝑀 ≤ 𝑗) |
57 | 56 | ad2antlr 698 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑀 ≤ 𝑗) |
58 | | simpr 471 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑗 ≤ 𝑁) |
59 | 49, 50, 52, 57, 58 | elfzd 40146 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑗 ∈ (𝑀...𝑁)) |
60 | 5, 8, 39 | fimaxre4 40135 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑗 ∈ (𝑀...𝑁)(𝐹‘𝑗) ≤ 𝑏) |
61 | 5, 39, 60 | suprubrnmpt 39980 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ≤ sup(ran (𝑗 ∈ (𝑀...𝑁) ↦ (𝐹‘𝑗)), ℝ, < )) |
62 | 61, 3 | syl6breqr 4826 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐹‘𝑗) ≤ 𝑊) |
63 | 48, 59, 62 | syl2anc 565 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → (𝐹‘𝑗) ≤ 𝑊) |
64 | | max1 12220 |
. . . . . . . . 9
⊢ ((𝑊 ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑊 ≤ if(𝑊 ≤ 𝑌, 𝑌, 𝑊)) |
65 | 41, 2, 64 | syl2anc 565 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ≤ if(𝑊 ≤ 𝑌, 𝑌, 𝑊)) |
66 | 65, 1 | syl6breqr 4826 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ≤ 𝑋) |
67 | 66 | ad2antrr 697 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → 𝑊 ≤ 𝑋) |
68 | 45, 46, 47, 63, 67 | letrd 10395 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 ≤ 𝑁) → (𝐹‘𝑗) ≤ 𝑋) |
69 | 13 | ad2antrr 697 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝐾 ∈ ℝ) |
70 | | uzssre 40130 |
. . . . . . . . . 10
⊢
(ℤ≥‘𝑀) ⊆ ℝ |
71 | 37, 70 | eqsstri 3782 |
. . . . . . . . 9
⊢ 𝑍 ⊆
ℝ |
72 | 71 | sseli 3746 |
. . . . . . . 8
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℝ) |
73 | 72 | ad2antlr 698 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝑗 ∈ ℝ) |
74 | 70, 24 | sseldi 3748 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℝ) |
75 | 74 | ad2antrr 697 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝑁 ∈ ℝ) |
76 | | ceilge 12852 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℝ → 𝐾 ≤ (⌈‘𝐾)) |
77 | 13, 76 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ≤ (⌈‘𝐾)) |
78 | | max1 12220 |
. . . . . . . . . . . 12
⊢
(((⌈‘𝐾)
∈ ℝ ∧ 𝑀
∈ ℝ) → (⌈‘𝐾) ≤ if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾))) |
79 | 18, 19, 78 | syl2anc 565 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌈‘𝐾) ≤ if((⌈‘𝐾) ≤ 𝑀, 𝑀, (⌈‘𝐾))) |
80 | 79, 22 | breqtrd 4810 |
. . . . . . . . . 10
⊢ (𝜑 → (⌈‘𝐾) ≤ 𝑁) |
81 | 13, 18, 74, 77, 80 | letrd 10395 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ≤ 𝑁) |
82 | 81 | ad2antrr 697 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝐾 ≤ 𝑁) |
83 | | simpr 471 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → ¬ 𝑗 ≤ 𝑁) |
84 | 75, 73 | ltnled 10385 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → (𝑁 < 𝑗 ↔ ¬ 𝑗 ≤ 𝑁)) |
85 | 83, 84 | mpbird 247 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝑁 < 𝑗) |
86 | 69, 75, 73, 82, 85 | lelttrd 10396 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝐾 < 𝑗) |
87 | 69, 73, 86 | ltled 10386 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → 𝐾 ≤ 𝑗) |
88 | 44 | adantr 466 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → (𝐹‘𝑗) ∈ ℝ) |
89 | 2 | ad2antrr 697 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝑌 ∈ ℝ) |
90 | 43 | ad2antrr 697 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝑋 ∈ ℝ) |
91 | | simpr 471 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝐾 ≤ 𝑗) |
92 | | limsupubuzlem.b |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑗 ∈ 𝑍 (𝐾 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑌)) |
93 | 92 | r19.21bi 3080 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐾 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑌)) |
94 | 93 | adantr 466 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → (𝐾 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝑌)) |
95 | 91, 94 | mpd 15 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → (𝐹‘𝑗) ≤ 𝑌) |
96 | | max2 12222 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑌 ≤ if(𝑊 ≤ 𝑌, 𝑌, 𝑊)) |
97 | 41, 2, 96 | syl2anc 565 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ≤ if(𝑊 ≤ 𝑌, 𝑌, 𝑊)) |
98 | 97, 1 | syl6breqr 4826 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ≤ 𝑋) |
99 | 98 | ad2antrr 697 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝑌 ≤ 𝑋) |
100 | 88, 89, 90, 95, 99 | letrd 10395 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → (𝐹‘𝑗) ≤ 𝑋) |
101 | 87, 100 | syldan 571 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝑗 ≤ 𝑁) → (𝐹‘𝑗) ≤ 𝑋) |
102 | 68, 101 | pm2.61dan 796 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) ≤ 𝑋) |
103 | 102 | ex 397 |
. . 3
⊢ (𝜑 → (𝑗 ∈ 𝑍 → (𝐹‘𝑗) ≤ 𝑋)) |
104 | 5, 103 | ralrimi 3105 |
. 2
⊢ (𝜑 → ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑋) |
105 | | nfv 1994 |
. . 3
⊢
Ⅎ𝑥∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑋 |
106 | | nfcv 2912 |
. . . . 5
⊢
Ⅎ𝑗𝑥 |
107 | | limsupubuzlem.e |
. . . . 5
⊢
Ⅎ𝑗𝑋 |
108 | 106, 107 | nfeq 2924 |
. . . 4
⊢
Ⅎ𝑗 𝑥 = 𝑋 |
109 | | breq2 4788 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝐹‘𝑗) ≤ 𝑥 ↔ (𝐹‘𝑗) ≤ 𝑋)) |
110 | 108, 109 | ralbid 3131 |
. . 3
⊢ (𝑥 = 𝑋 → (∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥 ↔ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑋)) |
111 | 105, 110 | rspce 3453 |
. 2
⊢ ((𝑋 ∈ ℝ ∧
∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑋) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥) |
112 | 43, 104, 111 | syl2anc 565 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐹‘𝑗) ≤ 𝑥) |