This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climuz

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 climuz.k ⊢ Ⅎ 𝑘 𝐹
climuz.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climuz.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climuz.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
Assertion climuz ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 climuz.k ⊢ Ⅎ 𝑘 𝐹
2 climuz.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 climuz.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 climuz.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℂ )
5 2 3 4 climuzlem ⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑦 ) ) )
6 breq2 ⊢ ( 𝑦 = 𝑥 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ) )
7 6 ralbidv ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑦 ↔ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ) )
8 7 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑦 ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ) )
9 fveq2 ⊢ ( 𝑖 = 𝑗 → ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑗 ) )
10 9 raleqdv ⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ↔ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ) )
11 nfcv ⊢ Ⅎ 𝑘 abs
12 nfcv ⊢ Ⅎ 𝑘 𝑙
13 1 12 nffv ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑙 )
14 nfcv ⊢ Ⅎ 𝑘 −
15 nfcv ⊢ Ⅎ 𝑘 𝐴
16 13 14 15 nfov ⊢ Ⅎ 𝑘 ( ( 𝐹 ‘ 𝑙 ) − 𝐴 )
17 11 16 nffv ⊢ Ⅎ 𝑘 ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) )
18 nfcv ⊢ Ⅎ 𝑘 <
19 nfcv ⊢ Ⅎ 𝑘 𝑥
20 17 18 19 nfbr ⊢ Ⅎ 𝑘 ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥
21 nfv ⊢ Ⅎ 𝑙 ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥
22 fveq2 ⊢ ( 𝑙 = 𝑘 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑘 ) )
23 22 fvoveq1d ⊢ ( 𝑙 = 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
24 23 breq1d ⊢ ( 𝑙 = 𝑘 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
25 20 21 24 cbvralw ⊢ ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 )
26 25 a1i ⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
27 10 26 bitrd ⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
28 27 cbvrexvw ⊢ ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 )
29 28 a1i ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
30 8 29 bitrd ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑦 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
31 30 cbvralvw ⊢ ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑦 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 )
32 31 anbi2i ⊢ ( ( 𝐴 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑦 ) ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
33 32 a1i ⊢ ( 𝜑 → ( ( 𝐴 ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − 𝐴 ) ) < 𝑦 ) ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
34 5 33 bitrd ⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )