R : Type ?u.860418
n✝ : ℕ
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
⊢ multiplicity 2 (x ^ n - y ^ n) = multiplicity 2 (x - y) + multiplicity 2 ↑n
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
⊢ multiplicity 2 (x ^ n - y ^ n) = multiplicity 2 (x - y) + multiplicity 2 ↑n
have hx_odd : Odd x := by rwa [Int.odd_iff_not_even, even_iff_two_dvd]
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
⊢ multiplicity 2 (x ^ n - y ^ n) = multiplicity 2 (x - y) + multiplicity 2 ↑n
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
⊢ multiplicity 2 (x ^ n - y ^ n) = multiplicity 2 (x - y) + multiplicity 2 ↑n
have hxy_even : Even (x - y) := even_iff_two_dvd.mpr (dvd_trans (by norm_num) hxy)
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ multiplicity 2 (x ^ n - y ^ n) = multiplicity 2 (x - y) + multiplicity 2 ↑n
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
⊢ multiplicity 2 (x ^ n - y ^ n) = multiplicity 2 (x - y) + multiplicity 2 ↑n
have hy_odd : Odd y := by simpa using hx_odd.sub_even hxy_even
case zero
R : Type ?u.860418
n : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ multiplicity 2 (x ^ Nat.zero - y ^ Nat.zero) = multiplicity 2 (x - y) + multiplicity 2 ↑Nat.zero

case succ
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
⊢ multiplicity 2 (x ^ Nat.succ n - y ^ Nat.succ n) = multiplicity 2 (x - y) + multiplicity 2 ↑(Nat.succ n)
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ multiplicity 2 (x ^ n - y ^ n) = multiplicity 2 (x - y) + multiplicity 2 ↑n
cases' n with n
case succ
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
⊢ multiplicity 2 (x ^ Nat.succ n - y ^ Nat.succ n) = multiplicity 2 (x - y) + multiplicity 2 ↑(Nat.succ n)
case succ
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
⊢ multiplicity 2 (x ^ Nat.succ n - y ^ Nat.succ n) = multiplicity 2 (x - y) + multiplicity 2 ↑(Nat.succ n)
have h : (multiplicity 2 n.succ).Dom := multiplicity.finite_nat_iff.mpr ⟨by norm_num, n.succ_pos⟩
case succ.intro.intro
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
hpn : ¬2 ^ (Part.get (multiplicity 2 (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
⊢ multiplicity 2 (x ^ Nat.succ n - y ^ Nat.succ n) = multiplicity 2 (x - y) + multiplicity 2 ↑(Nat.succ n)
case succ
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
⊢ multiplicity 2 (x ^ Nat.succ n - y ^ Nat.succ n) = multiplicity 2 (x - y) + multiplicity 2 ↑(Nat.succ n)
rcases multiplicity.eq_coe_iff.mp (PartENat.natCast_get h).symm with ⟨⟨k, hk⟩, hpn⟩
case succ.intro.intro
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
hpn : ¬2 ^ (Part.get (multiplicity 2 (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
⊢ multiplicity 2 (x - y) + multiplicity 2 (Nat.succ n) = multiplicity 2 (x - y) + multiplicity 2 ↑(Nat.succ n)

case succ.intro.intro.hp
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
hpn : ¬2 ^ (Part.get (multiplicity 2 (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
⊢ Prime 2

case succ.intro.intro.hxy
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
hpn : ¬2 ^ (Part.get (multiplicity 2 (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
⊢ 2 ∣ x ^ 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h - y ^ 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h

case succ.intro.intro.hx
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
hpn : ¬2 ^ (Part.get (multiplicity 2 (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
⊢ ¬2 ∣ x ^ 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h

case succ.intro.intro.hn
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
hpn : ¬2 ^ (Part.get (multiplicity 2 (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
⊢ ¬2 ∣ ↑k
case succ.intro.intro
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
hpn : ¬2 ^ (Part.get (multiplicity 2 (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
⊢ multiplicity 2 (x ^ Nat.succ n - y ^ Nat.succ n) = multiplicity 2 (x - y) + multiplicity 2 ↑(Nat.succ n)
rw [hk, pow_mul, pow_mul, multiplicity.pow_sub_pow_of_prime,
  Int.two_pow_two_pow_sub_pow_two_pow _ hxy hx, ← hk, PartENat.natCast_get]
case succ.intro.intro.hn
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
hpn : ¬2 ^ (Part.get (multiplicity 2 (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
⊢ ¬2 ∣ k
case succ.intro.intro.hn
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
hpn : ¬2 ^ (Part.get (multiplicity 2 (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
⊢ ¬2 ∣ ↑k
erw [Int.coe_nat_dvd]
case succ.intro.intro.hn
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
hpn : 2 ∣ k
⊢ 2 ^ (Part.get (multiplicity 2 (Nat.succ n)) h + 1) ∣ Nat.succ n
case succ.intro.intro.hn
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
hpn : ¬2 ^ (Part.get (multiplicity 2 (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
⊢ ¬2 ∣ k
contrapose! hpn
case succ.intro.intro.hn
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
hpn : 2 ∣ k
⊢ 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * 2 ∣ Nat.succ n
case succ.intro.intro.hn
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
hpn : 2 ∣ k
⊢ 2 ^ (Part.get (multiplicity 2 (Nat.succ n)) h + 1) ∣ Nat.succ n
rw [pow_succ']
case succ.intro.intro.hn
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
hpn : 2 ∣ k
⊢ 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * 2 ∣ 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
case succ.intro.intro.hn
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
hpn : 2 ∣ k
⊢ 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * 2 ∣ Nat.succ n
conv_rhs => rw [hk]
no goals
case succ.intro.intro.hn
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
hpn : 2 ∣ k
⊢ 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * 2 ∣ 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
exact mul_dvd_mul_left _ hpn
no goals
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
⊢ Odd x
rwa [Int.odd_iff_not_even, even_iff_two_dvd]
no goals
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
⊢ 2 ∣ 4
norm_num
no goals
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
⊢ Odd y
simpa using hx_odd.sub_even hxy_even
no goals
case zero
R : Type ?u.860418
n : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ multiplicity 2 (x ^ Nat.zero - y ^ Nat.zero) = multiplicity 2 (x - y) + multiplicity 2 ↑Nat.zero
simp only [pow_zero, sub_self, multiplicity.zero, Int.ofNat_zero, Nat.zero_eq, add_top]
no goals
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
⊢ 2 ≠ 1
norm_num
no goals
case succ.intro.intro
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
hpn : ¬2 ^ (Part.get (multiplicity 2 (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
⊢ multiplicity 2 (x - y) + multiplicity 2 (Nat.succ n) = multiplicity 2 (x - y) + multiplicity 2 ↑(Nat.succ n)
norm_cast
no goals
case succ.intro.intro.hp
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
hpn : ¬2 ^ (Part.get (multiplicity 2 (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
⊢ Prime 2
exact Int.prime_two
no goals
case succ.intro.intro.hxy
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
hpn : ¬2 ^ (Part.get (multiplicity 2 (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
⊢ 2 ∣ x ^ 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h - y ^ 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h
simpa only [even_iff_two_dvd] using hx_odd.pow.sub_odd hy_odd.pow
no goals
case succ.intro.intro.hx
R : Type ?u.860418
n✝ : ℕ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : (multiplicity 2 (Nat.succ n)).Dom
hpn : ¬2 ^ (Part.get (multiplicity 2 (Nat.succ n)) h + 1) ∣ Nat.succ n
k : ℕ
hk : Nat.succ n = 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h * k
⊢ ¬2 ∣ x ^ 2 ^ Part.get (multiplicity 2 (Nat.succ n)) h
simpa only [even_iff_two_dvd, Int.odd_iff_not_even] using hx_odd.pow