Metamath Proof Explorer

Theorem climleltrp

Description: The limit of complex number sequence F is eventually approximated. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses climleltrp.k ⊢ Ⅎ 𝑘 𝜑
climleltrp.f ⊢ Ⅎ 𝑘 𝐹
climleltrp.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climleltrp.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
climleltrp.r ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
climleltrp.a ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
climleltrp.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
climleltrp.l ⊢ ( 𝜑 → 𝐴 ≤ 𝐶 )
climleltrp.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
Assertion climleltrp ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) < ( 𝐶 + 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 climleltrp.k ⊢ Ⅎ 𝑘 𝜑
2 climleltrp.f ⊢ Ⅎ 𝑘 𝐹
3 climleltrp.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 climleltrp.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
5 climleltrp.r ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
6 climleltrp.a ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
7 climleltrp.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
8 climleltrp.l ⊢ ( 𝜑 → 𝐴 ≤ 𝐶 )
9 climleltrp.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
10 4 3 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
11 uzss ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
12 10 11 syl ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
13 12 3 sseqtrrdi ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) ⊆ 𝑍 )
14 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
15 14 10 sseldi ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
16 eqid ⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 )
17 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
18 1 2 15 16 6 17 9 clim2d ⊢ ( 𝜑 → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) )
19 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ ( ℤ≥ ‘ 𝑁 )
20 1 19 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) )
21 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → 𝜑 )
22 uzss ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ℤ≥ ‘ 𝑗 ) ⊆ ( ℤ≥ ‘ 𝑁 ) )
23 22 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ℤ≥ ‘ 𝑗 ) ⊆ ( ℤ≥ ‘ 𝑁 ) )
24 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) )
25 23 24 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) )
26 25 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) )
27 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 )
28 17 5 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
29 28 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
30 climcl ⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ )
31 6 30 syl ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐴 ∈ ℂ )
33 28 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
34 32 33 pncan3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐴 + ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) = ( 𝐹 ‘ 𝑘 ) )
35 34 eqcomd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐴 + ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
36 35 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐴 + ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
37 36 29 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( 𝐴 + ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ∈ ℝ )
38 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → 𝐶 ∈ ℝ )
39 1 2 16 15 6 5 climreclf ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
40 39 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → 𝐴 ∈ ℝ )
41 29 40 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ∈ ℝ )
42 38 41 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( 𝐶 + ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ∈ ℝ )
43 9 rpred ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
44 43 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → 𝑋 ∈ ℝ )
45 38 44 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( 𝐶 + 𝑋 ) ∈ ℝ )
46 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → 𝐴 ≤ 𝐶 )
47 40 38 41 46 leadd1dd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( 𝐴 + ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ≤ ( 𝐶 + ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
48 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
49 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → 𝐴 ∈ ℂ )
50 48 49 subcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ∈ ℂ )
51 50 abscld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ∈ ℝ )
52 41 leabsd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
53 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 )
54 41 51 44 52 53 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) < 𝑋 )
55 41 44 38 54 ltadd2dd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( 𝐶 + ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝐶 + 𝑋 ) )
56 37 42 45 47 55 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( 𝐴 + ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( 𝐶 + 𝑋 ) )
57 36 56 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( 𝐹 ‘ 𝑘 ) < ( 𝐶 + 𝑋 ) )
58 29 57 jca ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) < ( 𝐶 + 𝑋 ) ) )
59 21 26 27 58 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) < ( 𝐶 + 𝑋 ) ) )
60 59 adantrl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) < ( 𝐶 + 𝑋 ) ) )
61 60 ex ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) < ( 𝐶 + 𝑋 ) ) ) )
62 20 61 ralimdaa ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) < ( 𝐶 + 𝑋 ) ) ) )
63 62 reximdva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑋 ) → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) < ( 𝐶 + 𝑋 ) ) ) )
64 18 63 mpd ⊢ ( 𝜑 → ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) < ( 𝐶 + 𝑋 ) ) )
65 ssrexv ⊢ ( ( ℤ≥ ‘ 𝑁 ) ⊆ 𝑍 → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) < ( 𝐶 + 𝑋 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) < ( 𝐶 + 𝑋 ) ) ) )
66 13 64 65 sylc ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) < ( 𝐶 + 𝑋 ) ) )