Step |
Hyp |
Ref |
Expression |
1 |
|
liminfreuzlem.1 |
⊢ Ⅎ 𝑗 𝐹 |
2 |
|
liminfreuzlem.2 |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
3 |
|
liminfreuzlem.3 |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
4 |
|
liminfreuzlem.4 |
⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ ) |
5 |
|
nfv |
⊢ Ⅎ 𝑗 𝜑 |
6 |
5 1 2 3 4
|
liminfvaluz4 |
⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ) |
7 |
6
|
eleq1d |
⊢ ( 𝜑 → ( ( lim inf ‘ 𝐹 ) ∈ ℝ ↔ -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ) ) |
8 |
3
|
fvexi |
⊢ 𝑍 ∈ V |
9 |
8
|
mptex |
⊢ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ∈ V |
10 |
|
limsupcl |
⊢ ( ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ∈ V → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ* ) |
11 |
9 10
|
ax-mp |
⊢ ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ* |
12 |
11
|
a1i |
⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ* ) |
13 |
12
|
xnegred |
⊢ ( 𝜑 → ( ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ↔ -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ) ) |
14 |
7 13
|
bitr4d |
⊢ ( 𝜑 → ( ( lim inf ‘ 𝐹 ) ∈ ℝ ↔ ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ) ) |
15 |
4
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) |
16 |
15
|
renegcld |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → - ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) |
17 |
5 2 3 16
|
limsupreuzmpt |
⊢ ( 𝜑 → ( ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) ) ) |
18 |
|
renegcl |
⊢ ( 𝑦 ∈ ℝ → - 𝑦 ∈ ℝ ) |
19 |
18
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ) → - 𝑦 ∈ ℝ ) |
20 |
|
simpllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑦 ∈ ℝ ) |
21 |
4
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝐹 : 𝑍 ⟶ ℝ ) |
22 |
3
|
uztrn2 |
⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑗 ∈ 𝑍 ) |
23 |
22
|
adantll |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑗 ∈ 𝑍 ) |
24 |
21 23
|
ffvelrnd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) |
25 |
24
|
adantllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) |
26 |
20 25
|
leneg2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ↔ ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 ) ) |
27 |
26
|
rexbidva |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 ) ) |
28 |
27
|
ralbidva |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 ) ) |
29 |
28
|
biimpd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) → ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 ) ) |
30 |
29
|
imp |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 ) |
31 |
|
breq2 |
⊢ ( 𝑥 = - 𝑦 → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 ) ) |
32 |
31
|
rexbidv |
⊢ ( 𝑥 = - 𝑦 → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 ) ) |
33 |
32
|
ralbidv |
⊢ ( 𝑥 = - 𝑦 → ( ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 ) ) |
34 |
33
|
rspcev |
⊢ ( ( - 𝑦 ∈ ℝ ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) |
35 |
19 30 34
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) |
36 |
35
|
rexlimdva2 |
⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) |
37 |
|
renegcl |
⊢ ( 𝑥 ∈ ℝ → - 𝑥 ∈ ℝ ) |
38 |
37
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → - 𝑥 ∈ ℝ ) |
39 |
24
|
adantllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) |
40 |
|
simpllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑥 ∈ ℝ ) |
41 |
39 40
|
lenegd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) ) ) |
42 |
41
|
rexbidva |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) ) ) |
43 |
42
|
ralbidva |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) ) ) |
44 |
43
|
biimpd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 → ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) ) ) |
45 |
44
|
imp |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) ) |
46 |
|
breq1 |
⊢ ( 𝑦 = - 𝑥 → ( 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ↔ - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) ) ) |
47 |
46
|
rexbidv |
⊢ ( 𝑦 = - 𝑥 → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) ) ) |
48 |
47
|
ralbidv |
⊢ ( 𝑦 = - 𝑥 → ( ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) ) ) |
49 |
48
|
rspcev |
⊢ ( ( - 𝑥 ∈ ℝ ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ) |
50 |
38 45 49
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ) |
51 |
50
|
rexlimdva2 |
⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ) ) |
52 |
36 51
|
impbid |
⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) |
53 |
18
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) → - 𝑦 ∈ ℝ ) |
54 |
15
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) |
55 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → 𝑦 ∈ ℝ ) |
56 |
54 55
|
leneg3d |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → ( - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ↔ - 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) |
57 |
56
|
ralbidva |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ↔ ∀ 𝑗 ∈ 𝑍 - 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) |
58 |
57
|
biimpd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 → ∀ 𝑗 ∈ 𝑍 - 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) |
59 |
58
|
imp |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) → ∀ 𝑗 ∈ 𝑍 - 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) |
60 |
|
breq1 |
⊢ ( 𝑥 = - 𝑦 → ( 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ - 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) |
61 |
60
|
ralbidv |
⊢ ( 𝑥 = - 𝑦 → ( ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑗 ∈ 𝑍 - 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) ) |
62 |
61
|
rspcev |
⊢ ( ( - 𝑦 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝑍 - 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) |
63 |
53 59 62
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) |
64 |
63
|
rexlimdva2 |
⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) |
65 |
37
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → - 𝑥 ∈ ℝ ) |
66 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → 𝑥 ∈ ℝ ) |
67 |
15
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) |
68 |
66 67
|
lenegd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ - ( 𝐹 ‘ 𝑗 ) ≤ - 𝑥 ) ) |
69 |
68
|
ralbidva |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ - 𝑥 ) ) |
70 |
69
|
biimpd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) → ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ - 𝑥 ) ) |
71 |
70
|
imp |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ - 𝑥 ) |
72 |
|
brralrspcev |
⊢ ( ( - 𝑥 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ - 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) |
73 |
65 71 72
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) |
74 |
73
|
rexlimdva2 |
⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) ) |
75 |
64 74
|
impbid |
⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) |
76 |
52 75
|
anbi12d |
⊢ ( 𝜑 → ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) |
77 |
17 76
|
bitrd |
⊢ ( 𝜑 → ( ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) |
78 |
14 77
|
bitrd |
⊢ ( 𝜑 → ( ( lim inf ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) ) |