x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z
have hz' : 0 < -z := by rwa [lt_neg, neg_zero]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z
have hxz : 0 < x ^ (-z) := Real.rpow_pos_of_pos hx _
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
hyz : 0 < y ^ z⁻¹
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z
have hyz : 0 < y ^ z⁻¹ := Real.rpow_pos_of_pos hy _
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
hyz : 0 < y ^ z⁻¹
⊢ x ^ (-z) ≤ y ^ (z⁻¹ * -z) ↔ y ≤ x ^ z
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
hyz : 0 < y ^ z⁻¹
⊢ x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z
rw [← Real.rpow_le_rpow_iff hx.le hyz.le hz', ← Real.rpow_mul hy.le]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
hyz : 0 < y ^ z⁻¹
⊢ x ^ (-z) ≤ y⁻¹ ↔ y ≤ x ^ z
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
hyz : 0 < y ^ z⁻¹
⊢ x ^ (-z) ≤ y ^ (z⁻¹ * -z) ↔ y ≤ x ^ z
simp only [ne_of_lt hz, Real.rpow_neg_one, mul_neg, inv_mul_cancel, Ne.def, not_false_iff]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
hyz : 0 < y ^ z⁻¹
⊢ y ≤ x ^ (-z * -1) ↔ y ≤ x ^ z
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
hyz : 0 < y ^ z⁻¹
⊢ x ^ (-z) ≤ y⁻¹ ↔ y ≤ x ^ z
rw [le_inv hxz hy, ← Real.rpow_neg_one, ← Real.rpow_mul hx.le]
no goals
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
hz' : 0 < -z
hxz : 0 < x ^ (-z)
hyz : 0 < y ^ z⁻¹
⊢ y ≤ x ^ (-z * -1) ↔ y ≤ x ^ z
simp
no goals
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 < -z
rwa [lt_neg, neg_zero]