Step | Hyp | Ref
| Expression |
1 | | limsupval.1 |
. . . . 5
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
2 | 1 | limsupgval 14055 |
. . . 4
⊢ (𝐶 ∈ ℝ → (𝐺‘𝐶) = sup(((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
3 | 2 | 3ad2ant2 1076 |
. . 3
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (𝐺‘𝐶) = sup(((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
4 | 3 | breq1d 4593 |
. 2
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ((𝐺‘𝐶) ≤ 𝐴 ↔ sup(((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*),
ℝ*, < ) ≤ 𝐴)) |
5 | | inss2 3796 |
. . 3
⊢ ((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*)
⊆ ℝ* |
6 | | simp3 1056 |
. . 3
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ 𝐴 ∈
ℝ*) |
7 | | supxrleub 12028 |
. . 3
⊢ ((((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*)
⊆ ℝ* ∧ 𝐴 ∈ ℝ*) →
(sup(((𝐹 “ (𝐶[,)+∞)) ∩
ℝ*), ℝ*, < ) ≤ 𝐴 ↔ ∀𝑥 ∈ ((𝐹 “ (𝐶[,)+∞)) ∩
ℝ*)𝑥 ≤
𝐴)) |
8 | 5, 6, 7 | sylancr 694 |
. 2
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (sup(((𝐹 “
(𝐶[,)+∞)) ∩
ℝ*), ℝ*, < ) ≤ 𝐴 ↔ ∀𝑥 ∈ ((𝐹 “ (𝐶[,)+∞)) ∩
ℝ*)𝑥 ≤
𝐴)) |
9 | | imassrn 5396 |
. . . . . . 7
⊢ (𝐹 “ (𝐶[,)+∞)) ⊆ ran 𝐹 |
10 | | simp1r 1079 |
. . . . . . . 8
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ 𝐹:𝐵⟶ℝ*) |
11 | | frn 5966 |
. . . . . . . 8
⊢ (𝐹:𝐵⟶ℝ* → ran 𝐹 ⊆
ℝ*) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ran 𝐹 ⊆
ℝ*) |
13 | 9, 12 | syl5ss 3579 |
. . . . . 6
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (𝐹 “ (𝐶[,)+∞)) ⊆
ℝ*) |
14 | | df-ss 3554 |
. . . . . 6
⊢ ((𝐹 “ (𝐶[,)+∞)) ⊆ ℝ*
↔ ((𝐹 “ (𝐶[,)+∞)) ∩
ℝ*) = (𝐹
“ (𝐶[,)+∞))) |
15 | 13, 14 | sylib 207 |
. . . . 5
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ((𝐹 “ (𝐶[,)+∞)) ∩
ℝ*) = (𝐹
“ (𝐶[,)+∞))) |
16 | | imadmres 5544 |
. . . . 5
⊢ (𝐹 “ dom (𝐹 ↾ (𝐶[,)+∞))) = (𝐹 “ (𝐶[,)+∞)) |
17 | 15, 16 | syl6eqr 2662 |
. . . 4
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ((𝐹 “ (𝐶[,)+∞)) ∩
ℝ*) = (𝐹
“ dom (𝐹 ↾
(𝐶[,)+∞)))) |
18 | 17 | raleqdv 3121 |
. . 3
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (∀𝑥 ∈
((𝐹 “ (𝐶[,)+∞)) ∩
ℝ*)𝑥 ≤
𝐴 ↔ ∀𝑥 ∈ (𝐹 “ dom (𝐹 ↾ (𝐶[,)+∞)))𝑥 ≤ 𝐴)) |
19 | | ffn 5958 |
. . . . 5
⊢ (𝐹:𝐵⟶ℝ* → 𝐹 Fn 𝐵) |
20 | 10, 19 | syl 17 |
. . . 4
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ 𝐹 Fn 𝐵) |
21 | | fdm 5964 |
. . . . . . . 8
⊢ (𝐹:𝐵⟶ℝ* → dom 𝐹 = 𝐵) |
22 | 10, 21 | syl 17 |
. . . . . . 7
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ dom 𝐹 = 𝐵) |
23 | 22 | ineq2d 3776 |
. . . . . 6
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ((𝐶[,)+∞)
∩ dom 𝐹) = ((𝐶[,)+∞) ∩ 𝐵)) |
24 | | dmres 5339 |
. . . . . 6
⊢ dom
(𝐹 ↾ (𝐶[,)+∞)) = ((𝐶[,)+∞) ∩ dom 𝐹) |
25 | | incom 3767 |
. . . . . 6
⊢ (𝐵 ∩ (𝐶[,)+∞)) = ((𝐶[,)+∞) ∩ 𝐵) |
26 | 23, 24, 25 | 3eqtr4g 2669 |
. . . . 5
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ dom (𝐹 ↾
(𝐶[,)+∞)) = (𝐵 ∩ (𝐶[,)+∞))) |
27 | | inss1 3795 |
. . . . 5
⊢ (𝐵 ∩ (𝐶[,)+∞)) ⊆ 𝐵 |
28 | 26, 27 | syl6eqss 3618 |
. . . 4
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ dom (𝐹 ↾
(𝐶[,)+∞)) ⊆
𝐵) |
29 | | breq1 4586 |
. . . . 5
⊢ (𝑥 = (𝐹‘𝑗) → (𝑥 ≤ 𝐴 ↔ (𝐹‘𝑗) ≤ 𝐴)) |
30 | 29 | ralima 6402 |
. . . 4
⊢ ((𝐹 Fn 𝐵 ∧ dom (𝐹 ↾ (𝐶[,)+∞)) ⊆ 𝐵) → (∀𝑥 ∈ (𝐹 “ dom (𝐹 ↾ (𝐶[,)+∞)))𝑥 ≤ 𝐴 ↔ ∀𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞))(𝐹‘𝑗) ≤ 𝐴)) |
31 | 20, 28, 30 | syl2anc 691 |
. . 3
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (∀𝑥 ∈
(𝐹 “ dom (𝐹 ↾ (𝐶[,)+∞)))𝑥 ≤ 𝐴 ↔ ∀𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞))(𝐹‘𝑗) ≤ 𝐴)) |
32 | 26 | eleq2d 2673 |
. . . . . . . 8
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞)) ↔ 𝑗 ∈ (𝐵 ∩ (𝐶[,)+∞)))) |
33 | | elin 3758 |
. . . . . . . 8
⊢ (𝑗 ∈ (𝐵 ∩ (𝐶[,)+∞)) ↔ (𝑗 ∈ 𝐵 ∧ 𝑗 ∈ (𝐶[,)+∞))) |
34 | 32, 33 | syl6bb 275 |
. . . . . . 7
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞)) ↔ (𝑗 ∈ 𝐵 ∧ 𝑗 ∈ (𝐶[,)+∞)))) |
35 | | simpl2 1058 |
. . . . . . . . 9
⊢ ((((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
∧ 𝑗 ∈ 𝐵) → 𝐶 ∈ ℝ) |
36 | | simp1l 1078 |
. . . . . . . . . 10
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ 𝐵 ⊆
ℝ) |
37 | 36 | sselda 3568 |
. . . . . . . . 9
⊢ ((((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
∧ 𝑗 ∈ 𝐵) → 𝑗 ∈ ℝ) |
38 | | elicopnf 12140 |
. . . . . . . . . 10
⊢ (𝐶 ∈ ℝ → (𝑗 ∈ (𝐶[,)+∞) ↔ (𝑗 ∈ ℝ ∧ 𝐶 ≤ 𝑗))) |
39 | 38 | baibd 946 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑗 ∈ (𝐶[,)+∞) ↔ 𝐶 ≤ 𝑗)) |
40 | 35, 37, 39 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
∧ 𝑗 ∈ 𝐵) → (𝑗 ∈ (𝐶[,)+∞) ↔ 𝐶 ≤ 𝑗)) |
41 | 40 | pm5.32da 671 |
. . . . . . 7
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ((𝑗 ∈ 𝐵 ∧ 𝑗 ∈ (𝐶[,)+∞)) ↔ (𝑗 ∈ 𝐵 ∧ 𝐶 ≤ 𝑗))) |
42 | 34, 41 | bitrd 267 |
. . . . . 6
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞)) ↔ (𝑗 ∈ 𝐵 ∧ 𝐶 ≤ 𝑗))) |
43 | 42 | imbi1d 330 |
. . . . 5
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ((𝑗 ∈ dom
(𝐹 ↾ (𝐶[,)+∞)) → (𝐹‘𝑗) ≤ 𝐴) ↔ ((𝑗 ∈ 𝐵 ∧ 𝐶 ≤ 𝑗) → (𝐹‘𝑗) ≤ 𝐴))) |
44 | | impexp 461 |
. . . . 5
⊢ (((𝑗 ∈ 𝐵 ∧ 𝐶 ≤ 𝑗) → (𝐹‘𝑗) ≤ 𝐴) ↔ (𝑗 ∈ 𝐵 → (𝐶 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴))) |
45 | 43, 44 | syl6bb 275 |
. . . 4
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ((𝑗 ∈ dom
(𝐹 ↾ (𝐶[,)+∞)) → (𝐹‘𝑗) ≤ 𝐴) ↔ (𝑗 ∈ 𝐵 → (𝐶 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴)))) |
46 | 45 | ralbidv2 2967 |
. . 3
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (∀𝑗 ∈
dom (𝐹 ↾ (𝐶[,)+∞))(𝐹‘𝑗) ≤ 𝐴 ↔ ∀𝑗 ∈ 𝐵 (𝐶 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴))) |
47 | 18, 31, 46 | 3bitrd 293 |
. 2
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (∀𝑥 ∈
((𝐹 “ (𝐶[,)+∞)) ∩
ℝ*)𝑥 ≤
𝐴 ↔ ∀𝑗 ∈ 𝐵 (𝐶 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴))) |
48 | 4, 8, 47 | 3bitrd 293 |
1
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ((𝐺‘𝐶) ≤ 𝐴 ↔ ∀𝑗 ∈ 𝐵 (𝐶 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴))) |