p : ℕ
h : 1 < p
n : ℕ
⊢ 1 / (-1) ^ ↑p * (1 / ↑n ^ ↑p) = 1 / ↑(-↑n) ^ ↑p
p : ℕ
⊢ (Summable fun n => 1 / ↑n ^ ↑p) ↔ 1 < p
refine'
  ⟨fun h => Real.summable_one_div_nat_pow.mp (h.comp_injective Nat.cast_injective), fun h =>
    summable_int_of_summable_nat (Real.summable_one_div_nat_pow.mpr h)
      (((Real.summable_one_div_nat_pow.mpr h).mul_left <| 1 / (-1 : ℝ) ^ p).congr fun n => _)⟩
p : ℕ
h : 1 < p
n : ℕ
⊢ 1 / (-1) ^ ↑p * (1 / ↑n ^ ↑p) = 1 / (-1) ^ p / ↑↑n ^ p
p : ℕ
h : 1 < p
n : ℕ
⊢ 1 / (-1) ^ ↑p * (1 / ↑n ^ ↑p) = 1 / ↑(-↑n) ^ ↑p
conv_rhs =>
  rw [Int.cast_neg, neg_eq_neg_one_mul, Real.rpow_nat_cast, mul_pow, ← div_div]
p : ℕ
h : 1 < p
n : ℕ
⊢ 1 / (-1) ^ ↑p / ↑n ^ ↑p = 1 / (-1) ^ p / ↑↑n ^ p
p : ℕ
h : 1 < p
n : ℕ
⊢ 1 / (-1) ^ ↑p * (1 / ↑n ^ ↑p) = 1 / (-1) ^ p / ↑↑n ^ p
conv_lhs => rw [mul_div, mul_one]
no goals
p : ℕ
h : 1 < p
n : ℕ
⊢ 1 / (-1) ^ ↑p / ↑n ^ ↑p = 1 / (-1) ^ p / ↑↑n ^ p
norm_cast