Statement List for Metamath Proof Explorer - 6901-7000 - Page 70 of 107
| Type | Label | Description |
|---|
| Statement |
|---|
| |
| Theorem | faclbnd4lem1 6901 |
Lemma for faclbnd4 6905. Prepare the induction step. Warning:
The HTML
proof page is 0.6 megabyte in size.
|
| |
| Theorem | faclbnd4lem2 6902 |
Lemma for faclbnd4 6905. Use the weak deduction theorem to convert
the hypotheses of faclbnd4lem1 6901 to antecedents.
|
| |
| Theorem | faclbnd4lem3 6903 |
Lemma for faclbnd4 6905. The N =
0 case.
|
| |
| Theorem | faclbnd4lem4 6904 |
Lemma for faclbnd4 6905. Prove the 0 < N case by induction on
K.
|
| |
| Theorem | faclbnd4 6905 |
Variant of faclbnd5 6906 providing a non-strict lower bound.
|
| ⊢
((N ∈ ℕ0
⋀ K ∈ ℕ0
⋀ M ∈ ℕ0)
→ ((N↑K) · (M↑N)) ≤
(((2↑(K↑2)) · (M↑(M +
K))) · (! ‘N))) |
| |
| Theorem | faclbnd5 6906 |
The factorial function grows faster than powers and exponentiations. If
we consider K and M to be constants, the right-hand side of the
inequality is a constant times N
-factorial.
|
| ⊢
((N ∈ ℕ0
⋀ K ∈ ℕ0
⋀ M ∈ ℕ) →
((N↑K) · (M↑N)) <
((2 · ((2↑(K↑2)) ·
(M↑(M + K))))
· (! ‘N))) |
| |
| Theorem | faclbnd6 6907 |
Geometric lower bound for the factorial function, where N is usually
held constant. (Contributed by Paul Chapman, 28-Dec-2007.)
|
| ⊢
((N ∈ ℕ0
⋀ M ∈ ℕ0)
→ ((! ‘N) · ((N + 1)↑M))
≤ (! ‘(N + M))) |
| |
| Theorem | facavgt 6908 |
The product of two factorials is greater than or equal to the factorial of
(the floor of) their average.
|
| ⊢
((M ∈ ℕ0
⋀ N ∈ ℕ0)
→ (! ‘(⌊ ‘((M +
N) / 2))) ≤ ((! ‘M) · (! ‘N))) |
| |
| The
binomial coefficient operation |
| |
| Syntax | cbc 6909 |
Extend class notation to include the binomial coefficient operation
(combinatorial choose operation).
|
| class
C |
| |
| Definition | df-bc 6910 |
Define the binomial coefficient operation. In the literature, this
function is often written as a column vector of the two arguments, or
with the arguments as subscripts before and after the letter
"C".
(NCK) is read "N choose K." Definition of
binomial coefficient in [Gleason] p.
295. As suggested by Gleason,
we define it to be 0 when 0 ≤ k
≤ n does not hold.
|
| ⊢ C
= {⟨⟨n, k⟩, m⟩∣((n ∈ ℕ0 ⋀ k ∈ ℤ) ⋀ m = if((0 ≤ k ⋀ k
≤ n), ((! ‘n) / ((! ‘(n − k))
· (! ‘k))), 0))} |
| |
| Theorem | bcvalt 6911 |
Value of the binomial coefficient, N choose
K. Definition
of binomial coefficient in [Gleason] p.
295. As suggested by Gleason,
we define it to be 0 when 0 ≤ K
≤ N does not hold. See bcval2t 6913
for the value in the standard domain.
|
| ⊢
((N ∈ ℕ0
⋀ K ∈ ℤ) → (NCK) = if((0
≤ K ⋀ K ≤ N), ((!
‘N) / ((! ‘(N − K))
· (! ‘K))), 0)) |
| |
| Theorem | bcval3tOLD 6912 |
Value of the binomial coefficient, N choose
K, in its standard
domain.
|
| ⊢
(((N ∈ ℕ0
⋀ K ∈ ℤ) ⋀ (0 ≤
K ⋀ K ≤ N))
→ (NCK) = ((! ‘N) / ((! ‘(N − K))
· (! ‘K)))) |
| |
| Theorem | bcval2t 6913 |
Value of the binomial coefficient, N choose
K, in its standard
domain.
|
| ⊢
((N ∈ ℕ0
⋀ K ∈ ℕ0
⋀ K ≤ N) → (NCK) = ((!
‘N) / ((! ‘(N − K))
· (! ‘K)))) |
| |
| Theorem | bcval3t 6914 |
Value of the binomial coefficient, N choose
K, in its standard
domain.
|
| ⊢
((N ∈ ℕ0
⋀ K ∈ (0...N)) → (NCK) = ((!
‘N) / ((! ‘(N − K))
· (! ‘K)))) |
| |
| Theorem | bcval4t 6915 |
Value of the binomial coefficient, N choose
K, outside of its
standard domain. Remark in [Gleason]
p. 295.
|
| ⊢
((N ∈ ℕ0
⋀ K ∈ ℤ ⋀ (K < 0 ⋁ N < K))
→ (NCK) = 0) |
| |
| Theorem | bccmplt 6916 |
"Complementing" its second argument doesn't change a binary
coefficient.
|
| ⊢
((N ∈ ℕ0
⋀ K ∈ ℕ0
⋀ K ≤ N) → (NCK) =
(NC(N
− K))) |
| |
| Theorem | bcn0t 6917 |
N choose 0 is 1. Remark in [Gleason] p. 296.
|
| ⊢
(N ∈ ℕ0
→ (NC0) = 1) |
| |
| Theorem | bcnnt 6918 |
N choose N is 1. Remark in [Gleason] p. 296.
|
| ⊢
(N ∈ ℕ0
→ (NCN) = 1) |
| |
| Theorem | bcnp11t 6919 |
Binomial coefficient: N + 1 choose 1.
|
| ⊢
(N ∈ ℕ0
→ ((N + 1)C1) = (N + 1)) |
| |
| Theorem | bcnp1nt 6920 |
Binomial coefficient: N + 1 choose N.
|
| ⊢
(N ∈ ℕ0
→ ((N + 1)CN) = (N +
1)) |
| |
| Theorem | bcpasc2 6921 |
Pascal's rule for the binomial coefficient. Equation 2 of [Gleason]
p. 295.
|
| ⊢
N ∈ ℕ
& ⊢ K ∈ ℕ
& ⊢ K ≤ N ⇒ ⊢ ((NCK) +
(NC(K
− 1))) = ((N + 1)CK) |
| |
| Theorem | bcpasc2t 6922 |
Pascal's rule for the binomial coefficient. Equation 2 of [Gleason]
p. 295.
|
| ⊢
((N ∈ ℕ ⋀ K ∈ ℕ ⋀ K ≤ N)
→ ((NCK) + (NC(K −
1))) = ((N + 1)CK)) |
| |
| Theorem | bcpasc 6923 |
Pascal's rule for the binomial coefficient, generalized to all integers
K. Equation 2 of [Gleason] p. 295.
|
| ⊢
N ∈
ℕ0 & ⊢ K ∈
ℤ ⇒ ⊢ ((NCK) +
(NC(K
− 1))) = ((N + 1)CK) |
| |
| Theorem | bcpasct 6924 |
Pascal's rule for the binomial coefficient, generalized to all integers
K. Equation 2 of [Gleason] p. 295.
|
| ⊢
((N ∈ ℕ0
⋀ K ∈ ℤ) →
((NCK)
+ (NC(K − 1))) = ((N + 1)CK)) |
| |
| Theorem | bccl2t 6925 |
A binomial coefficient, in its standard domain, is a natural number.
|
| ⊢
((N ∈ ℕ0
⋀ K ∈ (0...N)) → (NCK) ∈
ℕ) |
| |
| Theorem | bcclt 6926 |
A binomial coefficient, in its extended domain, is a nonnegative
integer.
|
| ⊢
((N ∈ ℕ0
⋀ K ∈ ℤ) → (NCK) ∈
ℕ0) |
| |
| Theorem | permnnt 6927 |
The number of permutations of N −
R objects from a collection of N
objects is a natural number. (Contributed by Jason Orendorff,
24-Jan-2007.)
|
| ⊢
((N ∈ ℕ0
⋀ R ∈ (0...N)) → ((! ‘N) / (! ‘R)) ∈ ℕ) |
| |
| Limits |
| |
| Syntax | cli 6928 |
Extend class notation with convergence relation for limits.
|
| class
⇝ |
| |
| Definition | df-clim 6929 |
Define the limit relation for complex number sequences. See clim 6931
for its relational expression.
|
| ⊢
⇝ = {⟨f, y⟩∣(y ∈ ℂ ⋀ ∀x ∈ ℝ (0 < x → ∃j ∈ ℤ ∀k ∈ ℤ (j ≤ k →
((f ‘k) ∈ ℂ ⋀ (abs ‘((f ‘k)
− y)) < x))))} |
| |
| Theorem | climrel 6930 |
The limit relation is a relation.
|
| ⊢
Rel ⇝ |
| |
| Theorem | clim 6931 |
Express the predicate: The limit of complex number sequence F
is A, or F converges to A. This means that for any
real x, no matter how small, there
always exists an integer
j such that the absolute difference
of any later complex number
in the sequence and the limit is less than x.
|
| ⊢
((F ∈ C ⋀ A
∈ D) → (F ⇝ A
↔ (A ∈ ℂ ⋀
∀x ∈ ℝ (0 < x → ∃j ∈ ℤ ∀k ∈ ℤ (j ≤ k →
((F ‘k) ∈ ℂ ⋀ (abs ‘((F ‘k)
− A)) < x)))))) |
| |
| Theorem | climcl 6932 |
Closure of the limit of a sequence of complex numbers.
|
| ⊢
((A ∈ C ⋀ F
⇝ A) → A ∈ ℂ) |
| |
| Finite and infinite sums |
| |
| Syntax | csu 6933 |
Extend class notation to include finite summations. (An underscore was
added the ASCII token in order to facilitate text searches, since
"sum" is
is a commonly used word in comments.)
|
| class
Σk ∈ A B |
| |
| Definition | df-sum 6934 |
Define the sum of a series with an index set of integers A.
k is normally a free variable in
B, i.e. B can be thought
of as B(k). The definition is meaningful when A is a finite
set of sequential integers (representing a finite sum over them) or a
set of upper integers (representing an infinite sum, when the sum
converges). The left-hand side of the union expresses the finite sum
case, and the right-hand side expresses the infinite sum case. In
either case, the other side of the union equals the empty set.
Examples: Σk ∈ (2...4)
k means 2 + 3 + 4 = 9, and
Σk ∈ ℕ (1 /
(2↑k)) means 1/2 + 1/4 + 1/8 + ... =
1.
Note: The restrictions to ℤ force the class abstractions to be
sets.
|
| ⊢
Σk ∈ A B =
({x∣∃m∃n
∈ (ℤ≥ ‘m)(A =
(m...n) ⋀ x
∈ ((⟨m, +
⟩seq({⟨k, y⟩∣y
= B} ↾ ℤ)) ‘n))} ∪ ∪{x∣∃m ∈ ℤ (A = (ℤ≥ ‘m) ⋀ (⟨m, + ⟩seq({⟨k, y⟩∣y
= B} ↾ ℤ)) ⇝ x)}) |
| |
| Theorem | sumex 6935 |
A sum is a set.
|
| ⊢
Σk ∈ A B ∈
V |
| |
| Theorem | sumeq1 6936 |
Equality theorem for a sum.
|
| ⊢
(A = B → Σk ∈ A
C = Σk ∈ B
C) |
| |
| Theorem | hbsum1 6937 |
Bound-variable hypothesis builder for sum.
|
| ⊢
(x ∈ A → ∀k x ∈
A)
⇒ ⊢ (x ∈ Σk ∈ A
B → ∀k x ∈
Σk ∈ A B) |
| |
| Theorem | hbsum 6938 |
Bound-variable hypothesis builder for sum: if x is (effectively)
not free in A and B, it is not free in Σk ∈ AB.
|
| ⊢
(y ∈ A → ∀x y ∈
A)
& ⊢ (y ∈ B
→ ∀x y ∈ B) ⇒ ⊢ (y ∈
Σk ∈ A B →
∀x y ∈ Σk ∈ A
B) |
| |
| Theorem | sumeq2 6939 |
Equality theorem for sum.
|
| ⊢
(∀k ∈ A B = C → Σk ∈ A
B = Σk ∈ A
C) |
| |
| Theorem | cbvsum 6940 |
Change bound variable in a sum.
|
| ⊢
(x ∈ B → ∀k x ∈
B)
& ⊢ (x ∈ C
→ ∀j x ∈ C) & ⊢ (j =
k → B = C) ⇒ ⊢ Σj
∈ A B = Σk
∈ A C |
| |
| Theorem | sumeq1i 6941 |
Equality inference for sum.
|
| ⊢
A = B ⇒ ⊢ Σk
∈ A C = Σk
∈ B C |
| |
| Theorem | sumeq2i 6942 |
Equality inference for sum.
|
| ⊢
(k ∈ A → B =
C)
⇒ ⊢ Σk ∈ A
B = Σk ∈ A
C |
| |
| Theorem | sumeq12i 6943 |
Equality inference for sum. (Contributed by FL, 10-Dec-2006.)
|
| ⊢
A = B & ⊢ (k ∈
A → C = D) ⇒ ⊢ Σk
∈ A C = Σk
∈ B D |
| |
| Theorem | sumeq1d 6944 |
Equality deduction for sum.
|
| ⊢
(φ → A = B) ⇒ ⊢ (φ
→ Σk ∈ A C =
Σk ∈ B C) |
| |
| Theorem | sumeq2d 6945 |
Equality deduction for sum. Note that unlike sumeq2dv 6946, k may
occur in φ.
|
| ⊢
(φ → ∀k ∈ A
B = C) ⇒ ⊢ (φ
→ Σk ∈ A B =
Σk ∈ A C) |
| |
| Theorem | sumeq2dv 6946 |
Equality deduction for sum.
|
| ⊢
((φ ⋀ k ∈ A)
→ B = C) ⇒ ⊢ (φ
→ Σk ∈ A B =
Σk ∈ A C) |
| |
| Theorem | sumeq2sdv 6947 |
Equality deduction for sum.
|
| ⊢
(φ → B = C) ⇒ ⊢ (φ
→ Σk ∈ A B =
Σk ∈ A C) |
| |
| Theorem | 2sumeq2dv 6948 |
Equality deduction for double sum.
|
| ⊢
((φ ⋀ j ∈ A
⋀ k ∈ B) → C =
D)
⇒ ⊢ (φ → Σj ∈ A
Σk ∈ B C =
Σj ∈ A Σk
∈ B D) |
| |
| Theorem | sumeq12dv 6949 |
Equality deduction for sum.
|
| ⊢
(φ → A = B) & ⊢ ((φ
⋀ k ∈ A) → C =
D)
⇒ ⊢ (φ → Σk ∈ A
C = Σk ∈ B
D) |
| |
| Theorem | sumeq12rdv 6950 |
Equality deduction for sum.
|
| ⊢
(φ → A = B) & ⊢ ((φ
⋀ k ∈ B) → C =
D)
⇒ ⊢ (φ → Σk ∈ A
C = Σk ∈ B
D) |
| |
| Theorem | sumeqfv 6951 |
Convert a sum of function values to a sum of classes A(k).
|
| ⊢
A ∈ V
& ⊢ F = {⟨k,
y⟩∣(k ∈ B
⋀ y = A)}
⇒ ⊢ (C ⊆ B
→ Σk ∈ C (F
‘k) = Σk ∈ C
A) |
| |
| Finite sums (cont.) |
| |
| Theorem | dffsum 6952 |
Special case of series sum over a finite index set.
|
| ⊢
(N ∈ (ℤ≥
‘M) → Σk ∈ (M...N)A = ((⟨M,
+ ⟩seq({⟨k, y⟩∣y
= A} ↾ ℤ)) ‘N)) |
| |
| Theorem | fsumserz 6953 |
A finite sum expressed in terms of a partial sum of an infinite
series. The recursive definition of follows as fsum1 6959 and fsump1 6960,
which should make our notation clear and from which, along with closure
fsumclt 6969, we will derive the basic properties of
finite sums.
|
| ⊢
F ∈ V
⇒ ⊢ (N ∈ (ℤ≥ ‘M) → Σk ∈ (M...N)(F ‘k) =
((⟨M, + ⟩seqF) ‘N)) |
| |
| Theorem | fsumserzf 6954 |
Version of fsumserz 6953 with a bound-variable hypothesis instead of a
distinct variable condition.
|
| ⊢
F ∈ V
& ⊢ (x ∈ F
→ ∀k x ∈ F) ⇒ ⊢ (N ∈
(ℤ≥ ‘M) →
Σk ∈ (M...N)(F ‘k) =
((⟨M, + ⟩seqF) ‘N)) |
| |
| Theorem | fsumser0f 6955 |
A finite sum expressed in terms of a partial sum of an infinite
0-based series.
|
| ⊢
F ∈ V
& ⊢ (x ∈ F
→ ∀k x ∈ F) ⇒ ⊢ (N ∈
ℕ0 → Σk ∈
(0...N)(F ‘k) =
(( + seq0F) ‘N)) |
| |
| Theorem | fsumser1f 6956 |
A finite sum expressed in terms of a partial sum of an infinite
1-based series.
|
| ⊢
F ∈ V
& ⊢ (x ∈ F
→ ∀k x ∈ F) ⇒ ⊢ (N ∈
ℕ → Σk ∈
(1...N)(F ‘k) =
(( + seq1F) ‘N)) |
| |
| Theorem | fsumserz2 6957 |
A finite sum expressed in terms of a partial sum of an infinite
series.
|
| ⊢
A ∈ V
& ⊢ F = {⟨k,
y⟩∣(k ∈ (ℤ≥ ‘M) ⋀ y =
A)}
⇒ ⊢ (N ∈ (ℤ≥ ‘M) → Σk ∈ (M...N)A = ((⟨M,
+ ⟩seqF) ‘N)) |
| |
| Theorem | serzfsum 6958 |
An infinite series in terms of finite partial sums of A(k).
|
| ⊢
A ∈ V
& ⊢ F = {⟨k,
y⟩∣(k ∈ (ℤ≥ ‘M) ⋀ y =
A)}
& ⊢ G = {⟨n,
z⟩∣(n ∈ (ℤ≥ ‘M) ⋀ z =
Σk ∈ (M...n)A)}
⇒ ⊢ (M ∈ ℤ → (⟨M, + ⟩seqF) = G) |
| |
| Theorem | fsum1 6959 |
The finite sum of A(k) from k =
M to M
(i.e. a sum with
only one term) is B i.e. A(M).
|
| ⊢
(k = M → A =
B)
⇒ ⊢ ((B ∈ C
⋀ M ∈ ℤ) →
Σk ∈ (M...M)A = B) |
| |
| Theorem | fsump1 6960 |
The addition of the next term in a finite sum of A(k) is the
current term plus B i.e. A(N + 1).
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ (k = (N + 1)
→ A = B) ⇒ ⊢ (N ∈
(ℤ≥ ‘M) →
Σk ∈ (M...(N +
1))A = (Σk ∈ (M...N)A + B)) |
| |
| Theorem | fsum1f 6961 |
The finite sum of a term A(k) from M to
M (i.e. a sum
with only one term) is A(M) = B, where
k is effectively
not free in B.
|
| ⊢
(x ∈ B → ∀k x ∈
B)
& ⊢ (k = M →
A = B) ⇒ ⊢ ((B ∈
C ⋀ M ∈ ℤ) → Σk ∈ (M...M)A = B) |
| |
| Theorem | fsum1slem 6962 |
Lemma for fsum1s 6963.
|
| |
| Theorem | fsum1s 6963 |
The finite sum of a sequence A(k) from M to
M (i.e. a sum
with only one term) is A(M).
|
| ⊢
((M ∈ ℤ ⋀
∀k ∈ (M...M)A ∈ B)
→ Σk ∈ (M...M)A = [M /
k]A) |
| |
| Theorem | fsum1s2 6964 |
The finite sum of a sequence A(k) from M to
M (i.e. a sum
with only one term) is A(M).
|
| ⊢
((M ∈ ℤ ⋀
[M / k]A
∈ B) → Σk ∈ (M...M)A = [M /
k]A) |
| |
| Theorem | fsump1f 6965 |
The addition of the next term in a finite sum of A(k) is the
previous term plus A(N + 1) = B.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ (x ∈ B
→ ∀k x ∈ B) & ⊢ (k =
(N + 1) → A = B) ⇒ ⊢ (N ∈
(ℤ≥ ‘M) →
Σk ∈ (M...(N +
1))A = (Σk ∈ (M...N)A + B)) |
| |
| Theorem | fsump1slem 6966 |
Lemma for fsump1s 6967.
|
| |
| Theorem | fsump1s 6967 |
The addition of the next term in a finite sum of A(k) is the
previous term plus A(N + 1).
|
| ⊢
((N ∈ (ℤ≥
‘M) ⋀ ∀k ∈ (M...(N +
1))A ∈ B) → Σk ∈ (M...(N +
1))A = (Σk ∈ (M...N)A + [(N
+ 1) / k]A)) |
| |
| Theorem | fsumcllem 6968 |
- Lemma for finite sum closures. (The "-" before "Lemma"
forces the
math content to be displayed in the Statement List - NM 11-Feb-2008.)
|
| ⊢
((x ∈ C ⋀ y
∈ C) → (x + y) ∈
C)
⇒ ⊢ ((N ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...N)A ∈ C)
→ Σk ∈ (M...N)A ∈ C) |
| |
| Theorem | fsumclt 6969 |
Closure of a finite sum of complex numbers A(k).
|
| ⊢
((N ∈ (ℤ≥
‘M) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A ∈ ℂ) |
| |
| Theorem | fsum0clt 6970 |
Closure of a finite sum of complex numbers A(k), starting
at
index zero.
|
| ⊢
((N ∈ ℕ0
⋀ ∀k ∈ (0...N)A ∈
ℂ) → Σk ∈
(0...N)A ∈ ℂ) |
| |
| Theorem | fsumreclt 6971 |
Closure of a finite sum of reals.
|
| ⊢
((N ∈ (ℤ≥
‘M) ⋀ ∀k ∈ (M...N)A ∈ ℝ) → Σk ∈ (M...N)A ∈ ℝ) |
| |
| Theorem | fsum1ps 6972 |
Separate out the first term in a finite sum.
|
| ⊢
((N ∈ (ℤ≥
‘M) ⋀ M < N
⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = ([M
/ k]A + Σk
∈ ((M + 1)...N)A)) |
| |
| Theorem | fsum1p 6973 |
Separate out the first term in a finite sum.
|
| ⊢
(k = M → A =
B)
⇒ ⊢ ((N ∈ (ℤ≥ ‘M) ⋀ M
< N ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = (B +
Σk ∈ ((M + 1)...N)A)) |
| |
| Theorem | fsumsplit 6974 |
Split a finite sum into two parts. Warning: The HTML proof page is
0.6 megabyte in size.
|
| ⊢
((N ∈ ℤ ⋀ K ∈ (M...(N −
1)) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → Σk ∈ (M...N)A = (Σk
∈ (M...K)A +
Σk ∈ ((K + 1)...N)A)) |
| |
| Theorem | fsum0split 6975 |
Split a finite sum into two parts.
|
| ⊢
((N ∈ ℤ ⋀ K ∈ (1...N) ⋀ ∀k ∈ (0...N)A ∈
ℂ) → Σk ∈
(0...N)A = (Σk
∈ (0...(N − K))A +
Σk ∈ (((N − K) +
1)...N)A)) |
| |
| Theorem | fsumadd 6976 |
The sum of two finite sums.
|
| ⊢
((N ∈ (ℤ≥
‘M) ⋀ ∀k ∈ (M...N)(A ∈ ℂ ⋀ B ∈ ℂ)) → Σk ∈ (M...N)(A + B) =
(Σk ∈ (M...N)A + Σk
∈ (M...N)B)) |
| |
| Theorem | fsum2 6977 |
The sum of two terms.
|
| ⊢
A ∈ V
⇒ ⊢ (M ∈ ℤ → Σk ∈ (M...(M +
1))A = ([M / k]A +
[(M + 1) / k]A)) |
| |
| Theorem | fsum3 6978 |
The sum of three terms.
|
| ⊢
A ∈ V
⇒ ⊢ (M ∈ ℤ → Σk ∈ (M...(M +
2))A = (([M / k]A +
[(M + 1) / k]A) +
[(M + 2) / k]A)) |
| |
| Theorem | fsum4 6979 |
The sum of four terms.
|
| ⊢
A ∈ V
⇒ ⊢ (M ∈ ℤ → Σk ∈ (M...(M +
3))A = ((([M / k]A +
[(M + 1) / k]A) +
[(M + 2) / k]A) +
[(M + 3) / k]A)) |
| |
| Theorem | csbfsumlem 6980 |
Lemma for csbfsum 6981.
|
| |
| Theorem | csbfsum 6981 |
Distribute substitution for classes over a finite sum.
|
| ⊢
((A ∈ C ⋀ N
∈ (ℤ≥ ‘M)
⋀ ∀k ∈ (M...N)[A /
x]B ∈ ℂ) → [A / x]Σk ∈ (M...N)B = Σk
∈ (M...N)[A /
x]B) |
| |
| Theorem | fsumcom 6982 |
Interchange order of summation. Warning: The HTML proof page is 0.6MB
in size.
|
| ⊢
((K ∈ (ℤ≥
‘J) ⋀ N ∈ (ℤ≥ ‘M) ⋀ ∀j ∈ (J...K)∀m
∈ (M...N)A ∈
ℂ) → Σj ∈ (J...K)Σm
∈ (M...N)A =
Σm ∈ (M...N)Σj
∈ (J...K)A) |
| |
| Theorem | fsumrev 6983 |
Reversal of a finite sum. Warning: The HTML proof page is 0.6 MB
in size.
|
| ⊢
((N ∈ (ℤ≥
‘M) ⋀ K ∈ ℤ ⋀ ∀j ∈ (M...N)A ∈ ℂ) → Σj ∈ (M...N)A = Σk
∈ ((K − N)...(K −
M))[(K − k) /
j]A) |
| |
| Theorem | fsumrev2 6984 |
Reversal of a finite sum.
|
| ⊢
((N ∈ (ℤ≥
‘M) ⋀ ∀j ∈ (M...N)A ∈ ℂ) → Σj ∈ (M...N)A = Σk
∈ (M...N)[((M +
N) − k) / j]A) |
| |
| Theorem | fsumshft 6985 |
Index shift of a finite sum.
|
| ⊢
((N ∈ (ℤ≥
‘M) ⋀ K ∈ ℤ ⋀ ∀j ∈ (M...N)A ∈ ℂ) → Σj ∈ (M...N)A = Σk
∈ ((M + K)...(N +
K))[(k − K) /
j]A) |
| |
| Theorem | fsumshftm 6986 |
Negative index shift of a finite sum.
|
| ⊢
((N ∈ (ℤ≥
‘M) ⋀ K ∈ ℤ ⋀ ∀j ∈ (M...N)A ∈ ℂ) → Σj ∈ (M...N)A = Σk
∈ ((M − K)...(N −
K))[(k + K) /
j]A) |
| |
| Theorem | fsummulc1 6987 |
A finite sum multiplied by a constant.
|
| ⊢
((N ∈ (ℤ≥
‘M) ⋀ C ∈ ℂ ⋀ ∀k ∈ (M...N)A ∈ ℂ) → (C · Σk ∈ (M...N)A) = Σk
∈ (M...N)(C ·
A)) |
| |
| Theorem | fsummulc2 6988 |
A finite sum multiplied by a constant.
|
| ⊢
((N ∈ (ℤ≥
‘M) ⋀ C ∈ ℂ ⋀ ∀k ∈ (M...N)A ∈ ℂ) → (Σk ∈ (M...N)A · C) =
Σk ∈ (M...N)(A · C)) |
| |
| Theorem | fsumdivc 6989 |
A finite sum divided by a constant.
|
| ⊢
(((N ∈ (ℤ≥
‘M) ⋀ C ∈ ℂ) ⋀ (C ≠ 0 ⋀ ∀k ∈ (M...N)A ∈ ℂ)) → (Σk ∈ (M...N)A / C) =
Σk ∈ (M...N)(A / C)) |
| |
| Theorem | fsumdivcALT 6990 |
A finite sum divided by a constant. (An experiment: this version
of fsumdivc 6989 adds 5 bytes and 233 bytes to the compressed
and
uncompressed proofs, but saves 540 bytes on the HTML page.)
|
| ⊢
(((N ∈ (ℤ≥
‘M) ⋀ C ∈ ℂ) ⋀ (C ≠ 0 ⋀ ∀k ∈ (M...N)A ∈ ℂ)) → (Σk ∈ (M...N)A / C) =
Σk ∈ (M...N)(A / C)) |
| |
| Theorem | fsum2mul 6991 |
Separate the nested sum of the product A(j) ·
B(m).
|
| ⊢
(((K ∈ (ℤ≥
‘J) ⋀ ∀j ∈ (J...K)A ∈ ℂ) ⋀ (N ∈ (ℤ≥ ‘M) ⋀ ∀m ∈ (M...N)B ∈ ℂ)) → Σj ∈ (J...K)Σm
∈ (M...N)(A ·
B) = (Σj ∈ (J...K)A · Σm ∈ (M...N)B)) |
| |
| Theorem | fsumconst 6992 |
The sum of constant terms (k is not free in
A).
|
| ⊢
((N ∈ (ℤ≥
‘M) ⋀ A ∈ ℂ) → Σk ∈ (M...N)A = (((N
− M) + 1) · A)) |
| |
| Theorem | fsum0 6993 |
If all of the terms of a finite sum are zero, so is the sum.
|
| ⊢
(N ∈ (ℤ≥
‘M) → Σk ∈ (M...N)0 =
0) |
| |
| Theorem | fsumcmp 6994 |
If all of the terms of finite sums compare, so do the sums.
|
| ⊢
((N ∈ (ℤ≥
‘M) ⋀ ∀k ∈ (M...N)(A ∈ ℝ ⋀ B ∈ ℝ ⋀ A ≤ B))
→ Σk ∈ (M...N)A ≤ Σk
∈ (M...N)B) |
| |
| Theorem | fsumcmp0 6995 |
If all of the terms of a finite sum are nonnegative, so is the sum.
|
| ⊢
((N ∈ (ℤ≥
‘M) ⋀ ∀k ∈ (M...N)(A ∈ ℝ ⋀ 0 ≤ A)) → 0 ≤ Σk ∈ (M...N)A) |
| |
| Theorem | fsumcmpndx2 6996 |
A shorter sum of nonnegative terms is smaller than a longer one.
|
| ⊢
(((J ∈ (ℤ≥
‘M) ⋀ K ∈ (ℤ≥ ‘M)) ⋀ (∀k ∈ (M...K)(A ∈ ℝ ⋀ 0 ≤ A) ⋀ J
≤ K)) → Σk ∈ (M...J)A ≤ Σk
∈ (M...K)A) |
| |
| Theorem | fsumabs 6997 |
Generalized triangle inequality: the absolute value of a finite sum is
less than or equal to the sum of absolute values.
|
| ⊢
((N ∈ (ℤ≥
‘M) ⋀ ∀k ∈ (M...N)A ∈ ℂ) → (abs
‘Σk ∈ (M...N)A) ≤ Σk ∈ (M...N)(abs
‘A)) |
| |
| Theorem | fsumabs2mul 6998 |
The sum of absolute values of the product A(j) ·
B(m) is
less than or equal to the product of the two sums of absolute values.
|
| ⊢
(((K ∈ (ℤ≥
‘J) ⋀ ∀j ∈ (J...K)A ∈ ℂ) ⋀ (N ∈ (ℤ≥ ‘M) ⋀ ∀m ∈ (M...N)B ∈ ℂ)) → (abs
‘Σj ∈ (J...K)Σm
∈ (M...N)(A ·
B)) ≤ (Σj ∈ (J...K)(abs
‘A) · Σm ∈ (M...N)(abs
‘B))) |
| |
| Theorem | serzclt 6999 |
Closure of partial sums of an infinite series.
|
| ⊢
F ∈ V
⇒ ⊢ ((N ∈ (ℤ≥ ‘M) ⋀ ∀k ∈ (M...N)(F ‘k)
∈ ℂ) → ((⟨M, +
⟩seqF) ‘N) ∈ ℂ) |
| |
| Theorem | ser0clt 7000 |
Closure of partial sums of a 0-based infinite series.
|
| ⊢
F ∈ V
⇒ ⊢ ((N ∈ ℕ0 ⋀
∀k ∈ (0...N)(F
‘k) ∈ ℂ) → (( +
seq0F) ‘N) ∈ ℂ) |
Home
Hilbert Space Explorer
(8744-10691)