Step |
Hyp |
Ref |
Expression |
1 |
|
limsupval.1 |
⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) |
2 |
|
limsupval2.1 |
⊢ ( 𝜑 → 𝐹 ∈ 𝑉 ) |
3 |
|
limsupval2.2 |
⊢ ( 𝜑 → 𝐴 ⊆ ℝ ) |
4 |
|
limsupval2.3 |
⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ ) |
5 |
1
|
limsupval |
⊢ ( 𝐹 ∈ 𝑉 → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ* , < ) ) |
6 |
2 5
|
syl |
⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ* , < ) ) |
7 |
|
imassrn |
⊢ ( 𝐺 “ 𝐴 ) ⊆ ran 𝐺 |
8 |
1
|
limsupgf |
⊢ 𝐺 : ℝ ⟶ ℝ* |
9 |
|
frn |
⊢ ( 𝐺 : ℝ ⟶ ℝ* → ran 𝐺 ⊆ ℝ* ) |
10 |
8 9
|
ax-mp |
⊢ ran 𝐺 ⊆ ℝ* |
11 |
|
infxrlb |
⊢ ( ( ran 𝐺 ⊆ ℝ* ∧ 𝑥 ∈ ran 𝐺 ) → inf ( ran 𝐺 , ℝ* , < ) ≤ 𝑥 ) |
12 |
11
|
ralrimiva |
⊢ ( ran 𝐺 ⊆ ℝ* → ∀ 𝑥 ∈ ran 𝐺 inf ( ran 𝐺 , ℝ* , < ) ≤ 𝑥 ) |
13 |
10 12
|
mp1i |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ran 𝐺 inf ( ran 𝐺 , ℝ* , < ) ≤ 𝑥 ) |
14 |
|
ssralv |
⊢ ( ( 𝐺 “ 𝐴 ) ⊆ ran 𝐺 → ( ∀ 𝑥 ∈ ran 𝐺 inf ( ran 𝐺 , ℝ* , < ) ≤ 𝑥 → ∀ 𝑥 ∈ ( 𝐺 “ 𝐴 ) inf ( ran 𝐺 , ℝ* , < ) ≤ 𝑥 ) ) |
15 |
7 13 14
|
mpsyl |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐺 “ 𝐴 ) inf ( ran 𝐺 , ℝ* , < ) ≤ 𝑥 ) |
16 |
7 10
|
sstri |
⊢ ( 𝐺 “ 𝐴 ) ⊆ ℝ* |
17 |
|
infxrcl |
⊢ ( ran 𝐺 ⊆ ℝ* → inf ( ran 𝐺 , ℝ* , < ) ∈ ℝ* ) |
18 |
10 17
|
ax-mp |
⊢ inf ( ran 𝐺 , ℝ* , < ) ∈ ℝ* |
19 |
|
infxrgelb |
⊢ ( ( ( 𝐺 “ 𝐴 ) ⊆ ℝ* ∧ inf ( ran 𝐺 , ℝ* , < ) ∈ ℝ* ) → ( inf ( ran 𝐺 , ℝ* , < ) ≤ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ↔ ∀ 𝑥 ∈ ( 𝐺 “ 𝐴 ) inf ( ran 𝐺 , ℝ* , < ) ≤ 𝑥 ) ) |
20 |
16 18 19
|
mp2an |
⊢ ( inf ( ran 𝐺 , ℝ* , < ) ≤ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ↔ ∀ 𝑥 ∈ ( 𝐺 “ 𝐴 ) inf ( ran 𝐺 , ℝ* , < ) ≤ 𝑥 ) |
21 |
15 20
|
sylibr |
⊢ ( 𝜑 → inf ( ran 𝐺 , ℝ* , < ) ≤ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ) |
22 |
|
ressxr |
⊢ ℝ ⊆ ℝ* |
23 |
3 22
|
sstrdi |
⊢ ( 𝜑 → 𝐴 ⊆ ℝ* ) |
24 |
|
supxrunb1 |
⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑛 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) ) |
25 |
23 24
|
syl |
⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) ) |
26 |
4 25
|
mpbird |
⊢ ( 𝜑 → ∀ 𝑛 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 ) |
27 |
|
infxrcl |
⊢ ( ( 𝐺 “ 𝐴 ) ⊆ ℝ* → inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ∈ ℝ* ) |
28 |
16 27
|
mp1i |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ∈ ℝ* ) |
29 |
3
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ ) |
30 |
29
|
ad2ant2r |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ ) |
31 |
8
|
ffvelrni |
⊢ ( 𝑥 ∈ ℝ → ( 𝐺 ‘ 𝑥 ) ∈ ℝ* ) |
32 |
30 31
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ* ) |
33 |
8
|
ffvelrni |
⊢ ( 𝑛 ∈ ℝ → ( 𝐺 ‘ 𝑛 ) ∈ ℝ* ) |
34 |
33
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ* ) |
35 |
|
ffn |
⊢ ( 𝐺 : ℝ ⟶ ℝ* → 𝐺 Fn ℝ ) |
36 |
8 35
|
mp1i |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐺 Fn ℝ ) |
37 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐴 ⊆ ℝ ) |
38 |
|
simprl |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑥 ∈ 𝐴 ) |
39 |
|
fnfvima |
⊢ ( ( 𝐺 Fn ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐺 “ 𝐴 ) ) |
40 |
36 37 38 39
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐺 “ 𝐴 ) ) |
41 |
|
infxrlb |
⊢ ( ( ( 𝐺 “ 𝐴 ) ⊆ ℝ* ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐺 “ 𝐴 ) ) → inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑥 ) ) |
42 |
16 40 41
|
sylancr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑥 ) ) |
43 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑛 ∈ ℝ ) |
44 |
|
simprr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑛 ≤ 𝑥 ) |
45 |
|
limsupgord |
⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑛 ≤ 𝑥 ) → sup ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) |
46 |
43 30 44 45
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → sup ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) |
47 |
1
|
limsupgval |
⊢ ( 𝑥 ∈ ℝ → ( 𝐺 ‘ 𝑥 ) = sup ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) |
48 |
30 47
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) = sup ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) |
49 |
1
|
limsupgval |
⊢ ( 𝑛 ∈ ℝ → ( 𝐺 ‘ 𝑛 ) = sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) |
50 |
49
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑛 ) = sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) |
51 |
46 48 50
|
3brtr4d |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑛 ) ) |
52 |
28 32 34 42 51
|
xrletrd |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑛 ) ) |
53 |
52
|
rexlimdvaa |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) → ( ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 → inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑛 ) ) ) |
54 |
53
|
ralimdva |
⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 → ∀ 𝑛 ∈ ℝ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑛 ) ) ) |
55 |
26 54
|
mpd |
⊢ ( 𝜑 → ∀ 𝑛 ∈ ℝ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑛 ) ) |
56 |
8 35
|
ax-mp |
⊢ 𝐺 Fn ℝ |
57 |
|
breq2 |
⊢ ( 𝑥 = ( 𝐺 ‘ 𝑛 ) → ( inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ 𝑥 ↔ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑛 ) ) ) |
58 |
57
|
ralrn |
⊢ ( 𝐺 Fn ℝ → ( ∀ 𝑥 ∈ ran 𝐺 inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ 𝑥 ↔ ∀ 𝑛 ∈ ℝ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑛 ) ) ) |
59 |
56 58
|
ax-mp |
⊢ ( ∀ 𝑥 ∈ ran 𝐺 inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ 𝑥 ↔ ∀ 𝑛 ∈ ℝ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ ( 𝐺 ‘ 𝑛 ) ) |
60 |
55 59
|
sylibr |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ran 𝐺 inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ 𝑥 ) |
61 |
16 27
|
ax-mp |
⊢ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ∈ ℝ* |
62 |
|
infxrgelb |
⊢ ( ( ran 𝐺 ⊆ ℝ* ∧ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ∈ ℝ* ) → ( inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ inf ( ran 𝐺 , ℝ* , < ) ↔ ∀ 𝑥 ∈ ran 𝐺 inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ 𝑥 ) ) |
63 |
10 61 62
|
mp2an |
⊢ ( inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ inf ( ran 𝐺 , ℝ* , < ) ↔ ∀ 𝑥 ∈ ran 𝐺 inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ 𝑥 ) |
64 |
60 63
|
sylibr |
⊢ ( 𝜑 → inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ inf ( ran 𝐺 , ℝ* , < ) ) |
65 |
|
xrletri3 |
⊢ ( ( inf ( ran 𝐺 , ℝ* , < ) ∈ ℝ* ∧ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ∈ ℝ* ) → ( inf ( ran 𝐺 , ℝ* , < ) = inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ↔ ( inf ( ran 𝐺 , ℝ* , < ) ≤ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ∧ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ inf ( ran 𝐺 , ℝ* , < ) ) ) ) |
66 |
18 61 65
|
mp2an |
⊢ ( inf ( ran 𝐺 , ℝ* , < ) = inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ↔ ( inf ( ran 𝐺 , ℝ* , < ) ≤ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ∧ inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ≤ inf ( ran 𝐺 , ℝ* , < ) ) ) |
67 |
21 64 66
|
sylanbrc |
⊢ ( 𝜑 → inf ( ran 𝐺 , ℝ* , < ) = inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ) |
68 |
6 67
|
eqtrd |
⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ( 𝐺 “ 𝐴 ) , ℝ* , < ) ) |