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

Metamath Proof Explorer

Theorem clim0c

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 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
clim0c.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
Assertion clim0c ( 𝜑 → ( 𝐹 ⇝ 0 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ 𝐵 ) < 𝑥 ) )

Proof

Step Hyp Ref Expression
1 clim0.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 clim0.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 clim0.3 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
4 clim0.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
5 clim0c.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
6 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
7 1 2 3 4 6 5 clim2c ⊢ ( 𝜑 → ( 𝐹 ⇝ 0 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ) )
8 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
9 5 subid1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐵 − 0 ) = 𝐵 )
10 9 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( 𝐵 − 0 ) ) = ( abs ‘ 𝐵 ) )
11 10 breq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ↔ ( abs ‘ 𝐵 ) < 𝑥 ) )
12 8 11 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ↔ ( abs ‘ 𝐵 ) < 𝑥 ) )
13 12 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ↔ ( abs ‘ 𝐵 ) < 𝑥 ) )
14 13 ralbidva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ 𝐵 ) < 𝑥 ) )
15 14 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ 𝐵 ) < 𝑥 ) )
16 15 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐵 − 0 ) ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ 𝐵 ) < 𝑥 ) )
17 7 16 bitrd ⊢ ( 𝜑 → ( 𝐹 ⇝ 0 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ 𝐵 ) < 𝑥 ) )