Metamath Proof Explorer


Theorem clim0

Description: Express the predicate F converges to 0 . (Contributed by NM, 24-Feb-2008) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses clim0.1 𝑍 = ( ℤ𝑀 )
clim0.2 ( 𝜑𝑀 ∈ ℤ )
clim0.3 ( 𝜑𝐹𝑉 )
clim0.4 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) = 𝐵 )
Assertion clim0 ( 𝜑 → ( 𝐹 ⇝ 0 ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ 𝐵 ) < 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 clim0.1 𝑍 = ( ℤ𝑀 )
2 clim0.2 ( 𝜑𝑀 ∈ ℤ )
3 clim0.3 ( 𝜑𝐹𝑉 )
4 clim0.4 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) = 𝐵 )
5 1 2 3 4 clim2 ( 𝜑 → ( 𝐹 ⇝ 0 ↔ ( 0 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ) ) )
6 0cn 0 ∈ ℂ
7 6 biantrur ( ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ( 0 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ) )
8 subid1 ( 𝐵 ∈ ℂ → ( 𝐵 − 0 ) = 𝐵 )
9 8 fveq2d ( 𝐵 ∈ ℂ → ( abs ‘ ( 𝐵 − 0 ) ) = ( abs ‘ 𝐵 ) )
10 9 breq1d ( 𝐵 ∈ ℂ → ( ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ↔ ( abs ‘ 𝐵 ) < 𝑥 ) )
11 10 pm5.32i ( ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ( 𝐵 ∈ ℂ ∧ ( abs ‘ 𝐵 ) < 𝑥 ) )
12 11 ralbii ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ 𝐵 ) < 𝑥 ) )
13 12 rexbii ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ 𝐵 ) < 𝑥 ) )
14 13 ralbii ( ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ 𝐵 ) < 𝑥 ) )
15 7 14 bitr3i ( ( 0 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) ) ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ 𝐵 ) < 𝑥 ) )
16 5 15 bitrdi ( 𝜑 → ( 𝐹 ⇝ 0 ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( 𝐵 ∈ ℂ ∧ ( abs ‘ 𝐵 ) < 𝑥 ) ) )