case inl
R : Type ?u.838285
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y) + multiplicity p n

case inr
R : Type ?u.838285
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : x ≤ y
⊢ multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y) + multiplicity p n
R : Type ?u.838285
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
⊢ multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y) + multiplicity p n
obtain hyx | hyx := le_total y x
case inl
R : Type ?u.838285
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ multiplicity ↑p ↑(x ^ n - y ^ n) = multiplicity ↑p ↑(x - y) + multiplicity p n
case inl
R : Type ?u.838285
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y) + multiplicity p n
iterate 2 rw [← Int.coe_nat_multiplicity]
case inl
R : Type ?u.838285
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ multiplicity (↑p) (↑(x ^ n) - ↑(y ^ n)) = multiplicity ↑p ↑(x - y) + multiplicity p n
case inl
R : Type ?u.838285
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ multiplicity ↑p ↑(x ^ n - y ^ n) = multiplicity ↑p ↑(x - y) + multiplicity p n
rw [Int.ofNat_sub (Nat.pow_le_pow_of_le_left hyx n)]
case inl
R : Type ?u.838285
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : ↑p ∣ ↑(x - y)
hx : ¬↑p ∣ ↑x
n : ℕ
hyx : y ≤ x
⊢ multiplicity (↑p) (↑(x ^ n) - ↑(y ^ n)) = multiplicity ↑p ↑(x - y) + multiplicity p n
case inl
R : Type ?u.838285
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ multiplicity (↑p) (↑(x ^ n) - ↑(y ^ n)) = multiplicity ↑p ↑(x - y) + multiplicity p n
rw [← Int.coe_nat_dvd] at hxy hx
case inl
R : Type ?u.838285
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : ↑p ∣ ↑x - ↑y
hx : ¬↑p ∣ ↑x
n : ℕ
hyx : y ≤ x
⊢ multiplicity (↑p) (↑(x ^ n) - ↑(y ^ n)) = multiplicity (↑p) (↑x - ↑y) + multiplicity p n
case inl
R : Type ?u.838285
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : ↑p ∣ ↑(x - y)
hx : ¬↑p ∣ ↑x
n : ℕ
hyx : y ≤ x
⊢ multiplicity (↑p) (↑(x ^ n) - ↑(y ^ n)) = multiplicity ↑p ↑(x - y) + multiplicity p n
rw [Int.coe_nat_sub hyx] at *
case inl
R : Type ?u.838285
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : ↑p ∣ ↑x - ↑y
hx : ¬↑p ∣ ↑x
n : ℕ
hyx : y ≤ x
⊢ multiplicity (↑p) (↑x ^ n - ↑y ^ n) = multiplicity (↑p) (↑x - ↑y) + multiplicity p n
case inl
R : Type ?u.838285
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : ↑p ∣ ↑x - ↑y
hx : ¬↑p ∣ ↑x
n : ℕ
hyx : y ≤ x
⊢ multiplicity (↑p) (↑(x ^ n) - ↑(y ^ n)) = multiplicity (↑p) (↑x - ↑y) + multiplicity p n
push_cast at *
no goals
case inl
R : Type ?u.838285
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : ↑p ∣ ↑x - ↑y
hx : ¬↑p ∣ ↑x
n : ℕ
hyx : y ≤ x
⊢ multiplicity (↑p) (↑x ^ n - ↑y ^ n) = multiplicity (↑p) (↑x - ↑y) + multiplicity p n
exact Int.pow_sub_pow hp hp1 hxy hx n
case inl
R : Type ?u.838285
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ multiplicity ↑p ↑(x ^ n - y ^ n) = multiplicity ↑p ↑(x - y) + multiplicity p n
case inl
R : Type ?u.838285
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ multiplicity ↑p ↑(x ^ n - y ^ n) = multiplicity p (x - y) + multiplicity p n
rw [← Int.coe_nat_multiplicity]
no goals
case inr
R : Type ?u.838285
n✝ : ℕ
inst✝ : CommRing R
a b x✝ y✝ : R
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : x ≤ y
⊢ multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y) + multiplicity p n
simp only [Nat.sub_eq_zero_iff_le.mpr hyx,
  Nat.sub_eq_zero_iff_le.mpr (Nat.pow_le_pow_of_le_left hyx n), multiplicity.zero,
  PartENat.top_add]