English
If x ≥ 1 and a ≤ b are integers, then x^a ≤ x^b.
Русский
Если x ≥ 1 и a ≤ b целые, то x^a ≤ x^b.
LaTeX
$$$\\forall x \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\; x \\ge 1 \\Rightarrow \\forall a,b \\in \\mathbb{Z},\\; a \\le b \\Rightarrow x^a \\le x^b$$$
Lean4
@[gcongr]
theorem zpow_le_of_le {x : ℝ≥0∞} (hx : 1 ≤ x) {a b : ℤ} (h : a ≤ b) : x ^ a ≤ x ^ b :=
by
obtain a | a := a <;> obtain b | b := b
· simp only [Int.ofNat_eq_coe, zpow_natCast]
exact pow_right_mono₀ hx (Int.le_of_ofNat_le_ofNat h)
· apply absurd h (not_le_of_gt _)
exact lt_of_lt_of_le (Int.negSucc_lt_zero _) (Int.natCast_nonneg _)
· simp only [zpow_negSucc, Int.ofNat_eq_coe, zpow_natCast]
refine (ENNReal.inv_le_one.2 ?_).trans ?_ <;> exact one_le_pow_of_one_le' hx _
· simp only [zpow_negSucc, ENNReal.inv_le_inv]
apply pow_right_mono₀ hx
simpa only [← Int.ofNat_le, neg_le_neg_iff, Int.natCast_add, Int.ofNat_one] using h
