apply ContinuousOn.rpow (by fun_prop) (by fun_prop)
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ContinuousOn (fun x => x ^ (r - 1)) (Ici ↑N)
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ∀ x ∈ Ici ↑N, x ≠ 0 ∨ 0 < r - 1