Metamath Proof Explorer


Theorem climabs0

Description: Convergence to zero of the absolute value is equivalent to convergence to zero. (Contributed by NM, 8-Jul-2008) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses climabs0.1 𝑍 = ( ℤ𝑀 )
climabs0.2 ( 𝜑𝑀 ∈ ℤ )
climabs0.3 ( 𝜑𝐹𝑉 )
climabs0.4 ( 𝜑𝐺𝑊 )
climabs0.5 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
climabs0.6 ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) = ( abs ‘ ( 𝐹𝑘 ) ) )
Assertion climabs0 ( 𝜑 → ( 𝐹 ⇝ 0 ↔ 𝐺 ⇝ 0 ) )

Proof

Step Hyp Ref Expression
1 climabs0.1 𝑍 = ( ℤ𝑀 )
2 climabs0.2 ( 𝜑𝑀 ∈ ℤ )
3 climabs0.3 ( 𝜑𝐹𝑉 )
4 climabs0.4 ( 𝜑𝐺𝑊 )
5 climabs0.5 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
6 climabs0.6 ( ( 𝜑𝑘𝑍 ) → ( 𝐺𝑘 ) = ( abs ‘ ( 𝐹𝑘 ) ) )
7 1 uztrn2 ( ( 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ) → 𝑘𝑍 )
8 absidm ( ( 𝐹𝑘 ) ∈ ℂ → ( abs ‘ ( abs ‘ ( 𝐹𝑘 ) ) ) = ( abs ‘ ( 𝐹𝑘 ) ) )
9 5 8 syl ( ( 𝜑𝑘𝑍 ) → ( abs ‘ ( abs ‘ ( 𝐹𝑘 ) ) ) = ( abs ‘ ( 𝐹𝑘 ) ) )
10 9 breq1d ( ( 𝜑𝑘𝑍 ) → ( ( abs ‘ ( abs ‘ ( 𝐹𝑘 ) ) ) < 𝑥 ↔ ( abs ‘ ( 𝐹𝑘 ) ) < 𝑥 ) )
11 7 10 sylan2 ( ( 𝜑 ∧ ( 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ) ) → ( ( abs ‘ ( abs ‘ ( 𝐹𝑘 ) ) ) < 𝑥 ↔ ( abs ‘ ( 𝐹𝑘 ) ) < 𝑥 ) )
12 11 anassrs ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) → ( ( abs ‘ ( abs ‘ ( 𝐹𝑘 ) ) ) < 𝑥 ↔ ( abs ‘ ( 𝐹𝑘 ) ) < 𝑥 ) )
13 12 ralbidva ( ( 𝜑𝑗𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( abs ‘ ( 𝐹𝑘 ) ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( 𝐹𝑘 ) ) < 𝑥 ) )
14 13 rexbidva ( 𝜑 → ( ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( abs ‘ ( 𝐹𝑘 ) ) ) < 𝑥 ↔ ∃ 𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( 𝐹𝑘 ) ) < 𝑥 ) )
15 14 ralbidv ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( abs ‘ ( 𝐹𝑘 ) ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( 𝐹𝑘 ) ) < 𝑥 ) )
16 5 abscld ( ( 𝜑𝑘𝑍 ) → ( abs ‘ ( 𝐹𝑘 ) ) ∈ ℝ )
17 16 recnd ( ( 𝜑𝑘𝑍 ) → ( abs ‘ ( 𝐹𝑘 ) ) ∈ ℂ )
18 1 2 4 6 17 clim0c ( 𝜑 → ( 𝐺 ⇝ 0 ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( abs ‘ ( 𝐹𝑘 ) ) ) < 𝑥 ) )
19 eqidd ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) = ( 𝐹𝑘 ) )
20 1 2 3 19 5 clim0c ( 𝜑 → ( 𝐹 ⇝ 0 ↔ ∀ 𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ( abs ‘ ( 𝐹𝑘 ) ) < 𝑥 ) )
21 15 18 20 3bitr4rd ( 𝜑 → ( 𝐹 ⇝ 0 ↔ 𝐺 ⇝ 0 ) )