Metamath Proof Explorer


Theorem climuzlem

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A . (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses climuzlem.1 ( 𝜑𝑀 ∈ ℤ )
climuzlem.2 𝑍 = ( ℤ𝑀 )
climuzlem.3 ( 𝜑𝐹 : 𝑍 ⟶ ℂ )
Assertion climuzlem ( 𝜑 → ( 𝐹𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 climuzlem.1 ( 𝜑𝑀 ∈ ℤ )
2 climuzlem.2 𝑍 = ( ℤ𝑀 )
3 climuzlem.3 ( 𝜑𝐹 : 𝑍 ⟶ ℂ )
4 climcl ( 𝐹𝐴𝐴 ∈ ℂ )
5 4 adantl ( ( 𝜑𝐹𝐴 ) → 𝐴 ∈ ℂ )
6 id ( 𝐹𝐴𝐹𝐴 )
7 climrel Rel ⇝
8 7 brrelex1i ( 𝐹𝐴𝐹 ∈ V )
9 eqidd ( ( 𝐹𝐴𝑘 ∈ ℤ ) → ( 𝐹𝑘 ) = ( 𝐹𝑘 ) )
10 8 9 clim ( 𝐹𝐴 → ( 𝐹𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) )
11 6 10 mpbid ( 𝐹𝐴 → ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
12 11 simprd ( 𝐹𝐴 → ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) )
13 12 adantl ( ( 𝜑𝐹𝐴 ) → ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) )
14 simpr ( ( 𝜑 ∧ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) )
15 2 rexuz3 ( 𝑀 ∈ ℤ → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
16 1 15 syl ( 𝜑 → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
17 16 adantr ( ( 𝜑 ∧ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
18 14 17 mpbird ( ( 𝜑 ∧ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) )
19 simpr ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) → ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 )
20 19 ralimi ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) → ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 )
21 20 reximi ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 )
22 21 a1i ( ( 𝜑 ∧ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) )
23 18 22 mpd ( ( 𝜑 ∧ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 )
24 23 ex ( 𝜑 → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) )
25 24 adantr ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) )
26 25 ralimdva ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) )
27 26 adantr ( ( 𝜑𝐹𝐴 ) → ( ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) )
28 13 27 mpd ( ( 𝜑𝐹𝐴 ) → ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 )
29 5 28 jca ( ( 𝜑𝐹𝐴 ) → ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) )
30 simprl ( ( 𝜑 ∧ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) → 𝐴 ∈ ℂ )
31 nfv 𝑗 𝜑
32 nfre1 𝑗𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 )
33 2 uzssz2 𝑍 ⊆ ℤ
34 33 sseli ( 𝑗𝑍𝑗 ∈ ℤ )
35 34 3ad2ant2 ( ( 𝜑𝑗𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) → 𝑗 ∈ ℤ )
36 simpll ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → 𝜑 )
37 2 uztrn2 ( ( 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ) → 𝑘𝑍 )
38 37 adantll ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → 𝑘𝑍 )
39 3 ffvelrnda ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
40 36 38 39 syl2anc ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( 𝐹𝑘 ) ∈ ℂ )
41 40 adantr ( ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) → ( 𝐹𝑘 ) ∈ ℂ )
42 simpr ( ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) → ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 )
43 41 42 jca ( ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) → ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) )
44 43 ex ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 → ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
45 44 ralimdva ( ( 𝜑𝑗𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 → ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
46 45 3impia ( ( 𝜑𝑗𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) → ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) )
47 rspe ( ( 𝑗 ∈ ℤ ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) )
48 35 46 47 syl2anc ( ( 𝜑𝑗𝑍 ∧ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) )
49 48 3exp ( 𝜑 → ( 𝑗𝑍 → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) )
50 31 32 49 rexlimd ( 𝜑 → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
51 50 ralimdv ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 → ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
52 51 imp ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) )
53 52 adantrl ( ( 𝜑 ∧ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) → ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) )
54 30 53 jca ( ( 𝜑 ∧ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) → ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
55 2 fvexi 𝑍 ∈ V
56 55 a1i ( 𝜑𝑍 ∈ V )
57 3 56 fexd ( 𝜑𝐹 ∈ V )
58 eqidd ( ( 𝜑𝑘 ∈ ℤ ) → ( 𝐹𝑘 ) = ( 𝐹𝑘 ) )
59 57 58 clim ( 𝜑 → ( 𝐹𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) )
60 59 adantr ( ( 𝜑 ∧ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) → ( 𝐹𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) )
61 54 60 mpbird ( ( 𝜑 ∧ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) → 𝐹𝐴 )
62 29 61 impbida ( 𝜑 → ( 𝐹𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝐹𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )