| 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
|
sseldi |
⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( 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
|
sseldi |
⊢ ( ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ ℝ ∧ ( 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 ‘ 𝐹 ) < +∞ ) → 𝐺 : ℝ ⟶ ℝ ) |