Step |
Hyp |
Ref |
Expression |
1 |
|
mbflimsup.1 |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
2 |
|
mbflimsup.2 |
⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ) |
3 |
|
mbflimsup.h |
⊢ 𝐻 = ( 𝑚 ∈ ℝ ↦ sup ( ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) “ ( 𝑚 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) |
4 |
|
mbflimsup.3 |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
5 |
|
mbflimsup.4 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ) |
6 |
|
mbflimsup.5 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) |
7 |
|
mbflimsup.6 |
⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴 ) ) → 𝐵 ∈ ℝ ) |
8 |
1
|
fvexi |
⊢ 𝑍 ∈ V |
9 |
8
|
mptex |
⊢ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ∈ V |
10 |
9
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ∈ V ) |
11 |
|
uzssz |
⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ |
12 |
1 11
|
eqsstri |
⊢ 𝑍 ⊆ ℤ |
13 |
|
zssre |
⊢ ℤ ⊆ ℝ |
14 |
12 13
|
sstri |
⊢ 𝑍 ⊆ ℝ |
15 |
14
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑍 ⊆ ℝ ) |
16 |
1
|
uzsup |
⊢ ( 𝑀 ∈ ℤ → sup ( 𝑍 , ℝ* , < ) = +∞ ) |
17 |
4 16
|
syl |
⊢ ( 𝜑 → sup ( 𝑍 , ℝ* , < ) = +∞ ) |
18 |
17
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → sup ( 𝑍 , ℝ* , < ) = +∞ ) |
19 |
3 10 15 18
|
limsupval2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) = inf ( ( 𝐻 “ 𝑍 ) , ℝ* , < ) ) |
20 |
|
imassrn |
⊢ ( 𝐻 “ 𝑍 ) ⊆ ran 𝐻 |
21 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ∈ ℤ ) |
22 |
7
|
anass1rs |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → 𝐵 ∈ ℝ ) |
23 |
22
|
fmpttd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℝ ) |
24 |
5
|
ltpnfd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) < +∞ ) |
25 |
3 1
|
limsupgre |
⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) < +∞ ) → 𝐻 : ℝ ⟶ ℝ ) |
26 |
21 23 24 25
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐻 : ℝ ⟶ ℝ ) |
27 |
26
|
frnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ran 𝐻 ⊆ ℝ ) |
28 |
20 27
|
sstrid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 “ 𝑍 ) ⊆ ℝ ) |
29 |
26
|
fdmd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → dom 𝐻 = ℝ ) |
30 |
29
|
ineq1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( dom 𝐻 ∩ 𝑍 ) = ( ℝ ∩ 𝑍 ) ) |
31 |
|
sseqin2 |
⊢ ( 𝑍 ⊆ ℝ ↔ ( ℝ ∩ 𝑍 ) = 𝑍 ) |
32 |
14 31
|
mpbi |
⊢ ( ℝ ∩ 𝑍 ) = 𝑍 |
33 |
30 32
|
eqtrdi |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( dom 𝐻 ∩ 𝑍 ) = 𝑍 ) |
34 |
|
uzid |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
35 |
4 34
|
syl |
⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
36 |
35 1
|
eleqtrrdi |
⊢ ( 𝜑 → 𝑀 ∈ 𝑍 ) |
37 |
36
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ∈ 𝑍 ) |
38 |
37
|
ne0d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑍 ≠ ∅ ) |
39 |
33 38
|
eqnetrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( dom 𝐻 ∩ 𝑍 ) ≠ ∅ ) |
40 |
|
imadisj |
⊢ ( ( 𝐻 “ 𝑍 ) = ∅ ↔ ( dom 𝐻 ∩ 𝑍 ) = ∅ ) |
41 |
40
|
necon3bii |
⊢ ( ( 𝐻 “ 𝑍 ) ≠ ∅ ↔ ( dom 𝐻 ∩ 𝑍 ) ≠ ∅ ) |
42 |
39 41
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 “ 𝑍 ) ≠ ∅ ) |
43 |
5
|
leidd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ) |
44 |
22
|
rexrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → 𝐵 ∈ ℝ* ) |
45 |
44
|
fmpttd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℝ* ) |
46 |
5
|
rexrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ* ) |
47 |
3
|
limsuple |
⊢ ( ( 𝑍 ⊆ ℝ ∧ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℝ* ∧ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ* ) → ( ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ↔ ∀ 𝑦 ∈ ℝ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( 𝐻 ‘ 𝑦 ) ) ) |
48 |
15 45 46 47
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ↔ ∀ 𝑦 ∈ ℝ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( 𝐻 ‘ 𝑦 ) ) ) |
49 |
43 48
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ ℝ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( 𝐻 ‘ 𝑦 ) ) |
50 |
|
ssralv |
⊢ ( 𝑍 ⊆ ℝ → ( ∀ 𝑦 ∈ ℝ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( 𝐻 ‘ 𝑦 ) → ∀ 𝑦 ∈ 𝑍 ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( 𝐻 ‘ 𝑦 ) ) ) |
51 |
14 49 50
|
mpsyl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝑍 ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( 𝐻 ‘ 𝑦 ) ) |
52 |
3
|
limsupgf |
⊢ 𝐻 : ℝ ⟶ ℝ* |
53 |
|
ffn |
⊢ ( 𝐻 : ℝ ⟶ ℝ* → 𝐻 Fn ℝ ) |
54 |
52 53
|
ax-mp |
⊢ 𝐻 Fn ℝ |
55 |
|
breq2 |
⊢ ( 𝑧 = ( 𝐻 ‘ 𝑦 ) → ( ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ 𝑧 ↔ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( 𝐻 ‘ 𝑦 ) ) ) |
56 |
55
|
ralima |
⊢ ( ( 𝐻 Fn ℝ ∧ 𝑍 ⊆ ℝ ) → ( ∀ 𝑧 ∈ ( 𝐻 “ 𝑍 ) ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ 𝑧 ↔ ∀ 𝑦 ∈ 𝑍 ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( 𝐻 ‘ 𝑦 ) ) ) |
57 |
54 15 56
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ ( 𝐻 “ 𝑍 ) ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ 𝑧 ↔ ∀ 𝑦 ∈ 𝑍 ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( 𝐻 ‘ 𝑦 ) ) ) |
58 |
51 57
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑧 ∈ ( 𝐻 “ 𝑍 ) ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ 𝑧 ) |
59 |
|
breq1 |
⊢ ( 𝑦 = ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) → ( 𝑦 ≤ 𝑧 ↔ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ 𝑧 ) ) |
60 |
59
|
ralbidv |
⊢ ( 𝑦 = ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) → ( ∀ 𝑧 ∈ ( 𝐻 “ 𝑍 ) 𝑦 ≤ 𝑧 ↔ ∀ 𝑧 ∈ ( 𝐻 “ 𝑍 ) ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ 𝑧 ) ) |
61 |
60
|
rspcev |
⊢ ( ( ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ∧ ∀ 𝑧 ∈ ( 𝐻 “ 𝑍 ) ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ 𝑧 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝐻 “ 𝑍 ) 𝑦 ≤ 𝑧 ) |
62 |
5 58 61
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝐻 “ 𝑍 ) 𝑦 ≤ 𝑧 ) |
63 |
|
infxrre |
⊢ ( ( ( 𝐻 “ 𝑍 ) ⊆ ℝ ∧ ( 𝐻 “ 𝑍 ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ( 𝐻 “ 𝑍 ) 𝑦 ≤ 𝑧 ) → inf ( ( 𝐻 “ 𝑍 ) , ℝ* , < ) = inf ( ( 𝐻 “ 𝑍 ) , ℝ , < ) ) |
64 |
28 42 62 63
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → inf ( ( 𝐻 “ 𝑍 ) , ℝ* , < ) = inf ( ( 𝐻 “ 𝑍 ) , ℝ , < ) ) |
65 |
|
df-ima |
⊢ ( 𝐻 “ 𝑍 ) = ran ( 𝐻 ↾ 𝑍 ) |
66 |
26
|
feqmptd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐻 = ( 𝑖 ∈ ℝ ↦ ( 𝐻 ‘ 𝑖 ) ) ) |
67 |
66
|
reseq1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ↾ 𝑍 ) = ( ( 𝑖 ∈ ℝ ↦ ( 𝐻 ‘ 𝑖 ) ) ↾ 𝑍 ) ) |
68 |
|
resmpt |
⊢ ( 𝑍 ⊆ ℝ → ( ( 𝑖 ∈ ℝ ↦ ( 𝐻 ‘ 𝑖 ) ) ↾ 𝑍 ) = ( 𝑖 ∈ 𝑍 ↦ ( 𝐻 ‘ 𝑖 ) ) ) |
69 |
14 68
|
ax-mp |
⊢ ( ( 𝑖 ∈ ℝ ↦ ( 𝐻 ‘ 𝑖 ) ) ↾ 𝑍 ) = ( 𝑖 ∈ 𝑍 ↦ ( 𝐻 ‘ 𝑖 ) ) |
70 |
67 69
|
eqtrdi |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ↾ 𝑍 ) = ( 𝑖 ∈ 𝑍 ↦ ( 𝐻 ‘ 𝑖 ) ) ) |
71 |
14
|
sseli |
⊢ ( 𝑖 ∈ 𝑍 → 𝑖 ∈ ℝ ) |
72 |
|
ffvelrn |
⊢ ( ( 𝐻 : ℝ ⟶ ℝ ∧ 𝑖 ∈ ℝ ) → ( 𝐻 ‘ 𝑖 ) ∈ ℝ ) |
73 |
26 71 72
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑖 ) ∈ ℝ ) |
74 |
73
|
rexrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑖 ) ∈ ℝ* ) |
75 |
|
simplll |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝜑 ) |
76 |
1
|
uztrn2 |
⊢ ( ( 𝑖 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑛 ∈ 𝑍 ) |
77 |
76
|
adantll |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑛 ∈ 𝑍 ) |
78 |
|
simpllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑥 ∈ 𝐴 ) |
79 |
75 77 78 7
|
syl12anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝐵 ∈ ℝ ) |
80 |
79
|
fmpttd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) : ( ℤ≥ ‘ 𝑖 ) ⟶ ℝ ) |
81 |
80
|
frnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ⊆ ℝ ) |
82 |
|
eqid |
⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) = ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) |
83 |
82 79
|
dmmptd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → dom ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) = ( ℤ≥ ‘ 𝑖 ) ) |
84 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ 𝑍 ) |
85 |
84 1
|
eleqtrdi |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
86 |
|
eluzelz |
⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑖 ∈ ℤ ) |
87 |
85 86
|
syl |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ ℤ ) |
88 |
87
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ ℤ ) |
89 |
|
uzid |
⊢ ( 𝑖 ∈ ℤ → 𝑖 ∈ ( ℤ≥ ‘ 𝑖 ) ) |
90 |
|
ne0i |
⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑖 ) → ( ℤ≥ ‘ 𝑖 ) ≠ ∅ ) |
91 |
88 89 90
|
3syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑖 ) ≠ ∅ ) |
92 |
83 91
|
eqnetrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → dom ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ≠ ∅ ) |
93 |
|
dm0rn0 |
⊢ ( dom ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) = ∅ ↔ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) = ∅ ) |
94 |
93
|
necon3bii |
⊢ ( dom ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ≠ ∅ ↔ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ≠ ∅ ) |
95 |
92 94
|
sylib |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ≠ ∅ ) |
96 |
85
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
97 |
|
uzss |
⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑖 ) ⊆ ( ℤ≥ ‘ 𝑀 ) ) |
98 |
96 97
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑖 ) ⊆ ( ℤ≥ ‘ 𝑀 ) ) |
99 |
98 1
|
sseqtrrdi |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑖 ) ⊆ 𝑍 ) |
100 |
73
|
leidd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑖 ) ≤ ( 𝐻 ‘ 𝑖 ) ) |
101 |
14
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → 𝑍 ⊆ ℝ ) |
102 |
45
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℝ* ) |
103 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ 𝑍 ) |
104 |
14 103
|
sselid |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ ℝ ) |
105 |
3
|
limsupgle |
⊢ ( ( ( 𝑍 ⊆ ℝ ∧ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℝ* ) ∧ 𝑖 ∈ ℝ ∧ ( 𝐻 ‘ 𝑖 ) ∈ ℝ* ) → ( ( 𝐻 ‘ 𝑖 ) ≤ ( 𝐻 ‘ 𝑖 ) ↔ ∀ 𝑘 ∈ 𝑍 ( 𝑖 ≤ 𝑘 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ) ) ) |
106 |
101 102 104 74 105
|
syl211anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝐻 ‘ 𝑖 ) ≤ ( 𝐻 ‘ 𝑖 ) ↔ ∀ 𝑘 ∈ 𝑍 ( 𝑖 ≤ 𝑘 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ) ) ) |
107 |
100 106
|
mpbid |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ∀ 𝑘 ∈ 𝑍 ( 𝑖 ≤ 𝑘 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ) ) |
108 |
|
ssralv |
⊢ ( ( ℤ≥ ‘ 𝑖 ) ⊆ 𝑍 → ( ∀ 𝑘 ∈ 𝑍 ( 𝑖 ≤ 𝑘 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝑖 ≤ 𝑘 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ) ) ) |
109 |
99 107 108
|
sylc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝑖 ≤ 𝑘 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ) ) |
110 |
99
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ℤ≥ ‘ 𝑖 ) ⊆ 𝑍 ) |
111 |
110
|
resmptd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑖 ) ) = ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ) |
112 |
111
|
fveq1d |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑖 ) ) ‘ 𝑘 ) = ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ) |
113 |
|
fvres |
⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) → ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑖 ) ) ‘ 𝑘 ) = ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ) |
114 |
113
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑖 ) ) ‘ 𝑘 ) = ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ) |
115 |
112 114
|
eqtr3d |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) = ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ) |
116 |
115
|
breq1d |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ↔ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ) ) |
117 |
|
eluzle |
⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) → 𝑖 ≤ 𝑘 ) |
118 |
117
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑖 ≤ 𝑘 ) |
119 |
|
biimt |
⊢ ( 𝑖 ≤ 𝑘 → ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ↔ ( 𝑖 ≤ 𝑘 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ) ) ) |
120 |
118 119
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ↔ ( 𝑖 ≤ 𝑘 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ) ) ) |
121 |
116 120
|
bitrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ↔ ( 𝑖 ≤ 𝑘 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ) ) ) |
122 |
121
|
ralbidva |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝑖 ≤ 𝑘 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ) ) ) |
123 |
109 122
|
mpbird |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ) |
124 |
|
ffn |
⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) : ( ℤ≥ ‘ 𝑖 ) ⟶ ℝ → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) Fn ( ℤ≥ ‘ 𝑖 ) ) |
125 |
|
breq1 |
⊢ ( 𝑧 = ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) → ( 𝑧 ≤ ( 𝐻 ‘ 𝑖 ) ↔ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ) ) |
126 |
125
|
ralrn |
⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) Fn ( ℤ≥ ‘ 𝑖 ) → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) 𝑧 ≤ ( 𝐻 ‘ 𝑖 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ) ) |
127 |
80 124 126
|
3syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) 𝑧 ≤ ( 𝐻 ‘ 𝑖 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ≤ ( 𝐻 ‘ 𝑖 ) ) ) |
128 |
123 127
|
mpbird |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) 𝑧 ≤ ( 𝐻 ‘ 𝑖 ) ) |
129 |
|
brralrspcev |
⊢ ( ( ( 𝐻 ‘ 𝑖 ) ∈ ℝ ∧ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) 𝑧 ≤ ( 𝐻 ‘ 𝑖 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) |
130 |
73 128 129
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) |
131 |
81 95 130
|
suprcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ∈ ℝ ) |
132 |
131
|
rexrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ∈ ℝ* ) |
133 |
81
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘 ) ) → ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ⊆ ℝ ) |
134 |
95
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘 ) ) → ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ≠ ∅ ) |
135 |
130
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) |
136 |
12
|
sseli |
⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ ) |
137 |
|
eluz |
⊢ ( ( 𝑖 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↔ 𝑖 ≤ 𝑘 ) ) |
138 |
88 136 137
|
syl2an |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ↔ 𝑖 ≤ 𝑘 ) ) |
139 |
138
|
biimprd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑖 ≤ 𝑘 → 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) ) |
140 |
139
|
impr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) |
141 |
140 115
|
syldan |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘 ) ) → ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) = ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ) |
142 |
80
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘 ) ) → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) : ( ℤ≥ ‘ 𝑖 ) ⟶ ℝ ) |
143 |
142 124
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘 ) ) → ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) Fn ( ℤ≥ ‘ 𝑖 ) ) |
144 |
|
fnfvelrn |
⊢ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) Fn ( ℤ≥ ‘ 𝑖 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ∈ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ) |
145 |
143 140 144
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘 ) ) → ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ‘ 𝑘 ) ∈ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ) |
146 |
141 145
|
eqeltrrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘 ) ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ∈ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ) |
147 |
133 134 135 146
|
suprubd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑖 ≤ 𝑘 ) ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) |
148 |
147
|
expr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝑖 ≤ 𝑘 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) ) |
149 |
148
|
ralrimiva |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ∀ 𝑘 ∈ 𝑍 ( 𝑖 ≤ 𝑘 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) ) |
150 |
3
|
limsupgle |
⊢ ( ( ( 𝑍 ⊆ ℝ ∧ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℝ* ) ∧ 𝑖 ∈ ℝ ∧ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ∈ ℝ* ) → ( ( 𝐻 ‘ 𝑖 ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ↔ ∀ 𝑘 ∈ 𝑍 ( 𝑖 ≤ 𝑘 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) ) ) |
151 |
101 102 104 132 150
|
syl211anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝐻 ‘ 𝑖 ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ↔ ∀ 𝑘 ∈ 𝑍 ( 𝑖 ≤ 𝑘 → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) ) ) |
152 |
149 151
|
mpbird |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑖 ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) |
153 |
|
suprleub |
⊢ ( ( ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ⊆ ℝ ∧ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) ∧ ( 𝐻 ‘ 𝑖 ) ∈ ℝ ) → ( sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ≤ ( 𝐻 ‘ 𝑖 ) ↔ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) 𝑧 ≤ ( 𝐻 ‘ 𝑖 ) ) ) |
154 |
81 95 130 73 153
|
syl31anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ≤ ( 𝐻 ‘ 𝑖 ) ↔ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) 𝑧 ≤ ( 𝐻 ‘ 𝑖 ) ) ) |
155 |
128 154
|
mpbird |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ≤ ( 𝐻 ‘ 𝑖 ) ) |
156 |
74 132 152 155
|
xrletrid |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑖 ) = sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) |
157 |
156
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑖 ∈ 𝑍 ↦ ( 𝐻 ‘ 𝑖 ) ) = ( 𝑖 ∈ 𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) ) |
158 |
70 157
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ↾ 𝑍 ) = ( 𝑖 ∈ 𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) ) |
159 |
158
|
rneqd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ran ( 𝐻 ↾ 𝑍 ) = ran ( 𝑖 ∈ 𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) ) |
160 |
65 159
|
syl5eq |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 “ 𝑍 ) = ran ( 𝑖 ∈ 𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) ) |
161 |
160
|
infeq1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → inf ( ( 𝐻 “ 𝑍 ) , ℝ , < ) = inf ( ran ( 𝑖 ∈ 𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) , ℝ , < ) ) |
162 |
19 64 161
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) = inf ( ran ( 𝑖 ∈ 𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) , ℝ , < ) ) |
163 |
162
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ inf ( ran ( 𝑖 ∈ 𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) , ℝ , < ) ) ) |
164 |
2 163
|
syl5eq |
⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐴 ↦ inf ( ran ( 𝑖 ∈ 𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) , ℝ , < ) ) ) |
165 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐴 ↦ inf ( ran ( 𝑖 ∈ 𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) , ℝ , < ) ) = ( 𝑥 ∈ 𝐴 ↦ inf ( ran ( 𝑖 ∈ 𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) , ℝ , < ) ) |
166 |
|
eqid |
⊢ ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑖 ) |
167 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐴 ↦ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) = ( 𝑥 ∈ 𝐴 ↦ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) |
168 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝜑 ) |
169 |
76
|
adantll |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑛 ∈ 𝑍 ) |
170 |
168 169 6
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) |
171 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∧ 𝑥 ∈ 𝐴 ) ) → 𝜑 ) |
172 |
76
|
ad2ant2lr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∧ 𝑥 ∈ 𝐴 ) ) → 𝑛 ∈ 𝑍 ) |
173 |
|
simprr |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∧ 𝑥 ∈ 𝐴 ) ) → 𝑥 ∈ 𝐴 ) |
174 |
171 172 173 7
|
syl12anc |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ∧ 𝑥 ∈ 𝐴 ) ) → 𝐵 ∈ ℝ ) |
175 |
79
|
ralrimiva |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ∈ ℝ ) |
176 |
|
breq1 |
⊢ ( 𝑧 = 𝐵 → ( 𝑧 ≤ 𝑦 ↔ 𝐵 ≤ 𝑦 ) ) |
177 |
82 176
|
ralrnmptw |
⊢ ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ∈ ℝ → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) 𝑧 ≤ 𝑦 ↔ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) ) |
178 |
175 177
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) 𝑧 ≤ 𝑦 ↔ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) ) |
179 |
178
|
rexbidv |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) 𝑧 ≤ 𝑦 ↔ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) ) |
180 |
130 179
|
mpbid |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) |
181 |
180
|
an32s |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) 𝐵 ≤ 𝑦 ) |
182 |
166 167 87 170 174 181
|
mbfsup |
⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) ∈ MblFn ) |
183 |
131
|
an32s |
⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝐴 ) → sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ∈ ℝ ) |
184 |
183
|
anasss |
⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴 ) ) → sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ∈ ℝ ) |
185 |
3
|
limsuple |
⊢ ( ( 𝑍 ⊆ ℝ ∧ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℝ* ∧ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ* ) → ( ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ↔ ∀ 𝑖 ∈ ℝ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( 𝐻 ‘ 𝑖 ) ) ) |
186 |
15 45 46 185
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ↔ ∀ 𝑖 ∈ ℝ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( 𝐻 ‘ 𝑖 ) ) ) |
187 |
43 186
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑖 ∈ ℝ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( 𝐻 ‘ 𝑖 ) ) |
188 |
|
ssralv |
⊢ ( 𝑍 ⊆ ℝ → ( ∀ 𝑖 ∈ ℝ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( 𝐻 ‘ 𝑖 ) → ∀ 𝑖 ∈ 𝑍 ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( 𝐻 ‘ 𝑖 ) ) ) |
189 |
14 187 188
|
mpsyl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑖 ∈ 𝑍 ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( 𝐻 ‘ 𝑖 ) ) |
190 |
156
|
breq2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑖 ∈ 𝑍 ) → ( ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( 𝐻 ‘ 𝑖 ) ↔ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) ) |
191 |
190
|
ralbidva |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑖 ∈ 𝑍 ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ ( 𝐻 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ 𝑍 ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) ) |
192 |
189 191
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑖 ∈ 𝑍 ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) |
193 |
|
breq1 |
⊢ ( 𝑦 = ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) → ( 𝑦 ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ↔ ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) ) |
194 |
193
|
ralbidv |
⊢ ( 𝑦 = ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) → ( ∀ 𝑖 ∈ 𝑍 𝑦 ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ↔ ∀ 𝑖 ∈ 𝑍 ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) ) |
195 |
194
|
rspcev |
⊢ ( ( ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ∈ ℝ ∧ ∀ 𝑖 ∈ 𝑍 ( lim sup ‘ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ) ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 𝑦 ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) |
196 |
5 192 195
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 𝑦 ≤ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) |
197 |
1 165 4 182 184 196
|
mbfinf |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ inf ( ran ( 𝑖 ∈ 𝑍 ↦ sup ( ran ( 𝑛 ∈ ( ℤ≥ ‘ 𝑖 ) ↦ 𝐵 ) , ℝ , < ) ) , ℝ , < ) ) ∈ MblFn ) |
198 |
164 197
|
eqeltrd |
⊢ ( 𝜑 → 𝐺 ∈ MblFn ) |