case zero
R : Type ?u.883070
n✝ x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
hxy : p ∣ x + Nat.zero
⊢ padicValNat p (x ^ n + Nat.zero ^ n) = padicValNat p (x + Nat.zero) + padicValNat p n

case succ
R : Type ?u.883070
n✝ x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + Nat.succ y
⊢ padicValNat p (x ^ n + Nat.succ y ^ n) = padicValNat p (x + Nat.succ y) + padicValNat p n
R : Type ?u.883070
n✝ x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ padicValNat p (x ^ n + y ^ n) = padicValNat p (x + y) + padicValNat p n
cases' y with y
case succ
R : Type ?u.883070
n✝ x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + Nat.succ y
⊢ ↑(padicValNat p (x ^ n + Nat.succ y ^ n)) = ↑(padicValNat p (x + Nat.succ y)) + ↑(padicValNat p n)
case succ
R : Type ?u.883070
n✝ x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + Nat.succ y
⊢ padicValNat p (x ^ n + Nat.succ y ^ n) = padicValNat p (x + Nat.succ y) + padicValNat p n
rw [← PartENat.natCast_inj, Nat.cast_add]
case succ
R : Type ?u.883070
n✝ x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + Nat.succ y
⊢ multiplicity p (x ^ n + Nat.succ y ^ n) = multiplicity p (x + Nat.succ y) + multiplicity p n

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

case succ
R : Type ?u.883070
n✝ x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + Nat.succ y
⊢ 0 < x ^ n + Nat.succ y ^ n
rw [padicValNat_def, PartENat.natCast_get]
no goals
case succ
R : Type ?u.883070
n✝ x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + Nat.succ y
⊢ multiplicity p (x ^ n + Nat.succ y ^ n) = multiplicity p (x + Nat.succ y) + multiplicity p n
exact multiplicity.Nat.pow_add_pow hp.out hp1 hxy hx hn
no goals
case succ
R : Type ?u.883070
n✝ x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + Nat.succ y
⊢ 0 < n
exact Odd.pos hn
no goals
case succ
R : Type ?u.883070
n✝ x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + Nat.succ y
⊢ 0 < x + Nat.succ y
simp only [add_pos_iff, Nat.succ_pos', or_true_iff]
no goals
case succ
R : Type ?u.883070
n✝ x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + Nat.succ y
⊢ 0 < x ^ n + Nat.succ y ^ n
exact Nat.lt_add_left _ _ _ (pow_pos y.succ_pos _)