[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
n : ℕ
x✝ : 0 < n + 1
⊢ 0 ^ (n + 1) = 0
[PROOFSTEP]
rw [pow_succ, zero_mul]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
k : ℕ
x✝ : k + 1 ≠ 0
⊢ 0 ^ (k + 1) = 0
[PROOFSTEP]
rw [pow_succ]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
k : ℕ
x✝ : k + 1 ≠ 0
⊢ 0 * 0 ^ k = 0
[PROOFSTEP]
exact zero_mul _
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
n : ℕ
⊢ 0 ^ n = if n = 0 then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
n : ℕ
h : n = 0
⊢ 0 ^ n = 1
[PROOFSTEP]
rw [h, pow_zero]
[GOAL]
case neg
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
n : ℕ
h : ¬n = 0
⊢ 0 ^ n = 0
[PROOFSTEP]
rw [zero_pow (Nat.pos_of_ne_zero h)]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
x : M
n m : ℕ
hn : n ≤ m
hx : x ^ n = 0
⊢ x ^ m = 0
[PROOFSTEP]
rw [← tsub_add_cancel_of_le hn, pow_add, hx, mul_zero]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n : ℕ
H : x ^ n = 0
⊢ x = 0
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n : ℕ
H✝ : x ^ n = 0
H : x ^ Nat.zero = 0
⊢ x = 0
[PROOFSTEP]
rw [pow_zero] at H 
[GOAL]
case zero
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n : ℕ
H✝ : x ^ n = 0
H : 1 = 0
⊢ x = 0
[PROOFSTEP]
rw [← mul_one x, H, mul_zero]
[GOAL]
case succ
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n✝ : ℕ
H✝ : x ^ n✝ = 0
n : ℕ
ih : x ^ n = 0 → x = 0
H : x ^ Nat.succ n = 0
⊢ x = 0
[PROOFSTEP]
rw [pow_succ] at H 
[GOAL]
case succ
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
x : M
n✝ : ℕ
H✝ : x ^ n✝ = 0
n : ℕ
ih : x ^ n = 0 → x = 0
H : x * x ^ n = 0
⊢ x = 0
[PROOFSTEP]
exact Or.casesOn (mul_eq_zero.1 H) id ih
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
a : M
n : ℕ
hn : 0 < n
⊢ a ^ n = 0 ↔ a = 0
[PROOFSTEP]
refine' ⟨pow_eq_zero, _⟩
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
a : M
n : ℕ
hn : 0 < n
⊢ a = 0 → a ^ n = 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : NoZeroDivisors M
n : ℕ
hn : 0 < n
⊢ 0 ^ n = 0
[PROOFSTEP]
exact zero_pow hn
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝² : MonoidWithZero M
inst✝¹ : NoZeroDivisors M
inst✝ : Nontrivial M
a : M
n : ℕ
⊢ a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
[PROOFSTEP]
cases (zero_le n).eq_or_gt
[GOAL]
case inl
R : Type u_1
S : Type u_2
M : Type u_3
inst✝² : MonoidWithZero M
inst✝¹ : NoZeroDivisors M
inst✝ : Nontrivial M
a : M
n : ℕ
h✝ : n = 0
⊢ a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
[PROOFSTEP]
simp [*, ne_of_gt]
[GOAL]
case inr
R : Type u_1
S : Type u_2
M : Type u_3
inst✝² : MonoidWithZero M
inst✝¹ : NoZeroDivisors M
inst✝ : Nontrivial M
a : M
n : ℕ
h✝ : 0 < n
⊢ a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
[PROOFSTEP]
simp [*, ne_of_gt]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
a : M
n : ℕ
hn : n ≠ 0
⊢ a ^ n ≠ 0 → a ≠ 0
[PROOFSTEP]
contrapose!
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
a : M
n : ℕ
hn : n ≠ 0
⊢ a = 0 → a ^ n = 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
n : ℕ
hn : n ≠ 0
⊢ 0 ^ n = 0
[PROOFSTEP]
exact zero_pow' n hn
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
⊢ 0 ^ n = 0 ↔ 0 < n
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
⊢ 0 ^ n = 0 → 0 < n
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
⊢ 0 < n → 0 ^ n = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
h : 0 ^ n = 0
⊢ 0 < n
[PROOFSTEP]
rw [pos_iff_ne_zero]
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
h : 0 ^ n = 0
⊢ n ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
h : 0 ^ 0 = 0
⊢ False
[PROOFSTEP]
simp at h 
[GOAL]
case mpr
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : MonoidWithZero M
inst✝ : Nontrivial M
n : ℕ
h : 0 < n
⊢ 0 ^ n = 0
[PROOFSTEP]
exact zero_pow' n h.ne.symm
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
r : M
⊢ inverse r ^ 0 = inverse (r ^ 0)
[PROOFSTEP]
rw [pow_zero, pow_zero, Ring.inverse_one]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : MonoidWithZero M
r : M
n : ℕ
⊢ inverse r ^ (n + 1) = inverse (r ^ (n + 1))
[PROOFSTEP]
rw [pow_succ, pow_succ', Ring.mul_inverse_rev' ((Commute.refl r).pow_left n), Ring.inverse_pow r n]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
⊢ x ^ n ∣ x ^ m ↔ n ≤ m
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
⊢ x ^ n ∣ x ^ m → n ≤ m
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
⊢ n ≤ m
[PROOFSTEP]
rw [← not_lt]
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
⊢ ¬m < n
[PROOFSTEP]
intro hmn
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
⊢ False
[PROOFSTEP]
apply h1
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
⊢ IsUnit x
[PROOFSTEP]
have : x ^ m * x ∣ x ^ m * 1 := by
  rw [← pow_succ', mul_one]
  exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
⊢ x ^ m * x ∣ x ^ m * 1
[PROOFSTEP]
rw [← pow_succ', mul_one]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
⊢ x ^ (m + 1) ∣ x ^ m
[PROOFSTEP]
exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
this : x ^ m * x ∣ x ^ m * 1
⊢ IsUnit x
[PROOFSTEP]
rwa [mul_dvd_mul_iff_left, ← isUnit_iff_dvd_one] at this 
[GOAL]
case mp
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
h : x ^ n ∣ x ^ m
hmn : m < n
this : x ^ m * x ∣ x ^ m * 1
⊢ x ^ m ≠ 0
[PROOFSTEP]
apply pow_ne_zero m h0
[GOAL]
case mpr
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CancelCommMonoidWithZero R
x : R
n m : ℕ
h0 : x ≠ 0
h1 : ¬IsUnit x
⊢ n ≤ m → x ^ n ∣ x ^ m
[PROOFSTEP]
apply pow_dvd_pow
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
n m : ℕ
a b c : R
ha : c ^ n ∣ a
hb : c ^ m ∣ b
⊢ c ^ min n m ∣ a + b
[PROOFSTEP]
replace ha := (pow_dvd_pow c (min_le_left n m)).trans ha
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
n m : ℕ
a b c : R
hb : c ^ m ∣ b
ha : c ^ min n m ∣ a
⊢ c ^ min n m ∣ a + b
[PROOFSTEP]
replace hb := (pow_dvd_pow c (min_le_right n m)).trans hb
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
n m : ℕ
a b c : R
ha : c ^ min n m ∣ a
hb : c ^ min n m ∣ b
⊢ c ^ min n m ∣ a + b
[PROOFSTEP]
exact dvd_add ha hb
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CommSemiring R
a b : R
⊢ (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
[PROOFSTEP]
simp only [sq, add_mul_self_eq]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CommSemiring R
a b : R
⊢ (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2 * a * b
[PROOFSTEP]
rw [add_sq, add_assoc, add_comm _ (b ^ 2), add_assoc]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = -1
⊢ (-1) ^ (n + 1) = 1
[PROOFSTEP]
rw [pow_succ, h, neg_one_mul, neg_neg]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = 1
⊢ (-1) ^ (n + 1) = -1
[PROOFSTEP]
rw [pow_succ, h, mul_one]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
a : R
n : ℕ
⊢ (-a) ^ bit0 n = a ^ bit0 n
[PROOFSTEP]
rw [pow_bit0', neg_mul_neg, pow_bit0']
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
a : R
n : ℕ
⊢ (-a) ^ bit1 n = -a ^ bit1 n
[PROOFSTEP]
simp only [bit1, pow_succ, neg_pow_bit0, neg_mul_eq_neg_mul]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
a : R
⊢ (-a) ^ 2 = a ^ 2
[PROOFSTEP]
simp [sq]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
⊢ (-1) ^ 2 = 1
[PROOFSTEP]
simp [neg_sq, one_pow]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : Ring R
a b : R
h : Commute a b
⊢ a ^ 2 - b ^ 2 = (a + b) * (a - b)
[PROOFSTEP]
rw [sq, sq, h.mul_self_sub_mul_self_eq]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : Ring R
a b : R
n : ℕ
r : R
⊢ (-1) ^ n * r = 0 ↔ r = 0
[PROOFSTEP]
rcases neg_one_pow_eq_or R n with h | h
[GOAL]
case inl
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : Ring R
a b : R
n : ℕ
r : R
h : (-1) ^ n = 1
⊢ (-1) ^ n * r = 0 ↔ r = 0
[PROOFSTEP]
simp [h]
[GOAL]
case inr
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : Ring R
a b : R
n : ℕ
r : R
h : (-1) ^ n = -1
⊢ (-1) ^ n * r = 0 ↔ r = 0
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : Ring R
a b : R
n : ℕ
r : R
⊢ r * (-1) ^ n = 0 ↔ r = 0
[PROOFSTEP]
rcases neg_one_pow_eq_or R n with h | h
[GOAL]
case inl
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : Ring R
a b : R
n : ℕ
r : R
h : (-1) ^ n = 1
⊢ r * (-1) ^ n = 0 ↔ r = 0
[PROOFSTEP]
simp [h]
[GOAL]
case inr
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : Ring R
a b : R
n : ℕ
r : R
h : (-1) ^ n = -1
⊢ r * (-1) ^ n = 0 ↔ r = 0
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Ring R
a b : R
inst✝ : NoZeroDivisors R
h : Commute a b
⊢ a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
[PROOFSTEP]
rw [← sub_eq_zero, h.sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg, sub_eq_zero, or_comm]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : Ring R
a b : R
inst✝ : NoZeroDivisors R
⊢ a ^ 2 = 1 ↔ a = 1 ∨ a = -1
[PROOFSTEP]
rw [← (Commute.one_right a).sq_eq_sq_iff_eq_or_eq_neg, one_pow]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CommRing R
a b : R
⊢ (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2
[PROOFSTEP]
rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝ : CommRing R
a b : R
⊢ (a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b
[PROOFSTEP]
rw [sub_eq_add_neg, add_sq', neg_sq, mul_neg, ← sub_eq_add_neg]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a✝ b✝ : R
a b : Rˣ
⊢ a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
[PROOFSTEP]
simp_rw [ext_iff, val_pow_eq_pow_val, sq_eq_sq_iff_eq_or_eq_neg, Units.val_neg]
