Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  climxrre Structured version   Visualization version   GIF version

Theorem climxrre 43011
Description: If a sequence ranging over the extended reals converges w.r.t. the standard topology on the complex numbers, then there exists an upper set of the integers over which the function is real-valued (the weaker hypothesis 𝐹 ∈ dom ⇝ is probably not enough, since in principle we could have +∞ ∈ ℂ and -∞ ∈ ℂ). (Contributed by Glauco Siliprandi, 5-Feb-2022.)
Hypotheses
Ref Expression
climxrre.m (𝜑𝑀 ∈ ℤ)
climxrre.z 𝑍 = (ℤ𝑀)
climxrre.f (𝜑𝐹:𝑍⟶ℝ*)
climxrre.a (𝜑𝐴 ∈ ℝ)
climxrre.c (𝜑𝐹𝐴)
Assertion
Ref Expression
climxrre (𝜑 → ∃𝑗𝑍 (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ)
Distinct variable groups:   𝐴,𝑗   𝑗,𝐹   𝑗,𝑀   𝑗,𝑍   𝜑,𝑗

Proof of Theorem climxrre
Dummy variables 𝑘 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 climxrre.m . . . . 5 (𝜑𝑀 ∈ ℤ)
21ad2antrr 726 . . . 4 (((𝜑 ∧ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → 𝑀 ∈ ℤ)
3 climxrre.z . . . 4 𝑍 = (ℤ𝑀)
4 climxrre.f . . . . 5 (𝜑𝐹:𝑍⟶ℝ*)
54ad2antrr 726 . . . 4 (((𝜑 ∧ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → 𝐹:𝑍⟶ℝ*)
6 climxrre.c . . . . 5 (𝜑𝐹𝐴)
76ad2antrr 726 . . . 4 (((𝜑 ∧ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → 𝐹𝐴)
8 simpr 488 . . . . . . . 8 ((𝜑 ∧ +∞ ∈ ℂ) → +∞ ∈ ℂ)
9 climxrre.a . . . . . . . . . 10 (𝜑𝐴 ∈ ℝ)
109recnd 10890 . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
1110adantr 484 . . . . . . . 8 ((𝜑 ∧ +∞ ∈ ℂ) → 𝐴 ∈ ℂ)
128, 11subcld 11218 . . . . . . 7 ((𝜑 ∧ +∞ ∈ ℂ) → (+∞ − 𝐴) ∈ ℂ)
13 renepnf 10910 . . . . . . . . . . 11 (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
1413necomd 2999 . . . . . . . . . 10 (𝐴 ∈ ℝ → +∞ ≠ 𝐴)
159, 14syl 17 . . . . . . . . 9 (𝜑 → +∞ ≠ 𝐴)
1615adantr 484 . . . . . . . 8 ((𝜑 ∧ +∞ ∈ ℂ) → +∞ ≠ 𝐴)
178, 11, 16subne0d 11227 . . . . . . 7 ((𝜑 ∧ +∞ ∈ ℂ) → (+∞ − 𝐴) ≠ 0)
1812, 17absrpcld 15044 . . . . . 6 ((𝜑 ∧ +∞ ∈ ℂ) → (abs‘(+∞ − 𝐴)) ∈ ℝ+)
1918adantr 484 . . . . 5 (((𝜑 ∧ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → (abs‘(+∞ − 𝐴)) ∈ ℝ+)
20 simpr 488 . . . . . . . 8 ((𝜑 ∧ -∞ ∈ ℂ) → -∞ ∈ ℂ)
2110adantr 484 . . . . . . . 8 ((𝜑 ∧ -∞ ∈ ℂ) → 𝐴 ∈ ℂ)
2220, 21subcld 11218 . . . . . . 7 ((𝜑 ∧ -∞ ∈ ℂ) → (-∞ − 𝐴) ∈ ℂ)
239adantr 484 . . . . . . . . 9 ((𝜑 ∧ -∞ ∈ ℂ) → 𝐴 ∈ ℝ)
24 renemnf 10911 . . . . . . . . . 10 (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
2524necomd 2999 . . . . . . . . 9 (𝐴 ∈ ℝ → -∞ ≠ 𝐴)
2623, 25syl 17 . . . . . . . 8 ((𝜑 ∧ -∞ ∈ ℂ) → -∞ ≠ 𝐴)
2720, 21, 26subne0d 11227 . . . . . . 7 ((𝜑 ∧ -∞ ∈ ℂ) → (-∞ − 𝐴) ≠ 0)
2822, 27absrpcld 15044 . . . . . 6 ((𝜑 ∧ -∞ ∈ ℂ) → (abs‘(-∞ − 𝐴)) ∈ ℝ+)
2928adantlr 715 . . . . 5 (((𝜑 ∧ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → (abs‘(-∞ − 𝐴)) ∈ ℝ+)
3019, 29ifcld 4501 . . . 4 (((𝜑 ∧ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → if((abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴)), (abs‘(+∞ − 𝐴)), (abs‘(-∞ − 𝐴))) ∈ ℝ+)
3119rpred 12657 . . . . . 6 (((𝜑 ∧ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → (abs‘(+∞ − 𝐴)) ∈ ℝ)
3229rpred 12657 . . . . . 6 (((𝜑 ∧ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → (abs‘(-∞ − 𝐴)) ∈ ℝ)
3331, 32min1d 42732 . . . . 5 (((𝜑 ∧ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → if((abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴)), (abs‘(+∞ − 𝐴)), (abs‘(-∞ − 𝐴))) ≤ (abs‘(+∞ − 𝐴)))
3433adantr 484 . . . 4 ((((𝜑 ∧ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) ∧ +∞ ∈ ℂ) → if((abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴)), (abs‘(+∞ − 𝐴)), (abs‘(-∞ − 𝐴))) ≤ (abs‘(+∞ − 𝐴)))
3531, 32min2d 42733 . . . . 5 (((𝜑 ∧ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → if((abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴)), (abs‘(+∞ − 𝐴)), (abs‘(-∞ − 𝐴))) ≤ (abs‘(-∞ − 𝐴)))
3635adantr 484 . . . 4 ((((𝜑 ∧ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → if((abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴)), (abs‘(+∞ − 𝐴)), (abs‘(-∞ − 𝐴))) ≤ (abs‘(-∞ − 𝐴)))
372, 3, 5, 7, 30, 34, 36climxrrelem 43010 . . 3 (((𝜑 ∧ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → ∃𝑗𝑍 (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ)
381ad2antrr 726 . . . 4 (((𝜑 ∧ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) → 𝑀 ∈ ℤ)
394ad2antrr 726 . . . 4 (((𝜑 ∧ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) → 𝐹:𝑍⟶ℝ*)
406ad2antrr 726 . . . 4 (((𝜑 ∧ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) → 𝐹𝐴)
4118adantr 484 . . . 4 (((𝜑 ∧ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) → (abs‘(+∞ − 𝐴)) ∈ ℝ+)
4218rpred 12657 . . . . . 6 ((𝜑 ∧ +∞ ∈ ℂ) → (abs‘(+∞ − 𝐴)) ∈ ℝ)
4342leidd 11427 . . . . 5 ((𝜑 ∧ +∞ ∈ ℂ) → (abs‘(+∞ − 𝐴)) ≤ (abs‘(+∞ − 𝐴)))
4443ad2antrr 726 . . . 4 ((((𝜑 ∧ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ +∞ ∈ ℂ) → (abs‘(+∞ − 𝐴)) ≤ (abs‘(+∞ − 𝐴)))
45 pm2.21 123 . . . . . 6 (¬ -∞ ∈ ℂ → (-∞ ∈ ℂ → (abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴))))
4645imp 410 . . . . 5 ((¬ -∞ ∈ ℂ ∧ -∞ ∈ ℂ) → (abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴)))
4746adantll 714 . . . 4 ((((𝜑 ∧ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → (abs‘(+∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴)))
4838, 3, 39, 40, 41, 44, 47climxrrelem 43010 . . 3 (((𝜑 ∧ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) → ∃𝑗𝑍 (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ)
4937, 48pm2.61dan 813 . 2 ((𝜑 ∧ +∞ ∈ ℂ) → ∃𝑗𝑍 (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ)
501ad2antrr 726 . . . 4 (((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → 𝑀 ∈ ℤ)
514ad2antrr 726 . . . 4 (((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → 𝐹:𝑍⟶ℝ*)
526ad2antrr 726 . . . 4 (((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → 𝐹𝐴)
5328adantlr 715 . . . 4 (((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → (abs‘(-∞ − 𝐴)) ∈ ℝ+)
54 pm2.21 123 . . . . . 6 (¬ +∞ ∈ ℂ → (+∞ ∈ ℂ → (abs‘(-∞ − 𝐴)) ≤ (abs‘(+∞ − 𝐴))))
5554imp 410 . . . . 5 ((¬ +∞ ∈ ℂ ∧ +∞ ∈ ℂ) → (abs‘(-∞ − 𝐴)) ≤ (abs‘(+∞ − 𝐴)))
5655ad4ant24 754 . . . 4 ((((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) ∧ +∞ ∈ ℂ) → (abs‘(-∞ − 𝐴)) ≤ (abs‘(+∞ − 𝐴)))
5728rpred 12657 . . . . . 6 ((𝜑 ∧ -∞ ∈ ℂ) → (abs‘(-∞ − 𝐴)) ∈ ℝ)
5857leidd 11427 . . . . 5 ((𝜑 ∧ -∞ ∈ ℂ) → (abs‘(-∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴)))
5958ad4ant13 751 . . . 4 ((((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → (abs‘(-∞ − 𝐴)) ≤ (abs‘(-∞ − 𝐴)))
6050, 3, 51, 52, 53, 56, 59climxrrelem 43010 . . 3 (((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ -∞ ∈ ℂ) → ∃𝑗𝑍 (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ)
61 nfv 1922 . . . . . . 7 𝑘((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ)
62 nfv 1922 . . . . . . . 8 𝑘 𝑗𝑍
63 nfra1 3143 . . . . . . . 8 𝑘𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ
6462, 63nfan 1907 . . . . . . 7 𝑘(𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)
6561, 64nfan 1907 . . . . . 6 𝑘(((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ))
66 simp-4l 783 . . . . . . . 8 (((((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝜑)
673uztrn2 12486 . . . . . . . . . 10 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
6867adantlr 715 . . . . . . . . 9 (((𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
6968adantll 714 . . . . . . . 8 (((((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
70 simpr 488 . . . . . . . . 9 ((𝜑𝑘𝑍) → 𝑘𝑍)
714fdmd 6577 . . . . . . . . . 10 (𝜑 → dom 𝐹 = 𝑍)
7271adantr 484 . . . . . . . . 9 ((𝜑𝑘𝑍) → dom 𝐹 = 𝑍)
7370, 72eleqtrrd 2843 . . . . . . . 8 ((𝜑𝑘𝑍) → 𝑘 ∈ dom 𝐹)
7466, 69, 73syl2anc 587 . . . . . . 7 (((((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ dom 𝐹)
754ffvelrnda 6925 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ*)
7666, 69, 75syl2anc 587 . . . . . . . 8 (((((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ ℝ*)
77 rspa 3131 . . . . . . . . . . 11 ((∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ ℂ)
7877adantll 714 . . . . . . . . . 10 (((𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ ℂ)
7978adantll 714 . . . . . . . . 9 (((((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ ℂ)
80 simpllr 776 . . . . . . . . 9 (((((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ𝑗)) → ¬ -∞ ∈ ℂ)
81 nelne2 3042 . . . . . . . . 9 (((𝐹𝑘) ∈ ℂ ∧ ¬ -∞ ∈ ℂ) → (𝐹𝑘) ≠ -∞)
8279, 80, 81syl2anc 587 . . . . . . . 8 (((((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ≠ -∞)
83 simp-4r 784 . . . . . . . . 9 (((((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ𝑗)) → ¬ +∞ ∈ ℂ)
84 nelne2 3042 . . . . . . . . 9 (((𝐹𝑘) ∈ ℂ ∧ ¬ +∞ ∈ ℂ) → (𝐹𝑘) ≠ +∞)
8579, 83, 84syl2anc 587 . . . . . . . 8 (((((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ≠ +∞)
8676, 82, 85xrred 42624 . . . . . . 7 (((((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ ℝ)
8774, 86jca 515 . . . . . 6 (((((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ ℝ))
8865, 87ralrimia 3421 . . . . 5 ((((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)) → ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ ℝ))
894ffund 6570 . . . . . . 7 (𝜑 → Fun 𝐹)
90 ffvresb 6962 . . . . . . 7 (Fun 𝐹 → ((𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ ↔ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ ℝ)))
9189, 90syl 17 . . . . . 6 (𝜑 → ((𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ ↔ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ ℝ)))
9291ad3antrrr 730 . . . . 5 ((((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)) → ((𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ ↔ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ ℝ)))
9388, 92mpbird 260 . . . 4 ((((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) ∧ (𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)) → (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ)
94 r19.26 3095 . . . . . . . . 9 (∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < 1) ↔ (∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 1))
9594simplbi 501 . . . . . . . 8 (∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < 1) → ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)
9695ad2antll 729 . . . . . . 7 ((𝜑 ∧ (𝑗 ∈ ℤ ∧ ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < 1))) → ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)
97 breq2 5073 . . . . . . . . . 10 (𝑥 = 1 → ((abs‘((𝐹𝑘) − 𝐴)) < 𝑥 ↔ (abs‘((𝐹𝑘) − 𝐴)) < 1))
9897anbi2d 632 . . . . . . . . 9 (𝑥 = 1 → (((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < 𝑥) ↔ ((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < 1)))
9998rexralbidv 3230 . . . . . . . 8 (𝑥 = 1 → (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < 1)))
1003fvexi 6752 . . . . . . . . . . . . 13 𝑍 ∈ V
101100a1i 11 . . . . . . . . . . . 12 (𝜑𝑍 ∈ V)
1024, 101fexd 7064 . . . . . . . . . . 11 (𝜑𝐹 ∈ V)
103 eqidd 2740 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℤ) → (𝐹𝑘) = (𝐹𝑘))
104102, 103clim 15087 . . . . . . . . . 10 (𝜑 → (𝐹𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < 𝑥))))
1056, 104mpbid 235 . . . . . . . . 9 (𝜑 → (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < 𝑥)))
106105simprd 499 . . . . . . . 8 (𝜑 → ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < 𝑥))
107 1rp 12619 . . . . . . . . 9 1 ∈ ℝ+
108107a1i 11 . . . . . . . 8 (𝜑 → 1 ∈ ℝ+)
10999, 106, 108rspcdva 3554 . . . . . . 7 (𝜑 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) ∈ ℂ ∧ (abs‘((𝐹𝑘) − 𝐴)) < 1))
11096, 109reximddv 3204 . . . . . 6 (𝜑 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)
1113rexuz3 14944 . . . . . . 7 (𝑀 ∈ ℤ → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ))
1121, 111syl 17 . . . . . 6 (𝜑 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ))
113110, 112mpbird 260 . . . . 5 (𝜑 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)
114113ad2antrr 726 . . . 4 (((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) ∈ ℂ)
11593, 114reximddv 3204 . . 3 (((𝜑 ∧ ¬ +∞ ∈ ℂ) ∧ ¬ -∞ ∈ ℂ) → ∃𝑗𝑍 (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ)
11660, 115pm2.61dan 813 . 2 ((𝜑 ∧ ¬ +∞ ∈ ℂ) → ∃𝑗𝑍 (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ)
11749, 116pm2.61dan 813 1 (𝜑 → ∃𝑗𝑍 (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1543  wcel 2112  wne 2943  wral 3064  wrex 3065  Vcvv 3423  ifcif 4455   class class class wbr 5069  dom cdm 5568  cres 5570  Fun wfun 6394  wf 6396  cfv 6400  (class class class)co 7234  cc 10756  cr 10757  1c1 10759  +∞cpnf 10893  -∞cmnf 10894  *cxr 10895   < clt 10896  cle 10897  cmin 11091  cz 12205  cuz 12467  +crp 12615  abscabs 14829  cli 15077
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5195  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544  ax-cnex 10814  ax-resscn 10815  ax-1cn 10816  ax-icn 10817  ax-addcl 10818  ax-addrcl 10819  ax-mulcl 10820  ax-mulrcl 10821  ax-mulcom 10822  ax-addass 10823  ax-mulass 10824  ax-distr 10825  ax-i2m1 10826  ax-1ne0 10827  ax-1rid 10828  ax-rnegex 10829  ax-rrecex 10830  ax-cnre 10831  ax-pre-lttri 10832  ax-pre-lttrn 10833  ax-pre-ltadd 10834  ax-pre-mulgt0 10835  ax-pre-sup 10836
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4836  df-iun 4922  df-br 5070  df-opab 5132  df-mpt 5152  df-tr 5178  df-id 5471  df-eprel 5477  df-po 5485  df-so 5486  df-fr 5526  df-we 5528  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-pred 6178  df-ord 6236  df-on 6237  df-lim 6238  df-suc 6239  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-riota 7191  df-ov 7237  df-oprab 7238  df-mpo 7239  df-om 7666  df-2nd 7783  df-wrecs 8070  df-recs 8131  df-rdg 8169  df-er 8414  df-en 8650  df-dom 8651  df-sdom 8652  df-sup 9087  df-pnf 10898  df-mnf 10899  df-xr 10900  df-ltxr 10901  df-le 10902  df-sub 11093  df-neg 11094  df-div 11519  df-nn 11860  df-2 11922  df-3 11923  df-n0 12120  df-z 12206  df-uz 12468  df-rp 12616  df-seq 13606  df-exp 13667  df-cj 14694  df-re 14695  df-im 14696  df-sqrt 14830  df-abs 14831  df-clim 15081
This theorem is referenced by:  xlimclim2  43101
  Copyright terms: Public domain W3C validator