Need help on Casting proof in Exponents

Stream: new members

[Colin Jones ⚛️]

Can someone help me prove this:

example (x : ℝ) : 1 / x ^ 10 = x ^ (-(10:ℝ)) := by
  ring_nf
  simp only [inv_pow]
  sorry

A proof I have has the numbers exactly like this as a part of it, but I am unable to translate the 10 from the naturals to the reals.

[Aaron Liu]

@loogle "rpow", OfNat.ofNat

[loogle]

:search: ExteriorAlgebra.exteriorPower, ExteriorAlgebra.exteriorPower.eq_1, and 767 more

[Aaron Liu]

@loogle "rpow", Int.cast

[loogle]

:search: Real.rpow_intCast, Real.rpow_intCast_mul, and 19 more

[Yakov Pechersky]

import Mathlib

example (x : ℝ) : 1 / x ^ 10 = x ^ (-(10:ℝ)) := by
  ring_nf
  have : (-10 : ℝ) = (-10 : ℤ) := by norm_num
  rw [this, Real.rpow_intCast, inv_pow, ← zpow_natCast, ← zpow_neg]
  norm_cast

[Colin Jones ⚛️]

Thank you!

[Yakov Pechersky]

Seems like there are some simp lemmas that might be in a different direction for reals than for ints. Because norm_num wasn't being very helpful.

[Colin Jones ⚛️]

When I tried using simp? and rw? I had difficulty in finding good lemmas because they just wanted to convert the -10 into a fraction.

[Ilmārs Cīrulis]

Am I missing something?

import Mathlib

example (x : ℝ) : 1 / x ^ 10 = x ^ (-(10:ℝ)) := by
  ring_nf
  simp only [inv_pow]
  norm_cast

[Yakov Pechersky]

Might as well then do this:

import Mathlib

example (x : ℝ) : 1 / x ^ 10 = x ^ (-(10:ℝ)) := by
  simp; norm_cast

[Eric Wieser]

These are probably worth having:

theorem Real.rpow_ofNat (x : ℝ) (n : ℕ) [n.AtLeastTwo] : x ^ (ofNat(n) : ℝ) = x ^ ofNat(n) :=
  Real.rpow_natCast _ _


theorem Real.rpow_neg_ofNat (x : ℝ) (n : ℕ) [n.AtLeastTwo] : x ^ (-ofNat(n) : ℝ) = x ^ (-ofNat(n) : ℤ) := by
  rw [← Real.rpow_intCast, Int.cast_neg, Int.cast_ofNat]

[Eric Wieser]

not sure of the best RHS for that second one