Step |
Hyp |
Ref |
Expression |
1 |
|
limsupval.1 |
⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) |
2 |
|
limsupgre.z |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
3 |
|
xrltso |
⊢ < Or ℝ* |
4 |
3
|
supex |
⊢ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ V |
5 |
4
|
a1i |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑘 ∈ ℝ ) → sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ V ) |
6 |
1
|
a1i |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) → 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) ) |
7 |
1
|
limsupgval |
⊢ ( 𝑎 ∈ ℝ → ( 𝐺 ‘ 𝑎 ) = sup ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) |
8 |
7
|
adantl |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( 𝐺 ‘ 𝑎 ) = sup ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) |
9 |
|
simpl3 |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( lim sup ‘ 𝐹 ) < +∞ ) |
10 |
|
uzssz |
⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ |
11 |
2 10
|
eqsstri |
⊢ 𝑍 ⊆ ℤ |
12 |
|
zssre |
⊢ ℤ ⊆ ℝ |
13 |
11 12
|
sstri |
⊢ 𝑍 ⊆ ℝ |
14 |
13
|
a1i |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝑍 ⊆ ℝ ) |
15 |
|
simpl2 |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝐹 : 𝑍 ⟶ ℝ ) |
16 |
|
ressxr |
⊢ ℝ ⊆ ℝ* |
17 |
|
fss |
⊢ ( ( 𝐹 : 𝑍 ⟶ ℝ ∧ ℝ ⊆ ℝ* ) → 𝐹 : 𝑍 ⟶ ℝ* ) |
18 |
15 16 17
|
sylancl |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝐹 : 𝑍 ⟶ ℝ* ) |
19 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
20 |
19
|
a1i |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → +∞ ∈ ℝ* ) |
21 |
1
|
limsuplt |
⊢ ( ( 𝑍 ⊆ ℝ ∧ 𝐹 : 𝑍 ⟶ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( lim sup ‘ 𝐹 ) < +∞ ↔ ∃ 𝑛 ∈ ℝ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) |
22 |
14 18 20 21
|
syl3anc |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( ( lim sup ‘ 𝐹 ) < +∞ ↔ ∃ 𝑛 ∈ ℝ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) |
23 |
9 22
|
mpbid |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ∃ 𝑛 ∈ ℝ ( 𝐺 ‘ 𝑛 ) < +∞ ) |
24 |
|
fzfi |
⊢ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ∈ Fin |
25 |
15
|
adantr |
⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) → 𝐹 : 𝑍 ⟶ ℝ ) |
26 |
|
elfzuz |
⊢ ( 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
27 |
26 2
|
eleqtrrdi |
⊢ ( 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) → 𝑚 ∈ 𝑍 ) |
28 |
|
ffvelrn |
⊢ ( ( 𝐹 : 𝑍 ⟶ ℝ ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℝ ) |
29 |
25 27 28
|
syl2an |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ) → ( 𝐹 ‘ 𝑚 ) ∈ ℝ ) |
30 |
29
|
ralrimiva |
⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) → ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ∈ ℝ ) |
31 |
|
fimaxre3 |
⊢ ( ( ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ∈ Fin ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ∈ ℝ ) → ∃ 𝑟 ∈ ℝ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) |
32 |
24 30 31
|
sylancr |
⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) → ∃ 𝑟 ∈ ℝ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) |
33 |
|
simpr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ ) |
34 |
33
|
ad2antrr |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → 𝑎 ∈ ℝ ) |
35 |
1
|
limsupgf |
⊢ 𝐺 : ℝ ⟶ ℝ* |
36 |
35
|
ffvelrni |
⊢ ( 𝑎 ∈ ℝ → ( 𝐺 ‘ 𝑎 ) ∈ ℝ* ) |
37 |
34 36
|
syl |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → ( 𝐺 ‘ 𝑎 ) ∈ ℝ* ) |
38 |
|
simprl |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → 𝑟 ∈ ℝ ) |
39 |
16 38
|
sselid |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → 𝑟 ∈ ℝ* ) |
40 |
|
simprl |
⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) → 𝑛 ∈ ℝ ) |
41 |
40
|
adantr |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → 𝑛 ∈ ℝ ) |
42 |
35
|
ffvelrni |
⊢ ( 𝑛 ∈ ℝ → ( 𝐺 ‘ 𝑛 ) ∈ ℝ* ) |
43 |
41 42
|
syl |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ* ) |
44 |
39 43
|
ifcld |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ* ) |
45 |
19
|
a1i |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → +∞ ∈ ℝ* ) |
46 |
40
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → 𝑛 ∈ ℝ ) |
47 |
13
|
a1i |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → 𝑍 ⊆ ℝ ) |
48 |
47
|
sselda |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ ℝ ) |
49 |
43
|
xrleidd |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → ( 𝐺 ‘ 𝑛 ) ≤ ( 𝐺 ‘ 𝑛 ) ) |
50 |
18
|
ad2antrr |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → 𝐹 : 𝑍 ⟶ ℝ* ) |
51 |
1
|
limsupgle |
⊢ ( ( ( 𝑍 ⊆ ℝ ∧ 𝐹 : 𝑍 ⟶ ℝ* ) ∧ 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) ∈ ℝ* ) → ( ( 𝐺 ‘ 𝑛 ) ≤ ( 𝐺 ‘ 𝑛 ) ↔ ∀ 𝑖 ∈ 𝑍 ( 𝑛 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑛 ) ) ) ) |
52 |
47 50 41 43 51
|
syl211anc |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → ( ( 𝐺 ‘ 𝑛 ) ≤ ( 𝐺 ‘ 𝑛 ) ↔ ∀ 𝑖 ∈ 𝑍 ( 𝑛 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑛 ) ) ) ) |
53 |
49 52
|
mpbid |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → ∀ 𝑖 ∈ 𝑍 ( 𝑛 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑛 ) ) ) |
54 |
53
|
r19.21bi |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝑛 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑛 ) ) ) |
55 |
54
|
imp |
⊢ ( ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑛 ≤ 𝑖 ) → ( 𝐹 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑛 ) ) |
56 |
46 42
|
syl |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ* ) |
57 |
39
|
adantr |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → 𝑟 ∈ ℝ* ) |
58 |
|
xrmax1 |
⊢ ( ( ( 𝐺 ‘ 𝑛 ) ∈ ℝ* ∧ 𝑟 ∈ ℝ* ) → ( 𝐺 ‘ 𝑛 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) |
59 |
56 57 58
|
syl2anc |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑛 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) |
60 |
50
|
ffvelrnda |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑖 ) ∈ ℝ* ) |
61 |
44
|
adantr |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ* ) |
62 |
|
xrletr |
⊢ ( ( ( 𝐹 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝐺 ‘ 𝑛 ) ∈ ℝ* ∧ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ* ) → ( ( ( 𝐹 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑛 ) ∧ ( 𝐺 ‘ 𝑛 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) → ( 𝐹 ‘ 𝑖 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) ) |
63 |
60 56 61 62
|
syl3anc |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑛 ) ∧ ( 𝐺 ‘ 𝑛 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) → ( 𝐹 ‘ 𝑖 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) ) |
64 |
59 63
|
mpan2d |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑛 ) → ( 𝐹 ‘ 𝑖 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) ) |
65 |
64
|
adantr |
⊢ ( ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑛 ≤ 𝑖 ) → ( ( 𝐹 ‘ 𝑖 ) ≤ ( 𝐺 ‘ 𝑛 ) → ( 𝐹 ‘ 𝑖 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) ) |
66 |
55 65
|
mpd |
⊢ ( ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑛 ≤ 𝑖 ) → ( 𝐹 ‘ 𝑖 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) |
67 |
|
fveq2 |
⊢ ( 𝑚 = 𝑖 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑖 ) ) |
68 |
67
|
breq1d |
⊢ ( 𝑚 = 𝑖 → ( ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ↔ ( 𝐹 ‘ 𝑖 ) ≤ 𝑟 ) ) |
69 |
|
simprr |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) |
70 |
69
|
ad2antrr |
⊢ ( ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑖 ≤ 𝑛 ) → ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) |
71 |
|
simpr |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ 𝑍 ) |
72 |
71 2
|
eleqtrdi |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
73 |
41
|
flcld |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → ( ⌊ ‘ 𝑛 ) ∈ ℤ ) |
74 |
73
|
adantr |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → ( ⌊ ‘ 𝑛 ) ∈ ℤ ) |
75 |
|
elfz5 |
⊢ ( ( 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( ⌊ ‘ 𝑛 ) ∈ ℤ ) → ( 𝑖 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ↔ 𝑖 ≤ ( ⌊ ‘ 𝑛 ) ) ) |
76 |
72 74 75
|
syl2anc |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝑖 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ↔ 𝑖 ≤ ( ⌊ ‘ 𝑛 ) ) ) |
77 |
11 71
|
sselid |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ ℤ ) |
78 |
|
flge |
⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑖 ∈ ℤ ) → ( 𝑖 ≤ 𝑛 ↔ 𝑖 ≤ ( ⌊ ‘ 𝑛 ) ) ) |
79 |
46 77 78
|
syl2anc |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝑖 ≤ 𝑛 ↔ 𝑖 ≤ ( ⌊ ‘ 𝑛 ) ) ) |
80 |
76 79
|
bitr4d |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝑖 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ↔ 𝑖 ≤ 𝑛 ) ) |
81 |
80
|
biimpar |
⊢ ( ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑖 ≤ 𝑛 ) → 𝑖 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ) |
82 |
68 70 81
|
rspcdva |
⊢ ( ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑖 ≤ 𝑛 ) → ( 𝐹 ‘ 𝑖 ) ≤ 𝑟 ) |
83 |
|
xrmax2 |
⊢ ( ( ( 𝐺 ‘ 𝑛 ) ∈ ℝ* ∧ 𝑟 ∈ ℝ* ) → 𝑟 ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) |
84 |
43 39 83
|
syl2anc |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → 𝑟 ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) |
85 |
84
|
adantr |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → 𝑟 ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) |
86 |
|
xrletr |
⊢ ( ( ( 𝐹 ‘ 𝑖 ) ∈ ℝ* ∧ 𝑟 ∈ ℝ* ∧ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ* ) → ( ( ( 𝐹 ‘ 𝑖 ) ≤ 𝑟 ∧ 𝑟 ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) → ( 𝐹 ‘ 𝑖 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) ) |
87 |
60 57 61 86
|
syl3anc |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑖 ) ≤ 𝑟 ∧ 𝑟 ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) → ( 𝐹 ‘ 𝑖 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) ) |
88 |
85 87
|
mpan2d |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑖 ) ≤ 𝑟 → ( 𝐹 ‘ 𝑖 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) ) |
89 |
88
|
adantr |
⊢ ( ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑖 ≤ 𝑛 ) → ( ( 𝐹 ‘ 𝑖 ) ≤ 𝑟 → ( 𝐹 ‘ 𝑖 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) ) |
90 |
82 89
|
mpd |
⊢ ( ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑖 ≤ 𝑛 ) → ( 𝐹 ‘ 𝑖 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) |
91 |
46 48 66 90
|
lecasei |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑖 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) |
92 |
91
|
a1d |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) ∧ 𝑖 ∈ 𝑍 ) → ( 𝑎 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) ) |
93 |
92
|
ralrimiva |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → ∀ 𝑖 ∈ 𝑍 ( 𝑎 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) ) |
94 |
1
|
limsupgle |
⊢ ( ( ( 𝑍 ⊆ ℝ ∧ 𝐹 : 𝑍 ⟶ ℝ* ) ∧ 𝑎 ∈ ℝ ∧ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ∈ ℝ* ) → ( ( 𝐺 ‘ 𝑎 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ↔ ∀ 𝑖 ∈ 𝑍 ( 𝑎 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) ) ) |
95 |
47 50 34 44 94
|
syl211anc |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → ( ( 𝐺 ‘ 𝑎 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ↔ ∀ 𝑖 ∈ 𝑍 ( 𝑎 ≤ 𝑖 → ( 𝐹 ‘ 𝑖 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) ) ) |
96 |
93 95
|
mpbird |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → ( 𝐺 ‘ 𝑎 ) ≤ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) ) |
97 |
38
|
ltpnfd |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → 𝑟 < +∞ ) |
98 |
|
simplrr |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → ( 𝐺 ‘ 𝑛 ) < +∞ ) |
99 |
|
breq1 |
⊢ ( 𝑟 = if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) → ( 𝑟 < +∞ ↔ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) < +∞ ) ) |
100 |
|
breq1 |
⊢ ( ( 𝐺 ‘ 𝑛 ) = if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) → ( ( 𝐺 ‘ 𝑛 ) < +∞ ↔ if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) < +∞ ) ) |
101 |
99 100
|
ifboth |
⊢ ( ( 𝑟 < +∞ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) → if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) < +∞ ) |
102 |
97 98 101
|
syl2anc |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → if ( ( 𝐺 ‘ 𝑛 ) ≤ 𝑟 , 𝑟 , ( 𝐺 ‘ 𝑛 ) ) < +∞ ) |
103 |
37 44 45 96 102
|
xrlelttrd |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) ∧ ( 𝑟 ∈ ℝ ∧ ∀ 𝑚 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑛 ) ) ( 𝐹 ‘ 𝑚 ) ≤ 𝑟 ) ) → ( 𝐺 ‘ 𝑎 ) < +∞ ) |
104 |
32 103
|
rexlimddv |
⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) ∧ ( 𝑛 ∈ ℝ ∧ ( 𝐺 ‘ 𝑛 ) < +∞ ) ) → ( 𝐺 ‘ 𝑎 ) < +∞ ) |
105 |
23 104
|
rexlimddv |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( 𝐺 ‘ 𝑎 ) < +∞ ) |
106 |
8 105
|
eqbrtrrd |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → sup ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) < +∞ ) |
107 |
|
imassrn |
⊢ ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ⊆ ran 𝐹 |
108 |
15
|
frnd |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ran 𝐹 ⊆ ℝ ) |
109 |
107 108
|
sstrid |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ⊆ ℝ ) |
110 |
109 16
|
sstrdi |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ⊆ ℝ* ) |
111 |
|
df-ss |
⊢ ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ⊆ ℝ* ↔ ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) = ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ) |
112 |
110 111
|
sylib |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) = ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ) |
113 |
112 109
|
eqsstrd |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ ) |
114 |
|
simpl1 |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝑀 ∈ ℤ ) |
115 |
|
flcl |
⊢ ( 𝑎 ∈ ℝ → ( ⌊ ‘ 𝑎 ) ∈ ℤ ) |
116 |
115
|
adantl |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( ⌊ ‘ 𝑎 ) ∈ ℤ ) |
117 |
116
|
peano2zd |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( ( ⌊ ‘ 𝑎 ) + 1 ) ∈ ℤ ) |
118 |
117 114
|
ifcld |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ℤ ) |
119 |
114
|
zred |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝑀 ∈ ℝ ) |
120 |
117
|
zred |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( ( ⌊ ‘ 𝑎 ) + 1 ) ∈ ℝ ) |
121 |
|
max1 |
⊢ ( ( 𝑀 ∈ ℝ ∧ ( ( ⌊ ‘ 𝑎 ) + 1 ) ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ) |
122 |
119 120 121
|
syl2anc |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ) |
123 |
|
eluz2 |
⊢ ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ℤ ∧ 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ) ) |
124 |
114 118 122 123
|
syl3anbrc |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) |
125 |
124 2
|
eleqtrrdi |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ 𝑍 ) |
126 |
15
|
fdmd |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → dom 𝐹 = 𝑍 ) |
127 |
125 126
|
eleqtrrd |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ dom 𝐹 ) |
128 |
118
|
zred |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ℝ ) |
129 |
|
fllep1 |
⊢ ( 𝑎 ∈ ℝ → 𝑎 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) ) |
130 |
129
|
adantl |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝑎 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) ) |
131 |
|
max2 |
⊢ ( ( 𝑀 ∈ ℝ ∧ ( ( ⌊ ‘ 𝑎 ) + 1 ) ∈ ℝ ) → ( ( ⌊ ‘ 𝑎 ) + 1 ) ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ) |
132 |
119 120 131
|
syl2anc |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( ( ⌊ ‘ 𝑎 ) + 1 ) ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ) |
133 |
33 120 128 130 132
|
letrd |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → 𝑎 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ) |
134 |
|
elicopnf |
⊢ ( 𝑎 ∈ ℝ → ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ( 𝑎 [,) +∞ ) ↔ ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ℝ ∧ 𝑎 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ) ) ) |
135 |
134
|
adantl |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ( 𝑎 [,) +∞ ) ↔ ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ℝ ∧ 𝑎 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ) ) ) |
136 |
128 133 135
|
mpbir2and |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ( 𝑎 [,) +∞ ) ) |
137 |
|
inelcm |
⊢ ( ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ dom 𝐹 ∧ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑎 ) + 1 ) , ( ( ⌊ ‘ 𝑎 ) + 1 ) , 𝑀 ) ∈ ( 𝑎 [,) +∞ ) ) → ( dom 𝐹 ∩ ( 𝑎 [,) +∞ ) ) ≠ ∅ ) |
138 |
127 136 137
|
syl2anc |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( dom 𝐹 ∩ ( 𝑎 [,) +∞ ) ) ≠ ∅ ) |
139 |
|
imadisj |
⊢ ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) = ∅ ↔ ( dom 𝐹 ∩ ( 𝑎 [,) +∞ ) ) = ∅ ) |
140 |
139
|
necon3bii |
⊢ ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ≠ ∅ ↔ ( dom 𝐹 ∩ ( 𝑎 [,) +∞ ) ) ≠ ∅ ) |
141 |
138 140
|
sylibr |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ≠ ∅ ) |
142 |
112 141
|
eqnetrd |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) |
143 |
|
supxrre1 |
⊢ ( ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ ∧ ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) ≠ ∅ ) → ( sup ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ ↔ sup ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) < +∞ ) ) |
144 |
113 142 143
|
syl2anc |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( sup ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ ↔ sup ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) < +∞ ) ) |
145 |
106 144
|
mpbird |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → sup ( ( ( 𝐹 “ ( 𝑎 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ∈ ℝ ) |
146 |
8 145
|
eqeltrd |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) ∧ 𝑎 ∈ ℝ ) → ( 𝐺 ‘ 𝑎 ) ∈ ℝ ) |
147 |
5 6 146
|
fmpt2d |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( lim sup ‘ 𝐹 ) < +∞ ) → 𝐺 : ℝ ⟶ ℝ ) |