Metamath Proof Explorer


Theorem clim2d

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

Ref Expression
Hypotheses clim2d.k 𝑘 𝜑
clim2d.f 𝑘 𝐹
clim2d.m ( 𝜑𝑀 ∈ ℤ )
clim2d.z 𝑍 = ( ℤ𝑀 )
clim2d.c ( 𝜑𝐹𝐴 )
clim2d.b ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) = 𝐵 )
clim2d.x ( 𝜑𝑋 ∈ ℝ+ )
Assertion clim2d ( 𝜑 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵𝐴 ) ) < 𝑋 ) )

Proof

Step Hyp Ref Expression
1 clim2d.k 𝑘 𝜑
2 clim2d.f 𝑘 𝐹
3 clim2d.m ( 𝜑𝑀 ∈ ℤ )
4 clim2d.z 𝑍 = ( ℤ𝑀 )
5 clim2d.c ( 𝜑𝐹𝐴 )
6 clim2d.b ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) = 𝐵 )
7 clim2d.x ( 𝜑𝑋 ∈ ℝ+ )
8 climrel Rel ⇝
9 8 a1i ( 𝜑 → Rel ⇝ )
10 brrelex1 ( ( Rel ⇝ ∧ 𝐹𝐴 ) → 𝐹 ∈ V )
11 9 5 10 syl2anc ( 𝜑𝐹 ∈ V )
12 1 2 4 3 11 6 clim2f2 ( 𝜑 → ( 𝐹𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) ) ) )
13 5 12 mpbid ( 𝜑 → ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) ) )
14 13 simprd ( 𝜑 → ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) )
15 breq2 ( 𝑥 = 𝑋 → ( ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ↔ ( abs ‘ ( 𝐵𝐴 ) ) < 𝑋 ) )
16 15 anbi2d ( 𝑥 = 𝑋 → ( ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) ↔ ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵𝐴 ) ) < 𝑋 ) ) )
17 16 ralbidv ( 𝑥 = 𝑋 → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵𝐴 ) ) < 𝑋 ) ) )
18 17 rexbidv ( 𝑥 = 𝑋 → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) ↔ ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵𝐴 ) ) < 𝑋 ) ) )
19 18 rspcva ( ( 𝑋 ∈ ℝ+ ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵𝐴 ) ) < 𝑥 ) ) → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵𝐴 ) ) < 𝑋 ) )
20 7 14 19 syl2anc ( 𝜑 → ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵𝐴 ) ) < 𝑋 ) )