Step |
Hyp |
Ref |
Expression |
1 |
|
climxrre.m |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
2 |
|
climxrre.z |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
3 |
|
climxrre.f |
⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* ) |
4 |
|
climxrre.a |
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
5 |
|
climxrre.c |
⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 ) |
6 |
1
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → 𝑀 ∈ ℤ ) |
7 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → 𝐹 : 𝑍 ⟶ ℝ* ) |
8 |
5
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → 𝐹 ⇝ 𝐴 ) |
9 |
|
simpr |
⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → +∞ ∈ ℂ ) |
10 |
4
|
recnd |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
11 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → 𝐴 ∈ ℂ ) |
12 |
9 11
|
subcld |
⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → ( +∞ − 𝐴 ) ∈ ℂ ) |
13 |
|
renepnf |
⊢ ( 𝐴 ∈ ℝ → 𝐴 ≠ +∞ ) |
14 |
13
|
necomd |
⊢ ( 𝐴 ∈ ℝ → +∞ ≠ 𝐴 ) |
15 |
4 14
|
syl |
⊢ ( 𝜑 → +∞ ≠ 𝐴 ) |
16 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → +∞ ≠ 𝐴 ) |
17 |
9 11 16
|
subne0d |
⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → ( +∞ − 𝐴 ) ≠ 0 ) |
18 |
12 17
|
absrpcld |
⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ∈ ℝ+ ) |
19 |
18
|
adantr |
⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ∈ ℝ+ ) |
20 |
|
simpr |
⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → -∞ ∈ ℂ ) |
21 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → 𝐴 ∈ ℂ ) |
22 |
20 21
|
subcld |
⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → ( -∞ − 𝐴 ) ∈ ℂ ) |
23 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → 𝐴 ∈ ℝ ) |
24 |
|
renemnf |
⊢ ( 𝐴 ∈ ℝ → 𝐴 ≠ -∞ ) |
25 |
24
|
necomd |
⊢ ( 𝐴 ∈ ℝ → -∞ ≠ 𝐴 ) |
26 |
23 25
|
syl |
⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → -∞ ≠ 𝐴 ) |
27 |
20 21 26
|
subne0d |
⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → ( -∞ − 𝐴 ) ≠ 0 ) |
28 |
22 27
|
absrpcld |
⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ∈ ℝ+ ) |
29 |
28
|
adantlr |
⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ∈ ℝ+ ) |
30 |
19 29
|
ifcld |
⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → if ( ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) , ( abs ‘ ( +∞ − 𝐴 ) ) , ( abs ‘ ( -∞ − 𝐴 ) ) ) ∈ ℝ+ ) |
31 |
19
|
rpred |
⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ∈ ℝ ) |
32 |
29
|
rpred |
⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ∈ ℝ ) |
33 |
31 32
|
min1d |
⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → if ( ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) , ( abs ‘ ( +∞ − 𝐴 ) ) , ( abs ‘ ( -∞ − 𝐴 ) ) ) ≤ ( abs ‘ ( +∞ − 𝐴 ) ) ) |
34 |
33
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) ∧ +∞ ∈ ℂ ) → if ( ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) , ( abs ‘ ( +∞ − 𝐴 ) ) , ( abs ‘ ( -∞ − 𝐴 ) ) ) ≤ ( abs ‘ ( +∞ − 𝐴 ) ) ) |
35 |
31 32
|
min2d |
⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → if ( ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) , ( abs ‘ ( +∞ − 𝐴 ) ) , ( abs ‘ ( -∞ − 𝐴 ) ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) ) |
36 |
35
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → if ( ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) , ( abs ‘ ( +∞ − 𝐴 ) ) , ( abs ‘ ( -∞ − 𝐴 ) ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) ) |
37 |
6 2 7 8 30 34 36
|
climxrrelem |
⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) |
38 |
1
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) → 𝑀 ∈ ℤ ) |
39 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) → 𝐹 : 𝑍 ⟶ ℝ* ) |
40 |
5
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) → 𝐹 ⇝ 𝐴 ) |
41 |
18
|
adantr |
⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ∈ ℝ+ ) |
42 |
18
|
rpred |
⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ∈ ℝ ) |
43 |
42
|
leidd |
⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( +∞ − 𝐴 ) ) ) |
44 |
43
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ +∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( +∞ − 𝐴 ) ) ) |
45 |
|
pm2.21 |
⊢ ( ¬ -∞ ∈ ℂ → ( -∞ ∈ ℂ → ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) ) ) |
46 |
45
|
imp |
⊢ ( ( ¬ -∞ ∈ ℂ ∧ -∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) ) |
47 |
46
|
adantll |
⊢ ( ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ( abs ‘ ( +∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) ) |
48 |
38 2 39 40 41 44 47
|
climxrrelem |
⊢ ( ( ( 𝜑 ∧ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) |
49 |
37 48
|
pm2.61dan |
⊢ ( ( 𝜑 ∧ +∞ ∈ ℂ ) → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) |
50 |
1
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → 𝑀 ∈ ℤ ) |
51 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → 𝐹 : 𝑍 ⟶ ℝ* ) |
52 |
5
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → 𝐹 ⇝ 𝐴 ) |
53 |
28
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ∈ ℝ+ ) |
54 |
|
pm2.21 |
⊢ ( ¬ +∞ ∈ ℂ → ( +∞ ∈ ℂ → ( abs ‘ ( -∞ − 𝐴 ) ) ≤ ( abs ‘ ( +∞ − 𝐴 ) ) ) ) |
55 |
54
|
imp |
⊢ ( ( ¬ +∞ ∈ ℂ ∧ +∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ≤ ( abs ‘ ( +∞ − 𝐴 ) ) ) |
56 |
55
|
ad4ant24 |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) ∧ +∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ≤ ( abs ‘ ( +∞ − 𝐴 ) ) ) |
57 |
28
|
rpred |
⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ∈ ℝ ) |
58 |
57
|
leidd |
⊢ ( ( 𝜑 ∧ -∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) ) |
59 |
58
|
ad4ant13 |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ( abs ‘ ( -∞ − 𝐴 ) ) ≤ ( abs ‘ ( -∞ − 𝐴 ) ) ) |
60 |
50 2 51 52 53 56 59
|
climxrrelem |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ -∞ ∈ ℂ ) → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) |
61 |
|
nfv |
⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) |
62 |
|
nfv |
⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍 |
63 |
|
nfra1 |
⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ |
64 |
62 63
|
nfan |
⊢ Ⅎ 𝑘 ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
65 |
61 64
|
nfan |
⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) |
66 |
|
simp-4l |
⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝜑 ) |
67 |
2
|
uztrn2 |
⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 ) |
68 |
67
|
adantlr |
⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 ) |
69 |
68
|
adantll |
⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 ) |
70 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝑍 ) |
71 |
3
|
fdmd |
⊢ ( 𝜑 → dom 𝐹 = 𝑍 ) |
72 |
71
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → dom 𝐹 = 𝑍 ) |
73 |
70 72
|
eleqtrrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ dom 𝐹 ) |
74 |
66 69 73
|
syl2anc |
⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ dom 𝐹 ) |
75 |
3
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ) |
76 |
66 69 75
|
syl2anc |
⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ) |
77 |
|
rspa |
⊢ ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
78 |
77
|
adantll |
⊢ ( ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
79 |
78
|
adantll |
⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
80 |
|
simpllr |
⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ¬ -∞ ∈ ℂ ) |
81 |
|
nelne2 |
⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ¬ -∞ ∈ ℂ ) → ( 𝐹 ‘ 𝑘 ) ≠ -∞ ) |
82 |
79 80 81
|
syl2anc |
⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ≠ -∞ ) |
83 |
|
simp-4r |
⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ¬ +∞ ∈ ℂ ) |
84 |
|
nelne2 |
⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ¬ +∞ ∈ ℂ ) → ( 𝐹 ‘ 𝑘 ) ≠ +∞ ) |
85 |
79 83 84
|
syl2anc |
⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ≠ +∞ ) |
86 |
76 82 85
|
xrred |
⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) |
87 |
74 86
|
jca |
⊢ ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) |
88 |
65 87
|
ralrimia |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) |
89 |
3
|
ffund |
⊢ ( 𝜑 → Fun 𝐹 ) |
90 |
|
ffvresb |
⊢ ( Fun 𝐹 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) ) |
91 |
89 90
|
syl |
⊢ ( 𝜑 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) ) |
92 |
91
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ) ) |
93 |
88 92
|
mpbird |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) |
94 |
|
r19.26 |
⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 1 ) ↔ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 1 ) ) |
95 |
94
|
simplbi |
⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 1 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
96 |
95
|
ad2antll |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ℤ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 1 ) ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
97 |
|
breq2 |
⊢ ( 𝑥 = 1 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 1 ) ) |
98 |
97
|
anbi2d |
⊢ ( 𝑥 = 1 → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 1 ) ) ) |
99 |
98
|
rexralbidv |
⊢ ( 𝑥 = 1 → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 1 ) ) ) |
100 |
2
|
fvexi |
⊢ 𝑍 ∈ V |
101 |
100
|
a1i |
⊢ ( 𝜑 → 𝑍 ∈ V ) |
102 |
3 101
|
fexd |
⊢ ( 𝜑 → 𝐹 ∈ V ) |
103 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ) |
104 |
102 103
|
clim |
⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) ) |
105 |
5 104
|
mpbid |
⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) |
106 |
105
|
simprd |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) |
107 |
|
1rp |
⊢ 1 ∈ ℝ+ |
108 |
107
|
a1i |
⊢ ( 𝜑 → 1 ∈ ℝ+ ) |
109 |
99 106 108
|
rspcdva |
⊢ ( 𝜑 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 1 ) ) |
110 |
96 109
|
reximddv |
⊢ ( 𝜑 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
111 |
2
|
rexuz3 |
⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) |
112 |
1 111
|
syl |
⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ) |
113 |
110 112
|
mpbird |
⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
114 |
113
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) |
115 |
93 114
|
reximddv |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) ∧ ¬ -∞ ∈ ℂ ) → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) |
116 |
60 115
|
pm2.61dan |
⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ℂ ) → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) |
117 |
49 116
|
pm2.61dan |
⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) |