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

Theorem climxlim2lem 40566
Description: In this lemma for climxlim2 40567 there is the additional assumption that the converging function is complex valued on the whole domain. (Contributed by Glauco Siliprandi, 5-Feb-2022.)
Hypotheses
Ref Expression
climxlim2lem.1 (𝜑𝑀 ∈ ℤ)
climxlim2lem.2 𝑍 = (ℤ𝑀)
climxlim2lem.3 (𝜑𝐹:𝑍⟶ℝ*)
climxlim2lem.4 (𝜑𝐹:𝑍⟶ℂ)
climxlim2lem.5 (𝜑𝐹𝐴)
Assertion
Ref Expression
climxlim2lem (𝜑𝐹~~>*𝐴)

Proof of Theorem climxlim2lem
Dummy variables 𝑗 𝑘 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 climxlim2lem.5 . . . 4 (𝜑𝐹𝐴)
21adantr 472 . . 3 ((𝜑𝐴 ∈ ℝ) → 𝐹𝐴)
3 climxlim2lem.1 . . . . 5 (𝜑𝑀 ∈ ℤ)
43adantr 472 . . . 4 ((𝜑𝐴 ∈ ℝ) → 𝑀 ∈ ℤ)
5 climxlim2lem.2 . . . 4 𝑍 = (ℤ𝑀)
6 climxlim2lem.3 . . . . 5 (𝜑𝐹:𝑍⟶ℝ*)
76adantr 472 . . . 4 ((𝜑𝐴 ∈ ℝ) → 𝐹:𝑍⟶ℝ*)
8 simpr 479 . . . 4 ((𝜑𝐴 ∈ ℝ) → 𝐴 ∈ ℝ)
94, 5, 7, 8xlimclim2 40561 . . 3 ((𝜑𝐴 ∈ ℝ) → (𝐹~~>*𝐴𝐹𝐴))
102, 9mpbird 247 . 2 ((𝜑𝐴 ∈ ℝ) → 𝐹~~>*𝐴)
11 climxlim2lem.4 . . . . . . . . . . . 12 (𝜑𝐹:𝑍⟶ℂ)
1211ffvelrnda 6514 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
1312anim1i 593 . . . . . . . . . 10 (((𝜑𝑘𝑍) ∧ (𝐹𝑘) ≠ 𝐴) → ((𝐹𝑘) ∈ ℂ ∧ (𝐹𝑘) ≠ 𝐴))
1413adantllr 757 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑦 ∈ ℝ* ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴)))) ∧ 𝑘𝑍) ∧ (𝐹𝑘) ≠ 𝐴) → ((𝐹𝑘) ∈ ℂ ∧ (𝐹𝑘) ≠ 𝐴))
156adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ ∀𝑦 ∈ ℝ* ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴)))) → 𝐹:𝑍⟶ℝ*)
1615ffvelrnda 6514 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑦 ∈ ℝ* ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴)))) ∧ 𝑘𝑍) → (𝐹𝑘) ∈ ℝ*)
17 simplr 809 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑦 ∈ ℝ* ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴)))) ∧ 𝑘𝑍) → ∀𝑦 ∈ ℝ* ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))))
18 eleq1 2819 . . . . . . . . . . . . . 14 (𝑦 = (𝐹𝑘) → (𝑦 ∈ ℂ ↔ (𝐹𝑘) ∈ ℂ))
19 neeq1 2986 . . . . . . . . . . . . . 14 (𝑦 = (𝐹𝑘) → (𝑦𝐴 ↔ (𝐹𝑘) ≠ 𝐴))
2018, 19anbi12d 749 . . . . . . . . . . . . 13 (𝑦 = (𝐹𝑘) → ((𝑦 ∈ ℂ ∧ 𝑦𝐴) ↔ ((𝐹𝑘) ∈ ℂ ∧ (𝐹𝑘) ≠ 𝐴)))
21 oveq1 6812 . . . . . . . . . . . . . . 15 (𝑦 = (𝐹𝑘) → (𝑦𝐴) = ((𝐹𝑘) − 𝐴))
2221fveq2d 6348 . . . . . . . . . . . . . 14 (𝑦 = (𝐹𝑘) → (abs‘(𝑦𝐴)) = (abs‘((𝐹𝑘) − 𝐴)))
2322breq2d 4808 . . . . . . . . . . . . 13 (𝑦 = (𝐹𝑘) → (𝑥 ≤ (abs‘(𝑦𝐴)) ↔ 𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))))
2420, 23imbi12d 333 . . . . . . . . . . . 12 (𝑦 = (𝐹𝑘) → (((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))) ↔ (((𝐹𝑘) ∈ ℂ ∧ (𝐹𝑘) ≠ 𝐴) → 𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))))
2524rspcva 3439 . . . . . . . . . . 11 (((𝐹𝑘) ∈ ℝ* ∧ ∀𝑦 ∈ ℝ* ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴)))) → (((𝐹𝑘) ∈ ℂ ∧ (𝐹𝑘) ≠ 𝐴) → 𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))))
2616, 17, 25syl2anc 696 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑦 ∈ ℝ* ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴)))) ∧ 𝑘𝑍) → (((𝐹𝑘) ∈ ℂ ∧ (𝐹𝑘) ≠ 𝐴) → 𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))))
2726adantr 472 . . . . . . . . 9 ((((𝜑 ∧ ∀𝑦 ∈ ℝ* ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴)))) ∧ 𝑘𝑍) ∧ (𝐹𝑘) ≠ 𝐴) → (((𝐹𝑘) ∈ ℂ ∧ (𝐹𝑘) ≠ 𝐴) → 𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))))
2814, 27mpd 15 . . . . . . . 8 ((((𝜑 ∧ ∀𝑦 ∈ ℝ* ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴)))) ∧ 𝑘𝑍) ∧ (𝐹𝑘) ≠ 𝐴) → 𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))
2928ex 449 . . . . . . 7 (((𝜑 ∧ ∀𝑦 ∈ ℝ* ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴)))) ∧ 𝑘𝑍) → ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))))
3029ralrimiva 3096 . . . . . 6 ((𝜑 ∧ ∀𝑦 ∈ ℝ* ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴)))) → ∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))))
3130ad4ant14 1206 . . . . 5 ((((𝜑 ∧ ¬ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ ℝ+) ∧ ∀𝑦 ∈ ℝ* ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴)))) → ∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))))
32 climcl 14421 . . . . . . . 8 (𝐹𝐴𝐴 ∈ ℂ)
331, 32syl 17 . . . . . . 7 (𝜑𝐴 ∈ ℂ)
3433adantr 472 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 ∈ ℝ) → 𝐴 ∈ ℂ)
35 simpr 479 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 ∈ ℝ) → ¬ 𝐴 ∈ ℝ)
36 prfi 8392 . . . . . . 7 {+∞, -∞} ∈ Fin
3736a1i 11 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 ∈ ℝ) → {+∞, -∞} ∈ Fin)
38 df-xr 10262 . . . . . 6 * = (ℝ ∪ {+∞, -∞})
3934, 35, 37, 38cnrefiisp 40551 . . . . 5 ((𝜑 ∧ ¬ 𝐴 ∈ ℝ) → ∃𝑥 ∈ ℝ+𝑦 ∈ ℝ* ((𝑦 ∈ ℂ ∧ 𝑦𝐴) → 𝑥 ≤ (abs‘(𝑦𝐴))))
4031, 39reximddv3 39834 . . . 4 ((𝜑 ∧ ¬ 𝐴 ∈ ℝ) → ∃𝑥 ∈ ℝ+𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))))
41 nfv 1984 . . . . . . . . . 10 𝑘(𝜑𝑥 ∈ ℝ+)
42 nfra1 3071 . . . . . . . . . 10 𝑘𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))
4341, 42nfan 1969 . . . . . . . . 9 𝑘((𝜑𝑥 ∈ ℝ+) ∧ ∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))))
44 nfv 1984 . . . . . . . . 9 𝑘 𝑗𝑍
4543, 44nfan 1969 . . . . . . . 8 𝑘(((𝜑𝑥 ∈ ℝ+) ∧ ∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))) ∧ 𝑗𝑍)
46 nfra1 3071 . . . . . . . 8 𝑘𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥
4745, 46nfan 1969 . . . . . . 7 𝑘((((𝜑𝑥 ∈ ℝ+) ∧ ∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥)
48 simpll 807 . . . . . . . . . . . 12 (((∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))))
495uztrn2 11889 . . . . . . . . . . . . 13 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
5049adantll 752 . . . . . . . . . . . 12 (((∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
51 rspa 3060 . . . . . . . . . . . 12 ((∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))) ∧ 𝑘𝑍) → ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))))
5248, 50, 51syl2anc 696 . . . . . . . . . . 11 (((∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))))
53 neqne 2932 . . . . . . . . . . 11 (¬ (𝐹𝑘) = 𝐴 → (𝐹𝑘) ≠ 𝐴)
5452, 53impel 486 . . . . . . . . . 10 ((((∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ ¬ (𝐹𝑘) = 𝐴) → 𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))
5554ad5ant2345 1470 . . . . . . . . 9 ((((((𝜑𝑥 ∈ ℝ+) ∧ ∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ ¬ (𝐹𝑘) = 𝐴) → 𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))
5655adantllr 757 . . . . . . . 8 (((((((𝜑𝑥 ∈ ℝ+) ∧ ∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ ¬ (𝐹𝑘) = 𝐴) → 𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))
57 rspa 3060 . . . . . . . . . . . 12 ((∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥𝑘 ∈ (ℤ𝑗)) → (abs‘((𝐹𝑘) − 𝐴)) < 𝑥)
5857adantll 752 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥) ∧ 𝑘 ∈ (ℤ𝑗)) → (abs‘((𝐹𝑘) − 𝐴)) < 𝑥)
5911ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝐹:𝑍⟶ℂ)
6049adantll 752 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
6159, 60ffvelrnd 6515 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ ℂ)
6261adantlr 753 . . . . . . . . . . . . . . 15 ((((𝜑𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ ℂ)
6333ad3antrrr 768 . . . . . . . . . . . . . . 15 ((((𝜑𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝐴 ∈ ℂ)
6462, 63subcld 10576 . . . . . . . . . . . . . 14 ((((𝜑𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝐹𝑘) − 𝐴) ∈ ℂ)
6564abscld 14366 . . . . . . . . . . . . 13 ((((𝜑𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥) ∧ 𝑘 ∈ (ℤ𝑗)) → (abs‘((𝐹𝑘) − 𝐴)) ∈ ℝ)
6665adantl3r 803 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥) ∧ 𝑘 ∈ (ℤ𝑗)) → (abs‘((𝐹𝑘) − 𝐴)) ∈ ℝ)
67 simpr 479 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
6867ad3antrrr 768 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑥 ∈ ℝ+)
6968rpred 12057 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑥 ∈ ℝ)
7066, 69ltnled 10368 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥) ∧ 𝑘 ∈ (ℤ𝑗)) → ((abs‘((𝐹𝑘) − 𝐴)) < 𝑥 ↔ ¬ 𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴))))
7158, 70mpbid 222 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥) ∧ 𝑘 ∈ (ℤ𝑗)) → ¬ 𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))
7271adantl3r 803 . . . . . . . . 9 ((((((𝜑𝑥 ∈ ℝ+) ∧ ∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥) ∧ 𝑘 ∈ (ℤ𝑗)) → ¬ 𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))
7372adantr 472 . . . . . . . 8 (((((((𝜑𝑥 ∈ ℝ+) ∧ ∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ ¬ (𝐹𝑘) = 𝐴) → ¬ 𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))
7456, 73condan 870 . . . . . . 7 ((((((𝜑𝑥 ∈ ℝ+) ∧ ∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) = 𝐴)
7547, 74ralrimia 39806 . . . . . 6 (((((𝜑𝑥 ∈ ℝ+) ∧ ∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥) → ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) = 𝐴)
76 nfcv 2894 . . . . . . . . . . 11 𝑘𝐹
7776, 3, 5, 11climuz 40471 . . . . . . . . . 10 (𝜑 → (𝐹𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥)))
781, 77mpbid 222 . . . . . . . . 9 (𝜑 → (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥))
7978simprd 482 . . . . . . . 8 (𝜑 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥)
8079r19.21bi 3062 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥)
8180adantr 472 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ ∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘((𝐹𝑘) − 𝐴)) < 𝑥)
8275, 81reximddv3 39834 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ ∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) = 𝐴)
8382adantllr 757 . . . 4 ((((𝜑 ∧ ¬ 𝐴 ∈ ℝ) ∧ 𝑥 ∈ ℝ+) ∧ ∀𝑘𝑍 ((𝐹𝑘) ≠ 𝐴𝑥 ≤ (abs‘((𝐹𝑘) − 𝐴)))) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) = 𝐴)
8440, 83rexlimddv2 40544 . . 3 ((𝜑 ∧ ¬ 𝐴 ∈ ℝ) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝐹𝑘) = 𝐴)
85 nfv 1984 . . . . 5 𝑘((𝜑 ∧ ¬ 𝐴 ∈ ℝ) ∧ 𝑗𝑍)
86 nfra1 3071 . . . . 5 𝑘𝑘 ∈ (ℤ𝑗)(𝐹𝑘) = 𝐴
8785, 86nfan 1969 . . . 4 𝑘(((𝜑 ∧ ¬ 𝐴 ∈ ℝ) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) = 𝐴)
886ad3antrrr 768 . . . 4 ((((𝜑 ∧ ¬ 𝐴 ∈ ℝ) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) = 𝐴) → 𝐹:𝑍⟶ℝ*)
89 simplr 809 . . . 4 ((((𝜑 ∧ ¬ 𝐴 ∈ ℝ) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) = 𝐴) → 𝑗𝑍)
905uzid3 40152 . . . . . . . 8 (𝑗𝑍𝑗 ∈ (ℤ𝑗))
91 fveq2 6344 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝐹𝑘) = (𝐹𝑗))
9291eqeq1d 2754 . . . . . . . . 9 (𝑘 = 𝑗 → ((𝐹𝑘) = 𝐴 ↔ (𝐹𝑗) = 𝐴))
9392rspcva 3439 . . . . . . . 8 ((𝑗 ∈ (ℤ𝑗) ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) = 𝐴) → (𝐹𝑗) = 𝐴)
9490, 93sylan 489 . . . . . . 7 ((𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) = 𝐴) → (𝐹𝑗) = 𝐴)
95943adant1 1124 . . . . . 6 ((𝜑𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) = 𝐴) → (𝐹𝑗) = 𝐴)
966ffvelrnda 6514 . . . . . . 7 ((𝜑𝑗𝑍) → (𝐹𝑗) ∈ ℝ*)
97963adant3 1126 . . . . . 6 ((𝜑𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) = 𝐴) → (𝐹𝑗) ∈ ℝ*)
9895, 97eqeltrrd 2832 . . . . 5 ((𝜑𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) = 𝐴) → 𝐴 ∈ ℝ*)
9998ad4ant134 1179 . . . 4 ((((𝜑 ∧ ¬ 𝐴 ∈ ℝ) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) = 𝐴) → 𝐴 ∈ ℝ*)
100 rspa 3060 . . . . 5 ((∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) = 𝐴𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) = 𝐴)
101100adantll 752 . . . 4 (((((𝜑 ∧ ¬ 𝐴 ∈ ℝ) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) = 𝐴) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) = 𝐴)
10287, 76, 5, 88, 89, 99, 101xlimconst2 40556 . . 3 ((((𝜑 ∧ ¬ 𝐴 ∈ ℝ) ∧ 𝑗𝑍) ∧ ∀𝑘 ∈ (ℤ𝑗)(𝐹𝑘) = 𝐴) → 𝐹~~>*𝐴)
10384, 102rexlimddv2 40544 . 2 ((𝜑 ∧ ¬ 𝐴 ∈ ℝ) → 𝐹~~>*𝐴)
10410, 103pm2.61dan 867 1 (𝜑𝐹~~>*𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  w3a 1072   = wceq 1624  wcel 2131  wne 2924  wral 3042  wrex 3043  {cpr 4315   class class class wbr 4796  wf 6037  cfv 6041  (class class class)co 6805  Fincfn 8113  cc 10118  cr 10119  +∞cpnf 10255  -∞cmnf 10256  *cxr 10257   < clt 10258  cle 10259  cmin 10450  cz 11561  cuz 11871  +crp 12017  abscabs 14165  cli 14406  ~~>*clsxlim 40539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-cnex 10176  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-mulcom 10184  ax-addass 10185  ax-mulass 10186  ax-distr 10187  ax-i2m1 10188  ax-1ne0 10189  ax-1rid 10190  ax-rnegex 10191  ax-rrecex 10192  ax-cnre 10193  ax-pre-lttri 10194  ax-pre-lttrn 10195  ax-pre-ltadd 10196  ax-pre-mulgt0 10197  ax-pre-sup 10198
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-int 4620  df-iun 4666  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-om 7223  df-1st 7325  df-2nd 7326  df-wrecs 7568  df-recs 7629  df-rdg 7667  df-1o 7721  df-oadd 7725  df-er 7903  df-map 8017  df-pm 8018  df-en 8114  df-dom 8115  df-sdom 8116  df-fin 8117  df-fi 8474  df-sup 8505  df-inf 8506  df-pnf 10260  df-mnf 10261  df-xr 10262  df-ltxr 10263  df-le 10264  df-sub 10452  df-neg 10453  df-div 10869  df-nn 11205  df-2 11263  df-3 11264  df-4 11265  df-5 11266  df-6 11267  df-7 11268  df-8 11269  df-9 11270  df-n0 11477  df-z 11562  df-dec 11678  df-uz 11872  df-q 11974  df-rp 12018  df-xneg 12131  df-xadd 12132  df-xmul 12133  df-ioo 12364  df-ioc 12365  df-ico 12366  df-icc 12367  df-fz 12512  df-fl 12779  df-seq 12988  df-exp 13047  df-cj 14030  df-re 14031  df-im 14032  df-sqrt 14166  df-abs 14167  df-clim 14410  df-rlim 14411  df-struct 16053  df-ndx 16054  df-slot 16055  df-base 16057  df-plusg 16148  df-mulr 16149  df-starv 16150  df-tset 16154  df-ple 16155  df-ds 16158  df-unif 16159  df-rest 16277  df-topn 16278  df-topgen 16298  df-ordt 16355  df-ps 17393  df-tsr 17394  df-psmet 19932  df-xmet 19933  df-met 19934  df-bl 19935  df-mopn 19936  df-cnfld 19941  df-top 20893  df-topon 20910  df-topsp 20931  df-bases 20944  df-lm 21227  df-xms 22318  df-ms 22319  df-xlim 40540
This theorem is referenced by:  climxlim2  40567
  Copyright terms: Public domain W3C validator