theorem Real.rpow_ne_one {a b : ℝ} (ha : 0 < a) (ha' : a ≠ 1) (hb : b ≠ 0) : a ^ b ≠ 1