puzzle problem

Stream: new members

[vxctyxeha]

how to solve this problem

import Mathlib

theorem my (x : ℝ) : (x ^ (1 / 3 )) ^ 3 = x := by

[Peter Junglas]

Well, this is hard to prove, because it is wrong :slight_smile:

Two problems:

• you need 0 ≤ x
• 1 / 3 = 0 (natural numbers!)

Try the following

theorem my (x : ℝ) (hx : 0 ≤ x) : (x ^ ((1 : ℝ) / 3)) ^ (3 : ℝ) = x := by
  calc
    (x ^ ((1 : ℝ) / 3)) ^ (3 : ℝ) = x ^ (((1 : ℝ) / 3) * 3) := by
      exact Eq.symm (Real.rpow_mul hx ((1 : ℝ) / 3) (3 : ℝ))
    _= x := by
      norm_num

[vxctyxeha]

why 0 ≤ x？

[Yan Yablonovskiy 🇺🇦]

vxctyxeha said:

why 0 ≤ x？

This thread might help: #new members > ✔ Nth root of negative real number... @ 💬