Step | Hyp | Ref
| Expression |
1 | | limsupval.1 |
. . . . 5
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
2 | 1 | limsupgval 14207 |
. . . 4
⊢ (𝐶 ∈ ℝ → (𝐺‘𝐶) = sup(((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
3 | 2 | 3ad2ant2 1083 |
. . 3
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (𝐺‘𝐶) = sup(((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
4 | 3 | breq1d 4663 |
. 2
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ((𝐺‘𝐶) ≤ 𝐴 ↔ sup(((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*),
ℝ*, < ) ≤ 𝐴)) |
5 | | inss2 3834 |
. . 3
⊢ ((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*)
⊆ ℝ* |
6 | | simp3 1063 |
. . 3
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ 𝐴 ∈
ℝ*) |
7 | | supxrleub 12156 |
. . 3
⊢ ((((𝐹 “ (𝐶[,)+∞)) ∩ ℝ*)
⊆ ℝ* ∧ 𝐴 ∈ ℝ*) →
(sup(((𝐹 “ (𝐶[,)+∞)) ∩
ℝ*), ℝ*, < ) ≤ 𝐴 ↔ ∀𝑥 ∈ ((𝐹 “ (𝐶[,)+∞)) ∩
ℝ*)𝑥 ≤
𝐴)) |
8 | 5, 6, 7 | sylancr 695 |
. 2
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (sup(((𝐹 “
(𝐶[,)+∞)) ∩
ℝ*), ℝ*, < ) ≤ 𝐴 ↔ ∀𝑥 ∈ ((𝐹 “ (𝐶[,)+∞)) ∩
ℝ*)𝑥 ≤
𝐴)) |
9 | | imassrn 5477 |
. . . . . . 7
⊢ (𝐹 “ (𝐶[,)+∞)) ⊆ ran 𝐹 |
10 | | simp1r 1086 |
. . . . . . . 8
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ 𝐹:𝐵⟶ℝ*) |
11 | | frn 6053 |
. . . . . . . 8
⊢ (𝐹:𝐵⟶ℝ* → ran 𝐹 ⊆
ℝ*) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ran 𝐹 ⊆
ℝ*) |
13 | 9, 12 | syl5ss 3614 |
. . . . . 6
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (𝐹 “ (𝐶[,)+∞)) ⊆
ℝ*) |
14 | | df-ss 3588 |
. . . . . 6
⊢ ((𝐹 “ (𝐶[,)+∞)) ⊆ ℝ*
↔ ((𝐹 “ (𝐶[,)+∞)) ∩
ℝ*) = (𝐹
“ (𝐶[,)+∞))) |
15 | 13, 14 | sylib 208 |
. . . . 5
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ((𝐹 “ (𝐶[,)+∞)) ∩
ℝ*) = (𝐹
“ (𝐶[,)+∞))) |
16 | | imadmres 5627 |
. . . . 5
⊢ (𝐹 “ dom (𝐹 ↾ (𝐶[,)+∞))) = (𝐹 “ (𝐶[,)+∞)) |
17 | 15, 16 | syl6eqr 2674 |
. . . 4
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ((𝐹 “ (𝐶[,)+∞)) ∩
ℝ*) = (𝐹
“ dom (𝐹 ↾
(𝐶[,)+∞)))) |
18 | 17 | raleqdv 3144 |
. . 3
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (∀𝑥 ∈
((𝐹 “ (𝐶[,)+∞)) ∩
ℝ*)𝑥 ≤
𝐴 ↔ ∀𝑥 ∈ (𝐹 “ dom (𝐹 ↾ (𝐶[,)+∞)))𝑥 ≤ 𝐴)) |
19 | | ffn 6045 |
. . . . 5
⊢ (𝐹:𝐵⟶ℝ* → 𝐹 Fn 𝐵) |
20 | 10, 19 | syl 17 |
. . . 4
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ 𝐹 Fn 𝐵) |
21 | | fdm 6051 |
. . . . . . . 8
⊢ (𝐹:𝐵⟶ℝ* → dom 𝐹 = 𝐵) |
22 | 10, 21 | syl 17 |
. . . . . . 7
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ dom 𝐹 = 𝐵) |
23 | 22 | ineq2d 3814 |
. . . . . 6
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ((𝐶[,)+∞)
∩ dom 𝐹) = ((𝐶[,)+∞) ∩ 𝐵)) |
24 | | dmres 5419 |
. . . . . 6
⊢ dom
(𝐹 ↾ (𝐶[,)+∞)) = ((𝐶[,)+∞) ∩ dom 𝐹) |
25 | | incom 3805 |
. . . . . 6
⊢ (𝐵 ∩ (𝐶[,)+∞)) = ((𝐶[,)+∞) ∩ 𝐵) |
26 | 23, 24, 25 | 3eqtr4g 2681 |
. . . . 5
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ dom (𝐹 ↾
(𝐶[,)+∞)) = (𝐵 ∩ (𝐶[,)+∞))) |
27 | | inss1 3833 |
. . . . 5
⊢ (𝐵 ∩ (𝐶[,)+∞)) ⊆ 𝐵 |
28 | 26, 27 | syl6eqss 3655 |
. . . 4
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ dom (𝐹 ↾
(𝐶[,)+∞)) ⊆
𝐵) |
29 | | breq1 4656 |
. . . . 5
⊢ (𝑥 = (𝐹‘𝑗) → (𝑥 ≤ 𝐴 ↔ (𝐹‘𝑗) ≤ 𝐴)) |
30 | 29 | ralima 6498 |
. . . 4
⊢ ((𝐹 Fn 𝐵 ∧ dom (𝐹 ↾ (𝐶[,)+∞)) ⊆ 𝐵) → (∀𝑥 ∈ (𝐹 “ dom (𝐹 ↾ (𝐶[,)+∞)))𝑥 ≤ 𝐴 ↔ ∀𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞))(𝐹‘𝑗) ≤ 𝐴)) |
31 | 20, 28, 30 | syl2anc 693 |
. . 3
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (∀𝑥 ∈
(𝐹 “ dom (𝐹 ↾ (𝐶[,)+∞)))𝑥 ≤ 𝐴 ↔ ∀𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞))(𝐹‘𝑗) ≤ 𝐴)) |
32 | 26 | eleq2d 2687 |
. . . . . . . 8
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞)) ↔ 𝑗 ∈ (𝐵 ∩ (𝐶[,)+∞)))) |
33 | | elin 3796 |
. . . . . . . 8
⊢ (𝑗 ∈ (𝐵 ∩ (𝐶[,)+∞)) ↔ (𝑗 ∈ 𝐵 ∧ 𝑗 ∈ (𝐶[,)+∞))) |
34 | 32, 33 | syl6bb 276 |
. . . . . . 7
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞)) ↔ (𝑗 ∈ 𝐵 ∧ 𝑗 ∈ (𝐶[,)+∞)))) |
35 | | simpl2 1065 |
. . . . . . . . 9
⊢ ((((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
∧ 𝑗 ∈ 𝐵) → 𝐶 ∈ ℝ) |
36 | | simp1l 1085 |
. . . . . . . . . 10
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ 𝐵 ⊆
ℝ) |
37 | 36 | sselda 3603 |
. . . . . . . . 9
⊢ ((((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
∧ 𝑗 ∈ 𝐵) → 𝑗 ∈ ℝ) |
38 | | elicopnf 12269 |
. . . . . . . . . 10
⊢ (𝐶 ∈ ℝ → (𝑗 ∈ (𝐶[,)+∞) ↔ (𝑗 ∈ ℝ ∧ 𝐶 ≤ 𝑗))) |
39 | 38 | baibd 948 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑗 ∈ (𝐶[,)+∞) ↔ 𝐶 ≤ 𝑗)) |
40 | 35, 37, 39 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
∧ 𝑗 ∈ 𝐵) → (𝑗 ∈ (𝐶[,)+∞) ↔ 𝐶 ≤ 𝑗)) |
41 | 40 | pm5.32da 673 |
. . . . . . 7
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ((𝑗 ∈ 𝐵 ∧ 𝑗 ∈ (𝐶[,)+∞)) ↔ (𝑗 ∈ 𝐵 ∧ 𝐶 ≤ 𝑗))) |
42 | 34, 41 | bitrd 268 |
. . . . . 6
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (𝑗 ∈ dom (𝐹 ↾ (𝐶[,)+∞)) ↔ (𝑗 ∈ 𝐵 ∧ 𝐶 ≤ 𝑗))) |
43 | 42 | imbi1d 331 |
. . . . 5
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ((𝑗 ∈ dom
(𝐹 ↾ (𝐶[,)+∞)) → (𝐹‘𝑗) ≤ 𝐴) ↔ ((𝑗 ∈ 𝐵 ∧ 𝐶 ≤ 𝑗) → (𝐹‘𝑗) ≤ 𝐴))) |
44 | | impexp 462 |
. . . . 5
⊢ (((𝑗 ∈ 𝐵 ∧ 𝐶 ≤ 𝑗) → (𝐹‘𝑗) ≤ 𝐴) ↔ (𝑗 ∈ 𝐵 → (𝐶 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴))) |
45 | 43, 44 | syl6bb 276 |
. . . 4
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ((𝑗 ∈ dom
(𝐹 ↾ (𝐶[,)+∞)) → (𝐹‘𝑗) ≤ 𝐴) ↔ (𝑗 ∈ 𝐵 → (𝐶 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴)))) |
46 | 45 | ralbidv2 2984 |
. . 3
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (∀𝑗 ∈
dom (𝐹 ↾ (𝐶[,)+∞))(𝐹‘𝑗) ≤ 𝐴 ↔ ∀𝑗 ∈ 𝐵 (𝐶 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴))) |
47 | 18, 31, 46 | 3bitrd 294 |
. 2
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ (∀𝑥 ∈
((𝐹 “ (𝐶[,)+∞)) ∩
ℝ*)𝑥 ≤
𝐴 ↔ ∀𝑗 ∈ 𝐵 (𝐶 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴))) |
48 | 4, 8, 47 | 3bitrd 294 |
1
⊢ (((𝐵 ⊆ ℝ ∧ 𝐹:𝐵⟶ℝ*) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*)
→ ((𝐺‘𝐶) ≤ 𝐴 ↔ ∀𝑗 ∈ 𝐵 (𝐶 ≤ 𝑗 → (𝐹‘𝑗) ≤ 𝐴))) |