a b : ℝ
h : b ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (rpow a) b
a b : ℝ
h : b ≠ 0
⊢ ContinuousAt (rpow a) b
have : rpow a = fun x : ℝ => ((a : ℂ) ^ (x : ℂ)).re := by
  ext1 x
  rw [rpow_eq_pow, rpow_def]
a b : ℝ
h : b ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (fun x => (↑a ^ ↑x).re) b
a b : ℝ
h : b ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (rpow a) b
rw [this]
a b : ℝ
h : b ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (fun x => ↑a ^ ↑x) b
a b : ℝ
h : b ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (fun x => (↑a ^ ↑x).re) b
refine' Complex.continuous_re.continuousAt.comp _
a b : ℝ
h : b ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ↑b ≠ 0
a b : ℝ
h : b ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ContinuousAt (fun x => ↑a ^ ↑x) b
refine' (continuousAt_const_cpow' _).comp Complex.continuous_ofReal.continuousAt
no goals
a b : ℝ
h : b ≠ 0
this : rpow a = fun x => (↑a ^ ↑x).re
⊢ ↑b ≠ 0
norm_cast
case h
a b : ℝ
h : b ≠ 0
x : ℝ
⊢ rpow a x = (↑a ^ ↑x).re
a b : ℝ
h : b ≠ 0
⊢ rpow a = fun x => (↑a ^ ↑x).re
ext1 x
no goals
case h
a b : ℝ
h : b ≠ 0
x : ℝ
⊢ rpow a x = (↑a ^ ↑x).re
rw [rpow_eq_pow, rpow_def]