Grace/Cumulus/Nat/PowLemmas.g17

Open in Workbench Download source

Imports

Pow · OrderLemmas

Declarations

Source

1-- Laws of natural-number exponentiation: exponent arithmetic, positivity,2-- and monotonicity in the base and in the exponent3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Nat.PowLemmas9import Pow10import OrderLemmas1112theorem pow.add_one (a n : Nat)13  shows a ^ (n + 1) = a * a ^ n14proof15  have shape := add.right_one at n16  rw shape17  exact pow.succ with *1819theorem pow.succ_right (a n : Nat)20  shows a ^ (n + 1) = a ^ n * a21proof22  have powNat := pow.closed at a, n23  rw pow.add_one24  exact mul.commutative at a ^ n, a with *2526theorem pow.one_right (a : Nat)27  shows a ^ 1 = a28proof29  simp [pow, mul.right_unit]3031theorem pow.two (a : Nat)32  shows a ^ 2 = a * a33proof34  simp [pow, mul.right_unit]3536theorem pow.one_left (n : Nat)37  shows 1 ^ n = 138proof39  induction n40  | zero => simp [pow]41  | succ(k) using ih => simp [pow, ih, mul.left_unit]4243theorem pow.zero_left (n : Nat)44  shows 0 ^ (n + 1) = 045proof46  rw pow.add_one47  have powNat := pow.closed at 0, n48  exact mul.left_zero with *4950theorem pow.mul_base (a b n : Nat)51  shows (a * b) ^ n = a ^ n * b ^ n52proof53  induction n54  | zero => simp [pow, mul.right_unit]55  | succ(k) using ih =>56    have productNat : Nat(a * b) by typecheck57    have aPow := pow.closed at a, k58    have bPow := pow.closed at b, k59    rw [pow.succ, pow.succ, pow.succ, ih]60    ring6162theorem pow.mul_exponent (a m n : Nat)63  shows (a ^ m) ^ n = a ^ (m * n)64proof65  induction n66  | zero =>67    have vanish := mul.right_zero at m68    rw vanish69    have basePow := pow.closed at a, m70    rw [pow.zero, pow.zero]71    rfl72  | succ(k) using ih =>73    have basePow := pow.closed at a, m74    have productNat : Nat(m * k) by typecheck75    have shape : m * succ(k) = m + m * k by ring76    rw [pow.succ, ih, shape]77    have split := pow.add at a, m * k, m78    rw split79    rfl8081theorem pow.double_exponent (a k : Nat)82  shows a ^ (2 * k) = (a ^ k) ^ 283proof84  have inner := pow.mul_exponent at a, k, 285  have shape : k * 2 = 2 * k by ring86  rw [inner, shape]87  rfl8889theorem pow.positive (a n : Nat)90  requires positive : 0 < a91  shows 0 < a ^ n92proof93  induction n94  | zero =>95    rw pow.zero96    linarith97  | succ(k) using ih =>98    have powNat := pow.closed at a, k99    rw pow.succ100    exact Less.mul_positive with positive, ih101102theorem pow.ne_zero (a n : Nat)103  requires nonzero : a ≠ 0104  shows a ^ n ≠ 0105proof106  have positive := Less.positive_of_ne_zero with nonzero107  have powPositive := pow.positive at a, n with positive108  exact Less.ne_zero_of_positive with powPositive109110theorem pow.eq_zero (a n : Nat)111  requires zero : a ^ n = 0112  shows a = 0113proof114  by_contra nonzero115  have excluded := pow.ne_zero at a, n with nonzero116  exact excluded with zero117118theorem pow.eq_zero_iff (a n : Nat)119  shows a ^ (n + 1) = 0 ↔ a = 0120proof121  constructor122  . intro zero123    exact pow.eq_zero with zero124  . intro zero125    rw zero126    exact pow.zero_left with *127128theorem pow.ge_one (a n : Nat)129  requires one : 1 ≤ a130  shows 1 ≤ a ^ n131proof132  induction n133  | zero =>134    rw pow.zero135    linarith136  | succ(k) using ih =>137    have powNat := pow.closed at a, k138    rw pow.succ139    exact LessEqual.one_le_mul with one, ih140141theorem pow.one_lt (a n : Nat)142  requires above : 1 < a143  shows 1 < a ^ (n + 1)144proof145  have powNat := pow.closed at a, n146  have one : 1 ≤ a by linarith147  have tail := pow.ge_one at a, n with one148  have bound := LessEqual.mul at 1, a, 1, a ^ n with one, tail149  rw pow.add_one150  have unit := mul.left_unit at 1151  rw unit at bound152  have strict : 1 < a * 1153    have unit2 := mul.right_unit at a154    rw unit2155    exact above156  have scaled := LessEqual.mul_left at 1, a ^ n, a with tail157  exact Less.transitive_LessEqual with strict, scaled158159theorem pow.base_monotone (a b n : Nat)160  requires below : a ≤ b161  shows a ^ n ≤ b ^ n162proof163  induction n164  | zero =>165    rw [pow.zero, pow.zero]166    exact LessEqual.reflexive with *167  | succ(k) using ih =>168    have aPow := pow.closed at a, k169    have bPow := pow.closed at b, k170    rw [pow.succ, pow.succ]171    exact LessEqual.mul with below, ih172173theorem pow.base_strict (a b n : Nat)174  requires below : a < b175  shows a ^ (n + 1) < b ^ (n + 1)176proof177  induction n178  | zero =>179    have shape : 0 + 1 = 1 by ring180    rw [shape, pow.one_right, pow.one_right]181    exact below182  | succ(k) using ih =>183    have aPow := pow.closed at a, k + 1184    have bPow := pow.closed at b, k + 1185    have leftShape : a ^ (succ(k) + 1) = a * a ^ (k + 1)186      have step : succ(k) + 1 = (k + 1) + 1 by ring187      rw step188      exact pow.add_one with *189    have rightShape : b ^ (succ(k) + 1) = b * b ^ (k + 1)190      have step : succ(k) + 1 = (k + 1) + 1 by ring191      rw step192      exact pow.add_one with *193    rw [leftShape, rightShape]194    exact Less.mul with below, ih195196theorem pow.two_monotone (a b : Nat)197  requires below : a ≤ b198  shows a ^ 2 ≤ b ^ 2199proof200  exact pow.base_monotone at a, b, 2 with below201202theorem pow.two_strict (a b : Nat)203  requires below : a < b204  shows a ^ 2 < b ^ 2205proof206  have strict := pow.base_strict at a, b, 1 with below207  have shape : 1 + 1 = 2 by ring208  rw shape at strict209  exact strict210211theorem pow.injective_base (a b n : Nat)212  requires same : a ^ (n + 1) = b ^ (n + 1)213  shows a = b214proof215  have comparison := Less.trichotomy at a, b with *216  rcases comparison with less | equal | greater217  . have strict := pow.base_strict at a, b, n with less218    rw same at strict219    exfalso220    exact Less.irreflexive with strict221  . exact equal222  . have strict := pow.base_strict at b, a, n with greater223    rw same at strict224    exfalso225    exact Less.irreflexive with strict226227theorem pow.exponent_monotone (a m n : Nat)228  requires one : 1 ≤ a229  requires below : m ≤ n230  shows a ^ m ≤ a ^ n231proof232  obtain ⟨k, kNat, equation⟩ := below233  have aPow := pow.closed at a, m234  have tailNonzero : a ^ k ≠ 0235    have nonzero := LessEqual.one_iff_ne_zero.forward with one236    exact pow.ne_zero at a, k with nonzero237  have split := pow.add at a, k, m238  rw ← equation239  rw split240  exact LessEqual.le_mul_right at a ^ m, a ^ k with tailNonzero241242theorem pow.exponent_strict (a m n : Nat)243  requires above : 1 < a244  requires below : m < n245  shows a ^ m < a ^ n246proof247  obtain ⟨k, kNat, equation⟩ := Less.exists_add_one with below248  have aPow := pow.closed at a, m249  have tail := pow.one_lt at a, k with above250  have headNonzero : a ^ m ≠ 0251    have one : 1 ≤ a by linarith252    have nonzero := LessEqual.one_iff_ne_zero.forward with one253    exact pow.ne_zero at a, m with nonzero254  have split := pow.add at a, k + 1, m255  have shape : m + k + 1 = m + (k + 1) by ring256  rw [equation, shape, split]257  have scaled := Less.mul_left at 1, a ^ (k + 1), a ^ m with headNonzero, tail258  have unit := mul.right_unit at a ^ m259  rw unit at scaled260  exact scaled261262theorem pow.injective_exponent (a m n : Nat)263  requires above : 1 < a264  requires same : a ^ m = a ^ n265  shows m = n266proof267  have comparison := Less.trichotomy at m, n with *268  rcases comparison with less | equal | greater269  . have strict := pow.exponent_strict at a, m, n with above, less270    rw same at strict271    exfalso272    exact Less.irreflexive with strict273  . exact equal274  . have strict := pow.exponent_strict at a, n, m with above, greater275    rw same at strict276    exfalso277    exact Less.irreflexive with strict278279theorem pow.le_self (a n : Nat)280  requires one : 1 ≤ a281  shows a ≤ a ^ (n + 1)282proof283  have bound : 1 ≤ n + 1 by linarith284  have monotone := pow.exponent_monotone at a, 1, n + 1 with one, bound285  rw pow.one_right at monotone286  exact monotone287288theorem pow.eq_one (a n : Nat)289  requires one : a ^ (n + 1) = 1290  shows a = 1291proof292  have powNat := pow.closed at a, n293  rw pow.add_one at one294  have both := mul.eq_one with one295  exact both.left296297theorem pow.two_succ (n : Nat)298  shows 2 ^ (n + 1) = 2 ^ n + 2 ^ n299proof300  have powNat := pow.closed at 2, n301  rw pow.add_one302  ring303304theorem pow.two_gt (n : Nat)305  shows n < 2 ^ n306proof307  induction n308  | zero =>309    rw pow.zero310    linarith311  | succ(k) using ih =>312    have powNat := pow.closed at 2, k313    have positive : 0 < 2 ^ k314      have two : 0 < 2 by linarith315      exact pow.positive at 2, k with two316    have doubled := pow.two_succ at k317    have shape : succ(k) = k + 1 by ring318    rw [shape, doubled]319    linarith320321theorem pow.add_one_le_two (n : Nat)322  shows n + 1 ≤ 2 ^ n323proof324  have powNat := pow.closed at 2, n325  have strict := pow.two_gt at n326  linarith327328theorem pow.two_add (a b : Nat)329  shows (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2330proof331  rw [pow.two, pow.two, pow.two]332  ring333