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