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 ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 )