Step | Hyp | Ref
| Expression |
1 | | xrltso 11850 |
. . . 4
⊢ < Or
ℝ* |
2 | 1 | supex 8252 |
. . 3
⊢
sup(((𝐹 “
(𝑘[,)+∞)) ∩
ℝ*), ℝ*, < ) ∈ V |
3 | 2 | a1i 11 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑘 ∈ ℝ) →
sup(((𝐹 “ (𝑘[,)+∞)) ∩
ℝ*), ℝ*, < ) ∈ V) |
4 | | limsupval.1 |
. . 3
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
5 | 4 | a1i 11 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) → 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < ))) |
6 | 4 | limsupgval 14055 |
. . . 4
⊢ (𝑎 ∈ ℝ → (𝐺‘𝑎) = sup(((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
7 | 6 | adantl 481 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐺‘𝑎) = sup(((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
8 | | simpl3 1059 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (lim
sup‘𝐹) <
+∞) |
9 | | limsupgre.z |
. . . . . . . . . . 11
⊢ 𝑍 =
(ℤ≥‘𝑀) |
10 | | uzssz 11583 |
. . . . . . . . . . 11
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
11 | 9, 10 | eqsstri 3598 |
. . . . . . . . . 10
⊢ 𝑍 ⊆
ℤ |
12 | | zssre 11261 |
. . . . . . . . . 10
⊢ ℤ
⊆ ℝ |
13 | 11, 12 | sstri 3577 |
. . . . . . . . 9
⊢ 𝑍 ⊆
ℝ |
14 | 13 | a1i 11 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑍 ⊆
ℝ) |
15 | | simpl2 1058 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝐹:𝑍⟶ℝ) |
16 | | ressxr 9962 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ* |
17 | | fss 5969 |
. . . . . . . . 9
⊢ ((𝐹:𝑍⟶ℝ ∧ ℝ ⊆
ℝ*) → 𝐹:𝑍⟶ℝ*) |
18 | 15, 16, 17 | sylancl 693 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝐹:𝑍⟶ℝ*) |
19 | | pnfxr 9971 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
20 | 19 | a1i 11 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → +∞
∈ ℝ*) |
21 | 4 | limsuplt 14058 |
. . . . . . . 8
⊢ ((𝑍 ⊆ ℝ ∧ 𝐹:𝑍⟶ℝ* ∧ +∞
∈ ℝ*) → ((lim sup‘𝐹) < +∞ ↔ ∃𝑛 ∈ ℝ (𝐺‘𝑛) < +∞)) |
22 | 14, 18, 20, 21 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ((lim
sup‘𝐹) < +∞
↔ ∃𝑛 ∈
ℝ (𝐺‘𝑛) <
+∞)) |
23 | 8, 22 | mpbid 221 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
∃𝑛 ∈ ℝ
(𝐺‘𝑛) < +∞) |
24 | | fzfi 12633 |
. . . . . . . 8
⊢ (𝑀...(⌊‘𝑛)) ∈ Fin |
25 | 15 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺‘𝑛) < +∞)) → 𝐹:𝑍⟶ℝ) |
26 | | elfzuz 12209 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (𝑀...(⌊‘𝑛)) → 𝑚 ∈ (ℤ≥‘𝑀)) |
27 | 26, 9 | syl6eleqr 2699 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (𝑀...(⌊‘𝑛)) → 𝑚 ∈ 𝑍) |
28 | | ffvelrn 6265 |
. . . . . . . . . 10
⊢ ((𝐹:𝑍⟶ℝ ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ ℝ) |
29 | 25, 27, 28 | syl2an 493 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ 𝑚 ∈ (𝑀...(⌊‘𝑛))) → (𝐹‘𝑚) ∈ ℝ) |
30 | 29 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺‘𝑛) < +∞)) → ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ∈ ℝ) |
31 | | fimaxre3 10849 |
. . . . . . . 8
⊢ (((𝑀...(⌊‘𝑛)) ∈ Fin ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ∈ ℝ) → ∃𝑟 ∈ ℝ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟) |
32 | 24, 30, 31 | sylancr 694 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺‘𝑛) < +∞)) → ∃𝑟 ∈ ℝ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟) |
33 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑎 ∈
ℝ) |
34 | 33 | ad2antrr 758 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → 𝑎 ∈ ℝ) |
35 | 4 | limsupgf 14054 |
. . . . . . . . . 10
⊢ 𝐺:ℝ⟶ℝ* |
36 | 35 | ffvelrni 6266 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℝ → (𝐺‘𝑎) ∈
ℝ*) |
37 | 34, 36 | syl 17 |
. . . . . . . 8
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → (𝐺‘𝑎) ∈
ℝ*) |
38 | | simprl 790 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → 𝑟 ∈ ℝ) |
39 | 16, 38 | sseldi 3566 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → 𝑟 ∈ ℝ*) |
40 | | simprl 790 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺‘𝑛) < +∞)) → 𝑛 ∈ ℝ) |
41 | 40 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → 𝑛 ∈ ℝ) |
42 | 35 | ffvelrni 6266 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ → (𝐺‘𝑛) ∈
ℝ*) |
43 | 41, 42 | syl 17 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → (𝐺‘𝑛) ∈
ℝ*) |
44 | 39, 43 | ifcld 4081 |
. . . . . . . 8
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) ∈
ℝ*) |
45 | 19 | a1i 11 |
. . . . . . . 8
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → +∞ ∈
ℝ*) |
46 | 40 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → 𝑛 ∈ ℝ) |
47 | 13 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → 𝑍 ⊆ ℝ) |
48 | 47 | sselda 3568 |
. . . . . . . . . . . 12
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℝ) |
49 | | xrleid 11859 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺‘𝑛) ∈ ℝ* → (𝐺‘𝑛) ≤ (𝐺‘𝑛)) |
50 | 43, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → (𝐺‘𝑛) ≤ (𝐺‘𝑛)) |
51 | 18 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → 𝐹:𝑍⟶ℝ*) |
52 | 4 | limsupgle 14056 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑍 ⊆ ℝ ∧ 𝐹:𝑍⟶ℝ*) ∧ 𝑛 ∈ ℝ ∧ (𝐺‘𝑛) ∈ ℝ*) → ((𝐺‘𝑛) ≤ (𝐺‘𝑛) ↔ ∀𝑖 ∈ 𝑍 (𝑛 ≤ 𝑖 → (𝐹‘𝑖) ≤ (𝐺‘𝑛)))) |
53 | 47, 51, 41, 43, 52 | syl211anc 1324 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → ((𝐺‘𝑛) ≤ (𝐺‘𝑛) ↔ ∀𝑖 ∈ 𝑍 (𝑛 ≤ 𝑖 → (𝐹‘𝑖) ≤ (𝐺‘𝑛)))) |
54 | 50, 53 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → ∀𝑖 ∈ 𝑍 (𝑛 ≤ 𝑖 → (𝐹‘𝑖) ≤ (𝐺‘𝑛))) |
55 | 54 | r19.21bi 2916 |
. . . . . . . . . . . . . 14
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝑛 ≤ 𝑖 → (𝐹‘𝑖) ≤ (𝐺‘𝑛))) |
56 | 55 | imp 444 |
. . . . . . . . . . . . 13
⊢
(((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ≤ 𝑖) → (𝐹‘𝑖) ≤ (𝐺‘𝑛)) |
57 | 46, 42 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝐺‘𝑛) ∈
ℝ*) |
58 | 39 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → 𝑟 ∈ ℝ*) |
59 | | xrmax1 11880 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺‘𝑛) ∈ ℝ* ∧ 𝑟 ∈ ℝ*)
→ (𝐺‘𝑛) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
60 | 57, 58, 59 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝐺‘𝑛) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
61 | 51 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ∈
ℝ*) |
62 | 44 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) ∈
ℝ*) |
63 | | xrletr 11865 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑖) ∈ ℝ* ∧ (𝐺‘𝑛) ∈ ℝ* ∧ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) ∈ ℝ*) →
(((𝐹‘𝑖) ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
64 | 61, 57, 62, 63 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (((𝐹‘𝑖) ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
65 | 60, 64 | mpan2d 706 |
. . . . . . . . . . . . . 14
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → ((𝐹‘𝑖) ≤ (𝐺‘𝑛) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
66 | 65 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ≤ 𝑖) → ((𝐹‘𝑖) ≤ (𝐺‘𝑛) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
67 | 56, 66 | mpd 15 |
. . . . . . . . . . . 12
⊢
(((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ≤ 𝑖) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
68 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍) |
69 | 68, 9 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ (ℤ≥‘𝑀)) |
70 | 41 | flcld 12461 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → (⌊‘𝑛) ∈ ℤ) |
71 | 70 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (⌊‘𝑛) ∈ ℤ) |
72 | | elfz5 12205 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈
(ℤ≥‘𝑀) ∧ (⌊‘𝑛) ∈ ℤ) → (𝑖 ∈ (𝑀...(⌊‘𝑛)) ↔ 𝑖 ≤ (⌊‘𝑛))) |
73 | 69, 71, 72 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝑖 ∈ (𝑀...(⌊‘𝑛)) ↔ 𝑖 ≤ (⌊‘𝑛))) |
74 | 11, 68 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℤ) |
75 | | flge 12468 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℝ ∧ 𝑖 ∈ ℤ) → (𝑖 ≤ 𝑛 ↔ 𝑖 ≤ (⌊‘𝑛))) |
76 | 46, 74, 75 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝑖 ≤ 𝑛 ↔ 𝑖 ≤ (⌊‘𝑛))) |
77 | 73, 76 | bitr4d 270 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝑖 ∈ (𝑀...(⌊‘𝑛)) ↔ 𝑖 ≤ 𝑛)) |
78 | 77 | biimpar 501 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) ∧ 𝑖 ≤ 𝑛) → 𝑖 ∈ (𝑀...(⌊‘𝑛))) |
79 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟) |
80 | 79 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) ∧ 𝑖 ≤ 𝑛) → ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟) |
81 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑖 → (𝐹‘𝑚) = (𝐹‘𝑖)) |
82 | 81 | breq1d 4593 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑖 → ((𝐹‘𝑚) ≤ 𝑟 ↔ (𝐹‘𝑖) ≤ 𝑟)) |
83 | 82 | rspcv 3278 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑀...(⌊‘𝑛)) → (∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟 → (𝐹‘𝑖) ≤ 𝑟)) |
84 | 78, 80, 83 | sylc 63 |
. . . . . . . . . . . . 13
⊢
(((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) ∧ 𝑖 ≤ 𝑛) → (𝐹‘𝑖) ≤ 𝑟) |
85 | | xrmax2 11881 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺‘𝑛) ∈ ℝ* ∧ 𝑟 ∈ ℝ*)
→ 𝑟 ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
86 | 43, 39, 85 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → 𝑟 ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
87 | 86 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → 𝑟 ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
88 | | xrletr 11865 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑖) ∈ ℝ* ∧ 𝑟 ∈ ℝ*
∧ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) ∈ ℝ*) →
(((𝐹‘𝑖) ≤ 𝑟 ∧ 𝑟 ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
89 | 61, 58, 62, 88 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (((𝐹‘𝑖) ≤ 𝑟 ∧ 𝑟 ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
90 | 87, 89 | mpan2d 706 |
. . . . . . . . . . . . . 14
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → ((𝐹‘𝑖) ≤ 𝑟 → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
91 | 90 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) ∧ 𝑖 ≤ 𝑛) → ((𝐹‘𝑖) ≤ 𝑟 → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
92 | 84, 91 | mpd 15 |
. . . . . . . . . . . 12
⊢
(((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) ∧ 𝑖 ≤ 𝑛) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
93 | 46, 48, 67, 92 | lecasei 10022 |
. . . . . . . . . . 11
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
94 | 93 | a1d 25 |
. . . . . . . . . 10
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝑎 ≤ 𝑖 → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
95 | 94 | ralrimiva 2949 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → ∀𝑖 ∈ 𝑍 (𝑎 ≤ 𝑖 → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
96 | 4 | limsupgle 14056 |
. . . . . . . . . 10
⊢ (((𝑍 ⊆ ℝ ∧ 𝐹:𝑍⟶ℝ*) ∧ 𝑎 ∈ ℝ ∧ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) ∈ ℝ*) → ((𝐺‘𝑎) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) ↔ ∀𝑖 ∈ 𝑍 (𝑎 ≤ 𝑖 → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))))) |
97 | 47, 51, 34, 44, 96 | syl211anc 1324 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → ((𝐺‘𝑎) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) ↔ ∀𝑖 ∈ 𝑍 (𝑎 ≤ 𝑖 → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))))) |
98 | 95, 97 | mpbird 246 |
. . . . . . . 8
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → (𝐺‘𝑎) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
99 | 38 | ltpnfd 11831 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → 𝑟 < +∞) |
100 | | simplrr 797 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → (𝐺‘𝑛) < +∞) |
101 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑟 = if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) → (𝑟 < +∞ ↔ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) < +∞)) |
102 | | breq1 4586 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑛) = if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) → ((𝐺‘𝑛) < +∞ ↔ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) < +∞)) |
103 | 101, 102 | ifboth 4074 |
. . . . . . . . 9
⊢ ((𝑟 < +∞ ∧ (𝐺‘𝑛) < +∞) → if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) < +∞) |
104 | 99, 100, 103 | syl2anc 691 |
. . . . . . . 8
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) < +∞) |
105 | 37, 44, 45, 98, 104 | xrlelttrd 11867 |
. . . . . . 7
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → (𝐺‘𝑎) < +∞) |
106 | 32, 105 | rexlimddv 3017 |
. . . . . 6
⊢ ((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺‘𝑛) < +∞)) → (𝐺‘𝑎) < +∞) |
107 | 23, 106 | rexlimddv 3017 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐺‘𝑎) < +∞) |
108 | 7, 107 | eqbrtrrd 4607 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
sup(((𝐹 “ (𝑎[,)+∞)) ∩
ℝ*), ℝ*, < ) <
+∞) |
109 | | imassrn 5396 |
. . . . . . . . 9
⊢ (𝐹 “ (𝑎[,)+∞)) ⊆ ran 𝐹 |
110 | | frn 5966 |
. . . . . . . . . 10
⊢ (𝐹:𝑍⟶ℝ → ran 𝐹 ⊆ ℝ) |
111 | 15, 110 | syl 17 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ran
𝐹 ⊆
ℝ) |
112 | 109, 111 | syl5ss 3579 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐹 “ (𝑎[,)+∞)) ⊆
ℝ) |
113 | 112, 16 | syl6ss 3580 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐹 “ (𝑎[,)+∞)) ⊆
ℝ*) |
114 | | df-ss 3554 |
. . . . . . 7
⊢ ((𝐹 “ (𝑎[,)+∞)) ⊆ ℝ*
↔ ((𝐹 “ (𝑎[,)+∞)) ∩
ℝ*) = (𝐹
“ (𝑎[,)+∞))) |
115 | 113, 114 | sylib 207 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*) =
(𝐹 “ (𝑎[,)+∞))) |
116 | 115, 112 | eqsstrd 3602 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*)
⊆ ℝ) |
117 | | simpl1 1057 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑀 ∈
ℤ) |
118 | | flcl 12458 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℝ →
(⌊‘𝑎) ∈
ℤ) |
119 | 118 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
(⌊‘𝑎) ∈
ℤ) |
120 | 119 | peano2zd 11361 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
((⌊‘𝑎) + 1)
∈ ℤ) |
121 | 120, 117 | ifcld 4081 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ ℤ) |
122 | 117 | zred 11358 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑀 ∈
ℝ) |
123 | 120 | zred 11358 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
((⌊‘𝑎) + 1)
∈ ℝ) |
124 | | max1 11890 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℝ ∧
((⌊‘𝑎) + 1)
∈ ℝ) → 𝑀
≤ if(𝑀 ≤
((⌊‘𝑎) + 1),
((⌊‘𝑎) + 1),
𝑀)) |
125 | 122, 123,
124 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀)) |
126 | | eluz2 11569 |
. . . . . . . . . . 11
⊢ (if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ ℤ ∧ 𝑀 ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀))) |
127 | 117, 121,
125, 126 | syl3anbrc 1239 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ (ℤ≥‘𝑀)) |
128 | 127, 9 | syl6eleqr 2699 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ 𝑍) |
129 | | fdm 5964 |
. . . . . . . . . 10
⊢ (𝐹:𝑍⟶ℝ → dom 𝐹 = 𝑍) |
130 | 15, 129 | syl 17 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → dom
𝐹 = 𝑍) |
131 | 128, 130 | eleqtrrd 2691 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ dom 𝐹) |
132 | 121 | zred 11358 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ ℝ) |
133 | | fllep1 12464 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℝ → 𝑎 ≤ ((⌊‘𝑎) + 1)) |
134 | 133 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑎 ≤ ((⌊‘𝑎) + 1)) |
135 | | max2 11892 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℝ ∧
((⌊‘𝑎) + 1)
∈ ℝ) → ((⌊‘𝑎) + 1) ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀)) |
136 | 122, 123,
135 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
((⌊‘𝑎) + 1)
≤ if(𝑀 ≤
((⌊‘𝑎) + 1),
((⌊‘𝑎) + 1),
𝑀)) |
137 | 33, 123, 132, 134, 136 | letrd 10073 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑎 ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀)) |
138 | | elicopnf 12140 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℝ → (if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ (𝑎[,)+∞) ↔ (if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ ℝ ∧ 𝑎 ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀)))) |
139 | 138 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
(if(𝑀 ≤
((⌊‘𝑎) + 1),
((⌊‘𝑎) + 1),
𝑀) ∈ (𝑎[,)+∞) ↔ (if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ ℝ ∧ 𝑎 ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀)))) |
140 | 132, 137,
139 | mpbir2and 959 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ (𝑎[,)+∞)) |
141 | | inelcm 3984 |
. . . . . . . 8
⊢
((if(𝑀 ≤
((⌊‘𝑎) + 1),
((⌊‘𝑎) + 1),
𝑀) ∈ dom 𝐹 ∧ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ (𝑎[,)+∞)) → (dom 𝐹 ∩ (𝑎[,)+∞)) ≠ ∅) |
142 | 131, 140,
141 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (dom
𝐹 ∩ (𝑎[,)+∞)) ≠ ∅) |
143 | | imadisj 5403 |
. . . . . . . 8
⊢ ((𝐹 “ (𝑎[,)+∞)) = ∅ ↔ (dom 𝐹 ∩ (𝑎[,)+∞)) = ∅) |
144 | 143 | necon3bii 2834 |
. . . . . . 7
⊢ ((𝐹 “ (𝑎[,)+∞)) ≠ ∅ ↔ (dom 𝐹 ∩ (𝑎[,)+∞)) ≠ ∅) |
145 | 142, 144 | sylibr 223 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐹 “ (𝑎[,)+∞)) ≠ ∅) |
146 | 115, 145 | eqnetrd 2849 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*) ≠
∅) |
147 | | supxrre1 12032 |
. . . . 5
⊢ ((((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*)
⊆ ℝ ∧ ((𝐹
“ (𝑎[,)+∞))
∩ ℝ*) ≠ ∅) → (sup(((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*),
ℝ*, < ) ∈ ℝ ↔ sup(((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*),
ℝ*, < ) < +∞)) |
148 | 116, 146,
147 | syl2anc 691 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
(sup(((𝐹 “ (𝑎[,)+∞)) ∩
ℝ*), ℝ*, < ) ∈ ℝ ↔
sup(((𝐹 “ (𝑎[,)+∞)) ∩
ℝ*), ℝ*, < ) <
+∞)) |
149 | 108, 148 | mpbird 246 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
sup(((𝐹 “ (𝑎[,)+∞)) ∩
ℝ*), ℝ*, < ) ∈
ℝ) |
150 | 7, 149 | eqeltrd 2688 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐺‘𝑎) ∈ ℝ) |
151 | 3, 5, 150 | fmpt2d 6300 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) → 𝐺:ℝ⟶ℝ) |