R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ ↑(padicValNat p (x ^ n - y ^ n)) = ↑(padicValNat p (x - y)) + ↑(padicValNat p n)
R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ padicValNat p (x ^ n - y ^ n) = padicValNat p (x - y) + padicValNat p n
rw [← PartENat.natCast_inj, Nat.cast_add]
R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y) + multiplicity p n

R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < n

R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < n

R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < x - y

R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < x - y

R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < x ^ n - y ^ n

R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < x ^ n - y ^ n
R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ ↑(padicValNat p (x ^ n - y ^ n)) = ↑(padicValNat p (x - y)) + ↑(padicValNat p n)
iterate 3 rw [padicValNat_def, PartENat.natCast_get]
R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y) + multiplicity p n

R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < n

R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < n

R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < x - y

R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < x - y

R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < x ^ n - y ^ n

R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < x ^ n - y ^ n
R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y) + ↑(padicValNat p n)

R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < x - y

R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < x - y

R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < x ^ n - y ^ n

R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < x ^ n - y ^ n
rw [padicValNat_def, PartENat.natCast_get]
no goals
R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y) + multiplicity p n
exact multiplicity.Nat.pow_sub_pow hp.out hp1 hxy hx n
no goals
R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < n
exact hn
no goals
R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < x - y
exact Nat.sub_pos_of_lt hyx
no goals
R : Type ?u.882286
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : 0 < n
⊢ 0 < x ^ n - y ^ n
exact Nat.sub_pos_of_lt (Nat.pow_lt_pow_of_lt_left hyx hn)