Metamath Proof Explorer

Theorem climbdd

Description: A converging sequence of complex numbers is bounded. (Contributed by Mario Carneiro, 9-Jul-2017)

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

Proof

Step Hyp Ref Expression
1 climcau.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 simp3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
3 1 climcau ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑦 )
4 3 3adant3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑦 )
5 1 caubnd ⊢ ( ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ∀ 𝑦 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 )
6 2 4 5 syl2anc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 )
7 r19.26 ⊢ ( ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) ↔ ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
8 simpr ⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
9 8 abscld ⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
10 simpllr ⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → 𝑥 ∈ ℝ )
11 ltle ⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) )
12 9 10 11 syl2anc ⊢ ( ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) )
13 12 expimpd ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) )
14 13 ralimdva ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑘 ∈ 𝑍 ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) → ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) )
15 7 14 syl5bir ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) ∧ 𝑥 ∈ ℝ ) → ( ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) → ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) )
16 15 exp4b ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ( 𝑥 ∈ ℝ → ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ → ( ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 → ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) ) ) )
17 16 com23 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ) → ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ → ( 𝑥 ∈ ℝ → ( ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 → ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) ) ) )
18 17 3impia ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( 𝑥 ∈ ℝ → ( ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 → ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) ) )
19 18 reximdvai ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 ) )
20 6 19 mpd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ dom ⇝ ∧ ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 𝑥 )