Definition D1
The sequence (aₙ) satisfies aₙ₊₁ = r aₙ with first term a₁ = a and common ratio r.
Proof.
This equation determines aₙ uniquely for each natural number n. r does not vary with n.convention
∎
Definition D2
Sₙ is the sum from a₁ to aₙ, defined by S₁ = a₁, Sₖ₊₁ = Sₖ + aₖ₊₁.
Proof.
These two equations are used in place of an ellipsis. An ellipsis is an omission, not a rule.convention
∎
Definition D3
a ÷ b means the x satisfying b × x = a.
Proof.
a ÷ b has a value only when such an x is unique.convention
∎
Lemma L1
For every natural number n, aₙ₊₁ = a rⁿ
Proof.
(1)Let Q(n) be “aₙ₊₁ = a rⁿ”.convention
(2)a₂ = r a₁ = r a = a rD1, A4
(3)a r = a r¹, so Q(1) holds.(2), A7
(4)Suppose Q(k). aₖ₊₁ = a rᵏassumption
(5)aₖ₊₂ = r aₖ₊₁ = r(a rᵏ)D1, (4)
(6)r(a rᵏ) = (a rᵏ)r = a(rᵏ·r)A4, A5
(7)rᵏ·r = rᵏ⁺¹A7
(8)aₖ₊₂ = a rᵏ⁺¹, so Q(k+1) holds.(5), (6), (7)
(9)Therefore Q(n) holds for every n.(3), (8), A1
∎
Theorem T1
For every natural number n, (1 − r)Sₙ = a(1 − rⁿ)
Proof.
(1)Let P(n) be “(1−r)Sₙ = a(1−rⁿ)”.convention
(2)S₁ = aD2, D1
(3)(1−r)S₁ = (1−r)a = a(1−r) = a(1−r¹), so P(1) holds.(2), A4, A7
(4)Suppose P(k). (1−r)Sₖ = a(1−rᵏ)assumption
(5)Sₖ₊₁ = Sₖ + aₖ₊₁D2
(6)(1−r)Sₖ₊₁ = (1−r)Sₖ + (1−r)aₖ₊₁(5), E, A2
(7)aₖ₊₁ = a rᵏL1
(8)(1−r)a rᵏ = a rᵏ − (a rᵏ)r = a rᵏ − a rᵏ⁺¹(7), A4, A3, A6, A5, A7
(9)a(1−rᵏ) = a×1 − a rᵏ = a − a rᵏA3, A6
(10)(1−r)Sₖ₊₁ = (a − a rᵏ) + (a rᵏ − a rᵏ⁺¹)(6), (4), (8), (9)
(11)(a − a rᵏ) + (a rᵏ − a rᵏ⁺¹) = a − a rᵏ⁺¹A8
(12)a − a rᵏ⁺¹ = a×1 − a rᵏ⁺¹ = a(1 − rᵏ⁺¹)A6, A3
(13)(1−r)Sₖ₊₁ = a(1−rᵏ⁺¹), so P(k+1) holds.(10), (11), (12)
(14)Therefore P(n) holds for every n.(3), (13), A1
∎
Theorem T2
If r ≠ 1, then for every natural number n, Sₙ = a(1 − rⁿ)/(1 − r)
Proof.
(1)(1−r)Sₙ = a(1−rⁿ)T1
(2)Suppose r ≠ 1.assumption
(3)If 1 − r = 0, then (1−r) + r = 0 + r gives 1 = r.A9, A10, E
(4)Therefore 1 − r ≠ 0.(2), (3)
(5)There is a number (1−r)⁻¹ with (1−r)·(1−r)⁻¹ = 1.(4), A11
(6)If (1−r)x = (1−r)y, multiplying both sides by (1−r)⁻¹ gives x = y.(5), E, A4, A5, A6
(7)a(1−rⁿ) ÷ (1−r) is the x with (1−r)x = a(1−rⁿ).D3
(8)Sₙ is such an x, and such an x is unique.(1), (6), (7)
(9)Sₙ = a(1−rⁿ)/(1−r)(8), D3
∎