case ofNat.ofNat
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.ofNat a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.ofNat b
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ Int.ofNat a ≤ x ^ Int.ofNat b

case ofNat.negSucc
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.ofNat a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.negSucc b
h : Int.ofNat a ≤ Int.negSucc b
⊢ x ^ Int.ofNat a ≤ x ^ Int.negSucc b

case negSucc.ofNat
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.negSucc a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.ofNat b
h : Int.negSucc a ≤ Int.ofNat b
⊢ x ^ Int.negSucc a ≤ x ^ Int.ofNat b

case negSucc.negSucc
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.negSucc a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.negSucc b
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ Int.negSucc a ≤ x ^ Int.negSucc b
α : Type ?u.713362
β : Type ?u.713365
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℤ
h : a ≤ b
⊢ x ^ a ≤ x ^ b
induction' a with a a <;> induction' b with b b
case ofNat.ofNat
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.ofNat a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.ofNat b
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ a ≤ x ^ b
case ofNat.ofNat
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.ofNat a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.ofNat b
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ Int.ofNat a ≤ x ^ Int.ofNat b
simp only [Int.ofNat_eq_coe, zpow_ofNat]
no goals
case ofNat.ofNat
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.ofNat a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.ofNat b
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ a ≤ x ^ b
exact pow_le_pow hx (Int.le_of_ofNat_le_ofNat h)
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.ofNat a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.negSucc b
h : Int.ofNat a ≤ Int.negSucc b
⊢ Int.ofNat a > Int.negSucc b
case ofNat.negSucc
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.ofNat a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.negSucc b
h : Int.ofNat a ≤ Int.negSucc b
⊢ x ^ Int.ofNat a ≤ x ^ Int.negSucc b
apply absurd h (not_le_of_gt _)
no goals
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.ofNat a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.negSucc b
h : Int.ofNat a ≤ Int.negSucc b
⊢ Int.ofNat a > Int.negSucc b
exact lt_of_lt_of_le (Int.negSucc_lt_zero _) (Int.ofNat_nonneg _)
case negSucc.ofNat
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.negSucc a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.ofNat b
h : Int.negSucc a ≤ Int.ofNat b
⊢ (x ^ (a + 1))⁻¹ ≤ x ^ b
case negSucc.ofNat
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.negSucc a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.ofNat b
h : Int.negSucc a ≤ Int.ofNat b
⊢ x ^ Int.negSucc a ≤ x ^ Int.ofNat b
simp only [zpow_negSucc, Int.ofNat_eq_coe, zpow_ofNat]
no goals
case negSucc.ofNat
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.negSucc a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.ofNat b
h : Int.negSucc a ≤ Int.ofNat b
⊢ (x ^ (a + 1))⁻¹ ≤ x ^ b
refine' (ENNReal.inv_le_one.2 _).trans _ <;> exact one_le_pow_of_one_le' hx _
case negSucc.negSucc
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.negSucc a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.negSucc b
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ (b + 1) ≤ x ^ (a + 1)
case negSucc.negSucc
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.negSucc a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.negSucc b
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ Int.negSucc a ≤ x ^ Int.negSucc b
simp only [zpow_negSucc, ENNReal.inv_le_inv]
case negSucc.negSucc
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.negSucc a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.negSucc b
h : Int.negSucc a ≤ Int.negSucc b
⊢ b + 1 ≤ a + 1
case negSucc.negSucc
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.negSucc a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.negSucc b
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ (b + 1) ≤ x ^ (a + 1)
apply pow_le_pow hx
no goals
case negSucc.negSucc
α : Type ?u.713362
β : Type ?u.713365
a✝¹ b✝¹ c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ≥0∞
hx : 1 ≤ x
a✝ b✝ : ℤ
h✝² : a✝ ≤ b✝
a : ℕ
h✝¹ : Int.negSucc a ≤ b✝
b : ℕ
h✝ : a✝ ≤ Int.negSucc b
h : Int.negSucc a ≤ Int.negSucc b
⊢ b + 1 ≤ a + 1
simpa only [← Int.ofNat_le, neg_le_neg_iff, Int.ofNat_add, Int.ofNat_one, Int.negSucc_eq] using
  h