Step |
Hyp |
Ref |
Expression |
1 |
|
limsupub.j |
⊢ Ⅎ 𝑗 𝜑 |
2 |
|
limsupub.e |
⊢ Ⅎ 𝑗 𝐹 |
3 |
|
limsupub.a |
⊢ ( 𝜑 → 𝐴 ⊆ ℝ ) |
4 |
|
limsupub.f |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* ) |
5 |
|
limsupub.n |
⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≠ +∞ ) |
6 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) → 𝐴 ⊆ ℝ ) |
7 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) → 𝐹 : 𝐴 ⟶ ℝ* ) |
8 |
|
nfv |
⊢ Ⅎ 𝑗 𝑥 ∈ ℝ |
9 |
1 8
|
nfan |
⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑥 ∈ ℝ ) |
10 |
|
simprl |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) → 𝑘 ≤ 𝑗 ) |
11 |
|
simpllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → 𝑥 ∈ ℝ ) |
12 |
|
rexr |
⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* ) |
13 |
11 12
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → 𝑥 ∈ ℝ* ) |
14 |
4
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* ) |
15 |
14
|
ad4ant13 |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* ) |
16 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → 𝑥 < ( 𝐹 ‘ 𝑗 ) ) |
17 |
13 15 16
|
xrltled |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) |
18 |
17
|
adantrl |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) → 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) |
19 |
10 18
|
jca |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) → ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) |
20 |
19
|
ex |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) |
21 |
20
|
ex |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑗 ∈ 𝐴 → ( ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) ) |
22 |
9 21
|
reximdai |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) |
23 |
22
|
ralimdv |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) |
24 |
23
|
ralimdva |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) |
25 |
24
|
imp |
⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) → ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) |
26 |
2 6 7 25
|
limsuppnfd |
⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) → ( lim sup ‘ 𝐹 ) = +∞ ) |
27 |
5
|
neneqd |
⊢ ( 𝜑 → ¬ ( lim sup ‘ 𝐹 ) = +∞ ) |
28 |
27
|
adantr |
⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) → ¬ ( lim sup ‘ 𝐹 ) = +∞ ) |
29 |
26 28
|
pm2.65da |
⊢ ( 𝜑 → ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) |
30 |
|
imnan |
⊢ ( ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) |
31 |
30
|
ralbii |
⊢ ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ 𝐴 ¬ ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) |
32 |
|
ralnex |
⊢ ( ∀ 𝑗 ∈ 𝐴 ¬ ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) |
33 |
31 32
|
bitri |
⊢ ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) |
34 |
33
|
rexbii |
⊢ ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑘 ∈ ℝ ¬ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) |
35 |
|
rexnal |
⊢ ( ∃ 𝑘 ∈ ℝ ¬ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) |
36 |
34 35
|
bitri |
⊢ ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) |
37 |
36
|
rexbii |
⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ∃ 𝑥 ∈ ℝ ¬ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) |
38 |
|
rexnal |
⊢ ( ∃ 𝑥 ∈ ℝ ¬ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) |
39 |
37 38
|
bitri |
⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ↔ ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) |
40 |
29 39
|
sylibr |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) |
41 |
|
nfv |
⊢ Ⅎ 𝑗 𝑘 ∈ ℝ |
42 |
9 41
|
nfan |
⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) |
43 |
14
|
ad4ant14 |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* ) |
44 |
|
simpllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑥 ∈ ℝ ) |
45 |
44
|
rexrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → 𝑥 ∈ ℝ* ) |
46 |
43 45
|
xrlenltd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) |
47 |
46
|
imbi2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) ) |
48 |
42 47
|
ralbida |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) ) |
49 |
48
|
rexbidva |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) ) |
50 |
49
|
rexbidva |
⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ¬ 𝑥 < ( 𝐹 ‘ 𝑗 ) ) ) ) |
51 |
40 50
|
mpbird |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) |