case intro
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : ↑x < 1
⊢ ↑x ^ z < 1
x : ℝ≥0∞
z : ℝ
hx : x < 1
hz : 0 < z
⊢ x ^ z < 1
lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx le_top)
case intro
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : x < 1
⊢ ↑x ^ z < 1
case intro
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : ↑x < 1
⊢ ↑x ^ z < 1
simp only [coe_lt_one_iff] at hx
no goals
case intro
z : ℝ
hz : 0 < z
x : ℝ≥0
hx : x < 1
⊢ ↑x ^ z < 1
simp [coe_rpow_of_nonneg _ (le_of_lt hz), NNReal.rpow_lt_one hx hz]