| Step | Hyp | Ref
| Expression |
| 1 | | limsupval2.1 |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
| 2 | | limsupval.1 |
. . . 4
⊢ 𝐺 = (𝑘 ∈ ℝ ↦ sup(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
| 3 | 2 | limsupval 15510 |
. . 3
⊢ (𝐹 ∈ 𝑉 → (lim sup‘𝐹) = inf(ran 𝐺, ℝ*, <
)) |
| 4 | 1, 3 | syl 17 |
. 2
⊢ (𝜑 → (lim sup‘𝐹) = inf(ran 𝐺, ℝ*, <
)) |
| 5 | | imassrn 6089 |
. . . . 5
⊢ (𝐺 “ 𝐴) ⊆ ran 𝐺 |
| 6 | 2 | limsupgf 15511 |
. . . . . . 7
⊢ 𝐺:ℝ⟶ℝ* |
| 7 | | frn 6743 |
. . . . . . 7
⊢ (𝐺:ℝ⟶ℝ* →
ran 𝐺 ⊆
ℝ*) |
| 8 | 6, 7 | ax-mp 5 |
. . . . . 6
⊢ ran 𝐺 ⊆
ℝ* |
| 9 | | infxrlb 13376 |
. . . . . . 7
⊢ ((ran
𝐺 ⊆
ℝ* ∧ 𝑥
∈ ran 𝐺) →
inf(ran 𝐺,
ℝ*, < ) ≤ 𝑥) |
| 10 | 9 | ralrimiva 3146 |
. . . . . 6
⊢ (ran
𝐺 ⊆
ℝ* → ∀𝑥 ∈ ran 𝐺inf(ran 𝐺, ℝ*, < ) ≤ 𝑥) |
| 11 | 8, 10 | mp1i 13 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ran 𝐺inf(ran 𝐺, ℝ*, < ) ≤ 𝑥) |
| 12 | | ssralv 4052 |
. . . . 5
⊢ ((𝐺 “ 𝐴) ⊆ ran 𝐺 → (∀𝑥 ∈ ran 𝐺inf(ran 𝐺, ℝ*, < ) ≤ 𝑥 → ∀𝑥 ∈ (𝐺 “ 𝐴)inf(ran 𝐺, ℝ*, < ) ≤ 𝑥)) |
| 13 | 5, 11, 12 | mpsyl 68 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (𝐺 “ 𝐴)inf(ran 𝐺, ℝ*, < ) ≤ 𝑥) |
| 14 | 5, 8 | sstri 3993 |
. . . . 5
⊢ (𝐺 “ 𝐴) ⊆
ℝ* |
| 15 | | infxrcl 13375 |
. . . . . 6
⊢ (ran
𝐺 ⊆
ℝ* → inf(ran 𝐺, ℝ*, < ) ∈
ℝ*) |
| 16 | 8, 15 | ax-mp 5 |
. . . . 5
⊢ inf(ran
𝐺, ℝ*,
< ) ∈ ℝ* |
| 17 | | infxrgelb 13377 |
. . . . 5
⊢ (((𝐺 “ 𝐴) ⊆ ℝ* ∧ inf(ran
𝐺, ℝ*,
< ) ∈ ℝ*) → (inf(ran 𝐺, ℝ*, < ) ≤
inf((𝐺 “ 𝐴), ℝ*, < )
↔ ∀𝑥 ∈
(𝐺 “ 𝐴)inf(ran 𝐺, ℝ*, < ) ≤ 𝑥)) |
| 18 | 14, 16, 17 | mp2an 692 |
. . . 4
⊢ (inf(ran
𝐺, ℝ*,
< ) ≤ inf((𝐺 “
𝐴), ℝ*,
< ) ↔ ∀𝑥
∈ (𝐺 “ 𝐴)inf(ran 𝐺, ℝ*, < ) ≤ 𝑥) |
| 19 | 13, 18 | sylibr 234 |
. . 3
⊢ (𝜑 → inf(ran 𝐺, ℝ*, < ) ≤
inf((𝐺 “ 𝐴), ℝ*, <
)) |
| 20 | | limsupval2.3 |
. . . . . . 7
⊢ (𝜑 → sup(𝐴, ℝ*, < ) =
+∞) |
| 21 | | limsupval2.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
| 22 | | ressxr 11305 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ* |
| 23 | 21, 22 | sstrdi 3996 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆
ℝ*) |
| 24 | | supxrunb1 13361 |
. . . . . . . 8
⊢ (𝐴 ⊆ ℝ*
→ (∀𝑛 ∈
ℝ ∃𝑥 ∈
𝐴 𝑛 ≤ 𝑥 ↔ sup(𝐴, ℝ*, < ) =
+∞)) |
| 25 | 23, 24 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (∀𝑛 ∈ ℝ ∃𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 ↔ sup(𝐴, ℝ*, < ) =
+∞)) |
| 26 | 20, 25 | mpbird 257 |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ ℝ ∃𝑥 ∈ 𝐴 𝑛 ≤ 𝑥) |
| 27 | | infxrcl 13375 |
. . . . . . . . . 10
⊢ ((𝐺 “ 𝐴) ⊆ ℝ* →
inf((𝐺 “ 𝐴), ℝ*, < )
∈ ℝ*) |
| 28 | 14, 27 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥)) → inf((𝐺 “ 𝐴), ℝ*, < ) ∈
ℝ*) |
| 29 | 21 | sselda 3983 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
| 30 | 29 | ad2ant2r 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥)) → 𝑥 ∈ ℝ) |
| 31 | 6 | ffvelcdmi 7103 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → (𝐺‘𝑥) ∈
ℝ*) |
| 32 | 30, 31 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥)) → (𝐺‘𝑥) ∈
ℝ*) |
| 33 | 6 | ffvelcdmi 7103 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ → (𝐺‘𝑛) ∈
ℝ*) |
| 34 | 33 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥)) → (𝐺‘𝑛) ∈
ℝ*) |
| 35 | | ffn 6736 |
. . . . . . . . . . . 12
⊢ (𝐺:ℝ⟶ℝ* →
𝐺 Fn
ℝ) |
| 36 | 6, 35 | mp1i 13 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥)) → 𝐺 Fn ℝ) |
| 37 | 21 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥)) → 𝐴 ⊆ ℝ) |
| 38 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥)) → 𝑥 ∈ 𝐴) |
| 39 | | fnfvima 7253 |
. . . . . . . . . . 11
⊢ ((𝐺 Fn ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ (𝐺 “ 𝐴)) |
| 40 | 36, 37, 38, 39 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥)) → (𝐺‘𝑥) ∈ (𝐺 “ 𝐴)) |
| 41 | | infxrlb 13376 |
. . . . . . . . . 10
⊢ (((𝐺 “ 𝐴) ⊆ ℝ* ∧ (𝐺‘𝑥) ∈ (𝐺 “ 𝐴)) → inf((𝐺 “ 𝐴), ℝ*, < ) ≤ (𝐺‘𝑥)) |
| 42 | 14, 40, 41 | sylancr 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥)) → inf((𝐺 “ 𝐴), ℝ*, < ) ≤ (𝐺‘𝑥)) |
| 43 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ∈ ℝ) |
| 44 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ≤ 𝑥) |
| 45 | | limsupgord 15508 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑛 ≤ 𝑥) → sup(((𝐹 “ (𝑥[,)+∞)) ∩ ℝ*),
ℝ*, < ) ≤ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
| 46 | 43, 30, 44, 45 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥)) → sup(((𝐹 “ (𝑥[,)+∞)) ∩ ℝ*),
ℝ*, < ) ≤ sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
| 47 | 2 | limsupgval 15512 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → (𝐺‘𝑥) = sup(((𝐹 “ (𝑥[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
| 48 | 30, 47 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥)) → (𝐺‘𝑥) = sup(((𝐹 “ (𝑥[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
| 49 | 2 | limsupgval 15512 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ → (𝐺‘𝑛) = sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
| 50 | 49 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥)) → (𝐺‘𝑛) = sup(((𝐹 “ (𝑛[,)+∞)) ∩ ℝ*),
ℝ*, < )) |
| 51 | 46, 48, 50 | 3brtr4d 5175 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥)) → (𝐺‘𝑥) ≤ (𝐺‘𝑛)) |
| 52 | 28, 32, 34, 42, 51 | xrletrd 13204 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℝ) ∧ (𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥)) → inf((𝐺 “ 𝐴), ℝ*, < ) ≤ (𝐺‘𝑛)) |
| 53 | 52 | rexlimdvaa 3156 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℝ) → (∃𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 → inf((𝐺 “ 𝐴), ℝ*, < ) ≤ (𝐺‘𝑛))) |
| 54 | 53 | ralimdva 3167 |
. . . . . 6
⊢ (𝜑 → (∀𝑛 ∈ ℝ ∃𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 → ∀𝑛 ∈ ℝ inf((𝐺 “ 𝐴), ℝ*, < ) ≤ (𝐺‘𝑛))) |
| 55 | 26, 54 | mpd 15 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ ℝ inf((𝐺 “ 𝐴), ℝ*, < ) ≤ (𝐺‘𝑛)) |
| 56 | 6, 35 | ax-mp 5 |
. . . . . 6
⊢ 𝐺 Fn ℝ |
| 57 | | breq2 5147 |
. . . . . . 7
⊢ (𝑥 = (𝐺‘𝑛) → (inf((𝐺 “ 𝐴), ℝ*, < ) ≤ 𝑥 ↔ inf((𝐺 “ 𝐴), ℝ*, < ) ≤ (𝐺‘𝑛))) |
| 58 | 57 | ralrn 7108 |
. . . . . 6
⊢ (𝐺 Fn ℝ →
(∀𝑥 ∈ ran 𝐺inf((𝐺 “ 𝐴), ℝ*, < ) ≤ 𝑥 ↔ ∀𝑛 ∈ ℝ inf((𝐺 “ 𝐴), ℝ*, < ) ≤ (𝐺‘𝑛))) |
| 59 | 56, 58 | ax-mp 5 |
. . . . 5
⊢
(∀𝑥 ∈
ran 𝐺inf((𝐺 “ 𝐴), ℝ*, < ) ≤ 𝑥 ↔ ∀𝑛 ∈ ℝ inf((𝐺 “ 𝐴), ℝ*, < ) ≤ (𝐺‘𝑛)) |
| 60 | 55, 59 | sylibr 234 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ ran 𝐺inf((𝐺 “ 𝐴), ℝ*, < ) ≤ 𝑥) |
| 61 | 14, 27 | ax-mp 5 |
. . . . 5
⊢
inf((𝐺 “ 𝐴), ℝ*, < )
∈ ℝ* |
| 62 | | infxrgelb 13377 |
. . . . 5
⊢ ((ran
𝐺 ⊆
ℝ* ∧ inf((𝐺 “ 𝐴), ℝ*, < ) ∈
ℝ*) → (inf((𝐺 “ 𝐴), ℝ*, < ) ≤ inf(ran
𝐺, ℝ*,
< ) ↔ ∀𝑥
∈ ran 𝐺inf((𝐺 “ 𝐴), ℝ*, < ) ≤ 𝑥)) |
| 63 | 8, 61, 62 | mp2an 692 |
. . . 4
⊢
(inf((𝐺 “
𝐴), ℝ*,
< ) ≤ inf(ran 𝐺,
ℝ*, < ) ↔ ∀𝑥 ∈ ran 𝐺inf((𝐺 “ 𝐴), ℝ*, < ) ≤ 𝑥) |
| 64 | 60, 63 | sylibr 234 |
. . 3
⊢ (𝜑 → inf((𝐺 “ 𝐴), ℝ*, < ) ≤ inf(ran
𝐺, ℝ*,
< )) |
| 65 | | xrletri3 13196 |
. . . 4
⊢ ((inf(ran
𝐺, ℝ*,
< ) ∈ ℝ* ∧ inf((𝐺 “ 𝐴), ℝ*, < ) ∈
ℝ*) → (inf(ran 𝐺, ℝ*, < ) = inf((𝐺 “ 𝐴), ℝ*, < ) ↔
(inf(ran 𝐺,
ℝ*, < ) ≤ inf((𝐺 “ 𝐴), ℝ*, < ) ∧
inf((𝐺 “ 𝐴), ℝ*, < )
≤ inf(ran 𝐺,
ℝ*, < )))) |
| 66 | 16, 61, 65 | mp2an 692 |
. . 3
⊢ (inf(ran
𝐺, ℝ*,
< ) = inf((𝐺 “
𝐴), ℝ*,
< ) ↔ (inf(ran 𝐺,
ℝ*, < ) ≤ inf((𝐺 “ 𝐴), ℝ*, < ) ∧
inf((𝐺 “ 𝐴), ℝ*, < )
≤ inf(ran 𝐺,
ℝ*, < ))) |
| 67 | 19, 64, 66 | sylanbrc 583 |
. 2
⊢ (𝜑 → inf(ran 𝐺, ℝ*, < ) = inf((𝐺 “ 𝐴), ℝ*, <
)) |
| 68 | 4, 67 | eqtrd 2777 |
1
⊢ (𝜑 → (lim sup‘𝐹) = inf((𝐺 “ 𝐴), ℝ*, <
)) |