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

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 ) )