[GOAL]
p : ℕ
h : 1 < p
⊢ 0 < p ^ 0
[PROOFSTEP]
simp [zero_lt_one]
[GOAL]
n : ℕ
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
n m : ℕ
h : 0 < m
⊢ 1 ≤ m ^ n
[PROOFSTEP]
rw [← one_pow n]
[GOAL]
n m : ℕ
h : 0 < m
⊢ 1 ^ n ≤ m ^ n
[PROOFSTEP]
exact Nat.pow_le_pow_of_le_left h n
[GOAL]
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
n m : ℕ
h₀ : 0 < n
h₁ : 1 < m
⊢ 1 < m ^ n
[PROOFSTEP]
rw [← one_pow n]
[GOAL]
n m : ℕ
h₀ : 0 < n
h₁ : 1 < m
⊢ 1 ^ n < m ^ n
[PROOFSTEP]
exact pow_lt_pow_of_lt_left h₁ h₀
[GOAL]
k n : ℕ
h : 0 ≠ k
⊢ 1 < n ^ k ↔ 1 < n
[PROOFSTEP]
rcases n with (rfl | n)
[GOAL]
case zero
k : ℕ
h : 0 ≠ k
⊢ 1 < zero ^ k ↔ 1 < zero
[PROOFSTEP]
cases k
[GOAL]
case zero.zero
h : 0 ≠ zero
⊢ 1 < zero ^ zero ↔ 1 < zero
[PROOFSTEP]
simp [zero_pow_eq]
[GOAL]
case zero.succ
n✝ : ℕ
h : 0 ≠ succ n✝
⊢ 1 < zero ^ succ n✝ ↔ 1 < zero
[PROOFSTEP]
simp [zero_pow_eq]
[GOAL]
case succ
k : ℕ
h : 0 ≠ k
n : ℕ
⊢ 1 < succ n ^ k ↔ 1 < succ n
[PROOFSTEP]
rcases n with (rfl | n)
[GOAL]
case succ.zero
k : ℕ
h : 0 ≠ k
⊢ 1 < succ zero ^ k ↔ 1 < succ zero
[PROOFSTEP]
rw [← Nat.one_eq_succ_zero, one_pow]
[GOAL]
case succ.succ
k : ℕ
h : 0 ≠ k
n : ℕ
⊢ 1 < succ (succ n) ^ k ↔ 1 < succ (succ n)
[PROOFSTEP]
refine' ⟨fun _ => one_lt_succ_succ n, fun _ => _⟩
[GOAL]
case succ.succ
k : ℕ
h : 0 ≠ k
n : ℕ
x✝ : 1 < succ (succ n)
⊢ 1 < succ (succ n) ^ k
[PROOFSTEP]
induction' k with k hk
[GOAL]
case succ.succ.zero
k : ℕ
h✝ : 0 ≠ k
n : ℕ
x✝ : 1 < succ (succ n)
h : 0 ≠ zero
⊢ 1 < succ (succ n) ^ zero
[PROOFSTEP]
exact absurd rfl h
[GOAL]
case succ.succ.succ
k✝ : ℕ
h✝ : 0 ≠ k✝
n : ℕ
x✝ : 1 < succ (succ n)
k : ℕ
hk : 0 ≠ k → 1 < succ (succ n) ^ k
h : 0 ≠ succ k
⊢ 1 < succ (succ n) ^ succ k
[PROOFSTEP]
rcases k with (rfl | k)
[GOAL]
case succ.succ.succ.zero
k : ℕ
h✝ : 0 ≠ k
n : ℕ
x✝ : 1 < succ (succ n)
hk : 0 ≠ zero → 1 < succ (succ n) ^ zero
h : 0 ≠ succ zero
⊢ 1 < succ (succ n) ^ succ zero
[PROOFSTEP]
simp [← Nat.one_eq_succ_zero]
[GOAL]
case succ.succ.succ.succ
k✝ : ℕ
h✝ : 0 ≠ k✝
n : ℕ
x✝ : 1 < succ (succ n)
k : ℕ
hk : 0 ≠ succ k → 1 < succ (succ n) ^ succ k
h : 0 ≠ succ (succ k)
⊢ 1 < succ (succ n) ^ succ (succ k)
[PROOFSTEP]
rw [pow_succ']
[GOAL]
case succ.succ.succ.succ
k✝ : ℕ
h✝ : 0 ≠ k✝
n : ℕ
x✝ : 1 < succ (succ n)
k : ℕ
hk : 0 ≠ succ k → 1 < succ (succ n) ^ succ k
h : 0 ≠ succ (succ k)
⊢ 1 < succ (succ n) * succ (succ n) ^ (k + 1)
[PROOFSTEP]
exact one_lt_mul (one_lt_succ_succ _).le (hk (succ_ne_zero k).symm)
[GOAL]
n : ℕ
h₀ : 0 < n
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
n : ℕ
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
n a q : ℕ
a0 : 0 < a
q1 : 1 < q
⊢ n * q < a * q ^ (n + 1)
[PROOFSTEP]
rw [pow_succ, ← mul_assoc, mul_lt_mul_right (zero_lt_one.trans q1)]
[GOAL]
n a q : ℕ
a0 : 0 < a
q1 : 1 < q
⊢ n < a * q ^ n
[PROOFSTEP]
exact lt_mul_of_one_le_of_lt (Nat.succ_le_iff.mpr a0) (Nat.lt_pow_self q1 n)
[GOAL]
a b : ℕ
⊢ a ^ 2 - b ^ 2 = (a + b) * (a - b)
[PROOFSTEP]
rw [sq, sq]
[GOAL]
a b : ℕ
⊢ a * a - b * b = (a + b) * (a - b)
[PROOFSTEP]
exact Nat.mul_self_sub_mul_self_eq a b
[GOAL]
a b n : ℕ
⊢ a ^ b % n = (a % n) ^ b % n
[PROOFSTEP]
induction' b with b ih
[GOAL]
case zero
a n : ℕ
⊢ a ^ zero % n = (a % n) ^ zero % n
case succ a n b : ℕ ih : a ^ b % n = (a % n) ^ b % n ⊢ a ^ succ b % n = (a % n) ^ succ b % n
[PROOFSTEP]
rfl
[GOAL]
case succ
a n b : ℕ
ih : a ^ b % n = (a % n) ^ b % n
⊢ a ^ succ b % n = (a % n) ^ succ b % n
[PROOFSTEP]
simp [pow_succ, Nat.mul_mod, ih]
[GOAL]
b w m : ℕ
⊢ m % b ^ succ w = b * (m / b % b ^ w) + m % b
[PROOFSTEP]
by_cases b_h : b = 0
[GOAL]
case pos
b w m : ℕ
b_h : b = 0
⊢ m % b ^ succ w = b * (m / b % b ^ w) + m % b
[PROOFSTEP]
simp [b_h, pow_succ]
[GOAL]
case neg
b w m : ℕ
b_h : ¬b = 0
⊢ m % b ^ succ w = b * (m / b % b ^ w) + m % b
[PROOFSTEP]
have b_pos := Nat.pos_of_ne_zero b_h
[GOAL]
case neg
b w m : ℕ
b_h : ¬b = 0
b_pos : 0 < b
⊢ m % b ^ succ w = b * (m / b % b ^ w) + m % b
[PROOFSTEP]
induction m using Nat.strong_induction_on with
| h p IH =>
  cases' lt_or_ge p (b ^ succ w) with h₁ h₁
  ·
    -- base case: p < b^succ w
    have h₂ : p / b < b ^ w := by
      rw [div_lt_iff_lt_mul b_pos]
      simpa [pow_succ] using h₁
    rw [mod_eq_of_lt h₁, mod_eq_of_lt h₂]
    simp [div_add_mod]
  ·
    -- step: p ≥ b^succ w
            -- Generate condition for induction hypothesis
    have h₂ : p - b ^ succ w < p :=
      tsub_lt_self ((pow_pos b_pos _).trans_le h₁)
        (pow_pos b_pos _)
          -- Apply induction
    rw [mod_eq_sub_mod h₁, IH _ h₂]
      -- Normalize goal and h1
    simp only [pow_succ']
    simp only [GE.ge, pow_succ'] at h₁ 
    rw [sub_mul_mod h₁, sub_mul_div _ _ _ h₁]
      -- Cancel subtraction inside mod b^w
    have p_b_ge : b ^ w ≤ p / b := by
      rw [le_div_iff_mul_le b_pos, mul_comm]
      exact h₁
    rw [Eq.symm (mod_eq_sub_mod p_b_ge)]
[GOAL]
case neg
b w m : ℕ
b_h : ¬b = 0
b_pos : 0 < b
⊢ m % b ^ succ w = b * (m / b % b ^ w) + m % b
[PROOFSTEP]
induction m using Nat.strong_induction_on with
| h p IH =>
  cases' lt_or_ge p (b ^ succ w) with h₁ h₁
  ·
    -- base case: p < b^succ w
    have h₂ : p / b < b ^ w := by
      rw [div_lt_iff_lt_mul b_pos]
      simpa [pow_succ] using h₁
    rw [mod_eq_of_lt h₁, mod_eq_of_lt h₂]
    simp [div_add_mod]
  ·
    -- step: p ≥ b^succ w
            -- Generate condition for induction hypothesis
    have h₂ : p - b ^ succ w < p :=
      tsub_lt_self ((pow_pos b_pos _).trans_le h₁)
        (pow_pos b_pos _)
          -- Apply induction
    rw [mod_eq_sub_mod h₁, IH _ h₂]
      -- Normalize goal and h1
    simp only [pow_succ']
    simp only [GE.ge, pow_succ'] at h₁ 
    rw [sub_mul_mod h₁, sub_mul_div _ _ _ h₁]
      -- Cancel subtraction inside mod b^w
    have p_b_ge : b ^ w ≤ p / b := by
      rw [le_div_iff_mul_le b_pos, mul_comm]
      exact h₁
    rw [Eq.symm (mod_eq_sub_mod p_b_ge)]
[GOAL]
case neg.h
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
[PROOFSTEP]

| h p IH =>
  cases' lt_or_ge p (b ^ succ w) with h₁ h₁
  ·
    -- base case: p < b^succ w
    have h₂ : p / b < b ^ w := by
      rw [div_lt_iff_lt_mul b_pos]
      simpa [pow_succ] using h₁
    rw [mod_eq_of_lt h₁, mod_eq_of_lt h₂]
    simp [div_add_mod]
  ·
    -- step: p ≥ b^succ w
            -- Generate condition for induction hypothesis
    have h₂ : p - b ^ succ w < p :=
      tsub_lt_self ((pow_pos b_pos _).trans_le h₁)
        (pow_pos b_pos _)
          -- Apply induction
    rw [mod_eq_sub_mod h₁, IH _ h₂]
      -- Normalize goal and h1
    simp only [pow_succ']
    simp only [GE.ge, pow_succ'] at h₁ 
    rw [sub_mul_mod h₁, sub_mul_div _ _ _ h₁]
      -- Cancel subtraction inside mod b^w
    have p_b_ge : b ^ w ≤ p / b := by
      rw [le_div_iff_mul_le b_pos, mul_comm]
      exact h₁
    rw [Eq.symm (mod_eq_sub_mod p_b_ge)]
[GOAL]
case neg.h
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
cases' lt_or_ge p (b ^ succ w) with h₁ h₁
[GOAL]
case neg.h.inl
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
have h₂ : p / b < b ^ w := by
  rw [div_lt_iff_lt_mul b_pos]
  simpa [pow_succ] using h₁
[GOAL]
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
⊢ p / b < b ^ w
[PROOFSTEP]
rw [div_lt_iff_lt_mul b_pos]
[GOAL]
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
⊢ p < b ^ w * b
[PROOFSTEP]
simpa [pow_succ] using h₁
[GOAL]
case neg.h.inl
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
h₂ : p / b < b ^ w
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
rw [mod_eq_of_lt h₁, mod_eq_of_lt h₂]
[GOAL]
case neg.h.inl
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p < b ^ succ w
h₂ : p / b < b ^ w
⊢ p = b * (p / b) + p % b
[PROOFSTEP]
simp [div_add_mod]
[GOAL]
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p ≥ b ^ succ w
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
have h₂ : p - b ^ succ w < p :=
  tsub_lt_self ((pow_pos b_pos _).trans_le h₁)
    (pow_pos b_pos _)
      -- Apply induction
[GOAL]
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p ≥ b ^ succ w
h₂ : p - b ^ succ w < p
⊢ p % b ^ succ w = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
rw [mod_eq_sub_mod h₁, IH _ h₂]
  -- Normalize goal and h1
[GOAL]
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p ≥ b ^ succ w
h₂ : p - b ^ succ w < p
⊢ b * ((p - b ^ succ w) / b % b ^ w) + (p - b ^ succ w) % b = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
simp only [pow_succ']
[GOAL]
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₁ : p ≥ b ^ succ w
h₂ : p - b ^ succ w < p
⊢ b * ((p - b * b ^ w) / b % b ^ w) + (p - b * b ^ w) % b = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
simp only [GE.ge, pow_succ'] at h₁ 
[GOAL]
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
⊢ b * ((p - b * b ^ w) / b % b ^ w) + (p - b * b ^ w) % b = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
rw [sub_mul_mod h₁, sub_mul_div _ _ _ h₁]
  -- Cancel subtraction inside mod b^w
[GOAL]
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
⊢ b * ((p / b - b ^ w) % b ^ w) + p % b = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
have p_b_ge : b ^ w ≤ p / b := by
  rw [le_div_iff_mul_le b_pos, mul_comm]
  exact h₁
[GOAL]
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
⊢ b ^ w ≤ p / b
[PROOFSTEP]
rw [le_div_iff_mul_le b_pos, mul_comm]
[GOAL]
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
⊢ b * b ^ w ≤ p
[PROOFSTEP]
exact h₁
[GOAL]
case neg.h.inr
b w : ℕ
b_h : ¬b = 0
b_pos : 0 < b
p : ℕ
IH : ∀ (m : ℕ), m < p → m % b ^ succ w = b * (m / b % b ^ w) + m % b
h₂ : p - b ^ succ w < p
h₁ : b * b ^ w ≤ p
p_b_ge : b ^ w ≤ p / b
⊢ b * ((p / b - b ^ w) % b ^ w) + p % b = b * (p / b % b ^ w) + p % b
[PROOFSTEP]
rw [Eq.symm (mod_eq_sub_mod p_b_ge)]
[GOAL]
k l x : ℕ
w : 0 < x + 1
⊢ (x + 1) ^ k ∣ (x + 1) ^ l ↔ (x + 1) ^ k ≤ (x + 1) ^ l
[PROOFSTEP]
constructor
[GOAL]
case mp
k l x : ℕ
w : 0 < x + 1
⊢ (x + 1) ^ k ∣ (x + 1) ^ l → (x + 1) ^ k ≤ (x + 1) ^ l
[PROOFSTEP]
intro a
[GOAL]
case mp
k l x : ℕ
w : 0 < x + 1
a : (x + 1) ^ k ∣ (x + 1) ^ l
⊢ (x + 1) ^ k ≤ (x + 1) ^ l
[PROOFSTEP]
exact le_of_dvd (pow_pos (succ_pos x) l) a
[GOAL]
case mpr
k l x : ℕ
w : 0 < x + 1
⊢ (x + 1) ^ k ≤ (x + 1) ^ l → (x + 1) ^ k ∣ (x + 1) ^ l
[PROOFSTEP]
intro a
[GOAL]
case mpr
k l x : ℕ
w : 0 < x + 1
a : (x + 1) ^ k ≤ (x + 1) ^ l
⊢ (x + 1) ^ k ∣ (x + 1) ^ l
[PROOFSTEP]
cases' x with x
[GOAL]
case mpr.zero
k l : ℕ
w : 0 < zero + 1
a : (zero + 1) ^ k ≤ (zero + 1) ^ l
⊢ (zero + 1) ^ k ∣ (zero + 1) ^ l
[PROOFSTEP]
simp
[GOAL]
case mpr.succ
k l x : ℕ
w : 0 < succ x + 1
a : (succ x + 1) ^ k ≤ (succ x + 1) ^ l
⊢ (succ x + 1) ^ k ∣ (succ x + 1) ^ l
[PROOFSTEP]
have le := (pow_le_iff_le_right (Nat.le_add_left _ _)).mp a
[GOAL]
case mpr.succ
k l x : ℕ
w : 0 < succ x + 1
a : (succ x + 1) ^ k ≤ (succ x + 1) ^ l
le : k ≤ l
⊢ (succ x + 1) ^ k ∣ (succ x + 1) ^ l
[PROOFSTEP]
use(x + 2) ^ (l - k)
[GOAL]
case h
k l x : ℕ
w : 0 < succ x + 1
a : (succ x + 1) ^ k ≤ (succ x + 1) ^ l
le : k ≤ l
⊢ (succ x + 1) ^ l = (succ x + 1) ^ k * (x + 2) ^ (l - k)
[PROOFSTEP]
rw [← pow_add, add_comm k, tsub_add_cancel_of_le le]
[GOAL]
x k l : ℕ
w : 1 < x
⊢ x ^ k ∣ x ^ l ↔ k ≤ l
[PROOFSTEP]
rw [pow_dvd_pow_iff_pow_le_pow (lt_of_succ_lt w), pow_le_iff_le_right w]
[GOAL]
p k : ℕ
hp : 1 < succ p
hk : 1 < succ k
h : succ p ^ succ k ∣ succ p
⊢ succ p * succ p ^ k ∣ succ p * 1
[PROOFSTEP]
simpa [pow_succ'] using h
[GOAL]
p k : ℕ
hp : 1 < succ p
hk : 1 < succ k
h : succ p ^ succ k ∣ succ p
this✝¹ : succ p * succ p ^ k ∣ succ p * 1
this✝ : succ p ^ k ∣ 1
he : succ p ^ k = 1
this : k < succ p ^ k
⊢ k < 1
[PROOFSTEP]
rwa [he] at this 
[GOAL]
p k : ℕ
hp : 1 < succ p
hk : 1 < succ k
h : succ p ^ succ k ∣ succ p
this✝³ : succ p * succ p ^ k ∣ succ p * 1
this✝² : succ p ^ k ∣ 1
he : succ p ^ k = 1
this✝¹ : k < succ p ^ k
this✝ : k < 1
this : k = 0
⊢ 1 < 1
[PROOFSTEP]
rwa [this] at hk 
[GOAL]
p k : ℕ
hp : 1 < succ p
hk : 1 < succ k
h : succ p ^ succ k ∣ succ p
this✝⁴ : succ p * succ p ^ k ∣ succ p * 1
this✝³ : succ p ^ k ∣ 1
he : succ p ^ k = 1
this✝² : k < succ p ^ k
this✝¹ : k < 1
this✝ : k = 0
this : 1 < 1
⊢ ¬1 < 1
[PROOFSTEP]
decide
[GOAL]
p k m : ℕ
hk : 1 ≤ k
hpk : p ^ k ∣ m
⊢ p ∣ m
[PROOFSTEP]
rw [← pow_one p]
[GOAL]
p k m : ℕ
hk : 1 ≤ k
hpk : p ^ k ∣ m
⊢ p ^ 1 ∣ m
[PROOFSTEP]
exact pow_dvd_of_le_of_pow_dvd hk hpk
[GOAL]
x m n : ℕ
h : n ≤ m
hx : 0 < x
⊢ x ^ m / x ^ n = x ^ (m - n)
[PROOFSTEP]
rw [Nat.div_eq_iff_eq_mul_left (pow_pos hx n) (pow_dvd_pow _ h), pow_sub_mul_pow _ h]
[GOAL]
p i n : ℕ
hn : n ≠ 0
hp : 2 ≤ p
h : p ^ i ∣ n
⊢ i < n
[PROOFSTEP]
rw [← pow_lt_iff_lt_right hp]
[GOAL]
p i n : ℕ
hn : n ≠ 0
hp : 2 ≤ p
h : p ^ i ∣ n
⊢ p ^ i < p ^ n
[PROOFSTEP]
exact lt_of_le_of_lt (le_of_dvd hn.bot_lt h) (lt_pow_self (succ_le_iff.mp hp) n)
