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 ⊢ Ⅎ _ k F
climbddf.2 ⊢ Z = ℤ ≥ M
Assertion climbddf ⊢ M ∈ ℤ ∧ F ∈ dom ⁡ ⇝ ∧ ∀ k ∈ Z F ⁡ k ∈ ℂ → ∃ x ∈ ℝ ∀ k ∈ Z F ⁡ k ≤ x

Proof

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