Step | Hyp | Ref
| Expression |
1 | | xrltso 12617 |
. . . 4
⊢ < Or
ℝ* |
2 | 1 | supex 9000 |
. . 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 14923 |
. . . 4
⊢ (𝑎 ∈ ℝ → (𝐺‘𝑎) = sup(((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
7 | 6 | adantl 485 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐺‘𝑎) = sup(((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
8 | | simpl3 1194 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (lim
sup‘𝐹) <
+∞) |
9 | | limsupgre.z |
. . . . . . . . . . 11
⊢ 𝑍 =
(ℤ≥‘𝑀) |
10 | | uzssz 12345 |
. . . . . . . . . . 11
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
11 | 9, 10 | eqsstri 3911 |
. . . . . . . . . 10
⊢ 𝑍 ⊆
ℤ |
12 | | zssre 12069 |
. . . . . . . . . 10
⊢ ℤ
⊆ ℝ |
13 | 11, 12 | sstri 3886 |
. . . . . . . . 9
⊢ 𝑍 ⊆
ℝ |
14 | 13 | a1i 11 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑍 ⊆
ℝ) |
15 | | simpl2 1193 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝐹:𝑍⟶ℝ) |
16 | | ressxr 10763 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ* |
17 | | fss 6521 |
. . . . . . . . 9
⊢ ((𝐹:𝑍⟶ℝ ∧ ℝ ⊆
ℝ*) → 𝐹:𝑍⟶ℝ*) |
18 | 15, 16, 17 | sylancl 589 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝐹:𝑍⟶ℝ*) |
19 | | pnfxr 10773 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
20 | 19 | a1i 11 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → +∞
∈ ℝ*) |
21 | 4 | limsuplt 14926 |
. . . . . . . 8
⊢ ((𝑍 ⊆ ℝ ∧ 𝐹:𝑍⟶ℝ* ∧ +∞
∈ ℝ*) → ((lim sup‘𝐹) < +∞ ↔ ∃𝑛 ∈ ℝ (𝐺‘𝑛) < +∞)) |
22 | 14, 18, 20, 21 | syl3anc 1372 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ((lim
sup‘𝐹) < +∞
↔ ∃𝑛 ∈
ℝ (𝐺‘𝑛) <
+∞)) |
23 | 8, 22 | mpbid 235 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
∃𝑛 ∈ ℝ
(𝐺‘𝑛) < +∞) |
24 | | fzfi 13431 |
. . . . . . . 8
⊢ (𝑀...(⌊‘𝑛)) ∈ Fin |
25 | 15 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺‘𝑛) < +∞)) → 𝐹:𝑍⟶ℝ) |
26 | | elfzuz 12994 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (𝑀...(⌊‘𝑛)) → 𝑚 ∈ (ℤ≥‘𝑀)) |
27 | 26, 9 | eleqtrrdi 2844 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (𝑀...(⌊‘𝑛)) → 𝑚 ∈ 𝑍) |
28 | | ffvelrn 6859 |
. . . . . . . . . 10
⊢ ((𝐹:𝑍⟶ℝ ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ ℝ) |
29 | 25, 27, 28 | syl2an 599 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ 𝑚 ∈ (𝑀...(⌊‘𝑛))) → (𝐹‘𝑚) ∈ ℝ) |
30 | 29 | ralrimiva 3096 |
. . . . . . . 8
⊢ ((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺‘𝑛) < +∞)) → ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ∈ ℝ) |
31 | | fimaxre3 11664 |
. . . . . . . 8
⊢ (((𝑀...(⌊‘𝑛)) ∈ Fin ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ∈ ℝ) → ∃𝑟 ∈ ℝ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟) |
32 | 24, 30, 31 | sylancr 590 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺‘𝑛) < +∞)) → ∃𝑟 ∈ ℝ ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟) |
33 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑎 ∈
ℝ) |
34 | 33 | ad2antrr 726 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → 𝑎 ∈ ℝ) |
35 | 4 | limsupgf 14922 |
. . . . . . . . . 10
⊢ 𝐺:ℝ⟶ℝ* |
36 | 35 | ffvelrni 6860 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℝ → (𝐺‘𝑎) ∈
ℝ*) |
37 | 34, 36 | syl 17 |
. . . . . . . 8
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → (𝐺‘𝑎) ∈
ℝ*) |
38 | | simprl 771 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → 𝑟 ∈ ℝ) |
39 | 16, 38 | sseldi 3875 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → 𝑟 ∈ ℝ*) |
40 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺‘𝑛) < +∞)) → 𝑛 ∈ ℝ) |
41 | 40 | adantr 484 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → 𝑛 ∈ ℝ) |
42 | 35 | ffvelrni 6860 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ → (𝐺‘𝑛) ∈
ℝ*) |
43 | 41, 42 | syl 17 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → (𝐺‘𝑛) ∈
ℝ*) |
44 | 39, 43 | ifcld 4460 |
. . . . . . . 8
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) ∈
ℝ*) |
45 | 19 | a1i 11 |
. . . . . . . 8
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → +∞ ∈
ℝ*) |
46 | 40 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → 𝑛 ∈ ℝ) |
47 | 13 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → 𝑍 ⊆ ℝ) |
48 | 47 | sselda 3877 |
. . . . . . . . . . . 12
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℝ) |
49 | 43 | xrleidd 12628 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → (𝐺‘𝑛) ≤ (𝐺‘𝑛)) |
50 | 18 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → 𝐹:𝑍⟶ℝ*) |
51 | 4 | limsupgle 14924 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑍 ⊆ ℝ ∧ 𝐹:𝑍⟶ℝ*) ∧ 𝑛 ∈ ℝ ∧ (𝐺‘𝑛) ∈ ℝ*) → ((𝐺‘𝑛) ≤ (𝐺‘𝑛) ↔ ∀𝑖 ∈ 𝑍 (𝑛 ≤ 𝑖 → (𝐹‘𝑖) ≤ (𝐺‘𝑛)))) |
52 | 47, 50, 41, 43, 51 | syl211anc 1377 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → ((𝐺‘𝑛) ≤ (𝐺‘𝑛) ↔ ∀𝑖 ∈ 𝑍 (𝑛 ≤ 𝑖 → (𝐹‘𝑖) ≤ (𝐺‘𝑛)))) |
53 | 49, 52 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → ∀𝑖 ∈ 𝑍 (𝑛 ≤ 𝑖 → (𝐹‘𝑖) ≤ (𝐺‘𝑛))) |
54 | 53 | r19.21bi 3121 |
. . . . . . . . . . . . . 14
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝑛 ≤ 𝑖 → (𝐹‘𝑖) ≤ (𝐺‘𝑛))) |
55 | 54 | imp 410 |
. . . . . . . . . . . . 13
⊢
(((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ≤ 𝑖) → (𝐹‘𝑖) ≤ (𝐺‘𝑛)) |
56 | 46, 42 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝐺‘𝑛) ∈
ℝ*) |
57 | 39 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → 𝑟 ∈ ℝ*) |
58 | | xrmax1 12651 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺‘𝑛) ∈ ℝ* ∧ 𝑟 ∈ ℝ*)
→ (𝐺‘𝑛) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
59 | 56, 57, 58 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝐺‘𝑛) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
60 | 50 | ffvelrnda 6861 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ∈
ℝ*) |
61 | 44 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) ∈
ℝ*) |
62 | | xrletr 12634 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑖) ∈ ℝ* ∧ (𝐺‘𝑛) ∈ ℝ* ∧ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) ∈ ℝ*) →
(((𝐹‘𝑖) ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
63 | 60, 56, 61, 62 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (((𝐹‘𝑖) ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
64 | 59, 63 | mpan2d 694 |
. . . . . . . . . . . . . 14
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → ((𝐹‘𝑖) ≤ (𝐺‘𝑛) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
65 | 64 | adantr 484 |
. . . . . . . . . . . . 13
⊢
(((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ≤ 𝑖) → ((𝐹‘𝑖) ≤ (𝐺‘𝑛) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
66 | 55, 65 | mpd 15 |
. . . . . . . . . . . 12
⊢
(((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 ≤ 𝑖) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
67 | | fveq2 6674 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑖 → (𝐹‘𝑚) = (𝐹‘𝑖)) |
68 | 67 | breq1d 5040 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑖 → ((𝐹‘𝑚) ≤ 𝑟 ↔ (𝐹‘𝑖) ≤ 𝑟)) |
69 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟) |
70 | 69 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) ∧ 𝑖 ≤ 𝑛) → ∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟) |
71 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍) |
72 | 71, 9 | eleqtrdi 2843 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ (ℤ≥‘𝑀)) |
73 | 41 | flcld 13259 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → (⌊‘𝑛) ∈ ℤ) |
74 | 73 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (⌊‘𝑛) ∈ ℤ) |
75 | | elfz5 12990 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈
(ℤ≥‘𝑀) ∧ (⌊‘𝑛) ∈ ℤ) → (𝑖 ∈ (𝑀...(⌊‘𝑛)) ↔ 𝑖 ≤ (⌊‘𝑛))) |
76 | 72, 74, 75 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝑖 ∈ (𝑀...(⌊‘𝑛)) ↔ 𝑖 ≤ (⌊‘𝑛))) |
77 | 11, 71 | sseldi 3875 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ ℤ) |
78 | | flge 13266 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℝ ∧ 𝑖 ∈ ℤ) → (𝑖 ≤ 𝑛 ↔ 𝑖 ≤ (⌊‘𝑛))) |
79 | 46, 77, 78 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝑖 ≤ 𝑛 ↔ 𝑖 ≤ (⌊‘𝑛))) |
80 | 76, 79 | bitr4d 285 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝑖 ∈ (𝑀...(⌊‘𝑛)) ↔ 𝑖 ≤ 𝑛)) |
81 | 80 | biimpar 481 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) ∧ 𝑖 ≤ 𝑛) → 𝑖 ∈ (𝑀...(⌊‘𝑛))) |
82 | 68, 70, 81 | rspcdva 3528 |
. . . . . . . . . . . . 13
⊢
(((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) ∧ 𝑖 ≤ 𝑛) → (𝐹‘𝑖) ≤ 𝑟) |
83 | | xrmax2 12652 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺‘𝑛) ∈ ℝ* ∧ 𝑟 ∈ ℝ*)
→ 𝑟 ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
84 | 43, 39, 83 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → 𝑟 ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
85 | 84 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → 𝑟 ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
86 | | xrletr 12634 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑖) ∈ ℝ* ∧ 𝑟 ∈ ℝ*
∧ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) ∈ ℝ*) →
(((𝐹‘𝑖) ≤ 𝑟 ∧ 𝑟 ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
87 | 60, 57, 61, 86 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (((𝐹‘𝑖) ≤ 𝑟 ∧ 𝑟 ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
88 | 85, 87 | mpan2d 694 |
. . . . . . . . . . . . . 14
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → ((𝐹‘𝑖) ≤ 𝑟 → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
89 | 88 | adantr 484 |
. . . . . . . . . . . . 13
⊢
(((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) ∧ 𝑖 ≤ 𝑛) → ((𝐹‘𝑖) ≤ 𝑟 → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
90 | 82, 89 | mpd 15 |
. . . . . . . . . . . 12
⊢
(((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) ∧ 𝑖 ≤ 𝑛) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
91 | 46, 48, 66, 90 | lecasei 10824 |
. . . . . . . . . . 11
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
92 | 91 | a1d 25 |
. . . . . . . . . 10
⊢
((((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) ∧ 𝑖 ∈ 𝑍) → (𝑎 ≤ 𝑖 → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
93 | 92 | ralrimiva 3096 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → ∀𝑖 ∈ 𝑍 (𝑎 ≤ 𝑖 → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)))) |
94 | 4 | limsupgle 14924 |
. . . . . . . . . 10
⊢ (((𝑍 ⊆ ℝ ∧ 𝐹:𝑍⟶ℝ*) ∧ 𝑎 ∈ ℝ ∧ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) ∈ ℝ*) → ((𝐺‘𝑎) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) ↔ ∀𝑖 ∈ 𝑍 (𝑎 ≤ 𝑖 → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))))) |
95 | 47, 50, 34, 44, 94 | syl211anc 1377 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → ((𝐺‘𝑎) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) ↔ ∀𝑖 ∈ 𝑍 (𝑎 ≤ 𝑖 → (𝐹‘𝑖) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))))) |
96 | 93, 95 | mpbird 260 |
. . . . . . . 8
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → (𝐺‘𝑎) ≤ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛))) |
97 | 38 | ltpnfd 12599 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → 𝑟 < +∞) |
98 | | simplrr 778 |
. . . . . . . . 9
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → (𝐺‘𝑛) < +∞) |
99 | | breq1 5033 |
. . . . . . . . . 10
⊢ (𝑟 = if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) → (𝑟 < +∞ ↔ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) < +∞)) |
100 | | breq1 5033 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑛) = if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) → ((𝐺‘𝑛) < +∞ ↔ if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) < +∞)) |
101 | 99, 100 | ifboth 4453 |
. . . . . . . . 9
⊢ ((𝑟 < +∞ ∧ (𝐺‘𝑛) < +∞) → if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) < +∞) |
102 | 97, 98, 101 | syl2anc 587 |
. . . . . . . 8
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → if((𝐺‘𝑛) ≤ 𝑟, 𝑟, (𝐺‘𝑛)) < +∞) |
103 | 37, 44, 45, 96, 102 | xrlelttrd 12636 |
. . . . . . 7
⊢
(((((𝑀 ∈
ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim
sup‘𝐹) < +∞)
∧ 𝑎 ∈ ℝ)
∧ (𝑛 ∈ ℝ
∧ (𝐺‘𝑛) < +∞)) ∧ (𝑟 ∈ ℝ ∧
∀𝑚 ∈ (𝑀...(⌊‘𝑛))(𝐹‘𝑚) ≤ 𝑟)) → (𝐺‘𝑎) < +∞) |
104 | 32, 103 | rexlimddv 3201 |
. . . . . 6
⊢ ((((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) ∧ (𝑛 ∈ ℝ ∧ (𝐺‘𝑛) < +∞)) → (𝐺‘𝑎) < +∞) |
105 | 23, 104 | rexlimddv 3201 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐺‘𝑎) < +∞) |
106 | 7, 105 | eqbrtrrd 5054 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
sup(((𝐹 “ (𝑎[,)+∞)) ∩
ℝ*), ℝ*, < ) <
+∞) |
107 | | imassrn 5914 |
. . . . . . . . 9
⊢ (𝐹 “ (𝑎[,)+∞)) ⊆ ran 𝐹 |
108 | 15 | frnd 6512 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ran
𝐹 ⊆
ℝ) |
109 | 107, 108 | sstrid 3888 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐹 “ (𝑎[,)+∞)) ⊆
ℝ) |
110 | 109, 16 | sstrdi 3889 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐹 “ (𝑎[,)+∞)) ⊆
ℝ*) |
111 | | df-ss 3860 |
. . . . . . 7
⊢ ((𝐹 “ (𝑎[,)+∞)) ⊆ ℝ*
↔ ((𝐹 “ (𝑎[,)+∞)) ∩
ℝ*) = (𝐹
“ (𝑎[,)+∞))) |
112 | 110, 111 | sylib 221 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*) =
(𝐹 “ (𝑎[,)+∞))) |
113 | 112, 109 | eqsstrd 3915 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*)
⊆ ℝ) |
114 | | simpl1 1192 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑀 ∈
ℤ) |
115 | | flcl 13256 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℝ →
(⌊‘𝑎) ∈
ℤ) |
116 | 115 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
(⌊‘𝑎) ∈
ℤ) |
117 | 116 | peano2zd 12171 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
((⌊‘𝑎) + 1)
∈ ℤ) |
118 | 117, 114 | ifcld 4460 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ ℤ) |
119 | 114 | zred 12168 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑀 ∈
ℝ) |
120 | 117 | zred 12168 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
((⌊‘𝑎) + 1)
∈ ℝ) |
121 | | max1 12661 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℝ ∧
((⌊‘𝑎) + 1)
∈ ℝ) → 𝑀
≤ if(𝑀 ≤
((⌊‘𝑎) + 1),
((⌊‘𝑎) + 1),
𝑀)) |
122 | 119, 120,
121 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀)) |
123 | | eluz2 12330 |
. . . . . . . . . . 11
⊢ (if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ ℤ ∧ 𝑀 ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀))) |
124 | 114, 118,
122, 123 | syl3anbrc 1344 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ (ℤ≥‘𝑀)) |
125 | 124, 9 | eleqtrrdi 2844 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ 𝑍) |
126 | 15 | fdmd 6515 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → dom
𝐹 = 𝑍) |
127 | 125, 126 | eleqtrrd 2836 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ dom 𝐹) |
128 | 118 | zred 12168 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ ℝ) |
129 | | fllep1 13262 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℝ → 𝑎 ≤ ((⌊‘𝑎) + 1)) |
130 | 129 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑎 ≤ ((⌊‘𝑎) + 1)) |
131 | | max2 12663 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℝ ∧
((⌊‘𝑎) + 1)
∈ ℝ) → ((⌊‘𝑎) + 1) ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀)) |
132 | 119, 120,
131 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
((⌊‘𝑎) + 1)
≤ if(𝑀 ≤
((⌊‘𝑎) + 1),
((⌊‘𝑎) + 1),
𝑀)) |
133 | 33, 120, 128, 130, 132 | letrd 10875 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → 𝑎 ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀)) |
134 | | elicopnf 12919 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℝ → (if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ (𝑎[,)+∞) ↔ (if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ ℝ ∧ 𝑎 ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀)))) |
135 | 134 | adantl 485 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
(if(𝑀 ≤
((⌊‘𝑎) + 1),
((⌊‘𝑎) + 1),
𝑀) ∈ (𝑎[,)+∞) ↔ (if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ ℝ ∧ 𝑎 ≤ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀)))) |
136 | 128, 133,
135 | mpbir2and 713 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ (𝑎[,)+∞)) |
137 | | inelcm 4354 |
. . . . . . . 8
⊢
((if(𝑀 ≤
((⌊‘𝑎) + 1),
((⌊‘𝑎) + 1),
𝑀) ∈ dom 𝐹 ∧ if(𝑀 ≤ ((⌊‘𝑎) + 1), ((⌊‘𝑎) + 1), 𝑀) ∈ (𝑎[,)+∞)) → (dom 𝐹 ∩ (𝑎[,)+∞)) ≠ ∅) |
138 | 127, 136,
137 | syl2anc 587 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (dom
𝐹 ∩ (𝑎[,)+∞)) ≠ ∅) |
139 | | imadisj 5922 |
. . . . . . . 8
⊢ ((𝐹 “ (𝑎[,)+∞)) = ∅ ↔ (dom 𝐹 ∩ (𝑎[,)+∞)) = ∅) |
140 | 139 | necon3bii 2986 |
. . . . . . 7
⊢ ((𝐹 “ (𝑎[,)+∞)) ≠ ∅ ↔ (dom 𝐹 ∩ (𝑎[,)+∞)) ≠ ∅) |
141 | 138, 140 | sylibr 237 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐹 “ (𝑎[,)+∞)) ≠ ∅) |
142 | 112, 141 | eqnetrd 3001 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → ((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*) ≠
∅) |
143 | | supxrre1 12806 |
. . . . 5
⊢ ((((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*)
⊆ ℝ ∧ ((𝐹
“ (𝑎[,)+∞))
∩ ℝ*) ≠ ∅) → (sup(((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*),
ℝ*, < ) ∈ ℝ ↔ sup(((𝐹 “ (𝑎[,)+∞)) ∩ ℝ*),
ℝ*, < ) < +∞)) |
144 | 113, 142,
143 | syl2anc 587 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
(sup(((𝐹 “ (𝑎[,)+∞)) ∩
ℝ*), ℝ*, < ) ∈ ℝ ↔
sup(((𝐹 “ (𝑎[,)+∞)) ∩
ℝ*), ℝ*, < ) <
+∞)) |
145 | 106, 144 | mpbird 260 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) →
sup(((𝐹 “ (𝑎[,)+∞)) ∩
ℝ*), ℝ*, < ) ∈
ℝ) |
146 | 7, 145 | eqeltrd 2833 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) ∧ 𝑎 ∈ ℝ) → (𝐺‘𝑎) ∈ ℝ) |
147 | 3, 5, 146 | fmpt2d 6897 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℝ ∧ (lim sup‘𝐹) < +∞) → 𝐺:ℝ⟶ℝ) |