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

Metamath Proof Explorer

Theorem climbddf

Description: A converging sequence of complex numbers is bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses climbddf.1 ⊢ Ⅎ 𝑘 𝐹
climbddf.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion climbddf ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 )

Proof

Step Hyp Ref Expression
1 climbddf.1 ⊢ Ⅎ 𝑘 𝐹
2 climbddf.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 simp1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → 𝑀 ∈ ℤ )
4 simp2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → 𝐹 ∈ dom ⇝ )
5 nfv ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑘 ) ∈ ℂ
6 nfcv ⊢ Ⅎ 𝑘 𝑗
7 1 6 nffv ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 )
8 nfcv ⊢ Ⅎ 𝑘 ℂ
9 7 8 nfel ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 ) ∈ ℂ
10 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
11 10 eleq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) )
12 5 9 11 cbvralw ⊢ ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
13 12 biimpi ⊢ ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ → ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
14 13 3ad2ant3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
15 2 climbdd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ∈ ℂ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑥 )
16 3 4 14 15 syl3anc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑥 )
17 nfcv ⊢ Ⅎ 𝑘 abs
18 17 7 nffv ⊢ Ⅎ 𝑘 ( abs ‘ ( 𝐹 ‘ 𝑗 ) )
19 nfcv ⊢ Ⅎ 𝑘 ≤
20 nfcv ⊢ Ⅎ 𝑘 𝑥
21 18 19 20 nfbr ⊢ Ⅎ 𝑘 ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑥
22 nfv ⊢ Ⅎ 𝑗 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥
23 2fveq3 ⊢ ( 𝑗 = 𝑘 → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
24 23 breq1d ⊢ ( 𝑗 = 𝑘 → ( ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑥 ↔ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) )
25 21 22 24 cbvralw ⊢ ( ∀ 𝑗 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑥 ↔ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 )
26 25 rexbii ⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 )
27 16 26 sylib ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 )