English
Let a, b be real numbers and n an integer. If either n is nonnegative or n ≠ −1 and 0 is not in the closed interval [a, b], then the definite integral of x^n from a to b equals (b^(n+1) − a^(n+1)) / (n+1).
Русский
Пусть a, b — вещественные числа, а n — целое число. Тогда при условии: либо n ≥ 0, либо n ≠ −1 и 0 ∉ [a, b], выполняется равенство ∫_a^b x^n dx = (b^(n+1) − a^(n+1)) / (n+1).
LaTeX
$$$\forall a,b \in \mathbb{R},\ \forall n \in \mathbb{Z},\ (0 \le n) \lor (n \neq -1 \wedge 0 \notin [a,b]) \Rightarrow \displaystyle \int_a^b x^n \, dx = \frac{b^{n+1} - a^{n+1}}{n+1}$$$
Lean4
theorem integral_zpow {n : ℤ} (h : 0 ≤ n ∨ n ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]]) :
∫ x in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1) :=
by
replace h : -1 < (n : ℝ) ∨ (n : ℝ) ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]] := mod_cast h
exact mod_cast integral_rpow h
