Home(or GIF version for IE).
| Home |
Metamath Proof Explorer | < Previous Next > |
| Bad symbols?
Use Firefox (or GIF version for IE). |
| Color key: | Metamath Proof Explorer
(1-8782) |
Hilbert Space Explorer
(8783-10363) |
User Sandboxes
(10364-10752) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | climreu 7101 | An infinite sequence of complex numbers converges to at most one limit. |
| ⊢ A ∈ V ⇒ ⊢ (F ⇝ A → ∃!x ∈ ℂ F ⇝ x) | ||
| Theorem | 2climnn 7102 | If two sequences converge to each other, they converge to the same limit. |
| ⊢ G ∈ V ⇒ ⊢ (((A ∈ ℂ ⋀ ∀k ∈ ℕ ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) ⋀ (∀x ∈ ℝ (0 < x → ∃j ∈ ℕ ∀k ∈ ℕ (j ≤ k → (abs ‘((G ‘k) − (F ‘k))) < x)) ⋀ F ⇝ A)) → G ⇝ A) | ||
| Theorem | 2climnn0 7103 | If two sequences converge to each other, they converge to the same limit. |
| ⊢ G ∈ V ⇒ ⊢ (((A ∈ ℂ ⋀ ∀k ∈ ℕ0 ((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ)) ⋀ (∀x ∈ ℝ (0 < x → ∃j ∈ ℕ0 ∀k ∈ ℕ0 (j ≤ k → (abs ‘((G ‘k) − (F ‘k))) < x)) ⋀ F ⇝ A)) → G ⇝ A) | ||
| Theorem | climshft 7104 | A shifted function converges iff the original function converges. |
| ⊢ F ∈ V & ⊢ M ∈ ℤ ⇒ ⊢ (A ∈ ℂ → ((FshiftM) ⇝ A ↔ F ⇝ A)) | ||
| Theorem | climres 7105 | A function restricted to upper integers converges iff the original function converges. |
| ⊢ F ∈ V & ⊢ M ∈ ℤ ⇒ ⊢ (A ∈ B → ((F ↾ (ℤ≥ ‘M)) ⇝ A ↔ F ⇝ A)) | ||
| Theorem | climshft2 7106 | A shifted function converges iff the original function converges. (Contributed by Paul Chapman, 19-Nov-2007.) |
| ⊢ F ∈ V & ⊢ G ∈ V & ⊢ M ∈ ℤ & ⊢ K ∈ ℤ ⇒ ⊢ ((A ∈ B ⋀ ∀k ∈ (ℤ≥ ‘M)(G ‘(k + K)) = (F ‘k)) → (F ⇝ A ↔ G ⇝ A)) | ||
| Theorem | iserzshft2 7107 | Index shift of an infinite series. (Contributed by Paul Chapman, 19-Nov-2007.) |
| ⊢ F ∈ V & ⊢ G ∈ V & ⊢ M ∈ ℤ & ⊢ K ∈ ℤ ⇒ ⊢ ((A ∈ B ⋀ ∀k ∈ (ℤ≥ ‘M)((F ‘k) ∈ ℂ ⋀ (G ‘(k + K)) = (F ‘k))) → ((⟨M, + ⟩seqF) ⇝ A ↔ (⟨(M + K), + ⟩seqG) ⇝ A)) | ||
| Theorem | climuz0 7108 | A zero sequence converges to zero. |
| ⊢ M ∈ ℤ ⇒ ⊢ ((ℤ≥ ‘M) × {0}) ⇝ 0 | ||
| Theorem | serzclim0 7109 | The zero series converges to zero. (Contributed by Paul Chapman, 9-Feb-2007.) |
| ⊢ (M ∈ ℤ → (⟨M, + ⟩seq((ℤ≥ ‘M) × {0})) ⇝ 0) | ||
| Theorem | climrecl 7110 | The limit of a convergent real sequence is real. Corollary 12-2.5 of [Gleason] p. 172. |
| ⊢ A ∈ V ⇒ ⊢ ((M ∈ ℤ ⋀ F ⇝ A ⋀ ∀k ∈ (ℤ≥ ‘M)(F ‘k) ∈ ℝ) → A ∈ ℝ) | ||
| Theorem | climfnrcl 7111 | The limit of a convergent real sequence on natural numbers is real. Corollary 12-2.5 of [Gleason] p. 172. |
| ⊢ A ∈ V & ⊢ F:ℕ–→ℝ & ⊢ F ⇝ A ⇒ ⊢ A ∈ ℝ | ||
| Theorem | climge0 7112 | A nonnegative sequence converges to a nonnegative number. |
| ⊢ A ∈ V ⇒ ⊢ ((M ∈ ℤ ⋀ F ⇝ A ⋀ ∀k ∈ (ℤ≥ ‘M)((F ‘k) ∈ ℝ ⋀ 0 ≤ (F ‘k))) → 0 ≤ A) | ||
| Theorem | climabs0 7113 | Convergence to zero of the absolute value is equivalent to convergence to zero. |
| ⊢ F ∈ V & ⊢ G ∈ V & ⊢ (k ∈ ℕ → (G ‘k) = (abs ‘(F ‘k))) ⇒ ⊢ (∀k ∈ ℕ (F ‘k) ∈ ℂ → (F ⇝ 0 ↔ G ⇝ 0)) | ||
| Theorem | climaddlem1 7114 | Lemma for climadd 7117. |
| Theorem | climaddlem2 7115 | Lemma for climadd 7117. |
| Theorem | climaddlem3 7116 | Lemma for climadd 7117. Warning: The HTML proof page is 3/4 megabyte in size. |
| Theorem | climadd 7117 | Limit of the sum of two converging sequences. Proposition 12-2.1(a) of [Gleason] p. 168. |
| ⊢ F ∈ V & ⊢ G ∈ V & ⊢ H ∈ V & ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (((F ⇝ A ⋀ G ⇝ B) ⋀ (M ∈ ℤ ⋀ ∀k ∈ (ℤ≥ ‘M)((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ ⋀ (H ‘k) = ((F ‘k) + (G ‘k))))) → H ⇝ (A + B)) | ||
| Theorem | climaddc1 7118 | Limit of a constant C added to each term of a sequence. |
| ⊢ F ∈ V & ⊢ G ∈ V & ⊢ A ∈ V & ⊢ C ∈ V ⇒ ⊢ (((F ⇝ A ⋀ C ∈ ℂ) ⋀ (M ∈ ℤ ⋀ ∀k ∈ (ℤ≥ ‘M)((F ‘k) ∈ ℂ ⋀ (G ‘k) = ((F ‘k) + C)))) → G ⇝ (A + C)) | ||
| Theorem | climaddc2 7119 | Limit of a constant C added to each term of a sequence. |
| ⊢ F ∈ V & ⊢ G ∈ V & ⊢ A ∈ V & ⊢ C ∈ V ⇒ ⊢ (((F ⇝ A ⋀ C ∈ ℂ) ⋀ (M ∈ ℤ ⋀ ∀k ∈ (ℤ≥ ‘M)((F ‘k) ∈ ℂ ⋀ (G ‘k) = (C + (F ‘k))))) → G ⇝ (C + A)) | ||
| Theorem | climmullem1 7120 | Lemma for climmul 7128. |
| Theorem | climmullem2 7121 | Lemma for climmul 7128. |
| Theorem | climmullem3 7122 | Lemma for climmul 7128. |
| Theorem | climmullem4 7123 | Lemma for climmul 7128. |
| Theorem | climmullem5 7124 | Lemma for climmul 7128. Instead of the infimum that Gleason uses (bottom of p. 170), we use recrecltt 5904 to give us a number smaller than both a given number and 1. Warning: The HTML proof page is 1/2 megabyte in size. |
| Theorem | climmullem6 7125 | Lemma for climmul 7128. |
| Theorem | climmullem7 7126 | Lemma for climmul 7128. |
| Theorem | climmullem8 7127 | Lemma for climmul 7128. Warning: The HTML proof page is 3/4 megabyte in size. |
| Theorem | climmul 7128 | Limit of the product of two converging sequences. Proposition 12-2.1(c) of [Gleason] p. 168. |
| ⊢ F ∈ V & ⊢ G ∈ V & ⊢ H ∈ V & ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (((F ⇝ A ⋀ G ⇝ B) ⋀ (M ∈ ℤ ⋀ ∀k ∈ (ℤ≥ ‘M)((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ ⋀ (H ‘k) = ((F ‘k) · (G ‘k))))) → H ⇝ (A · B)) | ||
| Theorem | climmulc2 7129 | Limit of a sequence multiplied by a constant C. Corollary 12-2.2 of [Gleason] p. 171. |
| ⊢ F ∈ V & ⊢ G ∈ V & ⊢ A ∈ V ⇒ ⊢ (((C ∈ ℂ ⋀ F ⇝ A) ⋀ (M ∈ ℤ ⋀ ∀k ∈ (ℤ≥ ‘M)((F ‘k) ∈ ℂ ⋀ (G ‘k) = (C · (F ‘k))))) → G ⇝ (C · A)) | ||
| Theorem | climsub 7130 | Limit of the difference of two converging sequences. Proposition 12-2.1(b) of [Gleason] p. 168. |
| ⊢ F ∈ V & ⊢ G ∈ V & ⊢ H ∈ V & ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (((F ⇝ A ⋀ G ⇝ B) ⋀ (M ∈ ℤ ⋀ ∀k ∈ (ℤ≥ ‘M)((F ‘k) ∈ ℂ ⋀ (G ‘k) ∈ ℂ ⋀ (H ‘k) = ((F ‘k) − (G ‘k))))) → H ⇝ (A − B)) | ||
| Theorem | climsubc2 7131 | Limit of a constant C minus each term of a sequence. |
| ⊢ F ∈ V & ⊢ G ∈ V & ⊢ A ∈ V & ⊢ C ∈ V ⇒ ⊢ (((F ⇝ A ⋀ C ∈ ℂ) ⋀ (M ∈ ℤ ⋀ ∀k ∈ (ℤ≥ ‘M)((F ‘k) ∈ ℂ ⋀ (G ‘k) = (C − (F ‘k))))) → G ⇝ (C − A)) | ||
| Theorem | climaddc 7132 | Limit of a constant A added to a sequence. |
| ⊢ A ∈ ℂ & ⊢ B ∈ V & ⊢ F ⇝ B & ⊢ G Fn ℕ & ⊢ (k ∈ ℕ → ((F ‘k) ∈ ℂ ⋀ (G ‘k) = (A + (F ‘k)))) ⇒ ⊢ G ⇝ (A + B) | ||
| Theorem | climmulc 7133 | Limit of a sequence multiplied by a constant A. Corollary 12-2.2 of [Gleason] p. 171. |
| ⊢ A ∈ ℂ & ⊢ B ∈ V & ⊢ F ⇝ B & ⊢ G Fn ℕ & ⊢ (k ∈ ℕ → ((F ‘k) ∈ ℂ ⋀ (G ‘k) = (A · (F ‘k)))) ⇒ ⊢ G ⇝ (A · B) | ||
| Theorem | clim2serzt 7134 | The limit of an infinite series with an initial segment removed. (Contributed by Paul Chapman, 9-Feb-2007.) |
| ⊢ A ∈ V & ⊢ F ∈ V ⇒ ⊢ (((⟨M, + ⟩seqF) ⇝ A ⋀ N ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (ℤ≥ ‘M)(F ‘k) ∈ ℂ) → (⟨(N + 1), + ⟩seqF) ⇝ (A − ((⟨M, + ⟩seqF) ‘N))) | ||
| Theorem | iserzext 7135 | If an infinite series converges, so does the series with initial terms removed. (Contributed by Paul Chapman, 9-Feb-2007.) |
| ⊢ F ∈ V ⇒ ⊢ ((N ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (ℤ≥ ‘M)(F ‘k) ∈ ℂ ⋀ ∃x(⟨M, + ⟩seqF) ⇝ x) → ∃x(⟨(N + 1), + ⟩seqF) ⇝ x) | ||
| Theorem | iserzmulc1 7136 | Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) |
| ⊢ A ∈ V & ⊢ F ∈ V & ⊢ G ∈ V ⇒ ⊢ ((M ∈ ℤ ⋀ C ∈ ℂ ⋀ ∀k ∈ (ℤ≥ ‘M)((F ‘k) ∈ ℂ ⋀ (G ‘k) = (C · (F ‘k)))) → ((⟨M, + ⟩seqF) ⇝ A → (⟨M, + ⟩seqG) ⇝ (C · A))) | ||
| Theorem | climcmplem 7137 | Lemma for climcmp 7138. |
| Theorem | climcmp 7138 | Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) |
| ⊢ F ∈ V & ⊢ G ∈ V & ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (((F ⇝ A ⋀ G ⇝ B) ⋀ (M ∈ ℤ ⋀ ∀k ∈ (ℤ≥ ‘M)((F ‘k) ∈ ℝ ⋀ (G ‘k) ∈ ℝ ⋀ (F ‘k) ≤ (G ‘k)))) → A ≤ B) | ||
| Theorem | climcmpc1 7139 | Comparison of a constant to the limit of a sequence. |
| ⊢ F ∈ V & ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (((A ∈ ℝ ⋀ F ⇝ B) ⋀ (M ∈ ℤ ⋀ ∀k ∈ (ℤ≥ ‘M)((F ‘k) ∈ ℝ ⋀ A ≤ (F ‘k)))) → A ≤ B) | ||
| Theorem | climsqueeze 7140 | Convergence of a sequence sandwiched between another converging sequence and its limit. |
| ⊢ F ∈ V & ⊢ G ∈ V & ⊢ A ∈ V ⇒ ⊢ ((F ⇝ A ⋀ M ∈ ℤ ⋀ ∀k ∈ (ℤ≥ ‘M)(((F ‘k) ∈ ℝ ⋀ (G ‘k) ∈ ℝ) ⋀ ((F ‘k) ≤ (G ‘k) ⋀ (G ‘k) ≤ A))) → G ⇝ A) | ||
| Theorem | climsqueeze2 7141 | Convergence of a sequence sandwiched between another converging sequence and its limit. |
| ⊢ F ∈ V & ⊢ G ∈ V & ⊢ A ∈ V ⇒ ⊢ ((F ⇝ A ⋀ M ∈ ℤ ⋀ ∀k ∈ (ℤ≥ ‘M)(((F ‘k) ∈ ℝ ⋀ (G ‘k) ∈ ℝ) ⋀ (A ≤ (G ‘k) ⋀ (G ‘k) ≤ (F ‘k)))) → G ⇝ A) | ||
| Theorem | iserzcmp 7142 | Comparison of the limits of two infinite series. (Contributed by Paul Chapman, 12-Nov-2007.) |
| ⊢ A ∈ V & ⊢ B ∈ V & ⊢ F ∈ V & ⊢ G ∈ V ⇒ ⊢ ((((⟨M, + ⟩seqF) ⇝ A ⋀ (⟨M, + ⟩seqG) ⇝ B) ⋀ (M ∈ ℤ ⋀ ∀k ∈ (ℤ≥ ‘M)((F ‘k) ∈ ℝ ⋀ (G ‘k) ∈ ℝ ⋀ (F ‘k) ≤ (G ‘k)))) → A ≤ B) | ||
| Theorem | iserzcmp0 7143 | The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Paul Chapman, 9-Feb-2007.) |
| ⊢ A ∈ V & ⊢ F ∈ V ⇒ ⊢ ((M ∈ ℤ ⋀ (⟨M, + ⟩seqF) ⇝ A ⋀ ∀k ∈ (ℤ≥ ‘M)((F ‘k) ∈ ℝ ⋀ 0 ≤ (F ‘k))) → 0 ≤ A) | ||
| Theorem | iserzshft 7144 | Index shift of an infinite series. (Contributed by Paul Chapman, 31-Oct-2007.) |
| ⊢ F ∈ V & ⊢ M ∈ ℤ & ⊢ K ∈ ℤ & ⊢ N = (M + K) & ⊢ G = (FshiftK) ⇒ ⊢ (A ∈ B → ((⟨M, + ⟩seqF) ⇝ A ↔ (⟨N, + ⟩seqG) ⇝ A)) | ||
| Theorem | clim2serz 7145 | Limit of an infinite series with an initial segment removed. |
| ⊢ F ∈ V & ⊢ A ∈ V & ⊢ (⟨M, + ⟩seqF) ⇝ A & ⊢ F:(ℤ≥ ‘M)–→ℂ ⇒ ⊢ (N ∈ (ℤ≥ ‘M) → (⟨(N + 1), + ⟩seqF) ⇝ (A − ((⟨M, + ⟩seqF) ‘N))) | ||
| Theorem | iserzex 7146 | If an infinite series converges, so does the series with initial terms removed. (Contributed by Paul Chapman, 23-Nov-2007.) |
| ⊢ F ∈ V & ⊢ A ∈ V & ⊢ M ∈ ℤ & ⊢ F:(ℤ≥ ‘M)–→ℂ & ⊢ (⟨M, + ⟩seqF) ⇝ A ⇒ ⊢ ((N ∈ ℤ ⋀ M < N) → ∃x(⟨N, + ⟩seqF) ⇝ x) | ||
| Theorem | climserzle 7147 | The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. |
| ⊢ F ∈ V & ⊢ A ∈ V & ⊢ (⟨M, + ⟩seqF) ⇝ A & ⊢ F:(ℤ≥ ‘M)–→ℝ ⇒ ⊢ ((N ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (ℤ≥ ‘M)0 ≤ (F ‘k)) → ((⟨M, + ⟩seqF) ‘N) ≤ A) | ||
| Theorem | climabslem 7148 | Lemma for climabs 7149, climcj 7150, climre 7151, and climim 7152. |
| Theorem | climabs 7149 | Limit of the absolute value of a sequence. (Contributed by Paul Chapman, 7-Sep-2007.) |
| ⊢ A ∈ V & ⊢ G ∈ V & ⊢ M ∈ ℤ & ⊢ F ⇝ A & ⊢ (k ∈ (ℤ≥ ‘M) → ((F ‘k) ∈ ℂ ⋀ (G ‘k) = (abs ‘(F ‘k)))) ⇒ ⊢ G ⇝ (abs ‘A) | ||
| Theorem | climcj 7150 | Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. |
| ⊢ A ∈ V & ⊢ G ∈ V & ⊢ M ∈ ℤ & ⊢ F ⇝ A & ⊢ (k ∈ (ℤ≥ ‘M) → ((F ‘k) ∈ ℂ ⋀ (G ‘k) = (∗ ‘(F ‘k)))) ⇒ ⊢ G ⇝ (∗ ‘A) | ||
| Theorem | climre 7151 | Limit of the real part of a sequence. (Contributed by Paul Chapman, 24-Sep-2007.) |
| ⊢ A ∈ V & ⊢ G ∈ V & ⊢ M ∈ ℤ & ⊢ F ⇝ A & ⊢ (k ∈ (ℤ≥ ‘M) → ((F ‘k) ∈ ℂ ⋀ (G ‘k) = (ℜ ‘(F ‘k)))) ⇒ ⊢ G ⇝ (ℜ ‘A) | ||
| Theorem | climim 7152 | Limit of the imaginary part of a sequence. (Contributed by Paul Chapman, 7-Sep-2007.) |
| ⊢ A ∈ V & ⊢ G ∈ V & ⊢ M ∈ ℤ & ⊢ F ⇝ A & ⊢ (k ∈ (ℤ≥ ‘M) → ((F ‘k) ∈ ℂ ⋀ (G ‘k) = (ℑ ‘(F ‘k)))) ⇒ ⊢ G ⇝ (ℑ ‘A) | ||
| Theorem | climubi 7153 | The limit of a monotonic sequence is an upper bound. |
| ⊢ A ∈ V & ⊢ F:ℕ–→ℝ & ⊢ (k ∈ ℕ → (F ‘k) ≤ (F ‘(k + 1))) & ⊢ F ⇝ A & ⊢ N ∈ ℕ ⇒ ⊢ (F ‘N) ≤ A | ||
| Theorem | climub 7154 | The limit of a monotonic sequence is an upper bound. |
| ⊢ A ∈ V & ⊢ F:ℕ–→ℝ & ⊢ (k ∈ ℕ → (F ‘k) ≤ (F ‘(k + 1))) & ⊢ F ⇝ A ⇒ ⊢ (N ∈ ℕ → (F ‘N) ≤ A) | ||
| Theorem | climsup 7155 | A bounded monotonic sequence converges to the supremum of its range. Theorem 12-5.1 of [Gleason] p. 180. |
| ⊢ F:ℕ–→ℝ & ⊢ (k ∈ ℕ → (F ‘k) ≤ (F ‘(k + 1))) & ⊢ ∃x ∈ ℝ ∀k ∈ ℕ (F ‘k) ≤ x ⇒ ⊢ F ⇝ sup(ran F, ℝ, < ) | ||
| Theorem | climcau 7156 | A converging sequence of complex numbers is a Cauchy sequence. Theorem 12-5.3 of [Gleason] p. 180 (necessity part). |
| ⊢ A ∈ V & ⊢ F ⇝ A & ⊢ F:ℕ–→ℂ ⇒ ⊢ ∀x ∈ ℝ (0 < x → ∃y ∈ ℕ ∀z ∈ ℕ (y < z → (abs ‘((F ‘z) − (F ‘y))) < x)) | ||
| Theorem | caucvglem1 7157 | Lemma for caucvg 7163. This lemma shows the membership relation for S. |
| Theorem | caucvglem2 7158 | Lemma for caucvg 7163. S is a nonempty bounded subset of ℝ. |
| Theorem | caucvglem3 7159 | Lemma for caucvg 7163. The supremum of S is a real number. |
| Theorem | caucvglem4 7160 | Lemma for caucvg 7163. Anything less that the supremum of S belongs to S. |
| Theorem | caucvglem5 7161 | Lemma for caucvg 7163. |
| Theorem | caucvglem6 7162 | Lemma for caucvg 7163. |
| Theorem | caucvg 7163 | A Cauchy sequence of real numbers converges. The second hypothesis specifies that F is a Cauchy sequence. S is the set of numbers less than all values of F except for finitely many. Reference: Bert G. Wachsmuth, http://www.shu.edu/projects/reals/numseq/proofs/cauconv.html. Request: Please contact Norm Megill if you know of a textbook reference for the version of the proof in the link above. Warning: The HTML proof page is 1/2 megabyte in size. |
| ⊢ F:ℕ–→ℝ & ⊢ ∀z ∈ ℝ (0 < z → ∃w ∈ ℕ ∀y ∈ ℕ (w < y → (abs ‘((F ‘y) − (F ‘w))) < z)) & ⊢ S = {u ∈ ℝ∣∃v ∈ ℕ ∀y ∈ ℕ (v ≤ y → u < (F ‘y))} ⇒ ⊢ F ⇝ sup(S, ℝ, < ) | ||
| Theorem | caucvg3a 7164 | A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). This version shows the explicit value of the limit (which is why we need all the hypotheses) rather than just its existence. |
| ⊢ F:ℕ–→ℂ & ⊢ ∀z ∈ ℝ (0 < z → ∃w ∈ ℕ ∀y ∈ ℕ (w < y → (abs ‘((F ‘y) − (F ‘w))) < z)) & ⊢ G Fn ℕ & ⊢ (x ∈ ℕ → (G ‘x) = (ℜ ‘(F ‘x))) & ⊢ R = {u ∈ ℝ∣∃v ∈ ℕ ∀y ∈ ℕ (v ≤ y → u < (G ‘y))} & ⊢ H Fn ℕ & ⊢ (x ∈ ℕ → (H ‘x) = (ℑ ‘(F ‘x))) & ⊢ S = {u ∈ ℝ∣∃v ∈ ℕ ∀y ∈ ℕ (v ≤ y → u < (H ‘y))} & ⊢ D Fn ℕ & ⊢ (x ∈ ℕ → (D ‘x) = (i · (H ‘x))) ⇒ ⊢ F ⇝ (sup(R, ℝ, < ) + (i · sup(S, ℝ, < ))) | ||
| Theorem | caucvg2 7165 | A Cauchy sequence of real numbers converges to a real number. |
| ⊢ F:ℕ–→ℝ & ⊢ ∀z ∈ ℝ (0 < z → ∃w ∈ ℕ ∀y ∈ ℕ (w < y → (abs ‘((F ‘y) − (F ‘w))) < z)) ⇒ ⊢ ∃x ∈ ℝ F ⇝ x | ||
| Theorem | caucvg3lem 7166 | Lemma for caucvg3 7167. |
| Theorem | caucvg3 7167 | A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). |
| ⊢ F:ℕ–→ℂ & ⊢ ∀y ∈ ℝ (0 < y → ∃j ∈ ℕ ∀k ∈ ℕ (j ≤ k → (abs ‘((F ‘k) − (F ‘j))) < y)) ⇒ ⊢ ∃x ∈ ℂ F ⇝ x | ||
| Theorem | caucvg3t 7168 | A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). Warning: The HTML proof page is 0.6 megabyte in size. |
| ⊢ ((F:ℕ–→ℂ ⋀ ∀z ∈ ℝ (0 < z → ∃w ∈ ℕ ∀y ∈ ℕ (w ≤ y → (abs ‘((F ‘y) − (F ‘w))) < z))) → ∃x ∈ ℂ F ⇝ x) | ||
| Theorem | serzf0 7169 | If an infinite series converges, its underlying sequence converges to zero. Warning: The HTML proof page is 0.6 megabyte in size. |
| ⊢ F ∈ V & ⊢ M ∈ ℤ & ⊢ (k ∈ (ℤ≥ ‘M) → (F ‘k) ∈ ℂ) & ⊢ A ∈ V & ⊢ (⟨M, + ⟩seqF) ⇝ | ||